chore(category_theory): better definitional properties for kernel_lift (

#17328)

This PR makes `kernel.lift` definitionally equal to the application of `(kernel_is_kernel f).lift`, and similarly for `cokernel.desc`.

src/algebra/category/Group/colimits.lean

@@ -313,8 +313,8 @@ noncomputable def cokernel_iso_quotient {G H : AddCommGroup.{u}} (f : G ⟶ H) :
   end,
   inv_hom_id' := begin
     ext x : 2,
-    simp only [colimit.ι_desc_apply, id_apply, lift_mk, mk'_apply,
-               cofork.of_π_ι_app, comp_apply, add_monoid_hom.comp_apply],
+    simp only [add_monoid_hom.coe_comp, function.comp_app, comp_apply, lift_mk,
+      cokernel.π_desc_apply, mk'_apply, id_apply],
   end, }
 
 end AddCommGroup

src/category_theory/abelian/basic.lean

@@ -157,7 +157,7 @@ def image_factorisation {X Y : C} (f : X ⟶ Y) [is_iso (abelian.coimage_image_c
       simp only [image_mono_factorisation_m, is_iso.inv_comp_eq, category.assoc,
         abelian.coimage_image_comparison],
       ext,
-      rw [limits.coequalizer.π_desc_assoc, limits.coequalizer.π_desc_assoc, F.fac, kernel.lift_ι]
+      simp only [cokernel.π_desc_assoc, mono_factorisation.fac, image.fac],
     end } }
 
 instance [has_zero_object C] {X Y : C} (f : X ⟶ Y) [mono f]

src/category_theory/abelian/ext.lean

@@ -37,7 +37,7 @@ variables (R : Type*) [ring R] (C : Type*) [category C] [abelian C] [linear R C]
 `Ext R C n` is defined by deriving in the first argument of `(X, Y) ↦ Module.of R (unop X ⟶ Y)`
 (which is the second argument of `linear_yoneda`).
 -/
-@[simps]
+@[simps obj map]
 def Ext (n : ℕ) : Cᵒᵖ ⥤ C ⥤ Module R :=
 functor.flip
 { obj := λ Y, (((linear_yoneda R C).obj Y).right_op.left_derived n).left_op,

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

@@ -89,8 +89,8 @@ def preserves_kernel.of_iso_comparison [i : is_iso (kernel_comparison f G)] :
 begin
   apply preserves_limit_of_preserves_limit_cone (kernel_is_kernel f),
   apply (is_limit_map_cone_fork_equiv' G (kernel.condition f)).symm _,
-  apply is_limit.of_point_iso (limit.is_limit (parallel_pair (G.map f) 0)),
-  apply i,
+  apply is_limit.of_point_iso (kernel_is_kernel (G.map f)),
+  exact i,
 end
 
 variables [preserves_limit (parallel_pair f 0) G]
@@ -102,7 +102,7 @@ def preserves_kernel.iso :
   G.obj (kernel f) ≅ kernel (G.map f) :=
 is_limit.cone_point_unique_up_to_iso
   (is_limit_of_has_kernel_of_preserves_limit G f)
-  (limit.is_limit _)
+  (kernel_is_kernel _)
 
 @[simp]
 lemma preserves_kernel.iso_hom :
@@ -181,8 +181,8 @@ def preserves_cokernel.of_iso_comparison [i : is_iso (cokernel_comparison f G)]
 begin
   apply preserves_colimit_of_preserves_colimit_cocone (cokernel_is_cokernel f),
   apply (is_colimit_map_cocone_cofork_equiv' G (cokernel.condition f)).symm _,
-  apply is_colimit.of_point_iso (colimit.is_colimit (parallel_pair (G.map f) 0)),
-  apply i,
+  apply is_colimit.of_point_iso (cokernel_is_cokernel (G.map f)),
+  exact i,
 end
 
 variables [preserves_colimit (parallel_pair f 0) G]
@@ -194,7 +194,7 @@ def preserves_cokernel.iso :
   G.obj (cokernel f) ≅ cokernel (G.map f) :=
 is_colimit.cocone_point_unique_up_to_iso
   (is_colimit_of_has_cokernel_of_preserves_colimit G f)
-  (colimit.is_colimit _)
+  (cokernel_is_cokernel _)
 
 @[simp]
 lemma preserves_cokernel.iso_inv :

src/category_theory/limits/shapes/kernels.lean

@@ -182,11 +182,11 @@ is_limit.of_iso_limit (limit.is_limit _) (fork.ext (iso.refl _) (by tidy))
 /-- Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through `kernel.ι f`
     via `kernel.lift : W ⟶ kernel f`. -/
 abbreviation kernel.lift {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : W ⟶ kernel f :=
-limit.lift (parallel_pair f 0) (kernel_fork.of_ι k h)
+(kernel_is_kernel f).lift (kernel_fork.of_ι k h)
 
 @[simp, reassoc]
 lemma kernel.lift_ι {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : kernel.lift f k h ≫ kernel.ι f = k :=
-limit.lift_π _ _
+(kernel_is_kernel f).fac (kernel_fork.of_ι k h) walking_parallel_pair.zero
 
 @[simp]
 lemma kernel.lift_zero {W : C} {h} : kernel.lift f (0 : W ⟶ X) h = 0 :=
@@ -522,12 +522,12 @@ is_colimit.of_iso_colimit (colimit.is_colimit _) (cofork.ext (iso.refl _) (by ti
 /-- Given any morphism `k : Y ⟶ W` such that `f ≫ k = 0`, `k` factors through `cokernel.π f`
     via `cokernel.desc : cokernel f ⟶ W`. -/
 abbreviation cokernel.desc {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : cokernel f ⟶ W :=
-colimit.desc (parallel_pair f 0) (cokernel_cofork.of_π k h)
+(cokernel_is_cokernel f).desc (cokernel_cofork.of_π k h)
 
 @[simp, reassoc]
 lemma cokernel.π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) :
   cokernel.π f ≫ cokernel.desc f k h = k :=
-colimit.ι_desc _ _
+(cokernel_is_cokernel f).fac (cokernel_cofork.of_π k h) walking_parallel_pair.one
 
 @[simp]
 lemma cokernel.desc_zero {W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0 :=