refactor(category_theory): reverse simp lemmas about (co)forks (#13519)

Makes `fork.ι` instead of `t.π.app zero` so that we avoid any unnecessary references to `walking_parallel_pair` in (co)fork  homs. This induces quite a lot of changes in other files, but I think it's worth the pain. The PR also changes `fork.is_limit.mk` to avoid stating redundant morphisms.

Author: javra

src/algebra/category/Module/kernels.lean

@@ -11,7 +11,6 @@ import algebra.category.Module.epi_mono
 
 open category_theory
 open category_theory.limits
-open category_theory.limits.walking_parallel_pair
 
 universes u v
 
@@ -32,10 +31,7 @@ fork.is_limit.mk _
     by { rw [←@function.comp_apply _ _ _ f (fork.ι s) c, ←coe_comp, fork.condition,
       has_zero_morphisms.comp_zero (fork.ι s) N], refl }))
   (λ s, linear_map.subtype_comp_cod_restrict _ _ _)
-  (λ s m h, linear_map.ext $ λ x, subtype.ext_iff_val.2 $
-    have h₁ : (m ≫ (kernel_cone f).π.app zero).to_fun = (s.π.app zero).to_fun,
-      by { congr, exact h zero },
-    by convert @congr_fun _ _ _ _ h₁ x )
+  (λ s m h, linear_map.ext $ λ x, subtype.ext_iff_val.2 (by simpa [←h]))
 
 /-- The cokernel cocone induced by the projection onto the quotient. -/
 def cokernel_cocone : cokernel_cofork f :=
@@ -50,7 +46,7 @@ cofork.is_colimit.mk _
   begin
     haveI : epi (as_hom f.range.mkq) := (epi_iff_range_eq_top _).mpr (submodule.range_mkq _),
     apply (cancel_epi (as_hom f.range.mkq)).1,
-    convert h walking_parallel_pair.one,
+    convert h,
     exact submodule.liftq_mkq _ _ _
   end)
 end
@@ -86,7 +82,7 @@ limit.iso_limit_cone_inv_π _ _
 
 @[simp, elementwise] lemma kernel_iso_ker_hom_ker_subtype :
   (kernel_iso_ker f).hom ≫ f.ker.subtype = kernel.ι f :=
-is_limit.cone_point_unique_up_to_iso_inv_comp _ (limit.is_limit _) zero
+is_limit.cone_point_unique_up_to_iso_inv_comp _ (limit.is_limit _) walking_parallel_pair.zero
 
 /--
 The categorical cokernel of a morphism in `Module`

src/analysis/normed/group/SemiNormedGroup/kernels.lean

@@ -86,8 +86,7 @@ namespace SemiNormedGroup
 section equalizers_and_kernels
 
 /-- The equalizer cone for a parallel pair of morphisms of seminormed groups. -/
-def parallel_pair_cone {V W : SemiNormedGroup.{u}} (f g : V ⟶ W) :
-  cone (parallel_pair f g) :=
+def fork {V W : SemiNormedGroup.{u}} (f g : V ⟶ W) : fork f g :=
 @fork.of_ι _ _ _ _ _ _ (of (f - g).ker) (normed_group_hom.incl (f - g).ker) $
 begin
   ext v,
@@ -100,7 +99,7 @@ end
 instance has_limit_parallel_pair {V W : SemiNormedGroup.{u}} (f g : V ⟶ W) :
   has_limit (parallel_pair f g) :=
 { exists_limit := nonempty.intro
-  { cone := parallel_pair_cone f g,
+  { cone := fork f g,
     is_limit := fork.is_limit.mk _
       (λ c, normed_group_hom.ker.lift (fork.ι c) _ $
       show normed_group_hom.comp_hom (f - g) c.ι = 0,
@@ -297,7 +296,7 @@ def explicit_cokernel_iso {X Y : SemiNormedGroup.{u}} (f : X ⟶ Y) :
 @[simp]
 lemma explicit_cokernel_iso_hom_π {X Y : SemiNormedGroup.{u}} (f : X ⟶ Y) :
   explicit_cokernel_π f ≫ (explicit_cokernel_iso f).hom = cokernel.π _ :=
-by simp [explicit_cokernel_π, explicit_cokernel_iso]
+by simp [explicit_cokernel_π, explicit_cokernel_iso, is_colimit.cocone_point_unique_up_to_iso]
 
 @[simp]
 lemma explicit_cokernel_iso_inv_π {X Y : SemiNormedGroup.{u}} (f : X ⟶ Y) :
@@ -310,7 +309,8 @@ lemma explicit_cokernel_iso_hom_desc {X Y Z : SemiNormedGroup.{u}} {f : X ⟶ Y}
   (explicit_cokernel_iso f).hom ≫ cokernel.desc f g w = explicit_cokernel_desc w :=
 begin
   ext1,
-  simp [explicit_cokernel_desc, explicit_cokernel_π, explicit_cokernel_iso],
+  simp [explicit_cokernel_desc, explicit_cokernel_π, explicit_cokernel_iso,
+    is_colimit.cocone_point_unique_up_to_iso],
 end
 
 /-- A special case of `category_theory.limits.cokernel.map` adapted to `explicit_cokernel`. -/

src/category_theory/abelian/basic.lean

@@ -498,7 +498,7 @@ fork.is_limit.mk _
     { rw [biprod.lift_fst, pullback.lift_fst] },
     { rw [biprod.lift_snd, pullback.lift_snd] }
   end)
-  (λ s m h, by ext; simp [fork.ι_eq_app_zero, ←h walking_parallel_pair.zero])
+  (λ s m h, by ext; simp [←h])
 
 end pullback_to_biproduct_is_kernel
 
@@ -523,7 +523,7 @@ cofork.is_colimit.mk _
     sub_eq_zero.1 $ by rw [←category.assoc, ←category.assoc, ←sub_comp, sub_eq_add_neg, ←neg_comp,
       ←biprod.lift_eq, cofork.condition s, zero_comp])
   (λ s, by ext; simp)
-  (λ s m h, by ext; simp [cofork.π_eq_app_one, ←h walking_parallel_pair.one] )
+  (λ s m h, by ext; simp [←h] )
 
 end biproduct_to_pushout_is_cokernel
 

src/category_theory/abelian/non_preadditive.lean

@@ -230,7 +230,7 @@ begin
     { intros s m h,
       haveI : mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _),
       apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1,
-      convert h walking_parallel_pair.zero,
+      convert h,
       ext; simp } },
   let hp2 : is_colimit (cokernel_cofork.of_π (limits.prod.snd : A ⨯ A ⟶ A) hlp),
   { exact epi_is_cokernel_of_kernel _ hp1 },

src/category_theory/idempotents/basic.lean

@@ -68,10 +68,10 @@ begin
           split,
           { erw [assoc, h₂, ← limits.fork.condition s, comp_id], },
           { intros m hm,
-            erw [← hm],
-            simp only [← hm, assoc, fork.ι_eq_app_zero,
-              fork.of_ι_π_app, h₁],
-            erw comp_id m, }
+            rw fork.ι_of_ι at hm,
+            rw [← hm],
+            simp only [← hm, assoc, h₁],
+            exact (comp_id m).symm }
         end }⟩, },
   { intro h,
     refine ⟨_⟩,

src/category_theory/limits/preserves/shapes/equalizers.lean

@@ -39,7 +39,7 @@ def is_limit_map_cone_fork_equiv :
   is_limit (G.map_cone (fork.of_ι h w)) ≃
   is_limit (fork.of_ι (G.map h) (by simp only [←G.map_comp, w]) : fork (G.map f) (G.map g)) :=
 (is_limit.postcompose_hom_equiv (diagram_iso_parallel_pair.{v} _) _).symm.trans
-  (is_limit.equiv_iso_limit (fork.ext (iso.refl _) (by simp)))
+  (is_limit.equiv_iso_limit (fork.ext (iso.refl _) (by { simp [fork.ι] })))
 
 /-- The property of preserving equalizers expressed in terms of forks. -/
 def is_limit_fork_map_of_is_limit [preserves_limit (parallel_pair f g) G]
@@ -115,8 +115,12 @@ This essentially lets us commute `cofork.of_π` with `functor.map_cocone`.
 def is_colimit_map_cocone_cofork_equiv :
   is_colimit (G.map_cocone (cofork.of_π h w)) ≃
   is_colimit (cofork.of_π (G.map h) (by simp only [←G.map_comp, w]) : cofork (G.map f) (G.map g)) :=
-(is_colimit.precompose_inv_equiv (diagram_iso_parallel_pair.{v} _) _).symm.trans
-  (is_colimit.equiv_iso_colimit (cofork.ext (iso.refl _) (by { dsimp, simp })))
+(is_colimit.precompose_inv_equiv (diagram_iso_parallel_pair.{v} _) _).symm.trans $
+is_colimit.equiv_iso_colimit $ cofork.ext (iso.refl _) $
+begin
+  dsimp only [cofork.π, cofork.of_π_ι_app],
+  dsimp, rw [category.comp_id, category.id_comp]
+end
 
 /-- The property of preserving coequalizers expressed in terms of coforks. -/
 def is_colimit_cofork_map_of_is_colimit [preserves_colimit (parallel_pair f g) G]

src/category_theory/limits/preserves/shapes/kernels.lean

@@ -48,7 +48,7 @@ begin
   refine (is_limit.postcompose_hom_equiv _ _).symm.trans (is_limit.equiv_iso_limit _),
   refine parallel_pair.ext (iso.refl _) (iso.refl _) _ _; simp,
   refine fork.ext (iso.refl _) _,
-  simp,
+  simp [fork.ι]
 end
 
 /--
@@ -137,7 +137,10 @@ begin
   refine (is_colimit.precompose_hom_equiv _ _).symm.trans (is_colimit.equiv_iso_colimit _),
   refine parallel_pair.ext (iso.refl _) (iso.refl _) _ _; simp,
   refine cofork.ext (iso.refl _) _,
-  simp, dsimp, simp,
+  simp only [cofork.π, iso.refl_hom, id_comp, cocones.precompose_obj_ι,
+    nat_trans.comp_app, parallel_pair.ext_hom_app, functor.map_cocone_ι_app,
+    cofork.of_π_ι_app],
+  apply category.comp_id
 end
 
 /--

src/category_theory/limits/shapes/biproducts.lean

@@ -1408,16 +1408,7 @@ ht.hom_ext $ λ j, by { rw ht.fac, cases j; simp }
     bicone. -/
 def is_binary_bilimit_of_is_limit {X Y : C} (t : binary_bicone X Y) (ht : is_limit t.to_cone) :
   t.is_bilimit :=
-is_binary_bilimit_of_total _
-begin
-  refine binary_fan.is_limit.hom_ext ht _ _,
-  { rw [inl_of_is_limit ht, inr_of_is_limit ht, add_comp, category.assoc, category.assoc, ht.fac,
-      ht.fac, binary_fan.mk_π_app_left, binary_fan.mk_π_app_left, comp_zero, add_zero,
-      binary_bicone.binary_fan_fst_to_cone, category.comp_id, category.id_comp] },
-  { rw [inr_of_is_limit ht, inl_of_is_limit ht, add_comp, category.assoc, category.assoc, ht.fac,
-      ht.fac, binary_fan.mk_π_app_right, binary_fan.mk_π_app_right, comp_zero, zero_add,
-      binary_bicone.binary_fan_snd_to_cone, category.comp_id, category.id_comp] }
-end
+is_binary_bilimit_of_total _ (by refine binary_fan.is_limit.hom_ext ht _ _; simp)
 
 /-- We can turn any limit cone over a pair into a bilimit bicone. -/
 def binary_bicone_is_bilimit_of_limit_cone_of_is_limit {X Y : C} {t : cone (pair X Y)}
@@ -1477,15 +1468,9 @@ def is_binary_bilimit_of_is_colimit {X Y : C} (t : binary_bicone X Y)
   (ht : is_colimit t.to_cocone) : t.is_bilimit :=
 is_binary_bilimit_of_total _
 begin
-  refine binary_cofan.is_colimit.hom_ext ht _ _,
-  { rw [fst_of_is_colimit ht, snd_of_is_colimit ht, comp_add, ht.fac_assoc, ht.fac_assoc,
-      binary_cofan.mk_ι_app_left, binary_cofan.mk_ι_app_left,
-      binary_bicone.binary_cofan_inl_to_cocone, zero_comp, add_zero, category.id_comp t.inl,
-      category.comp_id t.inl] },
-  { rw [fst_of_is_colimit ht, snd_of_is_colimit ht, comp_add, ht.fac_assoc, ht.fac_assoc,
-      binary_cofan.mk_ι_app_right, binary_cofan.mk_ι_app_right,
-      binary_bicone.binary_cofan_inr_to_cocone, zero_comp, zero_add, category.comp_id t.inr,
-      category.id_comp t.inr] }
+  refine binary_cofan.is_colimit.hom_ext ht _ _; simp,
+  { rw [category.comp_id t.inl] },
+  { rw [category.comp_id t.inr] }
 end
 
 /-- We can turn any colimit cocone over a pair into a bilimit bicone. -/
@@ -1565,10 +1550,10 @@ def binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono
     rw [split_epi_of_idempotent_of_is_colimit_cofork_section_,
       is_colimit_cofork_of_cokernel_cofork_desc, is_cokernel_epi_comp_desc],
     dsimp only [cokernel_cofork_of_cofork_of_π],
-    letI := epi_of_is_colimit_parallel_pair i,
+    letI := epi_of_is_colimit_cofork i,
     apply zero_of_epi_comp c.π,
-    simp only [sub_comp, category.comp_id, category.assoc, split_mono.id, is_colimit.fac_assoc,
-      cofork.of_π_ι_app, category.id_comp, cofork.π_of_π],
+    simp only [sub_comp, comp_sub, category.comp_id, category.assoc, split_mono.id, sub_self,
+      cofork.is_colimit.π_comp_desc_assoc, cokernel_cofork.π_of_π, split_mono.id_assoc],
     apply sub_eq_zero_of_eq,
     apply category.id_comp
   end,
@@ -1586,8 +1571,8 @@ begin
     split_epi_of_idempotent_of_is_colimit_cofork_section_],
   dsimp only [binary_bicone_of_split_mono_of_cokernel_X],
   rw [is_colimit_cofork_of_cokernel_cofork_desc, is_cokernel_epi_comp_desc],
-  simp only [cofork.is_colimit.π_desc_of_π, cokernel_cofork_of_cofork_π,
-    cofork.π_of_π, binary_bicone_of_split_mono_of_cokernel_inl, add_sub_cancel'_right],
+  simp only [binary_bicone_of_split_mono_of_cokernel_inl, cofork.is_colimit.π_comp_desc, 
+    cokernel_cofork_of_cofork_π, cofork.π_of_π, add_sub_cancel'_right]
 end
 
 /--
@@ -1616,10 +1601,10 @@ def binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f]
     rw [split_mono_of_idempotent_of_is_limit_fork_retraction,
       is_limit_fork_of_kernel_fork_lift, is_kernel_comp_mono_lift],
     dsimp only [kernel_fork_of_fork_ι],
-    letI := mono_of_is_limit_parallel_pair i,
+    letI := mono_of_is_limit_fork i,
     apply zero_of_comp_mono c.ι,
-    simp only [comp_sub, category.comp_id, category.assoc, sub_self, fork.ι_eq_app_zero,
-      fork.is_limit.lift_of_ι_ι, fork.of_ι_π_app, split_epi.id_assoc]
+    simp only [comp_sub, category.comp_id, category.assoc, sub_self, fork.is_limit.lift_comp_ι,
+      fork.ι_of_ι, split_epi.id_assoc]
   end,
   inr_snd' := by simp }
 
@@ -1635,8 +1620,7 @@ begin
     split_mono_of_idempotent_of_is_limit_fork_retraction],
   dsimp only [binary_bicone_of_split_epi_of_kernel_X],
   rw [is_limit_fork_of_kernel_fork_lift, is_kernel_comp_mono_lift],
-  simp only [fork.ι_eq_app_zero, kernel_fork.condition, comp_zero, zero_comp, eq_self_iff_true,
-    fork.is_limit.lift_of_ι_ι, kernel_fork_of_fork_ι, fork.of_ι_π_app, sub_add_cancel]
+  simp only [fork.is_limit.lift_comp_ι, fork.ι_of_ι, kernel_fork_of_fork_ι, sub_add_cancel]
 end
 
 end