# mathlibdocumentation

category_theory.abelian.diagram_lemmas.four

# 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

theorem category_theory.abelian.mono_of_epi_of_mono_of_mono {V : Type u} {A B C D A' B' C' D' : V} {f : A B} {g : B C} {h : C D} {f' : A' B'} {g' : B' C'} {h' : C' D'} {α : A A'} {β : B B'} {γ : C C'} {δ : D D'} (comm₁ : α f' = f β) (comm₂ : β g' = g γ) (comm₃ : γ h' = h δ) (hfg : g) (hgh : h) (hf'g' : g') (hα : category_theory.epi α) (hβ : category_theory.mono β) (hδ : category_theory.mono δ) :

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'

theorem category_theory.abelian.epi_of_epi_of_epi_of_mono {V : Type u} {A B C D A' B' C' D' : V} {f : A B} {g : B C} {h : C D} {f' : A' B'} {g' : B' C'} {h' : C' D'} {α : A A'} {β : B B'} {γ : C C'} {δ : D D'} (comm₁ : α f' = f β) (comm₂ : β g' = g γ) (comm₃ : γ h' = h δ) (hgh : h) (hf'g' : g') (hg'h' : h') (hα : category_theory.epi α) (hγ : category_theory.epi γ) (hδ : category_theory.mono δ) :

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'

theorem category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso {V : Type u} {A B C D A' B' C' D' : V} {f : A B} {g : B C} {h : C D} {f' : A' B'} {g' : B' C'} {h' : C' D'} {α : A A'} {β : B B'} {γ : C C'} {δ : D D'} (comm₁ : α f' = f β) (comm₂ : β g' = g γ) (comm₃ : γ h' = h δ) {E E' : V} {i : D E} {i' : D' E'} {ε : E E'} (comm₄ : δ i' = i ε) (hfg : g) (hgh : h) (hhi : i) (hf'g' : g') (hg'h' : h') (hh'i' : i')  :

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'