refactor(category_theory/abelian): trivial generalisations (#12897)

Trivial generalisations of some facts in `category_theory/abelian/non_preadditive.lean`.

They are true more generally, and this refactor will make it easier to do some other clean-up I'd like to perform on abelian categories.




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/abelian/basic.lean

@@ -143,20 +143,12 @@ variables {P Q : C} (f : P ⟶ Q)
 
 section
 
-lemma mono_of_zero_kernel (R : C)
-  (l : is_limit (kernel_fork.of_ι (0 : R ⟶ P) (show 0 ≫ f = 0, by simp))) : mono f :=
-non_preadditive_abelian.mono_of_zero_kernel _ _ l
-
 lemma mono_of_kernel_ι_eq_zero (h : kernel.ι f = 0) : mono f :=
 mono_of_kernel_zero h
 
-lemma epi_of_zero_cokernel (R : C)
-  (l : is_colimit (cokernel_cofork.of_π (0 : Q ⟶ R) (show f ≫ 0 = 0, by simp))) : epi f :=
-non_preadditive_abelian.epi_of_zero_cokernel _ _ l
-
 lemma epi_of_cokernel_π_eq_zero (h : cokernel.π f = 0) : epi f :=
 begin
-  apply epi_of_zero_cokernel _ (cokernel f),
+  apply normal_mono_category.epi_of_zero_cokernel _ (cokernel f),
   simp_rw ←h,
   exact is_colimit.of_iso_colimit (colimit.is_colimit (parallel_pair f 0)) (iso_of_π _)
 end

src/category_theory/abelian/non_preadditive.lean

@@ -5,7 +5,7 @@ Authors: Markus Himmel
 -/
 import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.kernels
-import category_theory.limits.shapes.normal_mono
+import category_theory.limits.shapes.normal_mono.equalizers
 import category_theory.preadditive
 
 /-!
@@ -85,248 +85,7 @@ namespace category_theory.non_preadditive_abelian
 
 universes v u
 
-variables {C : Type u} [category.{v} C]
-
-
-section
-variables [non_preadditive_abelian C]
-
-/-- The pullback of two monomorphisms exists. -/
-@[irreducible]
-lemma pullback_of_mono {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [mono a] [mono b] :
-  has_limit (cospan a b) :=
-let ⟨P, f, haf, i⟩ := normal_mono_of_mono a in
-let ⟨Q, g, hbg, i'⟩ := normal_mono_of_mono b in
-let ⟨a', ha'⟩ := kernel_fork.is_limit.lift' i (kernel.ι (prod.lift f g)) $
-    calc kernel.ι (prod.lift f g) ≫ f
-        = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ limits.prod.fst : by rw prod.lift_fst
-    ... = (0 : kernel (prod.lift f g) ⟶ P ⨯ Q) ≫ limits.prod.fst : by rw kernel.condition_assoc
-    ... = 0 : zero_comp in
-let ⟨b', hb'⟩ := kernel_fork.is_limit.lift' i' (kernel.ι (prod.lift f g)) $
-    calc kernel.ι (prod.lift f g) ≫ g
-        = kernel.ι (prod.lift f g) ≫ (prod.lift f g) ≫ limits.prod.snd : by rw prod.lift_snd
-    ... = (0 : kernel (prod.lift f g) ⟶ P ⨯ Q) ≫ limits.prod.snd : by rw kernel.condition_assoc
-    ... = 0 : zero_comp in
-has_limit.mk { cone := pullback_cone.mk a' b' $ by { simp at ha' hb', rw [ha', hb'] },
-  is_limit := pullback_cone.is_limit.mk _
-    (λ s, kernel.lift (prod.lift f g) (pullback_cone.snd s ≫ b) $ prod.hom_ext
-      (calc ((pullback_cone.snd s ≫ b) ≫ prod.lift f g) ≫ limits.prod.fst
-            = pullback_cone.snd s ≫ b ≫ f : by simp only [prod.lift_fst, category.assoc]
-        ... = pullback_cone.fst s ≫ a ≫ f : by rw pullback_cone.condition_assoc
-        ... = pullback_cone.fst s ≫ 0 : by rw haf
-        ... = 0 ≫ limits.prod.fst :
-          by rw [comp_zero, zero_comp])
-      (calc ((pullback_cone.snd s ≫ b) ≫ prod.lift f g) ≫ limits.prod.snd
-            = pullback_cone.snd s ≫ b ≫ g : by simp only [prod.lift_snd, category.assoc]
-        ... = pullback_cone.snd s ≫ 0 : by rw hbg
-        ... = 0 ≫ limits.prod.snd :
-          by rw [comp_zero, zero_comp]))
-    (λ s, (cancel_mono a).1 $
-      by { rw kernel_fork.ι_of_ι at ha', simp [ha', pullback_cone.condition s] })
-    (λ s, (cancel_mono b).1 $
-      by { rw kernel_fork.ι_of_ι at hb', simp [hb'] })
-    (λ s m h₁ h₂, (cancel_mono (kernel.ι (prod.lift f g))).1 $ calc m ≫ kernel.ι (prod.lift f g)
-          = m ≫ a' ≫ a : by { congr, exact ha'.symm }
-      ... = pullback_cone.fst s ≫ a : by rw [←category.assoc, h₁]
-      ... = pullback_cone.snd s ≫ b : pullback_cone.condition s
-      ... = kernel.lift (prod.lift f g) (pullback_cone.snd s ≫ b) _ ≫ kernel.ι (prod.lift f g) :
-        by rw kernel.lift_ι) }
-
-/-- The pushout of two epimorphisms exists. -/
-@[irreducible]
-lemma pushout_of_epi {X Y Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [epi a] [epi b] :
-  has_colimit (span a b) :=
-let ⟨P, f, hfa, i⟩ := normal_epi_of_epi a in
-let ⟨Q, g, hgb, i'⟩ := normal_epi_of_epi b in
-let ⟨a', ha'⟩ := cokernel_cofork.is_colimit.desc' i (cokernel.π (coprod.desc f g)) $
-  calc f ≫ cokernel.π (coprod.desc f g)
-      = coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) : by rw coprod.inl_desc_assoc
-  ... = coprod.inl ≫ (0 : P ⨿ Q ⟶ cokernel (coprod.desc f g)) : by rw cokernel.condition
-  ... = 0 : has_zero_morphisms.comp_zero _ _ in
-let ⟨b', hb'⟩ := cokernel_cofork.is_colimit.desc' i' (cokernel.π (coprod.desc f g)) $
-  calc g ≫ cokernel.π (coprod.desc f g)
-      = coprod.inr ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) : by rw coprod.inr_desc_assoc
-  ... = coprod.inr ≫ (0 : P ⨿ Q ⟶ cokernel (coprod.desc f g)) :  by rw cokernel.condition
-  ... = 0 : has_zero_morphisms.comp_zero _ _ in
-has_colimit.mk
-{ cocone := pushout_cocone.mk a' b' $ by { simp only [cofork.π_of_π] at ha' hb', rw [ha', hb'] },
-  is_colimit := pushout_cocone.is_colimit.mk _
-  (λ s, cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) $ coprod.hom_ext
-    (calc coprod.inl ≫ coprod.desc f g ≫ b ≫ pushout_cocone.inr s
-          = f ≫ b ≫ pushout_cocone.inr s : by rw coprod.inl_desc_assoc
-      ... = f ≫ a ≫ pushout_cocone.inl s : by rw pushout_cocone.condition
-      ... = 0 ≫ pushout_cocone.inl s : by rw reassoc_of hfa
-      ... = coprod.inl ≫ 0 : by rw [comp_zero, zero_comp])
-    (calc coprod.inr ≫ coprod.desc f g ≫ b ≫ pushout_cocone.inr s
-          = g ≫ b ≫ pushout_cocone.inr s : by rw coprod.inr_desc_assoc
-      ... = 0 ≫ pushout_cocone.inr s : by rw reassoc_of hgb
-      ... = coprod.inr ≫ 0 : by rw [comp_zero, zero_comp]))
-  (λ s, (cancel_epi a).1 $
-    by { rw cokernel_cofork.π_of_π at ha', simp [reassoc_of ha', pushout_cocone.condition s] })
-  (λ s, (cancel_epi b).1 $ by { rw cokernel_cofork.π_of_π at hb', simp [reassoc_of hb'] })
-  (λ s m h₁ h₂, (cancel_epi (cokernel.π (coprod.desc f g))).1 $
-  calc cokernel.π (coprod.desc f g) ≫ m
-        = (a ≫ a') ≫ m : by { congr, exact ha'.symm }
-    ... = a ≫ pushout_cocone.inl s : by rw [category.assoc, h₁]
-    ... = b ≫ pushout_cocone.inr s : pushout_cocone.condition s
-    ... = cokernel.π (coprod.desc f g) ≫
-            cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) _ :
-      by rw cokernel.π_desc) }
-
-section
-
-local attribute [instance] pullback_of_mono
-
-/-- The pullback of `(𝟙 X, f)` and `(𝟙 X, g)` -/
-private abbreviation P {X Y : C} (f g : X ⟶ Y)
-  [mono (prod.lift (𝟙 X) f)] [mono (prod.lift (𝟙 X) g)] : C :=
-pullback (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
-
-/-- The equalizer of `f` and `g` exists. -/
-@[irreducible]
-lemma has_limit_parallel_pair {X Y : C} (f g : X ⟶ Y) : has_limit (parallel_pair f g) :=
-have huv : (pullback.fst : P f g ⟶ X) = pullback.snd, from
-  calc (pullback.fst : P f g ⟶ X) = pullback.fst ≫ 𝟙 _ : eq.symm $ category.comp_id _
-    ... = pullback.fst ≫ prod.lift (𝟙 X) f ≫ limits.prod.fst : by rw prod.lift_fst
-    ... = pullback.snd ≫ prod.lift (𝟙 X) g ≫ limits.prod.fst : by rw pullback.condition_assoc
-    ... = pullback.snd : by rw [prod.lift_fst, category.comp_id],
-have hvu : (pullback.fst : P f g ⟶ X) ≫ f = pullback.snd ≫ g, from
-  calc (pullback.fst : P f g ⟶ X) ≫ f
-        = pullback.fst ≫ prod.lift (𝟙 X) f ≫ limits.prod.snd : by rw prod.lift_snd
-    ... = pullback.snd ≫ prod.lift (𝟙 X) g ≫ limits.prod.snd : by rw pullback.condition_assoc
-    ... = pullback.snd ≫ g : by rw prod.lift_snd,
-have huu : (pullback.fst : P f g ⟶ X) ≫ f = pullback.fst ≫ g, by rw [hvu, ←huv],
-has_limit.mk { cone := fork.of_ι pullback.fst huu,
-  is_limit := fork.is_limit.mk _
-  (λ s, pullback.lift (fork.ι s) (fork.ι s) $ prod.hom_ext
-    (by simp only [prod.lift_fst, category.assoc])
-    (by simp only [fork.app_zero_right, fork.app_zero_left, prod.lift_snd, category.assoc]))
-  (λ s, by simp only [fork.ι_of_ι, pullback.lift_fst])
-  (λ s m h, pullback.hom_ext
-    (by simpa only [pullback.lift_fst] using h walking_parallel_pair.zero)
-    (by simpa only [huv.symm, pullback.lift_fst] using h walking_parallel_pair.zero)) }
-
-end
-
-section
-local attribute [instance] pushout_of_epi
-
-/-- The pushout of `(𝟙 Y, f)` and `(𝟙 Y, g)`. -/
-private abbreviation Q {X Y : C} (f g : X ⟶ Y)
-  [epi (coprod.desc (𝟙 Y) f)] [epi (coprod.desc (𝟙 Y) g)] : C :=
-pushout (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
-
-/-- The coequalizer of `f` and `g` exists. -/
-@[irreducible]
-lemma has_colimit_parallel_pair {X Y : C} (f g : X ⟶ Y) : has_colimit (parallel_pair f g) :=
-have huv : (pushout.inl : Y ⟶ Q f g) = pushout.inr, from
-  calc (pushout.inl : Y ⟶ Q f g) = 𝟙 _ ≫ pushout.inl : eq.symm $ category.id_comp _
-    ... = (coprod.inl ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl : by rw coprod.inl_desc
-    ... = (coprod.inl ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr :
-      by simp only [category.assoc, pushout.condition]
-    ... = pushout.inr : by rw [coprod.inl_desc, category.id_comp],
-have hvu : f ≫ (pushout.inl : Y ⟶ Q f g) = g ≫ pushout.inr, from
-  calc f ≫ (pushout.inl : Y ⟶ Q f g)
-        = (coprod.inr ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl : by rw coprod.inr_desc
-    ... = (coprod.inr ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr :
-      by simp only [category.assoc, pushout.condition]
-    ... = g ≫ pushout.inr : by rw coprod.inr_desc,
-have huu : f ≫ (pushout.inl : Y ⟶ Q f g) = g ≫ pushout.inl, by rw [hvu, huv],
-has_colimit.mk { cocone := cofork.of_π pushout.inl huu,
-  is_colimit := cofork.is_colimit.mk _
-  (λ s, pushout.desc (cofork.π s) (cofork.π s) $ coprod.hom_ext
-    (by simp only [coprod.inl_desc_assoc])
-    (by simp only [cofork.right_app_one, coprod.inr_desc_assoc, cofork.left_app_one]))
-  (λ s, by simp only [pushout.inl_desc, cofork.π_of_π])
-  (λ s m h, pushout.hom_ext
-    (by simpa only [pushout.inl_desc] using h walking_parallel_pair.one)
-    (by simpa only [huv.symm, pushout.inl_desc] using h walking_parallel_pair.one)) }
-
-end
-
-section
-local attribute [instance] has_limit_parallel_pair
-
-/-- A `non_preadditive_abelian` category has all equalizers. -/
-@[priority 100] instance has_equalizers : has_equalizers C :=
-has_equalizers_of_has_limit_parallel_pair _
-
-end
-
-section
-local attribute [instance] has_colimit_parallel_pair
-
-/-- A `non_preadditive_abelian` category has all coequalizers. -/
-@[priority 100] instance has_coequalizers : has_coequalizers C :=
-has_coequalizers_of_has_colimit_parallel_pair _
-
-end
-
-section
-
-/-- If a zero morphism is a kernel of `f`, then `f` is a monomorphism. -/
-lemma mono_of_zero_kernel {X Y : C} (f : X ⟶ Y) (Z : C)
-  (l : is_limit (kernel_fork.of_ι (0 : Z ⟶ X) (show 0 ≫ f = 0, by simp))) : mono f :=
-⟨λ P u v huv,
- begin
-  obtain ⟨W, w, hw, hl⟩ := normal_epi_of_epi (coequalizer.π u v),
-  obtain ⟨m, hm⟩ := coequalizer.desc' f huv,
-  have hwf : w ≫ f = 0,
-  { rw [←hm, reassoc_of hw, zero_comp] },
-  obtain ⟨n, hn⟩ := kernel_fork.is_limit.lift' l _ hwf,
-  rw [fork.ι_of_ι, has_zero_morphisms.comp_zero] at hn,
-  haveI : is_iso (coequalizer.π u v),
-  { apply is_iso_colimit_cocone_parallel_pair_of_eq hn.symm hl },
-  apply (cancel_mono (coequalizer.π u v)).1,
-  exact coequalizer.condition _ _
- end⟩
-
-/-- If a zero morphism is a cokernel of `f`, then `f` is an epimorphism. -/
-lemma epi_of_zero_cokernel {X Y : C} (f : X ⟶ Y) (Z : C)
-  (l : is_colimit (cokernel_cofork.of_π (0 : Y ⟶ Z) (show f ≫ 0 = 0, by simp))) : epi f :=
-⟨λ P u v huv,
- begin
-  obtain ⟨W, w, hw, hl⟩ := normal_mono_of_mono (equalizer.ι u v),
-  obtain ⟨m, hm⟩ := equalizer.lift' f huv,
-  have hwf : f ≫ w = 0,
-  { rw [←hm, category.assoc, hw, comp_zero] },
-  obtain ⟨n, hn⟩ := cokernel_cofork.is_colimit.desc' l _ hwf,
-  rw [cofork.π_of_π, zero_comp] at hn,
-  haveI : is_iso (equalizer.ι u v),
-  { apply is_iso_limit_cone_parallel_pair_of_eq hn.symm hl },
-  apply (cancel_epi (equalizer.ι u v)).1,
-  exact equalizer.condition _ _
- end⟩
-
-open_locale zero_object
-
-/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `0 : 0 ⟶ X` is a kernel of `f`. -/
-def zero_kernel_of_cancel_zero {X Y : C} (f : X ⟶ Y)
-  (hf : ∀ (Z : C) (g : Z ⟶ X) (hgf : g ≫ f = 0), g = 0) :
-    is_limit (kernel_fork.of_ι (0 : 0 ⟶ X) (show 0 ≫ f = 0, by simp)) :=
-fork.is_limit.mk _ (λ s, 0)
-  (λ s, by rw [hf _ _ (kernel_fork.condition s), zero_comp])
-  (λ s m h, by ext)
-
-/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `0 : Y ⟶ 0` is a cokernel of `f`. -/
-def zero_cokernel_of_zero_cancel {X Y : C} (f : X ⟶ Y)
-  (hf : ∀ (Z : C) (g : Y ⟶ Z) (hgf : f ≫ g = 0), g = 0) :
-    is_colimit (cokernel_cofork.of_π (0 : Y ⟶ 0) (show f ≫ 0 = 0, by simp)) :=
-cofork.is_colimit.mk _ (λ s, 0)
-  (λ s, by rw [hf _ _ (cokernel_cofork.condition s), comp_zero])
-  (λ s m h, by ext)
-
-/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `f` is a monomorphism. -/
-lemma mono_of_cancel_zero {X Y : C} (f : X ⟶ Y)
-  (hf : ∀ (Z : C) (g : Z ⟶ X) (hgf : g ≫ f = 0), g = 0) : mono f :=
-mono_of_zero_kernel f 0 $ zero_kernel_of_cancel_zero f hf
-
-/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `g` is a monomorphism. -/
-lemma epi_of_zero_cancel {X Y : C} (f : X ⟶ Y)
-  (hf : ∀ (Z : C) (g : Y ⟶ Z) (hgf : f ≫ g = 0), g = 0) : epi f :=
-epi_of_zero_cokernel f 0 $ zero_cokernel_of_zero_cancel f hf
-
-end
+variables {C : Type u} [category.{v} C] [non_preadditive_abelian C]
 
 section factor
 
@@ -353,7 +112,7 @@ instance : epi (non_preadditive_abelian.factor_thru_image f) :=
 let I := non_preadditive_abelian.image f, p := non_preadditive_abelian.factor_thru_image f,
     i := kernel.ι (cokernel.π f) in
 -- It will suffice to consider some g : I ⟶ R such that p ≫ g = 0 and show that g = 0.
-epi_of_zero_cancel _ $ λ R (g : I ⟶ R) (hpg : p ≫ g = 0),
+normal_mono_category.epi_of_zero_cancel _ $ λ R (g : I ⟶ R) (hpg : p ≫ g = 0),
 begin
   -- Since C is abelian, u := ker g ≫ i is the kernel of some morphism h.
   let u := kernel.ι g ≫ i,
@@ -407,7 +166,7 @@ cokernel.π_desc _ _ _
 instance : mono (non_preadditive_abelian.factor_thru_coimage f) :=
 let I := non_preadditive_abelian.coimage f, i := non_preadditive_abelian.factor_thru_coimage f,
     p := cokernel.π (kernel.ι f) in
-mono_of_cancel_zero _ $ λ R (g : R ⟶ I) (hgi : g ≫ i = 0),
+normal_epi_category.mono_of_cancel_zero _ $ λ R (g : R ⟶ I) (hgi : g ≫ i = 0),
 begin
   -- Since C is abelian, u := p ≫ coker g is the cokernel of some morphism h.
   let u := p ≫ cokernel.π g,
@@ -483,7 +242,7 @@ instance mono_r {A : C} : mono (r A) :=
 begin
   let hl : is_limit (kernel_fork.of_ι (diag A) (cokernel.condition (diag A))),
   { exact mono_is_kernel_of_cokernel _ (colimit.is_colimit _) },
-  apply mono_of_cancel_zero,
+  apply normal_epi_category.mono_of_cancel_zero,
   intros Z x hx,
   have hxx : (x ≫ prod.lift (𝟙 A) (0 : A ⟶ A)) ≫ cokernel.π (diag A) = 0,
   { rw [category.assoc, hx] },
@@ -511,7 +270,7 @@ begin
       ext; simp } },
   let hp2 : is_colimit (cokernel_cofork.of_π (limits.prod.snd : A ⨯ A ⟶ A) hlp),
   { exact epi_is_cokernel_of_kernel _ hp1 },
-  apply epi_of_zero_cancel,
+  apply normal_mono_category.epi_of_zero_cancel,
   intros Z z hz,
   have h : prod.lift (𝟙 A) (0 : A ⟶ A) ≫ cokernel.π (diag A) ≫ z = 0,
   { rw [←category.assoc, hz] },
@@ -687,6 +446,4 @@ def preadditive : preadditive C :=
 
 end
 
-end
-
 end category_theory.non_preadditive_abelian

src/category_theory/limits/shapes/kernels.lean

@@ -339,6 +339,14 @@ functor.map_iso (cones.forget _) $ is_limit.unique_up_to_iso
 lemma kernel.ι_of_mono [has_kernel f] [mono f] : kernel.ι f = 0 :=
 zero_of_source_iso_zero _ (kernel.of_mono f)
 
+/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `0 : 0 ⟶ X` is a kernel of `f`. -/
+def zero_kernel_of_cancel_zero {X Y : C} (f : X ⟶ Y)
+  (hf : ∀ (Z : C) (g : Z ⟶ X) (hgf : g ≫ f = 0), g = 0) :
+    is_limit (kernel_fork.of_ι (0 : 0 ⟶ X) (show 0 ≫ f = 0, by simp)) :=
+fork.is_limit.mk _ (λ s, 0)
+  (λ s, by rw [hf _ _ (kernel_fork.condition s), zero_comp])
+  (λ s m h, by ext)
+
 end has_zero_object
 
 section transport
@@ -714,6 +722,14 @@ instance cokernel.of_kernel_of_mono [has_kernel f]
   [has_cokernel (kernel.ι f)] [mono f] : is_iso (cokernel.π (kernel.ι f)) :=
 coequalizer.π_of_eq $ kernel.ι_of_mono f
 
+/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `0 : Y ⟶ 0` is a cokernel of `f`. -/
+def zero_cokernel_of_zero_cancel {X Y : C} (f : X ⟶ Y)
+  (hf : ∀ (Z : C) (g : Y ⟶ Z) (hgf : f ≫ g = 0), g = 0) :
+    is_colimit (cokernel_cofork.of_π (0 : Y ⟶ 0) (show f ≫ 0 = 0, by simp)) :=
+cofork.is_colimit.mk _ (λ s, 0)
+  (λ s, by rw [hf _ _ (cokernel_cofork.condition s), comp_zero])
+  (λ s m h, by ext)
+
 end has_zero_object
 
 section transport