mathlib documentation

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

Future work

@[class]

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.

theorem category_theory.comp_eq_zero_of_exact {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] {A B C : V} (f : A B) (g : B C) [category_theory.exact f g] {X Y : V} {ι : X B} (hι : ι g = 0) {π : B Y} :
f «π» = 0ι «π» = 0