refactor(topology/continuous_function/basic): rename `map_specializat…

…ion` (#14565)

Rename `continuous_map.map_specialization` to `continuous_map.map_specializes` to align with the name of the relation.

src/algebraic_geometry/stalks.lean

@@ -190,7 +190,7 @@ as_iso (stalk_map α.hom x)
 
 @[simp, reassoc, elementwise]
 lemma stalk_specializes_stalk_map {X Y : PresheafedSpace C} (f : X ⟶ Y) {x y : X} (h : x ⤳ y) :
-  Y.presheaf.stalk_specializes (f.base.map_specialization h) ≫ stalk_map f x =
+  Y.presheaf.stalk_specializes (f.base.map_specializes h) ≫ stalk_map f x =
     stalk_map f y ≫ X.presheaf.stalk_specializes h :=
 by { delta PresheafedSpace.stalk_map, simp [stalk_map] }
 

src/topology/continuous_function/basic.lean

@@ -105,8 +105,7 @@ lemma coe_injective : @function.injective (C(α, β)) (α → β) coe_fn :=
 @[simp] lemma coe_mk (f : α → β) (h : continuous f) :
   ⇑(⟨f, h⟩ : C(α, β)) = f := rfl
 
-lemma map_specialization {x y : α} (h : x ⤳ y) (f : C(α, β)) : f x ⤳ f y :=
-h.map f.2
+lemma map_specializes (f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y := h.map f.2
 
 section
 variables (α β)

src/topology/sheaves/stalks.lean

@@ -315,7 +315,7 @@ by { ext, delta stalk_functor, simpa [stalk_specializes] }
 
 @[simp, reassoc, elementwise]
 lemma stalk_specializes_stalk_pushforward (f : X ⟶ Y) (F : X.presheaf C) {x y : X} (h : x ⤳ y) :
-  (f _* F).stalk_specializes (f.map_specialization h) ≫ F.stalk_pushforward _ f x =
+  (f _* F).stalk_specializes (f.map_specializes h) ≫ F.stalk_pushforward _ f x =
     F.stalk_pushforward _ f y ≫ F.stalk_specializes h :=
 by { ext, delta stalk_pushforward, simpa [stalk_specializes] }