refactor(topology/continuous_function/{algebra, compact}): move `cont…

…inuous_map.comp_right_alg_hom` (#16875)

This moves `continuous_function.comp_right_alg_hom` to a better home. Along the way, we generalize it significantly. We also provide term-mode proofs for some very slow `tidy`s, and remove some unnecessary hypotheses in `topology/continuous_function/algebra`

src/topology/continuous_function/algebra.lean

@@ -575,8 +575,6 @@ def continuous_map.C : R →+* C(α, A) :=
 @[simp] lemma continuous_map.C_apply (r : R) (a : α) : continuous_map.C r a = algebra_map R A r :=
 rfl
 
-variables [has_continuous_const_smul R A] [has_continuous_const_smul R A₂]
-
 instance continuous_map.algebra : algebra R C(α, A) :=
 { to_ring_hom := continuous_map.C,
   commutes' := λ c f, by ext x; exact algebra.commutes' _ _,
@@ -592,6 +590,22 @@ variables (R)
 { commutes' := λ c, continuous_map.ext $ λ _, g.commutes' _,
   .. g.to_ring_hom.comp_left_continuous α hg }
 
+variables (A)
+
+/--
+Precomposition of functions into a normed ring by a continuous map is an algebra homomorphism.
+-/
+@[simps] def continuous_map.comp_right_alg_hom {α β : Type*} [topological_space α]
+  [topological_space β] (f : C(α, β)) : C(β, A) →ₐ[R] C(α, A) :=
+{ to_fun := λ g, g.comp f,
+  map_zero' := by { ext, refl, },
+  map_add' := λ g₁ g₂, by { ext, refl, },
+  map_one' := by { ext, refl, },
+  map_mul' := λ g₁ g₂, by { ext, refl, },
+  commutes' := λ r, by { ext, refl, }, }
+
+variables {A}
+
 /-- Coercion to a function as an `alg_hom`. -/
 @[simps]
 def continuous_map.coe_fn_alg_hom : C(α, A) →ₐ[R] (α → A) :=

src/topology/continuous_function/compact.lean

@@ -363,7 +363,7 @@ section comp_right
 Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
 -/
 def comp_right_continuous_map {X Y : Type*} (T : Type*) [topological_space X] [compact_space X]
-  [topological_space Y] [compact_space Y] [normed_add_comm_group T]
+  [topological_space Y] [compact_space Y] [metric_space T]
   (f : C(X, Y)) : C(C(Y, T), C(X, T)) :=
 { to_fun := λ g, g.comp f,
   continuous_to_fun :=
@@ -376,7 +376,7 @@ def comp_right_continuous_map {X Y : Type*} (T : Type*) [topological_space X] [c
   end }
 
 @[simp] lemma comp_right_continuous_map_apply {X Y : Type*} (T : Type*) [topological_space X]
-  [compact_space X] [topological_space Y] [compact_space Y] [normed_add_comm_group T]
+  [compact_space X] [topological_space Y] [compact_space Y] [metric_space T]
   (f : C(X, Y)) (g : C(Y, T)) :
   (comp_right_continuous_map T f) g = g.comp f :=
 rfl
@@ -385,39 +385,18 @@ rfl
 Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.
 -/
 def comp_right_homeomorph {X Y : Type*} (T : Type*) [topological_space X] [compact_space X]
-  [topological_space Y] [compact_space Y] [normed_add_comm_group T]
+  [topological_space Y] [compact_space Y] [metric_space T]
   (f : X ≃ₜ Y) : C(Y, T) ≃ₜ C(X, T) :=
 { to_fun := comp_right_continuous_map T f.to_continuous_map,
   inv_fun := comp_right_continuous_map T f.symm.to_continuous_map,
-  left_inv := by tidy,
-  right_inv := by tidy, }
-
-/--
-Precomposition of functions into a normed ring by continuous map is an algebra homomorphism.
--/
-def comp_right_alg_hom {X Y : Type*} (R : Type*)
-  [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) :
-  C(Y, R) →ₐ[R] C(X, R) :=
-{ to_fun := λ g, g.comp f,
-  map_zero' := by { ext, simp, },
-  map_add' := λ g₁ g₂, by { ext, simp, },
-  map_one' := by { ext, simp, },
-  map_mul' := λ g₁ g₂, by { ext, simp, },
-  commutes' := λ r, by { ext, simp, }, }
-
-@[simp] lemma comp_right_alg_hom_apply {X Y : Type*} (R : Type*)
-  [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) (g : C(Y, R)) :
-  (comp_right_alg_hom R f) g = g.comp f :=
-rfl
-
-lemma comp_right_alg_hom_continuous {X Y : Type*} (R : Type*)
-  [topological_space X] [compact_space X] [topological_space Y] [compact_space Y]
-  [normed_comm_ring R] (f : C(X, Y)) :
-  continuous (comp_right_alg_hom R f) :=
-begin
-  change continuous (comp_right_continuous_map R f),
-  continuity,
-end
+  left_inv := λ g, ext $ λ _, congr_arg g (f.apply_symm_apply _),
+  right_inv := λ g, ext $ λ _, congr_arg g (f.symm_apply_apply _) }
+
+lemma comp_right_alg_hom_continuous {X Y : Type*} (R A : Type*)
+  [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [comm_semiring R]
+  [semiring A] [metric_space A] [topological_semiring A] [algebra R A] (f : C(X, Y)) :
+  continuous (comp_right_alg_hom R A f) :=
+map_continuous (comp_right_continuous_map A f)
 
 end comp_right
 

src/topology/continuous_function/polynomial.lean

@@ -138,7 +138,7 @@ open continuous_map
 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
-    (comp_right_alg_hom ℝ (Icc_homeo_I a b h).symm.to_continuous_map) =
+    (comp_right_alg_hom ℝ ℝ (Icc_homeo_I a b h).symm.to_continuous_map) =
     polynomial_functions (set.Icc a b) :=
 begin
   ext f,

src/topology/continuous_function/weierstrass.lean

@@ -58,7 +58,7 @@ begin
   { -- We can pullback continuous functions on `[a,b]` to continuous functions on `[0,1]`,
     -- by precomposing with an affine map.
     let W : C(set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) :=
-      comp_right_alg_hom ℝ (Icc_homeo_I a b h).symm.to_continuous_map,
+      comp_right_alg_hom ℝ ℝ (Icc_homeo_I a b h).symm.to_continuous_map,
     -- This operation is itself a homeomorphism
     -- (with respect to the norm topologies on continuous functions).
     let W' : C(set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := comp_right_homeomorph ℝ (Icc_homeo_I a b h).symm,