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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {R₁ : CategoryTheory.ComposableArrows C 3} {R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂) (hR₁ : CategoryTheory.ComposableArrows.map' R₁ 0 2 ⋯ ⋯ = 0) (hR₁' : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' R₁ 1 2 ⋯ ⋯) (CategoryTheory.ComposableArrows.map' R₁ 2 3 ⋯ ⋯))) (hR₂ : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' R₂ 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.map' R₂ 1 2 ⋯ ⋯))) (h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)) (h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)) (h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)) : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)

theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {R₁ : CategoryTheory.ComposableArrows C 3} {R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂) (hR₁ : CategoryTheory.ComposableArrows.Exact R₁) (hR₂ : CategoryTheory.ComposableArrows.Exact R₂) (h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)) (h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)) (h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)) : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)

theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {R₁ : CategoryTheory.ComposableArrows C 3} {R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂) (hR₁ : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' R₁ 1 2 ⋯ ⋯) (CategoryTheory.ComposableArrows.map' R₁ 2 3 ⋯ ⋯))) (hR₂ : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' R₂ 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.map' R₂ 1 2 ⋯ ⋯))) (hR₂' : CategoryTheory.ComposableArrows.map' R₂ 1 3 ⋯ ⋯ = 0) (h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)) (h₂ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 2 ⋯)) (h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)) : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)

theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {R₁ : CategoryTheory.ComposableArrows C 3} {R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂) (hR₁ : CategoryTheory.ComposableArrows.Exact R₁) (hR₂ : CategoryTheory.ComposableArrows.Exact R₂) (h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)) (h₂ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 2 ⋯)) (h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)) : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)

theorem CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {R₁ : CategoryTheory.ComposableArrows C 4} {R₂ : CategoryTheory.ComposableArrows C 4} (hR₁ : CategoryTheory.ComposableArrows.Exact R₁) (hR₂ : CategoryTheory.ComposableArrows.Exact R₂) (φ : R₁ ⟶ R₂) (h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)) (h₁ : CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 1 ⋯)) (h₂ : CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 3 ⋯)) (h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 4 ⋯)) : CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 2 ⋯)

The five lemma.