Exact sequences

In a category with zero morphisms, images, and equalizers we say that f : A ⟶ B and g : B ⟶ C are exact if f ≫ g = 0 and the natural map image f ⟶ kernel g is an epimorphism.

In any preadditive category this is equivalent to the homology at B vanishing.

However in general it is weaker than other reasonable definitions of exactness, particularly that

1. the inclusion map image.ι f is a kernel of g or
2. image f ⟶ kernel g is an isomorphism or
3. imageSubobject f = kernelSubobject f. However when the category is abelian, these all become equivalent; these results are found in CategoryTheory/Abelian/Exact.lean.

Main results

• Suppose that cokernels exist and that f and g are exact. If s is any kernel fork over g and t is any cokernel cofork over f, then Fork.ι s ≫ Cofork.π t = 0.
• Precomposing the first morphism with an epimorphism retains exactness. Postcomposing the second morphism with a monomorphism retains exactness.
• If f and g are exact and i is an isomorphism, then f ≫ i.hom and i.inv ≫ g are also exact.

Future work

• Short exact sequences, split exact sequences, the splitting lemma (maybe only for abelian categories?)
• Two adjacent maps in a chain complex are exact iff the homology vanishes

structure CategoryTheory.Exact {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop

• w : CategoryTheory.CategoryStruct.comp f g = 0
• epi : CategoryTheory.Epi (imageToKernel f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))

Two morphisms f : A ⟶ B, g : B ⟶ C are called exact if w : f ≫ g = 0 and the natural map imageToKernel f g w : imageSubobject f ⟶ kernelSubobject g is an epimorphism.

In any preadditive category, this is equivalent to w : f ≫ g = 0 and homology f g w ≅ 0.

In an abelian category, this is equivalent to imageToKernel f g w being an isomorphism, and hence equivalent to the usual definition, imageSubobject f = kernelSubobject g.

theorem CategoryTheory.Exact.w_assoc {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} {C : V} {f : A ⟶ B} {g : B ⟶ C} (self : CategoryTheory.Exact f g) {Z : V} (h : C ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Preadditive.exact_iff_homology_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasCokernels V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) : CategoryTheory.Exact f g ↔ ∃ w, Nonempty (homology f g w ≅ 0)

In any preadditive category, composable morphisms f g are exact iff they compose to zero and the homology vanishes.

theorem CategoryTheory.Preadditive.exact_of_iso_of_exact {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasCokernels V] {A₁ : V} {B₁ : V} {C₁ : V} {A₂ : V} {B₂ : V} {C₂ : V} (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁) (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (α : CategoryTheory.Arrow.mk f₁ ≅ CategoryTheory.Arrow.mk f₂) (β : CategoryTheory.Arrow.mk g₁ ≅ CategoryTheory.Arrow.mk g₂) (p : α.hom.right = β.hom.left) (h : CategoryTheory.Exact f₁ g₁) : CategoryTheory.Exact f₂ g₂

theorem CategoryTheory.Preadditive.exact_of_iso_of_exact' {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasCokernels V] {A₁ : V} {B₁ : V} {C₁ : V} {A₂ : V} {B₂ : V} {C₂ : V} (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁) (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (α : A₁ ≅ A₂) (β : B₁ ≅ B₂) (γ : C₁ ≅ C₂) (hsq₁ : CategoryTheory.CategoryStruct.comp α.hom f₂ = CategoryTheory.CategoryStruct.comp f₁ β.hom) (hsq₂ : CategoryTheory.CategoryStruct.comp β.hom g₂ = CategoryTheory.CategoryStruct.comp g₁ γ.hom) (h : CategoryTheory.Exact f₁ g₁) : CategoryTheory.Exact f₂ g₂

A reformulation of Preadditive.exact_of_iso_of_exact that does not involve the arrow category.

theorem CategoryTheory.Preadditive.exact_iff_exact_of_iso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasCokernels V] {A₁ : V} {B₁ : V} {C₁ : V} {A₂ : V} {B₂ : V} {C₂ : V} (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁) (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (α : CategoryTheory.Arrow.mk f₁ ≅ CategoryTheory.Arrow.mk f₂) (β : CategoryTheory.Arrow.mk g₁ ≅ CategoryTheory.Arrow.mk g₂) (p : α.hom.right = β.hom.left) : CategoryTheory.Exact f₁ g₁ ↔ CategoryTheory.Exact f₂ g₂

theorem CategoryTheory.comp_eq_zero_of_image_eq_kernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) (p : CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g) : CategoryTheory.CategoryStruct.comp f g = 0

theorem CategoryTheory.imageToKernel_isIso_of_image_eq_kernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) (p : CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g) : CategoryTheory.IsIso (imageToKernel f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))

theorem CategoryTheory.exact_of_image_eq_kernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) (p : CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g) : CategoryTheory.Exact f g

theorem CategoryTheory.exact_comp_hom_inv_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (i : B ≅ D) (h : CategoryTheory.Exact f g) : CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g)

theorem CategoryTheory.exact_comp_inv_hom_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (i : D ≅ B) (h : CategoryTheory.Exact f g) : CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp f i.inv) (CategoryTheory.CategoryStruct.comp i.hom g)

theorem CategoryTheory.exact_comp_hom_inv_comp_iff {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (i : B ≅ D) : CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) ↔ CategoryTheory.Exact f g

theorem CategoryTheory.exact_epi_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (hgh : CategoryTheory.Exact g h) [CategoryTheory.Epi f] : CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp f g) h

@[simp]

theorem CategoryTheory.exact_iso_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.IsIso f] : CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp f g) h ↔ CategoryTheory.Exact g h

theorem CategoryTheory.exact_comp_mono {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (hfg : CategoryTheory.Exact f g) [CategoryTheory.Mono h] : CategoryTheory.Exact f (CategoryTheory.CategoryStruct.comp g h)

theorem CategoryTheory.exact_comp_mono_iff {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Mono h] : CategoryTheory.Exact f (CategoryTheory.CategoryStruct.comp g h) ↔ CategoryTheory.Exact f g

The dual of this lemma is only true when V is abelian, see Abelian.exact_epi_comp_iff.

@[simp]

theorem CategoryTheory.exact_comp_iso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {D : V} {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.IsIso h] : CategoryTheory.Exact f (CategoryTheory.CategoryStruct.comp g h) ↔ CategoryTheory.Exact f g

theorem CategoryTheory.exact_kernelSubobject_arrow {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {f : A ⟶ B} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] : CategoryTheory.Exact (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f)) f

theorem CategoryTheory.exact_kernel_ι {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {f : A ⟶ B} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] : CategoryTheory.Exact (CategoryTheory.Limits.kernel.ι f) f

instance CategoryTheory.Exact.epi_factorThruKernelSubobject {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (h : CategoryTheory.Exact f g) : CategoryTheory.Epi (CategoryTheory.Limits.factorThruKernelSubobject g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))

Equations

• @CategoryTheory.Exact.epi_factorThruKernelSubobject = @CategoryTheory.Exact.epi_factorThruKernelSubobject.proof_1

theorem CategoryTheory.Exact.epi_kernel_lift {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (h : CategoryTheory.Exact f g) : CategoryTheory.Epi (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))

theorem CategoryTheory.kernelSubobject_arrow_eq_zero_of_exact_zero_left {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] (A : V) {B : V} {C : V} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (h : CategoryTheory.Exact 0 g) : CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject g) = 0

theorem CategoryTheory.kernel_ι_eq_zero_of_exact_zero_left {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] (A : V) {B : V} {C : V} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] (h : CategoryTheory.Exact 0 g) : CategoryTheory.Limits.kernel.ι g = 0

theorem CategoryTheory.exact_zero_left_of_mono {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] (A : V) {B : V} {C : V} {g : B ⟶ C} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Mono g] : CategoryTheory.Exact 0 g

@[simp]

theorem CategoryTheory.kernel_comp_cokernel_assoc {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] (h : CategoryTheory.Exact f g) {Z : V} (h : CategoryTheory.Limits.cokernel f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.kernel_comp_cokernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] (h : CategoryTheory.Exact f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f) = 0

theorem CategoryTheory.comp_eq_zero_of_exact {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] (h : CategoryTheory.Exact f g) {X : V} {Y : V} {ι : X ⟶ B} (hι : CategoryTheory.CategoryStruct.comp ι g = 0) {π : B ⟶ Y} (hπ : CategoryTheory.CategoryStruct.comp f π = 0) : CategoryTheory.CategoryStruct.comp ι π = 0

@[simp]

theorem CategoryTheory.fork_ι_comp_cofork_π_assoc {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] (h : CategoryTheory.Exact f g) (s : CategoryTheory.Limits.KernelFork g) (t : CategoryTheory.Limits.CokernelCofork f) {Z : V} (h : ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.fork_ι_comp_cofork_π {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] {A : V} {B : V} {C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] (h : CategoryTheory.Exact f g) (s : CategoryTheory.Limits.KernelFork g) (t : CategoryTheory.Limits.CokernelCofork f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) (CategoryTheory.Limits.Cofork.π t) = 0

theorem CategoryTheory.exact_of_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {C : V} (f : A ⟶ 0) (g : 0 ⟶ C) : CategoryTheory.Exact f g

theorem CategoryTheory.exact_zero_mono {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {B : V} {C : V} (f : B ⟶ C) [CategoryTheory.Mono f] : CategoryTheory.Exact 0 f

theorem CategoryTheory.exact_epi_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {A : V} {B : V} (f : A ⟶ B) [CategoryTheory.Epi f] : CategoryTheory.Exact f 0

theorem CategoryTheory.mono_iff_exact_zero_left {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasKernels V] {B : V} {C : V} (f : B ⟶ C) : CategoryTheory.Mono f ↔ CategoryTheory.Exact 0 f

theorem CategoryTheory.epi_iff_exact_zero_right {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasEqualizers V] {A : V} {B : V} (f : A ⟶ B) : CategoryTheory.Epi f ↔ CategoryTheory.Exact f 0

class CategoryTheory.Functor.ReflectsExactSequences {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {W : Type u₂} [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.Limits.HasImages W] [CategoryTheory.Limits.HasZeroMorphisms W] [CategoryTheory.Limits.HasKernels W] (F : CategoryTheory.Functor V W) : Prop

• reflects : ∀ {A B C : V} (f : A ⟶ B) (g : B ⟶ C), CategoryTheory.Exact (F.map f) (F.map g) → CategoryTheory.Exact f g

A functor reflects exact sequences if any composable pair of morphisms that is mapped to an exact pair is itself exact.

theorem CategoryTheory.Functor.exact_of_exact_map {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] {W : Type u₂} [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.Limits.HasImages W] [CategoryTheory.Limits.HasZeroMorphisms W] [CategoryTheory.Limits.HasKernels W] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.ReflectsExactSequences F] {A : V} {B : V} {C : V} {f : A ⟶ B} {g : B ⟶ C} (hfg : CategoryTheory.Exact (F.map f) (F.map g)) : CategoryTheory.Exact f g