chore(Topology/ContinuousMap): remove assumptions (#24985)

- `ContinuousSMul R C(α, M)` and `ContinuousConstSMul R C(α, M)` no longer needs `LocallyCompactSpace α`.
- `ContinuousLinearMap.compLeftContinuous` is upgraded to a continuous linear map.
- `ContinuousLinearMap.compLeftContinuousCompact` is removed because it is a special case of the new `ContinuousLinearMap.compLeftContinuous`.
- Also added `ContinuousLinearMap.const : M →L[R] C(α, M)`.

Author: erdOne

Mathlib/Topology/CompactOpen.lean

@@ -140,6 +140,17 @@ protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
   continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _
   continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _
 
+/-- The map from `X × C(Y, Z)` to `C(Y, X × Z)` is continuous. -/
+lemma continuous_prodMk_const : Continuous fun p : X × C(Y, Z) ↦ prodMk (const Y p.1) p.2 := by
+  simp_rw [continuous_iff_continuousAt, ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen]
+  rintro ⟨r, f⟩ K hK U hU H
+  obtain ⟨V, W, hV, hW, hrV, hKW, hVW⟩ := generalized_tube_lemma (isCompact_singleton (x := r))
+    (hK.image f.continuous) hU (by simpa [Set.subset_def, forall_comm (α := X)])
+  refine Filter.eventually_of_mem (prod_mem_nhds (hV.mem_nhds (by simpa using hrV))
+    (ContinuousMap.eventually_mapsTo hK hW (Set.mapsTo'.mpr hKW))) ?_
+  rintro ⟨r', f'⟩ ⟨hr'V, hf'⟩ x hxK
+  exact hVW (Set.mk_mem_prod hr'V (hf' hxK))
+
 variable [LocallyCompactPair Y Z]
 
 /-- Composition is a continuous map from `C(X, Y) × C(Y, Z)` to `C(X, Z)`,
@@ -334,13 +345,9 @@ variable {X Y}
 theorem image_coev {y : Y} (s : Set X) : coev X Y y '' s = {y} ×ˢ s := by simp [singleton_prod]
 
 /-- The coevaluation map `Y → C(X, Y × X)` is continuous (always). -/
-theorem continuous_coev : Continuous (coev X Y) := by
-  have : ∀ {a K U}, MapsTo (coev X Y a) K U ↔ {a} ×ˢ K ⊆ U := by simp [singleton_prod, mapsTo']
-  simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen, this]
-  intro x K hK U hU hKU
-  rcases generalized_tube_lemma isCompact_singleton hK hU hKU with ⟨V, W, hV, -, hxV, hKW, hVWU⟩
-  filter_upwards [hV.mem_nhds (hxV rfl)] with a ha
-  exact (prod_mono (singleton_subset_iff.mpr ha) hKW).trans hVWU
+theorem continuous_coev : Continuous (coev X Y) :=
+  ((continuous_prodMk_const (X := Y) (Y := X) (Z := X)).comp
+    (.prodMk continuous_id (continuous_const (y := ContinuousMap.id _))):)
 
 end Coev
 

Mathlib/Topology/ContinuousMap/Algebra.lean

@@ -527,18 +527,13 @@ instance instSMul [SMul R M] [ContinuousConstSMul R M] : SMul R C(α, M) :=
   ⟨fun r f => ⟨r • ⇑f, f.continuous.const_smul r⟩⟩
 
 @[to_additive]
-instance [LocallyCompactSpace α] [SMul R M] [ContinuousConstSMul R M] :
-    ContinuousConstSMul R C(α, M) :=
-  ⟨fun γ => continuous_of_continuous_uncurry _ (continuous_eval.const_smul γ)⟩
+instance [SMul R M] [ContinuousConstSMul R M] : ContinuousConstSMul R C(α, M) where
+  continuous_const_smul r := continuous_postcomp ⟨_, continuous_const_smul r⟩
 
 @[to_additive]
-instance [LocallyCompactSpace α] [TopologicalSpace R] [SMul R M] [ContinuousSMul R M] :
+instance [TopologicalSpace R] [SMul R M] [ContinuousSMul R M] :
     ContinuousSMul R C(α, M) :=
-  ⟨by
-    refine continuous_of_continuous_uncurry _ ?_
-    have h : Continuous fun x : (R × C(α, M)) × α => x.fst.snd x.snd :=
-      continuous_eval.comp (continuous_snd.prodMap continuous_id)
-    exact (continuous_fst.comp continuous_fst).smul h⟩
+  ⟨(continuous_postcomp ⟨_, continuous_smul⟩).comp continuous_prodMk_const⟩
 
 @[to_additive (attr := simp, norm_cast)]
 theorem coe_smul [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) : ⇑(c • f) = c • ⇑f :=
@@ -594,13 +589,22 @@ instance module : Module R C(α, M) :=
 
 variable (R)
 
-/-- Composition on the left by a continuous linear map, as a `LinearMap`.
+/-- Composition on the left by a continuous linear map, as a `ContinuousLinearMap`.
 Similar to `LinearMap.compLeft`. -/
 @[simps]
 protected def _root_.ContinuousLinearMap.compLeftContinuous (α : Type*) [TopologicalSpace α]
-    (g : M →L[R] M₂) : C(α, M) →ₗ[R] C(α, M₂) :=
-  { g.toLinearMap.toAddMonoidHom.compLeftContinuous α g.continuous with
-    map_smul' := fun c _ => ext fun _ => g.map_smul' c _ }
+    (g : M →L[R] M₂) : C(α, M) →L[R] C(α, M₂) where
+  __ := g.toLinearMap.toAddMonoidHom.compLeftContinuous α g.continuous
+  map_smul' := fun c _ => ext fun _ => g.map_smul' c _
+  cont := ContinuousMap.continuous_postcomp _
+
+/-- The constant map `x ↦ y ↦ x` as a `ContinuousLinearMap`. -/
+@[simps!]
+def _root_.ContinuousLinearMap.const (α : Type*) [TopologicalSpace α] : M →L[R] C(α, M) where
+  toFun m := .const α m
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  cont := ContinuousMap.continuous_const'
 
 /-- Coercion to a function as a `LinearMap`. -/
 @[simps]

Mathlib/Topology/ContinuousMap/Compact.lean

@@ -371,34 +371,13 @@ end ContinuousMap
 
 section CompLeft
 
-variable (X : Type*) {𝕜 β γ : Type*} [TopologicalSpace X] [CompactSpace X]
-  [NontriviallyNormedField 𝕜]
+@[deprecated (since := "2025-05-18")]
+alias ContinuousLinearMap.compLeftContinuousCompact :=
+  ContinuousLinearMap.compLeftContinuous
 
-variable [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] [SeminormedAddCommGroup γ] [NormedSpace 𝕜 γ]
-
-open ContinuousMap
-
-/-- Postcomposition of continuous functions into a normed module by a continuous linear map is a
-continuous linear map.
-Transferred version of `ContinuousLinearMap.compLeftContinuousBounded`,
-upgraded version of `ContinuousLinearMap.compLeftContinuous`,
-similar to `LinearMap.compLeft`. -/
-protected def ContinuousLinearMap.compLeftContinuousCompact (g : β →L[𝕜] γ) :
-    C(X, β) →L[𝕜] C(X, γ) :=
-  (linearIsometryBoundedOfCompact X γ 𝕜).symm.toLinearIsometry.toContinuousLinearMap.comp <|
-    (g.compLeftContinuousBounded X).comp <|
-      (linearIsometryBoundedOfCompact X β 𝕜).toLinearIsometry.toContinuousLinearMap
-
-@[simp]
-theorem ContinuousLinearMap.toLinear_compLeftContinuousCompact (g : β →L[𝕜] γ) :
-    (g.compLeftContinuousCompact X : C(X, β) →ₗ[𝕜] C(X, γ)) = g.compLeftContinuous 𝕜 X := by
-  ext f
-  rfl
-
-@[simp]
-theorem ContinuousLinearMap.compLeftContinuousCompact_apply (g : β →L[𝕜] γ) (f : C(X, β)) (x : X) :
-    g.compLeftContinuousCompact X f x = g (f x) :=
-  rfl
+@[deprecated (since := "2025-05-18")]
+alias ContinuousLinearMap.compLeftContinuousCompact_apply :=
+  ContinuousLinearMap.compLeftContinuous_apply
 
 end CompLeft
 

Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

@@ -396,7 +396,7 @@ theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoint
     (A : StarSubalgebra 𝕜 C(X, 𝕜)) (hA : A.SeparatesPoints) : A.topologicalClosure = ⊤ := by
   rw [StarSubalgebra.eq_top_iff]
   -- Let `I` be the natural inclusion of `C(X, ℝ)` into `C(X, 𝕜)`
-  let I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ofRealCLM.compLeftContinuous ℝ X
+  let I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ofRealCLM.compLeftContinuous ℝ X
   -- The main point of the proof is that its range (i.e., every real-valued function) is contained
   -- in the closure of `A`
   have key : LinearMap.range I ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
@@ -411,7 +411,7 @@ theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoint
     rw [← Submodule.map_top, ← SW]
     -- So it suffices to prove that the image under `I` of the closure of `A₀` is contained in the
     -- closure of `A`, which follows by abstract nonsense
-    have h₁ := A₀.topologicalClosure_map ((@ofRealCLM 𝕜 _).compLeftContinuousCompact X)
+    have h₁ := A₀.topologicalClosure_map I
     have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I
     exact h₁.trans (Submodule.topologicalClosure_mono h₂)
   -- In particular, for a function `f` in `C(X, 𝕜)`, the real and imaginary parts of `f` are in the