# mathlib3documentation

algebra.homology.exact

# Exact sequences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
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.

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_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₂) (α : A₁ A₂) (β : B₁ B₂) (γ : C₁ C₂) (hsq₁ : α.hom f₂ = f₁ β.hom) (hsq₂ : β.hom g₂ = g₁ γ.hom) (h : g₁) :

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

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)  :
theorem category_theory.exact_comp_hom_inv_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} (i : B D) (h : g) :
theorem category_theory.exact_comp_inv_hom_comp {V : Type u} {A B C D : V} {f : A B} {g : B C} (i : D B) (h : g) :
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} (hgh : h)  :
@[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} (hfg : g)  :
(g h)
theorem category_theory.exact_comp_mono_iff {V : Type u} {A B C D : V} {f : A B} {g : B C} {h : C D}  :
(g h)

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

@[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_ι {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} (h : g) :
@[protected, instance]
def category_theory.limits.kernel.lift.epi {V : Type u} {A B C : V} {f : A B} {g : B C} (h : g) :
theorem category_theory.kernel_subobject_arrow_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B C : V} {g : B C} (h : g) :
theorem category_theory.kernel_ι_eq_zero_of_exact_zero_left {V : Type u} (A : V) {B C : V} {g : B C} (h : g) :
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) (h : g) :
@[simp]
theorem category_theory.kernel_comp_cokernel_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) (h : g) {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) (h : g) {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) (h : g)  :
@[simp]
theorem category_theory.fork_ι_comp_cofork_π_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) (h : g) {X' : V}  :
theorem category_theory.exact_of_zero {V : Type u} {A C : V} (f : A 0) (g : 0 C) :
theorem category_theory.exact_zero_mono {V : Type u} {B C : V} (f : B C)  :
theorem 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) :
@[class]

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

Instances of this typeclass
Instances of other typeclasses for category_theory.functor.reflects_exact_sequences
• category_theory.functor.reflects_exact_sequences.has_sizeof_inst
theorem category_theory.functor.exact_of_exact_map {V : Type u} {W : Type u₂} (F : V W) {A B C : V} {f : A B} {g : B C} (hfg : category_theory.exact (F.map f) (F.map g)) :