# The four and five lemmas #

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

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 #

The diagram of the five lemmas is given by a morphism in the category ComposableArrows C 4 between two objects which satisfy ComposableArrows.Exact. Similarly, the two versions of the four lemma are stated in terms of the category ComposableArrows C 3.

The five lemmas is deduced from the two versions of the four lemma. Both of these versions are proved separately. It would be easy to deduce the epi version from the mono version using duality, but this would require lengthy API developments for ComposableArrows (TODO).

## Tags #

four lemma, five lemma, diagram lemma, diagram chase

theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono' {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.map' 0 2 = 0) (hR₁' : (CategoryTheory.ComposableArrows.mk₂ (R₁.map' 1 2 ) (R₁.map' 2 3 )).Exact) (hR₂ : (CategoryTheory.ComposableArrows.mk₂ (R₂.map' 0 1 ) (R₂.map' 1 2 )).Exact) (h₀ : ) (h₁ : ) (h₃ : ) :
theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (h₀ : ) (h₁ : ) (h₃ : ) :
theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono' {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : (CategoryTheory.ComposableArrows.mk₂ (R₁.map' 1 2 ) (R₁.map' 2 3 )).Exact) (hR₂ : (CategoryTheory.ComposableArrows.mk₂ (R₂.map' 0 1 ) (R₂.map' 1 2 )).Exact) (hR₂' : R₂.map' 1 3 = 0) (h₀ : ) (h₂ : ) (h₃ : ) :
theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (h₀ : ) (h₂ : ) (h₃ : ) :
theorem CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (φ : R₁ R₂) (h₀ : ) (h₁ : ) (h₂ : ) (h₃ : ) :

The five lemma.

The following "three lemmas" for morphisms in ComposableArrows C 2 are special cases of "four lemmas" applied to diagrams where some of the leftmost or rightmost maps (or objects) are zero.

theorem CategoryTheory.Abelian.mono_of_epi_of_epi_mono' {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.map' 0 2 = 0) (hR₁' : CategoryTheory.Epi (R₁.map' 1 2 )) (hR₂ : R₂.Exact) (h₀ : ) (h₁ : ) :
theorem CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (hR₁' : CategoryTheory.Epi (R₁.map' 1 2 )) (h₀ : ) (h₁ : ) :
theorem CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono' {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂ : R₂.map' 0 2 = 0) (hR₂' : CategoryTheory.Mono (R₂.map' 0 1 )) (h₀ : ) (h₁ : ) :
theorem CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (hR₂' : CategoryTheory.Mono (R₂.map' 0 1 )) (h₀ : ) (h₁ : ) :
theorem CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₁ : R₁.Exact) (hR₂' : CategoryTheory.Mono (R₂.map' 0 1 )) (h₀ : ) (h₁ : ) :
theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi {C : Type u_1} [] {R₁ : } {R₂ : } (φ : R₁ R₂) (hR₂ : R₂.Exact) (hR₁' : CategoryTheory.Epi (R₁.map' 1 2 )) (h₀ : ) (h₁ : ) :