feat(category_theory/concrete_category): id_apply, comp_apply (#7530)

This PR renames

* `category_theory.coe_id` to `category_theory.id_apply`
* `category_theory.coe_comp` to `category_theory.comp_apply`

The names that are hence free up
are then redefined for "unapplied" versions of the same lemmas.

The `elementwise` tactic uses the old lemmas (with their new names).

We need minor fixes in the rest of the library because of the name changes.

src/algebra/category/Group/colimits.lean

@@ -314,8 +314,8 @@ noncomputable def cokernel_iso_quotient {G H : AddCommGroup} (f : G ⟶ H) :
   end,
   inv_hom_id' := begin
     ext1, induction x,
-    { simp only [colimit.ι_desc_apply, coe_id, add_monoid_hom.coe_of, lift_quot_mk,
-                 cofork.of_π_ι_app, coe_comp], refl },
+    { simp only [colimit.ι_desc_apply, id_apply, add_monoid_hom.coe_of, lift_quot_mk,
+                 cofork.of_π_ι_app, comp_apply], refl },
     { refl }
   end, }
 

src/algebraic_geometry/structure_sheaf.lean

@@ -497,14 +497,14 @@ def stalk_iso (x : Spec.Top R) :
   inv := localization_to_stalk R x,
   hom_inv_id' := (structure_sheaf R).presheaf.stalk_hom_ext $ λ U hxU,
   begin
-    ext s, simp only [coe_comp], rw [coe_id, stalk_to_fiber_ring_hom_germ'],
+    ext s, simp only [comp_apply], rw [id_apply, stalk_to_fiber_ring_hom_germ'],
     obtain ⟨V, hxV, iVU, f, g, hg, hs⟩ := exists_const _ _ s x hxU,
     erw [← res_apply R U V iVU s ⟨x, hxV⟩, ← hs, const_apply, localization_to_stalk_mk'],
     refine (structure_sheaf R).presheaf.germ_ext V hxV (hom_of_le hg) iVU _,
     erw [← hs, res_const']
   end,
   inv_hom_id' := (localization.of x.as_ideal.prime_compl).epic_of_localization_map $ λ f,
-    by simp only [ring_hom.comp_apply, coe_comp, coe_id, localization_to_stalk_of,
+    by simp only [ring_hom.comp_apply, comp_apply, id_apply, localization_to_stalk_of,
         stalk_to_fiber_ring_hom_to_stalk] }
 
 end algebraic_geometry

src/category_theory/abelian/diagram_lemmas/four.lean

@@ -28,7 +28,7 @@ The "epi" four lemma and the five lemma, which is then an easy corollary.
 
 four lemma, diagram lemma, diagram chase
 -/
-open category_theory
+open category_theory (hiding comp_apply)
 open category_theory.abelian.pseudoelement
 
 universes v u

src/category_theory/concrete_category/basic.lean

@@ -105,10 +105,17 @@ when `h : f = g` is an equality between morphisms in a concrete category.
 lemma congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
 congr_fun (congr_arg (λ k : X ⟶ Y, (k : X → Y)) h) x
 
-@[simp] lemma coe_id {X : C} (x : X) : ((𝟙 X) : X → X) x = x :=
+lemma coe_id {X : C} : ((𝟙 X) : X → X) = id :=
+(forget _).map_id X
+
+lemma coe_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  (f ≫ g : X → Z) = g ∘ f :=
+(forget _).map_comp f g
+
+@[simp] lemma id_apply {X : C} (x : X) : ((𝟙 X) : X → X) x = x :=
 congr_fun ((forget _).map_id X) x
 
-@[simp] lemma coe_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
+@[simp] lemma comp_apply {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
   (f ≫ g) x = g (f x) :=
 congr_fun ((forget _).map_comp _ _) x
 

src/tactic/elementwise.lean

@@ -106,8 +106,8 @@ do
    -- Now the key step: replace morphism composition with function composition,
    -- and identity morphisms with nothing.
    let s := simp_lemmas.mk,
-   s ← s.add_simp ``coe_id,
-   s ← s.add_simp ``coe_comp,
+   s ← s.add_simp ``id_apply,
+   s ← s.add_simp ``comp_apply,
    (t'', pr', _) ← simplify s [] t' {fail_if_unchanged := ff},
    pr' ← mk_eq_mp pr' pr,
    -- Further, if we're in `Type`, get rid of the coercions entirely.

src/topology/sheaves/stalks.lean

@@ -124,7 +124,7 @@ lemma germ_ext {D : Type u} [category.{v} D] [concrete_category D] [has_colimits
   (ih : F.map iWU.op sU = F.map iWV.op sV) :
   F.germ ⟨x, hxU⟩ sU = F.germ ⟨x, hxV⟩ sV :=
 by erw [← F.germ_res iWU ⟨x, hxW⟩,
-    ← F.germ_res iWV ⟨x, hxW⟩, coe_comp, coe_comp, ih]
+    ← F.germ_res iWV ⟨x, hxW⟩, comp_apply, comp_apply, ih]
 
 end