refactor(algebra/algebra/subalgebra/basic): Remove ' from `subalgeb…

…ra.comap'` (#15349)

This PR removes `'` from `subalgebra.comap'`.
<https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/subalgebra.2Ecomap'>

src/algebra/algebra/subalgebra/basic.lean

@@ -9,7 +9,7 @@ import data.set.Union_lift
 /-!
 # Subalgebras over Commutative Semiring
 
-In this file we define `subalgebra`s and the usual operations on them (`map`, `comap'`).
+In this file we define `subalgebra`s and the usual operations on them (`map`, `comap`).
 
 More lemmas about `adjoin` can be found in `ring_theory.adjoin`.
 -/
@@ -339,24 +339,24 @@ set_like.coe_injective rfl
 rfl
 
 /-- Preimage of a subalgebra under an algebra homomorphism. -/
-def comap' (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
+def comap (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
 { algebra_map_mem' := λ r, show f (algebra_map R A r) ∈ S,
     from (f.commutes r).symm ▸ S.algebra_map_mem r,
   .. S.to_subsemiring.comap (f : A →+* B) }
 
 theorem map_le {S : subalgebra R A} {f : A →ₐ[R] B} {U : subalgebra R B} :
-  map S f ≤ U ↔ S ≤ comap' U f :=
+  map S f ≤ U ↔ S ≤ comap U f :=
 set.image_subset_iff
 
-lemma gc_map_comap (f : A →ₐ[R] B) : galois_connection (λ S, map S f) (λ S, comap' S f) :=
+lemma gc_map_comap (f : A →ₐ[R] B) : galois_connection (λ S, map S f) (λ S, comap S f) :=
 λ S U, map_le
 
 @[simp] lemma mem_comap (S : subalgebra R B) (f : A →ₐ[R] B) (x : A) :
-  x ∈ S.comap' f ↔ f x ∈ S :=
+  x ∈ S.comap f ↔ f x ∈ S :=
 iff.rfl
 
 @[simp, norm_cast] lemma coe_comap (S : subalgebra R B) (f : A →ₐ[R] B) :
-  (S.comap' f : set A) = f ⁻¹' (S : set B) :=
+  (S.comap f : set A) = f ⁻¹' (S : set B) :=
 rfl
 
 instance no_zero_divisors {R A : Type*} [comm_semiring R] [semiring A] [no_zero_divisors A]
@@ -649,7 +649,7 @@ set_like.coe_injective set.image_univ
 set_like.coe_injective $
   by simp only [← set.range_comp, (∘), algebra.coe_bot, subalgebra.coe_map, f.commutes]
 
-@[simp] theorem comap_top (f : A →ₐ[R] B) : subalgebra.comap' (⊤ : subalgebra R B) f = ⊤ :=
+@[simp] theorem comap_top (f : A →ₐ[R] B) : subalgebra.comap (⊤ : subalgebra R B) f = ⊤ :=
 eq_top_iff.2 $ λ x, mem_top
 
 /-- `alg_hom` to `⊤ : subalgebra R A`. -/

src/topology/algebra/algebra.lean

@@ -102,11 +102,11 @@ but we don't have those, so we use the clunky approach of talking about
 an algebra homomorphism, and a separate homeomorphism,
 along with a witness that as functions they are the same.
 -/
-lemma subalgebra.topological_closure_comap'_homeomorph
+lemma subalgebra.topological_closure_comap_homeomorph
   (s : subalgebra R A)
   {B : Type*} [topological_space B] [ring B] [topological_ring B] [algebra R B]
   (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : (f : B → A) = f') :
-  s.topological_closure.comap' f = (s.comap' f).topological_closure :=
+  s.topological_closure.comap f = (s.comap f).topological_closure :=
 begin
   apply set_like.ext',
   simp only [subalgebra.topological_closure_coe],

src/topology/continuous_function/polynomial.lean

@@ -136,8 +136,8 @@ open continuous_map
 
 /-- The preimage of polynomials on `[0,1]` under the pullback map by `x ↦ (b-a) * x + a`
 is the polynomials on `[a,b]`. -/
-lemma polynomial_functions.comap'_comp_right_alg_hom_Icc_homeo_I (a b : ℝ) (h : a < b) :
-  (polynomial_functions I).comap'
+lemma polynomial_functions.comap_comp_right_alg_hom_Icc_homeo_I (a b : ℝ) (h : a < b) :
+  (polynomial_functions I).comap
     (comp_right_alg_hom ℝ (Icc_homeo_I a b h).symm.to_continuous_map) =
     polynomial_functions (set.Icc a b) :=
 begin

src/topology/continuous_function/stone_weierstrass.lean

@@ -384,7 +384,7 @@ open continuous_map
 of its purely real-valued elements also separates points. -/
 lemma subalgebra.separates_points.is_R_or_C_to_real {A : subalgebra 𝕜 C(X, 𝕜)}
   (hA : A.separates_points) (hA' : conj_invariant_subalgebra (A.restrict_scalars ℝ)) :
-  ((A.restrict_scalars ℝ).comap'
+  ((A.restrict_scalars ℝ).comap
     (of_real_am.comp_left_continuous ℝ continuous_of_real)).separates_points :=
 begin
   intros x₁ x₂ hx,

src/topology/continuous_function/weierstrass.lean

@@ -66,12 +66,12 @@ begin
     -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`,
     have p := polynomial_functions_closure_eq_top',
     -- and pullback both sides, obtaining an equation between subalgebras of `C([a,b], ℝ)`.
-    apply_fun (λ s, s.comap' W) at p,
+    apply_fun (λ s, s.comap W) at p,
     simp only [algebra.comap_top] at p,
     -- Since the pullback operation is continuous, it commutes with taking `topological_closure`,
-    rw subalgebra.topological_closure_comap'_homeomorph _ W W' w at p,
+    rw subalgebra.topological_closure_comap_homeomorph _ W W' w at p,
     -- and precomposing with an affine map takes polynomial functions to polynomial functions.
-    rw polynomial_functions.comap'_comp_right_alg_hom_Icc_homeo_I at p,
+    rw polynomial_functions.comap_comp_right_alg_hom_Icc_homeo_I at p,
     -- 🎉
     exact p },
   { -- Otherwise, `b ≤ a`, and the interval is a subsingleton,