chore(category_theory/idempotents) replaced "idempotence" by "idem" (#12362)

Author: joelriou

src/category_theory/idempotents/basic.lean

@@ -92,7 +92,7 @@ variables {C}
 
 /-- In a preadditive category, when `p : X ⟶ X` is idempotent,
 then `𝟙 X - p` is also idempotent. -/
-lemma idempotence_of_id_sub_idempotent [preadditive C]
+lemma idem_of_id_sub_idem [preadditive C]
   {X : C} (p : X ⟶ X) (hp : p ≫ p = p) :
   (𝟙 _ - p) ≫ (𝟙 _ - p) = (𝟙 _ - p) :=
 by simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]
@@ -106,11 +106,11 @@ begin
   rw is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent,
   split,
   { intros h X p hp,
-    haveI := h X (𝟙 _ - p) (idempotence_of_id_sub_idempotent p hp),
+    haveI := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp),
     convert has_kernel_of_has_equalizer (𝟙 X) (𝟙 X - p),
     rw [sub_sub_cancel], },
   { intros h X p hp,
-    haveI : has_kernel (𝟙 _ - p) := h X (𝟙 _ - p) (idempotence_of_id_sub_idempotent p hp),
+    haveI : has_kernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp),
     apply preadditive.has_limit_parallel_pair, },
 end
 

src/category_theory/idempotents/biproducts.lean

@@ -47,25 +47,25 @@ def bicone [has_finite_biproducts C] {J : Type v} [decidable_eq J] [fintype J]
 { X :=
   { X := biproduct (λ j, (F j).X),
     p := biproduct.map (λ j, (F j).p),
-    idempotence := begin
+    idem := begin
       ext j,
       simp only [biproduct.ι_map_assoc, biproduct.ι_map],
-      slice_lhs 1 2 { rw (F j).idempotence, },
+      slice_lhs 1 2 { rw (F j).idem, },
     end, },
   π := λ j,
     { f := biproduct.map (λ j, (F j).p) ≫ bicone.π _ j,
       comm := by simp only [assoc, biproduct.bicone_π, biproduct.map_π,
-        biproduct.map_π_assoc, (F j).idempotence], },
+        biproduct.map_π_assoc, (F j).idem], },
   ι := λ j,
     { f := (by exact bicone.ι _ j) ≫ biproduct.map (λ j, (F j).p),
-      comm := by rw [biproduct.ι_map, ← assoc, ← assoc, (F j).idempotence,
-        assoc, biproduct.ι_map, ← assoc, (F j).idempotence], },
+      comm := by rw [biproduct.ι_map, ← assoc, ← assoc, (F j).idem,
+        assoc, biproduct.ι_map, ← assoc, (F j).idem], },
   ι_π := λ j j', begin
     split_ifs,
     { subst h,
       simp only [biproduct.bicone_ι, biproduct.ι_map, biproduct.bicone_π,
         biproduct.ι_π_self_assoc, comp, category.assoc, eq_to_hom_refl, id_eq,
-        biproduct.map_π, (F j).idempotence], },
+        biproduct.map_π, (F j).idem], },
     { simpa only [hom_ext, biproduct.ι_π_ne_assoc _ h, assoc,
         biproduct.map_π, biproduct.map_π_assoc, zero_comp, comp], },
   end, }
@@ -95,7 +95,7 @@ lemma karoubi_has_finite_biproducts [has_finite_biproducts C] :
           biproduct.ι_map, assoc, biproducts.bicone_ι_f, biproduct.map_π],
         slice_lhs 1 2 { rw biproduct.ι_π, },
         split_ifs, swap, { exfalso, exact h rfl, },
-        simp only [eq_to_hom_refl, id_comp, (F j).idempotence], },
+        simp only [eq_to_hom_refl, id_comp, (F j).idem], },
     end, } }
 
 instance {D : Type*} [category D] [additive_category D] : additive_category (karoubi D) :=
@@ -108,7 +108,7 @@ endomorphism `𝟙 P.X - P.p` -/
 def complement (P : karoubi C) : karoubi C :=
 { X := P.X,
   p := 𝟙 _ - P.p,
-  idempotence := idempotence_of_id_sub_idempotent P.p P.idempotence, }
+  idem := idem_of_id_sub_idem P.p P.idem, }
 
 instance (P : karoubi C) : has_binary_biproduct P P.complement :=
 has_binary_biproduct_of_total
@@ -120,12 +120,12 @@ has_binary_biproduct_of_total
   inl_fst' := P.decomp_id.symm,
   inl_snd' := begin
     simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp,
-      hom_ext, quiver.hom.add_comm_group_zero_f, P.idempotence],
+      hom_ext, quiver.hom.add_comm_group_zero_f, P.idem],
     erw [comp_id, sub_self],
   end,
   inr_fst' := begin
     simp only [decomp_id_i_f, complement_p, decomp_id_p_f, sub_comp, comp,
-      hom_ext, quiver.hom.add_comm_group_zero_f, P.idempotence],
+      hom_ext, quiver.hom.add_comm_group_zero_f, P.idem],
     erw [id_comp, sub_self],
   end,
   inr_snd' := P.complement.decomp_id.symm, }
@@ -145,14 +145,14 @@ def decomposition (P : karoubi C) : P ⊞ P.complement ≅ (to_karoubi _).obj P.
       convert zero_comp,
       ext,
       simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp,
-        quiver.hom.add_comm_group_zero_f, P.idempotence],
+        quiver.hom.add_comm_group_zero_f, P.idem],
       erw [comp_id, sub_self], },
     { simp only [← assoc, biprod.inr_desc, biprod.lift_eq, comp_add,
         ← decomp_id, comp_id, id_comp, add_left_eq_self],
       convert zero_comp,
       ext,
       simp only [decomp_id_i_f, decomp_id_p_f, complement_p, sub_comp, comp,
-        quiver.hom.add_comm_group_zero_f, P.idempotence],
+        quiver.hom.add_comm_group_zero_f, P.idem],
       erw [id_comp, sub_self], }
   end,
   inv_hom_id' := begin

src/category_theory/idempotents/functor_categories.lean

@@ -73,19 +73,19 @@ functor `F : J ⥤ C` to the functor `J ⥤ karoubi C` which sends `(j : J)` to
 the corresponding direct factor of `F.obj j`. -/
 @[simps]
 def obj (P : karoubi (J ⥤ C)) : J ⥤ karoubi C :=
-{ obj := λ j, ⟨P.X.obj j, P.p.app j, congr_app P.idempotence j⟩,
+{ obj := λ j, ⟨P.X.obj j, P.p.app j, congr_app P.idem j⟩,
   map := λ j j' φ,
   { f := P.p.app j ≫ P.X.map φ,
     comm := begin
       simp only [nat_trans.naturality, assoc],
-      have h := congr_app P.idempotence j,
+      have h := congr_app P.idem j,
       rw [nat_trans.comp_app] at h,
       slice_rhs 1 3 { erw [h, h], },
     end },
   map_id' := λ j, by { ext, simp only [functor.map_id, comp_id, id_eq], },
   map_comp' := λ j j' j'' φ φ', begin
     ext,
-    have h := congr_app P.idempotence j,
+    have h := congr_app P.idem j,
     rw [nat_trans.comp_app] at h,
     simp only [assoc, nat_trans.naturality_assoc, functor.map_comp, comp],
     slice_rhs 1 2 { rw h, },

src/category_theory/idempotents/karoubi.lean

@@ -42,7 +42,7 @@ one may define a formal direct factor of an object `X : C` : it consists of an i
 `p : X ⟶ X` which is thought as the "formal image" of `p`. The type `karoubi C` shall be the
 type of the objects of the karoubi enveloppe of `C`. It makes sense for any category `C`. -/
 @[nolint has_inhabited_instance]
-structure karoubi := (X : C) (p : X ⟶ X) (idempotence : p ≫ p = p)
+structure karoubi := (X : C) (p : X ⟶ X) (idem : p ≫ p = p)
 
 namespace karoubi
 
@@ -80,11 +80,11 @@ end
 
 @[simp, reassoc]
 lemma p_comp {P Q : karoubi C} (f : hom P Q) : P.p ≫ f.f = f.f :=
-by rw [f.comm, ← assoc, P.idempotence]
+by rw [f.comm, ← assoc, P.idem]
 
 @[simp, reassoc]
 lemma comp_p {P Q : karoubi C} (f : hom P Q) : f.f ≫ Q.p = f.f :=
-by rw [f.comm, assoc, assoc, Q.idempotence]
+by rw [f.comm, assoc, assoc, Q.idem]
 
 lemma p_comm {P Q : karoubi C} (f : hom P Q) : P.p ≫ f.f = f.f ≫ Q.p :=
 by rw [p_comp, comp_p]
@@ -96,15 +96,15 @@ by rw [assoc, comp_p, ← assoc, p_comp]
 /-- The category structure on the karoubi envelope of a category. -/
 instance : category (karoubi C) :=
 { hom      := karoubi.hom,
-  id       := λ P, ⟨P.p, by { repeat { rw P.idempotence, }, }⟩,
+  id       := λ P, ⟨P.p, by { repeat { rw P.idem, }, }⟩,
   comp     := λ P Q R f g, ⟨f.f ≫ g.f, karoubi.comp_proof g f⟩, }
 
 @[simp]
 lemma comp {P Q R : karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) :
   f ≫ g = ⟨f.f ≫ g.f, comp_proof g f⟩ := by refl
 
 @[simp]
-lemma id_eq {P : karoubi C} : 𝟙 P = ⟨P.p, by repeat { rw P.idempotence, }⟩ := by refl
+lemma id_eq {P : karoubi C} : 𝟙 P = ⟨P.p, by repeat { rw P.idem, }⟩ := by refl
 
 /-- It is possible to coerce an object of `C` into an object of `karoubi C`.
 See also the functor `to_karoubi`. -/
@@ -198,7 +198,7 @@ end
 
 instance [is_idempotent_complete C] : ess_surj (to_karoubi C) := ⟨λ P, begin
   have h : is_idempotent_complete C := infer_instance,
-  rcases is_idempotent_complete.idempotents_split P.X P.p P.idempotence
+  rcases is_idempotent_complete.idempotents_split P.X P.p P.idem
     with ⟨Y,i,e,⟨h₁,h₂⟩⟩,
   use Y,
   exact nonempty.intro
@@ -217,22 +217,22 @@ variables {C}
 
 /-- The split mono which appears in the factorisation `decomp_id P`. -/
 @[simps]
-def decomp_id_i (P : karoubi C) : P ⟶ P.X := ⟨P.p, by erw [coe_p, comp_id, P.idempotence]⟩
+def decomp_id_i (P : karoubi C) : P ⟶ P.X := ⟨P.p, by erw [coe_p, comp_id, P.idem]⟩
 
 /-- The split epi which appears in the factorisation `decomp_id P`. -/
 @[simps]
 def decomp_id_p (P : karoubi C) : (P.X : karoubi C) ⟶ P :=
-⟨P.p, by erw [coe_p, id_comp, P.idempotence]⟩
+⟨P.p, by erw [coe_p, id_comp, P.idem]⟩
 
 /-- The formal direct factor of `P.X` given by the idempotent `P.p` in the category `C`
 is actually a direct factor in the category `karoubi C`. -/
 lemma decomp_id (P : karoubi C) :
   𝟙 P = (decomp_id_i P) ≫ (decomp_id_p P) :=
-by { ext, simp only [comp, id_eq, P.idempotence, decomp_id_i, decomp_id_p], }
+by { ext, simp only [comp, id_eq, P.idem, decomp_id_i, decomp_id_p], }
 
 lemma decomp_p (P : karoubi C) :
   (to_karoubi C).map P.p = (decomp_id_p P) ≫ (decomp_id_i P) :=
-by { ext, simp only [comp, decomp_id_p_f, decomp_id_i_f, P.idempotence, to_karoubi_map_f], }
+by { ext, simp only [comp, decomp_id_p_f, decomp_id_i_f, P.idem, to_karoubi_map_f], }
 
 lemma decomp_id_i_to_karoubi (X : C) : decomp_id_i ((to_karoubi C).obj X) = 𝟙 _ :=
 by { ext, refl, }

src/category_theory/idempotents/karoubi_karoubi.lean

@@ -28,7 +28,7 @@ variables (C : Type*) [category C]
 /-- The canonical functor `karoubi (karoubi C) ⥤ karoubi C` -/
 @[simps]
 def inverse : karoubi (karoubi C) ⥤ karoubi C :=
-{ obj := λ P, ⟨P.X.X, P.p.f, by simpa only [hom_ext] using P.idempotence⟩,
+{ obj := λ P, ⟨P.X.X, P.p.f, by simpa only [hom_ext] using P.idem⟩,
   map := λ P Q f, ⟨f.f.f, by simpa only [hom_ext] using f.comm⟩, }
 
 instance [preadditive C] : functor.additive (inverse C) := { }
@@ -57,12 +57,12 @@ def counit_iso : inverse C ⋙ to_karoubi (karoubi C) ≅ 𝟭 (karoubi (karoubi
     { f :=
       { f := P.p.1,
         comm := begin
-          have h := P.idempotence,
+          have h := P.idem,
           simp only [hom_ext, comp] at h,
           erw [← assoc, h, comp_p],
         end, },
       comm := begin
-        have h := P.idempotence,
+        have h := P.idem,
         simp only [hom_ext, comp] at h ⊢,
         erw [h, h],
       end, },
@@ -72,18 +72,18 @@ def counit_iso : inverse C ⋙ to_karoubi (karoubi C) ≅ 𝟭 (karoubi (karoubi
     { f :=
       { f := P.p.1,
         comm := begin
-          have h := P.idempotence,
+          have h := P.idem,
           simp only [hom_ext, comp] at h,
           erw [h, p_comp],
         end, },
       comm := begin
-        have h := P.idempotence,
+        have h := P.idem,
         simp only [hom_ext, comp] at h ⊢,
         erw [h, h],
       end, },
     naturality' := λ P Q f, by simpa [hom_ext] using (p_comm f).symm, },
-  hom_inv_id' := by { ext P, simpa only [hom_ext, id_eq] using P.idempotence, },
-  inv_hom_id' := by { ext P, simpa only [hom_ext, id_eq] using P.idempotence, }, }
+  hom_inv_id' := by { ext P, simpa only [hom_ext, id_eq] using P.idem, },
+  inv_hom_id' := by { ext P, simpa only [hom_ext, id_eq] using P.idem, }, }
 
 /-- The equivalence `karoubi C ≌ karoubi (karoubi C)` -/
 @[simps]
@@ -96,7 +96,7 @@ def equivalence : karoubi C ≌ karoubi (karoubi C) :=
     ext,
     simp only [eq_to_hom_f, eq_to_hom_refl, comp_id, counit_iso_hom_app_f_f,
       to_karoubi_obj_p, id_eq, assoc, comp, unit_iso_hom, eq_to_hom_app, eq_to_hom_map],
-    erw [P.idempotence, P.idempotence],
+    erw [P.idem, P.idem],
   end, }
 
 instance equivalence.additive_functor [preadditive C] :