# Documentation

Mathlib.Algebra.Homology.Exact

# 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} {A : V} {B : V} {C : V} (f : A B) (g : B C) :

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.

Instances For
theorem CategoryTheory.Exact.w_assoc {V : Type u} {A : V} {B : V} {C : V} {f : A B} {g : B C} (self : ) {Z : V} (h : C Z) :
theorem CategoryTheory.Preadditive.exact_iff_homology_zero {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) :
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} {A₁ : V} {B₁ : V} {C₁ : V} {A₂ : V} {B₂ : V} {C₂ : V} (f₁ : A₁ B₁) (g₁ : B₁ C₁) (f₂ : A₂ B₂) (g₂ : B₂ C₂) (α : ) (β : ) (p : α.hom.right = β.hom.left) (h : ) :
theorem CategoryTheory.Preadditive.exact_of_iso_of_exact' {V : Type u} {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₁ : = ) (hsq₂ : = ) (h : ) :

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} {A₁ : V} {B₁ : V} {C₁ : V} {A₂ : V} {B₂ : V} {C₂ : V} (f₁ : A₁ B₁) (g₁ : B₁ C₁) (f₂ : A₂ B₂) (g₂ : B₂ C₂) (α : ) (β : ) (p : α.hom.right = β.hom.left) :
theorem CategoryTheory.comp_eq_zero_of_image_eq_kernel {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) :
theorem CategoryTheory.imageToKernel_isIso_of_image_eq_kernel {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) :
theorem CategoryTheory.exact_of_image_eq_kernel {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) :
theorem CategoryTheory.exact_comp_hom_inv_comp {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} (i : B D) (h : ) :
theorem CategoryTheory.exact_comp_inv_hom_comp {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} (i : D B) (h : ) :
theorem CategoryTheory.exact_comp_hom_inv_comp_iff {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} (i : B D) :
theorem CategoryTheory.exact_epi_comp {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} {h : C D} (hgh : ) :
@[simp]
theorem CategoryTheory.exact_iso_comp {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} {h : C D} :
theorem CategoryTheory.exact_comp_mono {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} {h : C D} (hfg : ) :
theorem CategoryTheory.exact_comp_mono_iff {V : Type u} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} {h : C D} :

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} {A : V} {B : V} {C : V} {D : V} {f : A B} {g : B C} {h : C D} :
theorem CategoryTheory.exact_kernelSubobject_arrow {V : Type u} {A : V} {B : V} {f : A B} :
theorem CategoryTheory.exact_kernel_ι {V : Type u} {A : V} {B : V} {f : A B} :
instance CategoryTheory.Exact.epi_factorThruKernelSubobject {V : Type u} {A : V} {B : V} {C : V} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Exact.epi_kernel_lift {V : Type u} {A : V} {B : V} {C : V} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.kernelSubobject_arrow_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B : V} {C : V} {g : B C} (h : ) :
theorem CategoryTheory.kernel_ι_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B : V} {C : V} {g : B C} (h : ) :
theorem CategoryTheory.exact_zero_left_of_mono {V : Type u} (A : V) {B : V} {C : V} {g : B C} :
@[simp]
theorem CategoryTheory.kernel_comp_cokernel_assoc {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) (h : ) {Z : V} (h : ) :
@[simp]
theorem CategoryTheory.kernel_comp_cokernel {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) (h : ) :
theorem CategoryTheory.comp_eq_zero_of_exact {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) (h : ) {X : V} {Y : V} {ι : X B} (hι : ) {π : B Y} (hπ : ) :
@[simp]
theorem CategoryTheory.fork_ι_comp_cofork_π_assoc {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) (h : ) {Z : V} (h : ) :
@[simp]
theorem CategoryTheory.fork_ι_comp_cofork_π {V : Type u} {A : V} {B : V} {C : V} (f : A B) (g : B C) (h : ) :
theorem CategoryTheory.exact_of_zero {V : Type u} {A : V} {C : V} (f : A 0) (g : 0 C) :
theorem CategoryTheory.exact_zero_mono {V : Type u} {B : V} {C : V} (f : B C) :
theorem CategoryTheory.exact_epi_zero {V : Type u} {A : V} {B : V} (f : A B) :
theorem CategoryTheory.mono_iff_exact_zero_left {V : Type u} {B : V} {C : V} (f : B C) :
theorem CategoryTheory.epi_iff_exact_zero_right {V : Type u} {A : V} {B : V} (f : A B) :

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

Instances
theorem CategoryTheory.Functor.exact_of_exact_map {V : Type u} {W : Type u₂} [] (F : ) {A : V} {B : V} {C : V} {f : A B} {g : B C} (hfg : CategoryTheory.Exact (F.map f) (F.map g)) :