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.

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'] (comm₁ : α f' = f β) (comm₂ : β g' = g γ) (comm₃ : γ h' = h δ) (hα : category_theory.epi α) (hβ : category_theory.mono β) (hδ : 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'