The four lemma
Consider the following commutative diagram with exact rows in an abelian category:
A ---f--> B ---g--> C ---h--> D | | | | α β γ δ | | | | v v v v A' --f'-> B' --g'-> C' --h'-> D'
We prove the "mono" version of the four lemma: if α is an epimorphism and β and δ are monomorphisms, then γ is a monomorphism.
Future work
The "epi" four lemma and the five lemma, which is then an easy corollary.
Tags
four lemma, diagram lemma, diagram chase
theorem
category_theory.abelian.mono_of_epi_of_mono_of_mono
{V : Type u}
[category_theory.category V]
[category_theory.abelian V]
{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'}
[category_theory.exact f g]
[category_theory.exact g h]
[category_theory.exact f' g'] :
α ≫ f' = f ≫ β → β ≫ g' = g ≫ γ → γ ≫ h' = h ≫ δ → category_theory.epi α → category_theory.mono β → category_theory.mono δ → category_theory.mono γ
The four lemma, mono version. For names of objects and morphisms, consider the following diagram:
A ---f--> B ---g--> C ---h--> D
| | | |
α β γ δ
| | | |
v v v v
A' --f'-> B' --g'-> C' --h'-> D'