feat(category_theory/abelian): the five lemma (#8265)

src/algebra/homology/exact.lean

@@ -184,6 +184,12 @@ begin
   apply epi_comp,
 end
 
+instance [exact f g] : epi (kernel.lift g f (by simp)) :=
+begin
+  rw ←factor_thru_kernel_subobject_comp_kernel_subobject_iso,
+  apply epi_comp
+end
+
 variables (A)
 
 lemma kernel_subobject_arrow_eq_zero_of_exact_zero_left [exact (0 : A ⟶ B) g] :

src/category_theory/abelian/basic.lean

@@ -246,6 +246,14 @@ cokernel.π_desc _ _ _
 instance : mono (coimages.factor_thru_coimage f) :=
 show mono (non_preadditive_abelian.factor_thru_coimage f), by apply_instance
 
+section
+variables {f}
+
+lemma comp_coimage_π_eq_zero {R : C} {g : Q ⟶ R} (h : f ≫ g = 0) : f ≫ coimages.coimage.π g = 0 :=
+zero_of_comp_mono (coimages.factor_thru_coimage g) $ by simp [h]
+
+end
+
 instance epi_factor_thru_coimage [epi f] : epi (coimages.factor_thru_coimage f) :=
 epi_of_epi_fac $ coimage.fac f
 
@@ -386,7 +394,7 @@ fork.is_limit.mk _
 end pullback_to_biproduct_is_kernel
 
 namespace biproduct_to_pushout_is_cokernel
-variables [limits.has_pushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
+variables [limits.has_pushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
 
 /-- The canonical map `Y ⊞ Z ⟶ pushout f g` -/
 abbreviation biproduct_to_pushout : Y ⊞ Z ⟶ pushout f g :=
@@ -411,7 +419,7 @@ cofork.is_colimit.mk _
 end biproduct_to_pushout_is_cokernel
 
 section epi_pullback
-variables [limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
+variables [limits.has_pullbacks C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
 
 /-- In an abelian category, the pullback of an epimorphism is an epimorphism.
     Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6] -/
@@ -482,10 +490,32 @@ begin
     ... = 0 : has_zero_morphisms.comp_zero _ _
 end
 
+lemma epi_snd_of_is_limit [epi f] {s : pullback_cone f g} (hs : is_limit s) : epi s.snd :=
+begin
+  convert epi_of_epi_fac (is_limit.cone_point_unique_up_to_iso_hom_comp (limit.is_limit _) hs _),
+  { refl },
+  { exact abelian.epi_pullback_of_epi_f _ _ }
+end
+
+lemma epi_fst_of_is_limit [epi g] {s : pullback_cone f g} (hs : is_limit s) : epi s.fst :=
+begin
+  convert epi_of_epi_fac (is_limit.cone_point_unique_up_to_iso_hom_comp (limit.is_limit _) hs _),
+  { refl },
+  { exact abelian.epi_pullback_of_epi_g _ _ }
+end
+
+/-- Suppose `f` and `g` are two morphisms with a common codomain and suppose we have written `g` as
+    an epimorphism followed by a monomorphism. If `f` factors through the mono part of this
+    factorization, then any pullback of `g` along `f` is an epimorphism. -/
+lemma epi_fst_of_factor_thru_epi_mono_factorization
+  (g₁ : Y ⟶ W) [epi g₁] (g₂ : W ⟶ Z) [mono g₂] (hg : g₁ ≫ g₂ = g) (f' : X ⟶ W) (hf : f' ≫ g₂ = f)
+  (t : pullback_cone f g) (ht : is_limit t) : epi t.fst :=
+by apply epi_fst_of_is_limit _ _ (pullback_cone.is_limit_of_factors f g g₂ f' g₁ hf hg t ht)
+
 end epi_pullback
 
 section mono_pushout
-variables [limits.has_pushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
+variables [limits.has_pushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
 
 instance mono_pushout_of_mono_f [mono f] : mono (pushout.inr : Z ⟶ pushout f g) :=
 mono_of_cancel_zero _ $ λ R e h,
@@ -533,6 +563,30 @@ begin
     ... = 0 : zero_comp
 end
 
+lemma mono_inr_of_is_colimit [mono f] {s : pushout_cocone f g} (hs : is_colimit s) : mono s.inr :=
+begin
+  convert mono_of_mono_fac
+    (is_colimit.comp_cocone_point_unique_up_to_iso_hom hs (colimit.is_colimit _) _),
+  { refl },
+  { exact abelian.mono_pushout_of_mono_f _ _ }
+end
+
+lemma mono_inl_of_is_colimit [mono g] {s : pushout_cocone f g} (hs : is_colimit s) : mono s.inl :=
+begin
+  convert mono_of_mono_fac
+    (is_colimit.comp_cocone_point_unique_up_to_iso_hom hs (colimit.is_colimit _) _),
+  { refl },
+  { exact abelian.mono_pushout_of_mono_g _ _ }
+end
+
+/-- Suppose `f` and `g` are two morphisms with a common domain and suppose we have written `g` as
+    an epimorphism followed by a monomorphism. If `f` factors through the epi part of this
+    factorization, then any pushout of `g` along `f` is a monomorphism. -/
+lemma mono_inl_of_factor_thru_epi_mono_factorization (f : X ⟶ Y) (g : X ⟶ Z)
+  (g₁ : X ⟶ W) [epi g₁] (g₂ : W ⟶ Z) [mono g₂] (hg : g₁ ≫ g₂ = g) (f' : W ⟶ Y) (hf : g₁ ≫ f' = f)
+  (t : pushout_cocone f g) (ht : is_colimit t) : mono t.inl :=
+by apply mono_inl_of_is_colimit _ _ (pushout_cocone.is_colimit_of_factors _ _ _ _ _ hf hg t ht)
+
 end mono_pushout
 
 end category_theory.abelian

src/category_theory/abelian/diagram_lemmas/four.lean

@@ -6,32 +6,49 @@ Authors: Markus Himmel
 import category_theory.abelian.pseudoelements
 
 /-!
-# The four lemma
+# The four and five lemmas
 
 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'
+A ---f--> B ---g--> C ---h--> D ---i--> E
+|         |         |         |         |
+α         β         γ         δ         ε
+|         |         |         |         |
+v         v         v         v         v
+A' --f'-> B' --g'-> C' --h'-> D' --i'-> E'
 ```
 
-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.
+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
+
+To show the mono version, we use pseudoelements. For the epi version, we use a completely different
+arrow-theoretic proof. In theory, it should be sufficient to have one version and the other should
+follow automatically by duality. In practice, mathlib's knowledge about duality isn't quite at the
+point where this is doable easily.
+
+However, one key duality statement about exactness is needed in the proof of the epi version of the
+four lemma: we need to know that exactness of a pair `(f, g)`, which we defined via the map from
+the image of `f` to the kernel of `g`, is the same as "co-exactness", defined via the map from the
+cokernel of `f` to the coimage of `g` (more precisely, we only need the consequence that if `(f, g)`
+is exact, then the factorization of `g` through the cokernel of `f` is monomorphic). Luckily, in the
+case of abelian categories, we have the characterization that `(f, g)` is exact if and only if
+`f ≫ g = 0` and `kernel.ι g ≫ cokernel.π f = 0`, and the latter condition is self dual, so the
+equivalence of exactness and co-exactness follows easily.
 
 ## Tags
 
-four lemma, diagram lemma, diagram chase
+four lemma, five lemma, diagram lemma, diagram chase
 -/
 open category_theory (hiding comp_apply)
 open category_theory.abelian.pseudoelement
+open category_theory.limits
 
 universes v u
 
@@ -46,11 +63,14 @@ variables {A B C D A' B' C' D' : V}
 variables {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D}
 variables {f' : A' ⟶ B'} {g' : B' ⟶ C'} {h' : C' ⟶ D'}
 variables {α : A ⟶ A'} {β : B ⟶ B'} {γ : C ⟶ C'} {δ : D ⟶ D'}
-variables [exact f g] [exact g h] [exact f' g']
 variables (comm₁ : α ≫ f' = f ≫ β) (comm₂ : β ≫ g' = g ≫ γ) (comm₃ : γ ≫ h' = h ≫ δ)
 include comm₁ comm₂ comm₃
 
-/-- The four lemma, mono version. For names of objects and morphisms, consider the following
+section
+variables [exact f g] [exact g h] [exact f' g']
+
+
+/-- The four lemma, mono version. For names of objects and morphisms, refer to the following
     diagram:
 
 ```
@@ -85,4 +105,76 @@ mono_of_zero_of_map_zero _ $ λ c hc,
          ... = g (f a) : by rw this
          ... = 0       : pseudo_exact_of_exact.1 _
 
+end
+
+section
+variables [exact g h] [exact f' g'] [exact g' h']
+
+/-- The four lemma, epi version. For names of objects and morphisms, refer to the following
+    diagram:
+
+```
+A ---f--> B ---g--> C ---h--> D
+|         |         |         |
+α         β         γ         δ
+|         |         |         |
+v         v         v         v
+A' --f'-> B' --g'-> C' --h'-> D'
+```
+-/
+lemma epi_of_epi_of_epi_of_mono (hα : epi α) (hγ : epi γ) (hδ : mono δ) : epi β :=
+preadditive.epi_of_cancel_zero _ $ λ R r hβr,
+  have hf'r : f' ≫ r = 0, from limits.zero_of_epi_comp α $
+    calc α ≫ f' ≫ r = f ≫ β ≫ r : by rw reassoc_of comm₁
+                 ... = f ≫ 0      : by rw hβr
+                 ... = 0           : has_zero_morphisms.comp_zero _ _,
+  let y : R ⟶ pushout r g' := pushout.inl, z : C' ⟶ pushout r g' := pushout.inr in
+  have mono y, from mono_inl_of_factor_thru_epi_mono_factorization r g' (cokernel.π f')
+    (cokernel.desc f' g' (by simp)) (by simp) (cokernel.desc f' r hf'r) (by simp) _
+    (colimit.is_colimit _),
+  have hz : g ≫ γ ≫ z = 0, from
+    calc g ≫ γ ≫ z = β ≫ g' ≫ z : by rw ←reassoc_of comm₂
+                ... = β ≫ r ≫ y  : by rw ←pushout.condition
+                ... = 0 ≫ y       : by rw reassoc_of hβr
+                ... = 0           : has_zero_morphisms.zero_comp _ _,
+  let v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl,
+      w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr in
+  have mono v, from mono_inl_of_factor_thru_epi_mono_factorization _ _ (cokernel.π g)
+    (cokernel.desc g h (by simp) ≫ δ) (by simp) (cokernel.desc _ _ hz) (by simp) _
+    (colimit.is_colimit _),
+  have hzv : z ≫ v = h' ≫ w, from (cancel_epi γ).1 $
+    calc γ ≫ z ≫ v = h ≫ δ ≫ w  : by rw [←category.assoc, pushout.condition, category.assoc]
+                ... = γ ≫ h' ≫ w : by rw reassoc_of comm₃,
+  suffices (r ≫ y) ≫ v = 0, by exactI zero_of_comp_mono _ (zero_of_comp_mono _ this),
+  calc (r ≫ y) ≫ v = g' ≫ z ≫ v : by rw [pushout.condition, category.assoc]
+                ... = g' ≫ h' ≫ w : by rw hzv
+                ... = 0 ≫ w        : exact.w_assoc _
+                ... = 0            : has_zero_morphisms.zero_comp _ _
+
+end
+
+section five
+variables {E E' : V} {i : D ⟶ E} {i' : D' ⟶ E'} {ε : E ⟶ E'} (comm₄ : δ ≫ i' = i ≫ ε)
+variables [exact f g] [exact g h] [exact h i] [exact f' g'] [exact g' h'] [exact h' i']
+variables [is_iso α] [is_iso β] [is_iso δ] [is_iso ε]
+include comm₄
+
+
+/-- The five lemma. For names of objects and morphisms, refer to the following diagram:
+
+```
+A ---f--> B ---g--> C ---h--> D ---i--> E
+|         |         |         |         |
+α         β         γ         δ         ε
+|         |         |         |         |
+v         v         v         v         v
+A' --f'-> B' --g'-> C' --h'-> D' --i'-> E'
+```
+-/
+lemma is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso : is_iso γ :=
+have mono γ, by apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃; apply_instance,
+have epi γ, by apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄; apply_instance,
+by exactI is_iso_of_mono_of_epi _
+
+end five
 end category_theory.abelian

src/category_theory/abelian/exact.lean

@@ -117,9 +117,32 @@ def is_limit_image' [h : exact f g] :
   is_limit (kernel_fork.of_ι (image.ι f) (image_ι_comp_eq_zero h.1)) :=
 is_kernel.iso_kernel _ _ (is_limit_image f g) (image_iso_image f).symm $ is_image.lift_fac _ _
 
+/-- If `(f, g)` is exact, then `coimages.coimage.π g` is a cokernel of `f`. -/
+def is_colimit_coimage [h : exact f g] : is_colimit (cokernel_cofork.of_π (coimages.coimage.π g)
+  (coimages.comp_coimage_π_eq_zero h.1) : cokernel_cofork f) :=
+begin
+  rw exact_iff at h,
+  refine is_colimit.of_π _ _ _ _ _,
+  { refine λ W u hu, cokernel.desc (kernel.ι g) u _,
+    rw [←cokernel.π_desc f u hu, ←category.assoc, h.2, has_zero_morphisms.zero_comp] },
+  tidy
+end
+
+/-- If `(f, g)` is exact, then `factor_thru_image g` is a cokernel of `f`. -/
+def is_colimit_image [h : exact f g] :
+  is_colimit (cokernel_cofork.of_π (factor_thru_image g) (comp_factor_thru_image_eq_zero h.1)) :=
+is_cokernel.cokernel_iso _ _ (is_colimit_coimage f g) (coimage_iso_image' g) $
+  (cancel_mono (image.ι g)).1 $ by simp
+
 lemma exact_cokernel : exact f (cokernel.π f) :=
 by { rw exact_iff, tidy }
 
+instance [exact f g] : mono (cokernel.desc f g (by simp)) :=
+suffices h : cokernel.desc f g (by simp) =
+  (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) (is_colimit_image f g)).hom
+    ≫ image.ι g, by { rw h, apply mono_comp },
+(cancel_epi (cokernel.π f)).1 $ by simp
+
 section
 variables (Z)
 

src/category_theory/limits/shapes/pullbacks.lean

@@ -144,7 +144,7 @@ def diagram_iso_span (F : walking_span ⥤ C) :
   F ≅ span (F.map fst) (F.map snd) :=
 nat_iso.of_components (λ j, eq_to_iso (by tidy)) (by tidy)
 
-variables {X Y Z : C}
+variables {W X Y Z : C}
 
 /-- A pullback cone is just a cone on the cospan formed by two morphisms `f : X ⟶ Z` and
     `g : Y ⟶ Z`.-/
@@ -278,6 +278,25 @@ lemma mono_of_is_limit_mk_id_id (f : X ⟶ Y)
   mono f :=
 ⟨λ Z g h eq, by { rcases pullback_cone.is_limit.lift' t _ _ eq with ⟨_, rfl, rfl⟩, refl } ⟩
 
+/-- Suppose `f` and `g` are two morphisms with a common codomain and `s` is a limit cone over the
+    diagram formed by `f` and `g`. Suppose `f` and `g` both factor through a monomorphism `h` via
+    `x` and `y`, respectively.  Then `s` is also a limit cone over the diagram formed by `x` and
+    `y`.  -/
+def is_limit_of_factors (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [mono h]
+  (x : X ⟶ W) (y : Y ⟶ W) (hxh : x ≫ h = f) (hyh : y ≫ h = g) (s : pullback_cone f g)
+  (hs : is_limit s) : is_limit (pullback_cone.mk _ _ (show s.fst ≫ x = s.snd ≫ y,
+    from (cancel_mono h).1 $ by simp only [category.assoc, hxh, hyh, s.condition])) :=
+pullback_cone.is_limit_aux' _ $ λ t,
+  ⟨hs.lift (pullback_cone.mk t.fst t.snd $ by rw [←hxh, ←hyh, reassoc_of t.condition]),
+  ⟨hs.fac _ walking_cospan.left, hs.fac _ walking_cospan.right, λ r hr hr',
+  begin
+    apply pullback_cone.is_limit.hom_ext hs;
+    simp only [pullback_cone.mk_fst, pullback_cone.mk_snd] at ⊢ hr hr';
+    simp only [hr, hr'];
+    symmetry,
+    exacts [hs.fac _ walking_cospan.left, hs.fac _ walking_cospan.right]
+  end⟩⟩
+
 end pullback_cone
 
 /-- A pushout cocone is just a cocone on the span formed by two morphisms `f : X ⟶ Y` and
@@ -391,6 +410,26 @@ begin
   { rwa (is_colimit.desc' t _ _ _).2.2 },
 end
 
+/-- Suppose `f` and `g` are two morphisms with a common domain and `s` is a colimit cocone over the
+    diagram formed by `f` and `g`. Suppose `f` and `g` both factor through an epimorphism `h` via
+    `x` and `y`, respectively. Then `s` is also a colimit cocone over the diagram formed by `x` and
+    `y`.  -/
+def is_colimit_of_factors (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) [epi h]
+  (x : W ⟶ Y) (y : W ⟶ Z) (hhx : h ≫ x = f) (hhy : h ≫ y = g) (s : pushout_cocone f g)
+  (hs : is_colimit s) : is_colimit (pushout_cocone.mk _ _ (show x ≫ s.inl = y ≫ s.inr,
+    from (cancel_epi h).1 $ by rw [reassoc_of hhx, reassoc_of hhy, s.condition])) :=
+pushout_cocone.is_colimit_aux' _ $ λ t,
+  ⟨hs.desc (pushout_cocone.mk t.inl t.inr $
+    by rw [←hhx, ←hhy, category.assoc, category.assoc, t.condition]),
+  ⟨hs.fac _ walking_span.left, hs.fac _ walking_span.right, λ r hr hr',
+  begin
+    apply pushout_cocone.is_colimit.hom_ext hs;
+    simp only [pushout_cocone.mk_inl, pushout_cocone.mk_inr] at ⊢ hr hr';
+    simp only [hr, hr'];
+    symmetry,
+    exacts [hs.fac _ walking_span.left, hs.fac _ walking_span.right]
+  end⟩⟩
+
 end pushout_cocone
 
 /-- This is a helper construction that can be useful when verifying that a category has all

src/category_theory/limits/shapes/zero.lean

@@ -415,6 +415,10 @@ lemma image_ι_comp_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [has_image f
   [epi (factor_thru_image f)] (h : f ≫ g = 0) : image.ι f ≫ g = 0 :=
 zero_of_epi_comp (factor_thru_image f) $ by simp [h]
 
+lemma comp_factor_thru_image_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [has_image g]
+  (h : f ≫ g = 0) : f ≫ factor_thru_image g = 0 :=
+zero_of_comp_mono (image.ι g) $ by simp [h]
+
 variables [has_zero_object C]
 open_locale zero_object
 

src/category_theory/subobject/limits.lean

@@ -115,6 +115,11 @@ def factor_thru_kernel_subobject {W : C} (h : W ⟶ X) (w : h ≫ f = 0) :
   factor_thru_kernel_subobject f h w ≫ (kernel_subobject f).arrow = h :=
 by { dsimp [factor_thru_kernel_subobject], simp, }
 
+@[simp] lemma factor_thru_kernel_subobject_comp_kernel_subobject_iso {W : C} (h : W ⟶ X)
+  (w : h ≫ f = 0) :
+  factor_thru_kernel_subobject f h w ≫ (kernel_subobject_iso f).hom = kernel.lift f h w :=
+(cancel_mono (kernel.ι f)).1 $ by simp
+
 section
 variables {f} {X' Y' : C} {f' : X' ⟶ Y'} [has_kernel f']