feat: {NonUnital}{Star}Subalgebra.map_topologicalClosure (#29535)

This adds the following 5 results for each of variant of `{NonUnital}{Star}Subalgebra`

```lean
lemma map_topologicalClosure_le (hφ : Continuous φ) :
    map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
  image_closure_subset_closure_image hφ

lemma topologicalClosure_map_le (hφ : IsClosedMap φ) :
    (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
  hφ.closure_image_subset _

lemma topologicalClosure_map (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

lemma topologicalClosure_adjoin_le_centralizer_centralizer (s : Set A) :
    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

lemma elemental.le_centralizer_centralizer (x : A) :
    elemental R x ≤ centralizer R (centralizer R {x}) :=
  topologicalClosure_adjoin_le_centralizer_centralizer R {x}
```

In the case of `Subalgebra`, we repurpose the existing `Subalgebra.topologicalClosure_map`, as this was the wrong name for the lemma anyway. Moreover, for those results we use the bundled `ContinuousAlgHom` for continuity.

There's also some minor clean up of the explicitness of some variables in `topologicalClosure_minimal`.

Author: j-loreaux

Mathlib/Topology/Algebra/Algebra.lean

@@ -107,6 +107,8 @@ notation:25 A " →A[" R "] " B => ContinuousAlgHom R A B
 
 namespace ContinuousAlgHom
 
+open Subalgebra
+
 section Semiring
 
 variable {R} {A}
@@ -232,11 +234,21 @@ def _root_.Subalgebra.topologicalClosure (s : Subalgebra R A) : Subalgebra R A w
 
 /-- Under a continuous algebra map, the image of the `TopologicalClosure` of a subalgebra is
 contained in the `TopologicalClosure` of its image. -/
-theorem _root_.Subalgebra.topologicalClosure_map
+theorem _root_.Subalgebra.map_topologicalClosure_le
     [IsTopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A) :
-    s.topologicalClosure.map f ≤ (s.map f.toAlgHom).topologicalClosure :=
+    map f s.topologicalClosure ≤ (map f.toAlgHom s).topologicalClosure :=
   image_closure_subset_closure_image f.continuous
 
+lemma _root_.Subalgebra.topologicalClosure_map_le [IsTopologicalSemiring B]
+    (f : A →ₐ[R] B) (hf : IsClosedMap f) (s : Subalgebra R A) :
+    (map f s).topologicalClosure ≤ map f s.topologicalClosure :=
+  hf.closure_image_subset _
+
+lemma _root_.Subalgebra.topologicalClosure_map [IsTopologicalSemiring B]
+    (f : A →A[R] B) (hf : IsClosedMap f) (s : Subalgebra R A) :
+    (map f.toAlgHom s).topologicalClosure = map f.toAlgHom s.topologicalClosure :=
+  SetLike.coe_injective <| hf.closure_image_eq_of_continuous f.continuous _
+
 @[simp]
 theorem _root_.Subalgebra.topologicalClosure_coe (s : Subalgebra R A) :
     (s.topologicalClosure : Set A) = closure ↑s := rfl
@@ -553,10 +565,16 @@ theorem Subalgebra.le_topologicalClosure (s : Subalgebra R A) : s ≤ s.topologi
 theorem Subalgebra.isClosed_topologicalClosure (s : Subalgebra R A) :
     IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A _ s
 
-theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t)
+theorem Subalgebra.topologicalClosure_minimal {s t : Subalgebra R A} (h : s ≤ t)
     (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
+variable (R) in
+open Algebra in
+lemma Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer [T2Space A] (s : Set A) :
+    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
+  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
+
 /-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
 
 See note [reducible non-instances]. -/
@@ -595,7 +613,7 @@ theorem self_mem (x : A) : x ∈ elemental R x :=
 variable {R} in
 theorem le_of_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
     elemental R x ≤ s :=
-  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs
+  topologicalClosure_minimal (adjoin_le <| by simpa using hx) hs
 
 variable {R} in
 theorem le_iff_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) :
@@ -624,6 +642,10 @@ theorem isClosedEmbedding_coe (x : A) : IsClosedEmbedding ((↑) : elemental R x
   injective := Subtype.coe_injective
   isClosed_range := by simpa using isClosed R x
 
+lemma le_centralizer_centralizer [T2Space A] (x : A) :
+    elemental R x ≤ centralizer R (centralizer R {x}) :=
+  topologicalClosure_adjoin_le_centralizer_centralizer ..
+
 end Algebra.elemental
 
 end TopologicalAlgebra

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -40,6 +40,15 @@ universe u v w x
 
 variable {G : Type w} {H : Type x} {α : Type u} {β : Type v}
 
+/-- In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed. -/
+lemma Set.isClosed_centralizer {M : Type*} (s : Set M) [Mul M] [TopologicalSpace M]
+    [ContinuousMul M] [T2Space M] : IsClosed (centralizer s) := by
+  rw [centralizer, setOf_forall]
+  refine isClosed_sInter ?_
+  rintro - ⟨m, ht, rfl⟩
+  refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_
+  all_goals fun_prop
+
 section ContinuousMulGroup
 
 /-!

Mathlib/Topology/Algebra/NonUnitalAlgebra.lean

@@ -24,7 +24,7 @@ namespace NonUnitalSubalgebra
 
 section Semiring
 
-variable {R A : Type*} [CommSemiring R] [TopologicalSpace A]
+variable {R A B : Type*} [CommSemiring R] [TopologicalSpace A]
 variable [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A]
 variable [ContinuousConstSMul R A]
 
@@ -43,7 +43,7 @@ theorem le_topologicalClosure (s : NonUnitalSubalgebra R A) : s ≤ s.topologica
 theorem isClosed_topologicalClosure (s : NonUnitalSubalgebra R A) :
     IsClosed (s.topologicalClosure : Set A) := isClosed_closure
 
-theorem topologicalClosure_minimal (s : NonUnitalSubalgebra R A) {t : NonUnitalSubalgebra R A}
+theorem topologicalClosure_minimal {s t : NonUnitalSubalgebra R A}
     (h : s ≤ t) (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
@@ -55,6 +55,28 @@ abbrev nonUnitalCommSemiringTopologicalClosure [T2Space A] (s : NonUnitalSubalge
     (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommSemiring s.topologicalClosure :=
   s.toNonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure hs
 
+variable [TopologicalSpace B] [NonUnitalSemiring B] [Module R B] [IsTopologicalSemiring B]
+    [ContinuousConstSMul R B] (s : NonUnitalSubalgebra R A) {φ : A →ₙₐ[R] B}
+
+lemma map_topologicalClosure_le (hφ : Continuous φ) :
+    map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
+  image_closure_subset_closure_image hφ
+
+lemma topologicalClosure_map_le (hφ : IsClosedMap φ) :
+    (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
+  hφ.closure_image_subset _
+
+lemma topologicalClosure_map (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
+    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
+  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _
+
+variable (R) in
+open NonUnitalAlgebra in
+lemma topologicalClosure_adjoin_le_centralizer_centralizer
+    [IsScalarTower R A A] [SMulCommClass R A A] [T2Space A] (s : Set A) :
+    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
+  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
+
 end Semiring
 
 section Ring
@@ -99,7 +121,7 @@ theorem self_mem (x : A) : x ∈ elemental R x :=
 variable {R} in
 theorem le_of_mem {x : A} {s : NonUnitalSubalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
     elemental R x ≤ s :=
-  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs
+  topologicalClosure_minimal (adjoin_le <| by simpa using hx) hs
 
 variable {R} in
 theorem le_iff_mem {x : A} {s : NonUnitalSubalgebra R A} (hs : IsClosed (s : Set A)) :
@@ -135,6 +157,10 @@ theorem isClosedEmbedding_coe (x : A) : Topology.IsClosedEmbedding ((↑) : elem
   injective := Subtype.coe_injective
   isClosed_range := by simpa using isClosed R x
 
+lemma le_centralizer_centralizer [T2Space A] (x : A) :
+    elemental R x ≤ centralizer R (centralizer R {x}) :=
+  topologicalClosure_adjoin_le_centralizer_centralizer R {x}
+
 end elemental
 
 end NonUnitalAlgebra

Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean

@@ -26,7 +26,7 @@ namespace NonUnitalStarSubalgebra
 
 section Semiring
 
-variable {R A : Type*} [CommSemiring R] [TopologicalSpace A] [Star A]
+variable {R A B : Type*} [CommSemiring R] [TopologicalSpace A] [Star A]
 variable [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A]
 variable [ContinuousConstSMul R A]
 
@@ -59,6 +59,31 @@ abbrev nonUnitalCommSemiringTopologicalClosure [T2Space A] (s : NonUnitalStarSub
     (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommSemiring s.topologicalClosure :=
   s.toNonUnitalSubalgebra.nonUnitalCommSemiringTopologicalClosure hs
 
+variable [TopologicalSpace B] [Star B] [NonUnitalSemiring B] [Module R B]
+    [IsTopologicalSemiring B] [ContinuousConstSMul R B] [ContinuousStar B]
+    (s : NonUnitalStarSubalgebra R A) {φ : A →⋆ₙₐ[R] B}
+
+lemma map_topologicalClosure_le (hφ : Continuous φ) :
+    map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
+  image_closure_subset_closure_image hφ
+
+lemma topologicalClosure_map_le (hφ : IsClosedMap φ) :
+    (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
+  hφ.closure_image_subset _
+
+lemma topologicalClosure_map (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
+    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
+  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _
+
+open NonUnitalStarAlgebra in
+-- we have to shadow the variables because some things currently require `StarRing`
+lemma topologicalClosure_adjoin_le_centralizer_centralizer (R : Type*) {A : Type*}
+    [CommSemiring R] [StarRing R] [TopologicalSpace A] [NonUnitalSemiring A] [StarRing A]
+    [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A]
+    [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [T2Space A] (s : Set A) :
+    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
+  topologicalClosure_minimal _ (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
+
 end Semiring
 
 section Ring
@@ -146,6 +171,10 @@ theorem isClosedEmbedding_coe (x : A) : Topology.IsClosedEmbedding ((↑) : elem
   injective := Subtype.coe_injective
   isClosed_range := by simpa using isClosed R x
 
+lemma le_centralizer_centralizer [T2Space A] (x : A) :
+    elemental R x ≤ centralizer R (centralizer R {x}) :=
+  topologicalClosure_adjoin_le_centralizer_centralizer ..
+
 end elemental
 
 end NonUnitalStarAlgebra

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -101,9 +101,15 @@ theorem map_topologicalClosure_le [StarModule R B] [IsTopologicalSemiring B] [Co
   image_closure_subset_closure_image hφ
 
 theorem topologicalClosure_map [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B]
-    (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedEmbedding φ) :
+    (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
     (map φ s).topologicalClosure = map φ s.topologicalClosure :=
-  SetLike.coe_injective <| hφ.closure_image_eq _
+  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _
+
+variable (R) in
+open StarAlgebra in
+lemma topologicalClosure_adjoin_le_centralizer_centralizer [T2Space A] (s : Set A) :
+    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
+  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
 
 theorem _root_.Subalgebra.topologicalClosure_star_comm (s : Subalgebra R A) :
     (star s).topologicalClosure = star s.topologicalClosure := by
@@ -213,6 +219,10 @@ theorem isClosedEmbedding_coe (x : A) : IsClosedEmbedding ((↑) : elemental R x
   injective := Subtype.coe_injective
   isClosed_range := by simpa using isClosed R x
 
+lemma le_centralizer_centralizer [T2Space A] (x : A) :
+    elemental R x ≤ centralizer R (centralizer R {x}) :=
+  topologicalClosure_adjoin_le_centralizer_centralizer ..
+
 @[elab_as_elim]
 theorem induction_on {x y : A}
     (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop}

Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

@@ -497,7 +497,7 @@ theorem ContinuousMap.algHom_ext_map_X {A : Type*} [Semiring A]
   suffices (⊤ : Subalgebra ℝ C(s, ℝ)) ≤ AlgHom.equalizer φ ψ from
     AlgHom.ext fun x => this (by trivial)
   rw [← polynomialFunctions.topologicalClosure s]
-  exact Subalgebra.topologicalClosure_minimal (polynomialFunctions s)
+  exact Subalgebra.topologicalClosure_minimal
     (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)
 
 /-- Continuous star algebra homomorphisms from `C(s, 𝕜)` into a star `𝕜`-algebra `A` which agree