The four and five lemmas #

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

Consider the following commutative diagram with exact rows in an abelian category:

A ---f--> B ---g--> C ---h--> D ---i--> E
|         |         |         |         |
α         β         γ         δ         ε
|         |         |         |         |
v         v         v         v         v
A' --f'-> B' --g'-> C' --h'-> D' --i'-> E'

We show:

• the "mono" version of the four lemma: if α is an epimorphism and β and δ are monomorphisms, then γ is a monomorphism,
• the "epi" version of the four lemma: if β and δ are epimorphisms and ε is a monomorphism, then γ is an epimorphism,
• the five lemma: if α, β, δ and ε are isomorphisms, then γ is an isomorphism.

Implementation details #

To show the mono version, we use pseudoelements. For the epi version, we use a completely different arrow-theoretic proof. In theory, it should be sufficient to have one version and the other should follow automatically by duality. In practice, mathlib's knowledge about duality isn't quite at the point where this is doable easily.

However, one key duality statement about exactness is needed in the proof of the epi version of the four lemma: we need to know that exactness of a pair (f, g), which we defined via the map from the image of f to the kernel of g, is the same as "co-exactness", defined via the map from the cokernel of f to the coimage of g (more precisely, we only need the consequence that if (f, g) is exact, then the factorization of g through the cokernel of f is monomorphic). Luckily, in the case of abelian categories, we have the characterization that (f, g) is exact if and only if f ≫ g = 0 and kernel.ι g ≫ cokernel.π f = 0, and the latter condition is self dual, so the equivalence of exactness and co-exactness follows easily.

Tags #

four lemma, five lemma, diagram lemma, diagram chase