The four and five lemmas #
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
The four lemma, mono version. For names of objects and morphisms, refer to the following diagram:
A ---f--> B ---g--> C ---h--> D
| | | |
α β γ δ
| | | |
v v v v
A' --f'-> B' --g'-> C' --h'-> D'
The four lemma, epi version. For names of objects and morphisms, refer to the following diagram:
A ---f--> B ---g--> C ---h--> D
| | | |
α β γ δ
| | | |
v v v v
A' --f'-> B' --g'-> C' --h'-> D'
The five lemma. For names of objects and morphisms, refer to the following diagram:
A ---f--> B ---g--> C ---h--> D ---i--> E
| | | | |
α β γ δ ε
| | | | |
v v v v v
A' --f'-> B' --g'-> C' --h'-> D' --i'-> E'