feat(CategoryTheory/Karoubi): cleanup (#14786)

Author: kim-em

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -245,7 +245,7 @@ theorem identity_N₂_objectwise (P : Karoubi (SimplicialObject C)) :
       len_mk, NatTrans.naturality, PInfty_f_idem_assoc,
       PInfty_f_naturality_assoc, app_idem_assoc]
     erw [P.X.map_id, comp_id]
-  simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_eq, N₂_obj_p_f, assoc,
+  simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_f, N₂_obj_p_f, assoc,
     eq₁, eq₂, PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.identity_N₂_objectwise AlgebraicTopology.DoldKan.identity_N₂_objectwise

Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

@@ -47,7 +47,7 @@ instance : (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)).Reflects
     have h₃ := fun n =>
       Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op [n]))
     simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
-      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_eq, assoc] at h₁ h₂ h₃
+      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃
     -- we have to construct an inverse to f in degree n, by induction on n
     intro n
     induction' n with n hn

Mathlib/AlgebraicTopology/DoldKan/Normalized.lean

@@ -149,11 +149,11 @@ def N₁_iso_normalizedMooreComplex_comp_toKaroubi : N₁ ≅ normalizedMooreCom
   hom_inv_id := by
     ext X : 3
     simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
-      NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p, NatTrans.id_app, Karoubi.id_eq]
+      NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p, NatTrans.id_app, Karoubi.id_f]
   inv_hom_id := by
     ext X : 3
     rw [← cancel_mono (inclusionOfMooreComplexMap X)]
-    simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_eq,
+    simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
       PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
       inclusionOfMooreComplexMap_comp_PInfty]
     dsimp only [Functor.comp_obj, toKaroubi]

Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

@@ -223,7 +223,7 @@ noncomputable def toKaroubiNondegComplexIsoN₁ :
   inv_hom_id := by
     ext n
     simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f,
-      HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_eq]
+      HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_f]
 set_option linter.uppercaseLean3 false in
 #align simplicial_object.splitting.to_karoubi_nondeg_complex_iso_N₁ SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁
 

Mathlib/CategoryTheory/Idempotents/Biproducts.lean

@@ -63,7 +63,7 @@ def bicone [HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → Karoubi C) :
     split_ifs with h
     · subst h
       simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl,
-        id_eq, hom_ext_iff, comp_f, assoc, bicone_ι_π_self_assoc, idem]
+        id_f, hom_ext_iff, comp_f, assoc, bicone_ι_π_self_assoc, idem]
     · dsimp
       simp only [biproduct.ι_map, biproduct.map_π, hom_ext_iff, comp_f,
         assoc, biproduct.ι_π_ne_assoc _ h, zero_comp, comp_zero, instZero_zero]
@@ -79,7 +79,7 @@ theorem karoubi_hasFiniteBiproducts [HasFiniteBiproducts C] : HasFiniteBiproduct
           refine biproduct.hom_ext' _ _ (fun j => ?_)
           simp only [Biproducts.bicone_pt_X, sum_hom, comp_f, Biproducts.bicone_π_f,
             biproduct.bicone_π, biproduct.map_π, Biproducts.bicone_ι_f, biproduct.ι_map, assoc,
-            idem_assoc, id_eq, Biproducts.bicone_pt_p, comp_sum]
+            idem_assoc, id_f, Biproducts.bicone_pt_p, comp_sum]
           rw [Finset.sum_eq_single j]
           · simp only [bicone_ι_π_self_assoc]
           · intro b _ hb
@@ -115,9 +115,9 @@ instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
           decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self]
       inr_snd := P.complement.decompId.symm }
     (by
-      simp only [id_eq, complement_X, comp_f,
-        decompId_i_f, decompId_p_f, complement_p, instAdd_add, idem,
-        comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel])
+      ext
+      simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, instAdd_add, idem,
+        comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f])
 
 attribute [-simp] hom_ext_iff
 
@@ -142,10 +142,10 @@ def decomposition (P : Karoubi C) : P ⊞ P.complement ≅ (toKaroubi _).obj P.X
       simp only [complement_X, comp_f, decompId_i_f, complement_p,
         decompId_p_f, sub_comp, id_comp, idem, sub_self, instZero_zero]
   inv_hom_id := by
-    simp only [biprod.lift_desc, instAdd_add, toKaroubi_obj_X, comp_f,
-      decompId_p_f, decompId_i_f, idem, complement_X, complement_p, comp_sub, comp_id,
-      sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel,
-      id_eq, toKaroubi_obj_p]
+    ext
+    simp only [toKaroubi_obj_X, biprod.lift_desc, instAdd_add, comp_f, decompId_p_f, decompId_i_f,
+      idem, complement_X, complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero,
+      add_sub_cancel, id_f, toKaroubi_obj_p]
 #align category_theory.idempotents.karoubi.decomposition CategoryTheory.Idempotents.Karoubi.decomposition
 
 end Karoubi

Mathlib/CategoryTheory/Idempotents/Karoubi.lean

@@ -121,6 +121,9 @@ theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f
 #align category_theory.idempotents.karoubi.comp_f CategoryTheory.Idempotents.Karoubi.comp_f
 
 @[simp]
+theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl
+
+@[deprecated (since := "2024-07-15")]
 theorem id_eq {P : Karoubi C} : 𝟙 P = ⟨P.p, by repeat' rw [P.idem]⟩ := rfl
 #align category_theory.idempotents.karoubi.id_eq CategoryTheory.Idempotents.Karoubi.id_eq
 
@@ -143,7 +146,7 @@ theorem coe_p (X : C) : (X : Karoubi C).p = 𝟙 X := rfl
 theorem eqToHom_f {P Q : Karoubi C} (h : P = Q) :
     Karoubi.Hom.f (eqToHom h) = P.p ≫ eqToHom (congr_arg Karoubi.X h) := by
   subst h
-  simp only [eqToHom_refl, Karoubi.id_eq, comp_id]
+  simp only [eqToHom_refl, Karoubi.id_f, comp_id]
 #align category_theory.idempotents.karoubi.eq_to_hom_f CategoryTheory.Idempotents.Karoubi.eqToHom_f
 
 end Karoubi
@@ -283,7 +286,7 @@ is actually a direct factor in the category `Karoubi C`. -/
 @[reassoc]
 theorem decompId (P : Karoubi C) : 𝟙 P = decompId_i P ≫ decompId_p P := by
   ext
-  simp only [comp_f, id_eq, P.idem, decompId_i, decompId_p]
+  simp only [comp_f, id_f, P.idem, decompId_i, decompId_p]
 #align category_theory.idempotents.karoubi.decomp_id CategoryTheory.Idempotents.Karoubi.decompId
 
 theorem decomp_p (P : Karoubi C) : (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P := by

Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean

@@ -37,8 +37,6 @@ lemma idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := by
 lemma p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f := by
   simpa only [hom_ext_iff, comp_f] using p_comm f
 
-attribute [local simp] p_comm_f
-
 /-- The canonical functor `Karoubi (Karoubi C) ⥤ Karoubi C` -/
 @[simps]
 def inverse : Karoubi (Karoubi C) ⥤ Karoubi C where
@@ -54,21 +52,12 @@ def unitIso : 𝟭 (Karoubi C) ≅ toKaroubi (Karoubi C) ⋙ inverse C :=
   eqToIso (Functor.ext (by aesop_cat) (by aesop_cat))
 #align category_theory.idempotents.karoubi_karoubi.unit_iso CategoryTheory.Idempotents.KaroubiKaroubi.unitIso
 
+attribute [local simp] p_comm_f in
 /-- The counit isomorphism of the equivalence -/
 @[simps]
 def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where
-  hom :=
-    { app := fun P =>
-        { f :=
-            { f := P.p.1
-              comm := by simp }
-          comm := by simp } }
-  inv :=
-    { app := fun P =>
-        { f :=
-            { f := P.p.1
-              comm := by simp }
-          comm := by simp } }
+  hom := { app := fun P => { f := { f := P.p.1 } } }
+  inv := { app := fun P => { f := { f := P.p.1 }  } }
 #align category_theory.idempotents.karoubi_karoubi.counit_iso CategoryTheory.Idempotents.KaroubiKaroubi.counitIso
 
 /-- The equivalence `Karoubi C ≌ Karoubi (Karoubi C)` -/