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