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

This definition is equivalent to the homology at B vanishing (at least for preadditive categories). At this level of generality, this is not necessarily equivalent to other reasonable definitions of exactness, for example that the inclusion map image.ι f is a kernel of g or that the map image f ⟶ kernel g is an isomorphism. By adding more assumptions on our category, we get these equivalences and more. Currently, there is one particular set of assumptions mathlib knows about: abelian categories. Consequently, many interesting results about exact sequences 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 f ≫ g = 0 and the natural map image f ⟶ kernel g is an epimorphism.

@[simp]
theorem category_theory.exact.w_assoc {V : Type u} {A B C : V} {f : A B} {g : B C} [c : g] {X' : V} (f' : C X') :
f g f' = 0 f'

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) :

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}  :

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)

theorem category_theory.exact_kernel {V : Type u} {A B : V} {f : A B} :

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}  :

theorem category_theory.exact_of_zero {V : Type u} {A C : V} (f : A 0) (g : 0 C) :