mathlibdocumentation

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. image_subobject f = kernel_subobject f. However when the category is abelian, these all become equivalent; these results are found in category_theory/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
@[class]
structure category_theory.exact {V : Type u} {A B C : V} (f : A B) (g : B C) :
Prop
• w : f g = 0
• epi :

Two morphisms f : A ⟶ B, g : B ⟶ C are called exact if w : f ≫ g = 0 and the natural map image_to_kernel f g w : image_subobject f ⟶ kernel_subobject 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 image_to_kernel f g w being an isomorphism, and hence equivalent to the usual definition, image_subobject f = kernel_subobject g.

Instances
@[simp]
theorem category_theory.exact.w_assoc {V : Type u} {A B C : V} {f : A B} {g : B C} [self : g] {X' : V} (f' : C X') :
f g f' = 0 f'
theorem category_theory.preadditive.exact_iff_homology_zero {V : Type u} {A B C : V} (f : A B) (g : B C) :
∃ (w : f g = 0), 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 category_theory.preadditive.exact_of_iso_of_exact {V : Type u} {A₁ B₁ C₁ A₂ B₂ C₂ : V} (f₁ : A₁ B₁) (g₁ : B₁ C₁) (f₂ : A₂ B₂) (g₂ : B₂ C₂) (p : α.hom.right = β.hom.left) (h : g₁) :
theorem category_theory.preadditive.exact_iff_exact_of_iso {V : Type u} {A₁ B₁ C₁ A₂ B₂ C₂ : V} (f₁ : A₁ B₁) (g₁ : B₁ C₁) (f₂ : A₂ B₂) (g₂ : B₂ C₂) (p : α.hom.right = β.hom.left) :
theorem category_theory.comp_eq_zero_of_image_eq_kernel {V : Type u} {A B C : V} (f : A B) (g : B C)  :
f g = 0
theorem category_theory.image_to_kernel_is_iso_of_image_eq_kernel {V : Type u} {A B C : V} (f : A B) (g : B C)  :
theorem category_theory.exact_of_image_eq_kernel {V : Type u} {A B C : V} (f : A B) (g : B C)  :
@[protected, instance]
def category_theory.exact_comp_hom_inv_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} (i : B D) :
@[protected, instance]
def category_theory.exact_comp_inv_hom_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} (i : D B) :
theorem category_theory.exact_comp_hom_inv_comp_iff {V : Type u} {A B C D : V} {f : A B} {g : B C} (i : B D) :
theorem category_theory.exact_epi_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} {h : C D}  :
@[simp]
theorem category_theory.exact_iso_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} {h : C D}  :
theorem category_theory.exact_comp_mono {V : Type u} {A B C D : V} {f : A B} {g : B C} {h : C D}  :
(g h)
@[simp]
theorem category_theory.exact_comp_iso {V : Type u} {A B C D : V} {f : A B} {g : B C} {h : C D}  :
(g h)
theorem category_theory.exact_kernel_subobject_arrow {V : Type u} {A B : V} {f : A B}  :
theorem category_theory.exact_kernel_ι {V : Type u} {A B : V} {f : A B}  :
@[protected, instance]
def category_theory.limits.factor_thru_kernel_subobject.epi {V : Type u} {A B C : V} {f : A B} {g : B C}  :
@[protected, instance]
def category_theory.limits.kernel.lift.epi {V : Type u} {A B C : V} {f : A B} {g : B C}  :
theorem category_theory.kernel_subobject_arrow_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B C : V} {g : B C}  :
theorem category_theory.kernel_ι_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B C : V} {g : B C}  :
theorem category_theory.exact_zero_left_of_mono {V : Type u} (A : V) {B C : V} {g : B C}  :
@[simp]
theorem category_theory.kernel_comp_cokernel {V : Type u} {A B C : V} (f : A B) (g : B C)  :
@[simp]
theorem category_theory.kernel_comp_cokernel_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) {X' : V} (f' : X') :
theorem category_theory.comp_eq_zero_of_exact {V : Type u} {A B C : V} (f : A B) (g : B C) {X Y : V} {ι : X B} (hι : ι g = 0) {π : B Y} (hπ : f π = 0) :
ι π = 0
@[simp]
theorem category_theory.fork_ι_comp_cofork_π {V : Type u} {A B C : V} (f : A B) (g : B C)  :
@[simp]
theorem category_theory.fork_ι_comp_cofork_π_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) {X' : V}  :
@[protected, instance]
def category_theory.exact_of_zero {V : Type u} {A C : V} (f : A 0) (g : 0 C) :
@[protected, instance]
def category_theory.exact_zero_mono {V : Type u} {B C : V} (f : B C)  :
@[protected, instance]
def category_theory.exact_epi_zero {V : Type u} {A B : V} (f : A B)  :
theorem category_theory.mono_iff_exact_zero_left {V : Type u} {B C : V} (f : B C) :
theorem category_theory.epi_iff_exact_zero_right {V : Type u} {A B : V} (f : A B) :