feat(category_theory): (co)equalizers and (co)kernels when composing …

…with monos/epis (#12828)

src/category_theory/limits/shapes/equalizers.lean

@@ -922,6 +922,23 @@ def split_mono_of_equalizer {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : f ≫ r
   id' := fork.is_limit.hom_ext h
     ((category.assoc _ _ _).trans $ hr.trans (category.id_comp _).symm) }
 
+variables {C f g}
+
+/-- The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer. -/
+def is_equalizer_comp_mono {c : fork f g} (i : is_limit c) {Z : C} (h : Y ⟶ Z) [hm : mono h] :
+  is_limit (fork.of_ι c.ι (by simp) : fork (f ≫ h) (g ≫ h)) :=
+fork.is_limit.mk' _ $ λ s,
+  let s' : fork f g := fork.of_ι s.ι (by apply hm.right_cancellation; simp [s.condition]) in
+  let l := fork.is_limit.lift' i s'.ι s'.condition in
+  ⟨l.1, l.2, λ m hm, by apply fork.is_limit.hom_ext i; rw fork.ι_of_ι at hm; rw hm; exact l.2.symm⟩
+
+variables (C f g)
+
+@[instance]
+lemma has_equalizer_comp_mono [has_equalizer f g] {Z : C} (h : Y ⟶ Z) [mono h] :
+  has_equalizer (f ≫ h) (g ≫ h) :=
+⟨⟨{ cone := _, is_limit := is_equalizer_comp_mono (limit.is_limit _) h }⟩⟩
+
 /-- An equalizer of an idempotent morphism and the identity is split mono. -/
 def split_mono_of_idempotent_of_is_limit_fork {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
   {c : fork f (𝟙 X)} (i : is_limit c) : split_mono c.ι :=
@@ -971,6 +988,25 @@ def split_epi_of_coequalizer {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s
 { section_ := s,
   id' := cofork.is_colimit.hom_ext h (hs.trans (category.comp_id _).symm) }
 
+variables {C f g}
+
+/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is 
+a coequalizer. -/
+def is_coequalizer_epi_comp {c : cofork f g} (i : is_colimit c) {W : C} (h : W ⟶ X) [hm : epi h] :
+  is_colimit (cofork.of_π c.π (by simp) : cofork (h ≫ f) (h ≫ g)) :=
+cofork.is_colimit.mk' _ $ λ s,
+  let s' : cofork f g := cofork.of_π s.π 
+    (by apply hm.left_cancellation; simp_rw [←category.assoc, s.condition]) in
+  let l := cofork.is_colimit.desc' i s'.π s'.condition in
+  ⟨l.1, l.2,
+    λ m hm,by apply cofork.is_colimit.hom_ext i; rw cofork.π_of_π at hm; rw hm; exact l.2.symm⟩
+
+lemma has_coequalizer_epi_comp [has_coequalizer f g] {W : C} (h : W ⟶ X) [hm : epi h] :
+  has_coequalizer (h ≫ f) (h ≫ g) :=
+⟨⟨{ cocone := _, is_colimit := is_coequalizer_epi_comp (colimit.is_colimit _) h }⟩⟩
+
+variables (C f g)
+
 /-- A coequalizer of an idempotent morphism and the identity is split epi. -/
 def split_epi_of_idempotent_of_is_colimit_cofork {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
   {c : cofork f (𝟙 X)} (i : is_colimit c) : split_epi c.π :=

src/category_theory/limits/shapes/kernels.lean

@@ -135,6 +135,14 @@ def is_limit.of_ι {W : C} (g : W ⟶ X) (eq : g ≫ f = 0)
   is_limit (kernel_fork.of_ι g eq) :=
 is_limit_aux _ (λ s, lift s.ι s.condition) (λ s, fac s.ι s.condition) (λ s, uniq s.ι s.condition)
 
+/-- Every kernel of `f` induces a kernel of `f ≫ g` if `g` is mono. -/
+def is_kernel_comp_mono  {c : kernel_fork f} (i : is_limit c) {Z} (g : Y ⟶ Z) [hg : mono g] :
+  is_limit (kernel_fork.of_ι c.ι (by simp) : kernel_fork (f ≫ g)) :=
+fork.is_limit.mk' _ $ λ s,
+  let s' : kernel_fork f := fork.of_ι s.ι (by apply hg.right_cancellation; simp [s.condition]) in
+  let l := kernel_fork.is_limit.lift' i s'.ι s'.condition in
+  ⟨l.1, l.2, λ m hm, by apply fork.is_limit.hom_ext i; rw fork.ι_of_ι at hm; rw hm; exact l.2.symm⟩
+
 end
 
 section
@@ -273,14 +281,9 @@ lemma kernel_not_epi_of_nonzero (w : f ≠ 0) : ¬epi (kernel.ι f) :=
 lemma kernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (kernel.ι f)) → false :=
 λ I, kernel_not_epi_of_nonzero w $ by { resetI, apply_instance }
 
--- TODO the remainder of this section has obvious generalizations to `has_equalizer f g`.
-
 instance has_kernel_comp_mono {X Y Z : C} (f : X ⟶ Y) [has_kernel f] (g : Y ⟶ Z) [mono g] :
   has_kernel (f ≫ g) :=
-{ exists_limit :=
-  ⟨{ cone := kernel_fork.of_ι (kernel.ι f) (by simp),
-     is_limit := is_limit_aux _ (λ s, kernel.lift _ s.ι ((cancel_mono g).mp (by simp)))
-      (by tidy) (by tidy) }⟩ }
+⟨⟨{ cone := _, is_limit := is_kernel_comp_mono (limit.is_limit _) g }⟩⟩
 
 /--
 When `g` is a monomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.
@@ -440,6 +443,16 @@ def is_colimit.of_π {Z : C} (g : Y ⟶ Z) (eq : f ≫ g = 0)
   is_colimit (cokernel_cofork.of_π g eq) :=
 is_colimit_aux _ (λ s, desc s.π s.condition) (λ s, fac s.π s.condition) (λ s, uniq s.π s.condition)
 
+/-- Every cokernel of `f` induces a cokernel of `g ≫ f` if `g` is epi. -/
+def is_cokernel_epi_comp  {c : cokernel_cofork f} (i : is_colimit c) {W} (g : W ⟶ X) [hg : epi g] :
+  is_colimit (cokernel_cofork.of_π c.π (by simp) : cokernel_cofork (g ≫ f)) :=
+cofork.is_colimit.mk' _ $ λ s,
+  let s' : cokernel_cofork f := cofork.of_π s.π
+    (by apply hg.left_cancellation; simp [←category.assoc, s.condition]) in
+  let l := cokernel_cofork.is_colimit.desc' i s'.π s'.condition in
+  ⟨l.1, l.2, 
+    λ m hm, by apply cofork.is_colimit.hom_ext i; rw cofork.π_of_π at hm; rw hm; exact l.2.symm⟩
+
 end
 
 section
@@ -602,13 +615,9 @@ def cokernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel f
 { hom := cokernel.desc _ (inv g ≫ cokernel.π f) (by simp),
   inv := cokernel.desc _ (g ≫ cokernel.π (f ≫ g)) (by rw [←category.assoc, cokernel.condition]), }
 
-instance has_cokernel_epi_comp {X Y Z : C} (f : X ⟶ Y) [epi f] (g : Y ⟶ Z) [has_cokernel g] :
-  has_cokernel (f ≫ g) :=
-{ exists_colimit :=
-  ⟨{ cocone := cokernel_cofork.of_π (cokernel.π g) (by simp),
-     is_colimit := is_colimit_aux _
-      (λ s, cokernel.desc _ s.π ((cancel_epi f).mp (by { rw ← category.assoc, simp })))
-      (by tidy) (by tidy) }⟩ }
+instance has_cokernel_epi_comp {X Y : C} (f : X ⟶ Y) [has_cokernel f] {W} (g : W ⟶ X) [epi g] :
+  has_cokernel (g ≫ f) :=
+⟨⟨{ cocone := _, is_colimit := is_cokernel_epi_comp (colimit.is_colimit _) g }⟩⟩
 
 /--
 When `f` is an epimorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.