chore(category_theory/*): move some elementwise lemmas earlier (#13998)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/basic.lean

@@ -6,6 +6,7 @@ Authors: Robert A. Spencer, Markus Himmel
 import algebra.category.Group.basic
 import category_theory.limits.shapes.kernels
 import category_theory.linear
+import category_theory.elementwise
 import linear_algebra.basic
 import category_theory.conj
 

src/algebra/category/Mon/basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import tactic.elementwise
 import category_theory.concrete_category.bundled_hom
 import algebra.punit_instances
 import category_theory.functor.reflects_isomorphisms

src/algebra/category/Ring/basic.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 import algebra.category.Group.basic
 import category_theory.concrete_category.reflects_isomorphisms
+import category_theory.elementwise
 import algebra.ring.equiv
 
 /-!

src/algebra/category/Semigroup/basic.lean

@@ -7,6 +7,7 @@ import algebra.pempty_instances
 import algebra.hom.equiv
 import category_theory.concrete_category.bundled_hom
 import category_theory.functor.reflects_isomorphisms
+import category_theory.elementwise
 
 /-!
 # Category instances for has_mul, has_add, semigroup and add_semigroup
@@ -156,8 +157,8 @@ namespace category_theory.iso
 def Magma_iso_to_mul_equiv {X Y : Magma} (i : X ≅ Y) : X ≃* Y :=
 { to_fun := i.hom,
   inv_fun := i.inv,
-  left_inv := begin rw function.left_inverse, simp end,
-  right_inv := begin rw function.right_inverse, rw function.left_inverse, simp end,
+  left_inv := λ x, by simp,
+  right_inv := λ y, by simp,
   map_mul' := by simp }
 
 /-- Build a `mul_equiv` from an isomorphism in the category `Semigroup`. -/
@@ -166,8 +167,8 @@ def Magma_iso_to_mul_equiv {X Y : Magma} (i : X ≅ Y) : X ≃* Y :=
 def Semigroup_iso_to_mul_equiv {X Y : Semigroup} (i : X ≅ Y) : X ≃* Y :=
 { to_fun := i.hom,
   inv_fun := i.inv,
-  left_inv := begin rw function.left_inverse, simp end,
-  right_inv := begin rw function.right_inverse, rw function.left_inverse, simp end,
+  left_inv := λ x, by simp,
+  right_inv := λ y, by simp,
   map_mul' := by simp }
 
 end category_theory.iso

src/algebraic_geometry/Scheme.lean

@@ -261,7 +261,7 @@ lemma basic_open_eq_of_affine' {R : CommRing}
     prime_spectrum.basic_open ((Spec_Γ_identity.app R).hom f) :=
 begin
   convert basic_open_eq_of_affine ((Spec_Γ_identity.app R).hom f),
-  exact (coe_hom_inv_id _ _).symm
+  exact (iso.hom_inv_id_apply _ _).symm
 end
 
 end algebraic_geometry

src/algebraic_geometry/Spec.lean

@@ -194,10 +194,10 @@ begin
   -- *locally* ringed spaces, i.e. that the induced map on the stalks is a local ring homomorphism.
   rw ← local_ring_hom_comp_stalk_iso_apply at ha,
   replace ha := (stalk_iso S p).hom.is_unit_map ha,
-  rw coe_inv_hom_id at ha,
+  rw iso.inv_hom_id_apply at ha,
   replace ha := is_local_ring_hom.map_nonunit _ ha,
   convert ring_hom.is_unit_map (stalk_iso R (prime_spectrum.comap f p)).inv ha,
-  rw coe_hom_inv_id,
+  rw iso.hom_inv_id_apply,
 end
 
 @[simp] lemma Spec.LocallyRingedSpace_map_id (R : CommRing) :

src/algebraic_geometry/properties.lean

@@ -204,7 +204,7 @@ begin
     replace hs := (hs.map (Spec_Γ_identity.app R).inv),
     -- what the hell?!
     replace hs := @is_nilpotent.eq_zero _ _ _ _ (show _, from _) hs,
-    rw coe_hom_inv_id at hs,
+    rw iso.hom_inv_id_apply at hs,
     rw [hs, map_zero],
     exact @@is_reduced.component_reduced hX ⊤ }
 end

src/analysis/normed/group/SemiNormedGroup.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Riccardo Brasca
 import analysis.normed.group.hom
 import category_theory.limits.shapes.zero_morphisms
 import category_theory.concrete_category.bundled_hom
+import category_theory.elementwise
 
 /-!
 # The category of seminormed groups
@@ -69,7 +70,7 @@ begin
   apply normed_group_hom.isometry_of_norm,
   intro v,
   apply le_antisymm (h1 v),
-  calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [coe_hom_inv_id]
+  calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [iso.hom_inv_id_apply]
   ... ≤ ∥i.hom v∥ : h2 _,
 end
 
@@ -166,7 +167,7 @@ begin
   apply normed_group_hom.isometry_of_norm,
   intro v,
   apply le_antisymm (i.hom.2 v),
-  calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [coe_hom_inv_id]
+  calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [iso.hom_inv_id_apply]
       ... ≤ ∥i.hom v∥ : i.inv.2 _,
 end
 

src/category_theory/concrete_category/basic.lean

@@ -118,13 +118,6 @@ congr_fun ((forget _).map_id X) x
   (f ≫ g) x = g (f x) :=
 congr_fun ((forget _).map_comp _ _) x
 
-@[simp] lemma coe_hom_inv_id {X Y : C} (f : X ≅ Y) (x : X) :
-  f.inv (f.hom x) = x :=
-congr_fun ((forget C).map_iso f).hom_inv_id x
-@[simp] lemma coe_inv_hom_id {X Y : C} (f : X ≅ Y) (y : Y) :
-  f.hom (f.inv y) = y :=
-congr_fun ((forget C).map_iso f).inv_hom_id y
-
 lemma concrete_category.congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
 congr_fun (congr_arg (λ f : X ⟶ Y, (f : X → Y)) h) x
 

src/category_theory/concrete_category/elementwise.lean

@@ -17,6 +17,3 @@ attribute [elementwise]
   cone.w limit.lift_π limit.w cocone.w colimit.ι_desc colimit.w
   kernel.lift_ι cokernel.π_desc
   kernel.condition cokernel.condition
-  -- Note that the elementwise forms of `iso.hom_inv_id` and `iso.inv_hom_id` are already
-  -- provided as `category_theory.coe_hom_inv_id` and `category_theory.coe_inv_hom_id`.
-  is_iso.hom_inv_id is_iso.inv_hom_id

src/category_theory/elementwise.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import tactic.elementwise
+
+/-!
+# Use the `elementwise` attribute to create applied versions of lemmas.
+
+Usually we would use `@[elementwise]` at the point of definition,
+however some early parts of the category theory library are imported by `tactic.elementwise`,
+so we need to add the attribute after the fact.
+-/
+
+/-! We now add some `elementwise` attributes to lemmas that were proved earlier. -/
+open category_theory
+
+-- This list is incomplete, and it would probably be useful to add more.
+attribute [elementwise] iso.hom_inv_id iso.inv_hom_id is_iso.hom_inv_id is_iso.inv_hom_id

src/ring_theory/ideal/local_ring.lean

@@ -240,7 +240,7 @@ lemma is_local_ring_hom_of_iso {R S : CommRing} (f : R ≅ S) : is_local_ring_ho
 { map_nonunit := λ a ha,
   begin
     convert f.inv.is_unit_map ha,
-    rw category_theory.coe_hom_inv_id,
+    rw category_theory.iso.hom_inv_id_apply,
   end }
 
 @[priority 100] -- see Note [lower instance priority]

src/topology/category/Top/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Scott Morrison, Mario Carneiro
 -/
 import category_theory.concrete_category.bundled_hom
+import category_theory.elementwise
 import topology.continuous_function.basic
 
 /-!

src/topology/sheaves/sheaf_condition/equalizer_products.lean

@@ -6,7 +6,6 @@ Authors: Scott Morrison
 import category_theory.full_subcategory
 import category_theory.limits.shapes.equalizers
 import category_theory.limits.shapes.products
-import tactic.elementwise
 import topology.sheaves.presheaf
 
 /-!

src/topology/sheaves/stalks.lean

@@ -17,11 +17,8 @@ import algebra.category.Ring
 # Stalks
 
 For a presheaf `F` on a topological space `X`, valued in some category `C`, the *stalk* of `F`
-at the point `x : X` is defined as the colimit of the following functor
-
-(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ ⥤ C
-
-where the functor on the left is the inclusion of categories and the functor on the right is `F`.
+at the point `x : X` is defined as the colimit of the composition of the inclusion of categories
+`(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ` and the functor `F : (opens X)ᵒᵖ ⥤ C`.
 For an open neighborhood `U` of `x`, we define the map `F.germ x : F.obj (op U) ⟶ F.stalk x` as the
 canonical morphism into this colimit.