mathlib documentation


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.


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'