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