feat: the non-unital star subalgebra generated by id is dense in `C…

…(s, 𝕜)₀` (#13326)

This is a version of the Weierstrass approximation theorem for `C(s, 𝕜)₀`, and is necessary for instances of the non-unital continuous functional calculus.

Co-authored by: @ADedecker

- [ ] depends on: #13323

Mathlib/Topology/ContinuousFunction/Algebra.lean

@@ -1107,3 +1107,25 @@ def compStarAlgEquiv' (f : X ≃ₜ Y) : C(Y, A) ≃⋆ₐ[𝕜] C(X, A) :=
 #align homeomorph.comp_star_alg_equiv' Homeomorph.compStarAlgEquiv'
 
 end Homeomorph
+
+/-! ### Evaluation as a bundled map -/
+
+variable {X : Type*} (S R : Type*) [TopologicalSpace X] [CommSemiring S] [CommSemiring R]
+variable [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R]
+
+/-- Evaluation of continuous maps at a point, bundled as an algebra homomorphism. -/
+@[simps]
+def ContinuousMap.evalAlgHom (x : X) : C(X, R) →ₐ[S] R where
+  toFun f := f x
+  map_zero' := rfl
+  map_one' := rfl
+  map_add' _ _ := rfl
+  map_mul' _ _ := rfl
+  commutes' _ := rfl
+
+/-- Evaluation of continuous maps at a point, bundled as a star algebra homomorphism. -/
+@[simps!]
+def ContinuousMap.evalStarAlgHom [StarRing R] [ContinuousStar R] (x : X) :
+    C(X, R) →⋆ₐ[S] R :=
+  { ContinuousMap.evalAlgHom S R x with
+    map_star' := fun _ => rfl }

Mathlib/Topology/ContinuousFunction/Polynomial.lean

@@ -43,6 +43,10 @@ def toContinuousMap (p : R[X]) : C(R, R) :=
   ⟨fun x : R => p.eval x, by continuity⟩
 #align polynomial.to_continuous_map Polynomial.toContinuousMap
 
+open ContinuousMap in
+lemma toContinuousMap_X_eq_id : X.toContinuousMap = .id R := by
+  ext; simp
+
 /-- A polynomial as a continuous function,
 with domain restricted to some subset of the semiring of coefficients.
 
@@ -54,6 +58,12 @@ def toContinuousMapOn (p : R[X]) (X : Set R) : C(X, R) :=
   ⟨fun x : X => p.toContinuousMap x, Continuous.comp (by continuity) (by continuity)⟩
 #align polynomial.to_continuous_map_on Polynomial.toContinuousMapOn
 
+open ContinuousMap in
+lemma toContinuousMapOn_X_eq_restrict_id (s : Set R) :
+    X.toContinuousMapOn s = restrict s (.id R) := by
+  ext; simp
+
+
 -- TODO some lemmas about when `toContinuousMapOn` is injective?
 end
 

Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

@@ -3,8 +3,10 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Heather Macbeth
 -/
+import Mathlib.Algebra.Algebra.Subalgebra.Unitization
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Topology.Algebra.StarSubalgebra
+import Mathlib.Topology.ContinuousFunction.ContinuousMapZero
 import Mathlib.Topology.ContinuousFunction.Weierstrass
 
 #align_import topology.continuous_function.stone_weierstrass from "leanprover-community/mathlib"@"16e59248c0ebafabd5d071b1cd41743eb8698ffb"
@@ -470,3 +472,120 @@ theorem ContinuousMap.starAlgHom_ext_map_X {𝕜 A : Type*} [RCLike 𝕜] [Ring
     (polynomialFunctions.starClosure_le_equalizer s φ ψ h) (isClosed_eq hφ hψ)
 
 end PolynomialFunctions
+
+/-! ### Continuous maps sending zero to zero -/
+
+section ContinuousMapZero
+
+variable {X : Type*} [TopologicalSpace X] {𝕜 : Type*} [RCLike 𝕜]
+open NonUnitalStarAlgebra Submodule
+
+namespace ContinuousMap
+
+lemma adjoin_id_eq_span_one_union (s : Set 𝕜) :
+    ((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
+      span 𝕜 ({(1 : C(s, 𝕜))} ∪ (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))})) := by
+  ext x
+  rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
+    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
+    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
+
+open Pointwise in
+lemma adjoin_id_eq_span_one_add (s : Set 𝕜) :
+    ((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
+      (span 𝕜 {(1 : C(s, 𝕜))} : Set C(s, 𝕜)) + (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) := by
+  ext x
+  rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
+    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
+    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]
+  simp [Set.mem_add]
+
+-- annoyingly, things break below without these shortcut instances.
+instance : IsScalarTower 𝕜 C(X, 𝕜) C(X, 𝕜) := @IsScalarTower.right _ C(X, 𝕜) _ _ _
+instance : SMulCommClass 𝕜 C(X, 𝕜) C(X, 𝕜) := @Algebra.to_smulCommClass _ C(X, 𝕜) _ _ _
+
+lemma nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom {s : Set 𝕜} (h0 : 0 ∈ s) :
+    (adjoin 𝕜 {restrict s (.id 𝕜)} : Set C(s, 𝕜)) ⊆
+      RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) := by
+  intro f hf
+  induction hf using adjoin_induction' with
+  | mem f hf =>
+    obtain rfl := Set.mem_singleton_iff.mp hf
+    rfl
+  | add f _ g _ hf hg => exact add_mem hf hg
+  | zero => exact zero_mem _
+  | mul f _ g _ _ hg => exact Ideal.mul_mem_left _ f hg
+  | smul r f _ hf =>
+    rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
+    rw [map_smul, hf, smul_zero]
+  | star f _ hf =>
+    rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
+    rw [map_star, hf, star_zero]
+
+lemma ker_evalStarAlgHom_inter_adjoin_id (s : Set 𝕜) (h0 : 0 ∈ s) :
+    (StarAlgebra.adjoin 𝕜 {restrict s (.id 𝕜)} : Set C(s, 𝕜)) ∩
+      RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) = adjoin 𝕜 {restrict s (.id 𝕜)} := by
+  ext f
+  constructor
+  · rintro ⟨hf₁, hf₂⟩
+    rw [SetLike.mem_coe] at hf₂ ⊢
+    simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁
+    obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁
+    have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
+    simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this
+    rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂
+    rwa [hf₂, zero_smul, zero_add]
+  · simp only [Set.mem_inter_iff, SetLike.mem_coe]
+    refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩
+    exact adjoin_le_starAlgebra_adjoin _ _ hf
+
+-- the statement should be in terms of non unital subalgebras, but we lack API
+open RingHom Filter Topology in
+theorem AlgHom.closure_ker_inter {F S K A : Type*} [CommRing K] [Ring A] [Algebra K A]
+    [TopologicalSpace K] [T1Space K] [TopologicalSpace A] [ContinuousSub A] [ContinuousSMul K A]
+    [FunLike F A K] [AlgHomClass F K A K] [SetLike S A] [OneMemClass S A] [AddSubgroupClass S A]
+    [SMulMemClass S K A] (φ : F) (hφ : Continuous φ) (s : S) :
+    closure (s ∩ RingHom.ker φ) = closure s ∩ (ker φ : Set A) := by
+  refine subset_antisymm ?_ ?_
+  · simpa only [ker_eq, (isClosed_singleton.preimage hφ).closure_eq]
+      using closure_inter_subset_inter_closure s (ker φ : Set A)
+  · intro x ⟨hxs, (hxφ : φ x = 0)⟩
+    rw [mem_closure_iff_clusterPt, ClusterPt] at hxs
+    have : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 s) (𝓝 x) := by
+      conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
+      exact Filter.tendsto_inf_left (Continuous.tendsto (by fun_prop) x)
+    refine mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_
+    filter_upwards [] with g hg using
+      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩
+
+lemma ker_evalStarAlgHom_eq_closure_adjoin_id (s : Set 𝕜) (h0 : 0 ∈ s) [CompactSpace s] :
+    (RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) : Set C(s, 𝕜)) =
+      closure (adjoin 𝕜 {(restrict s (.id 𝕜))}) := by
+  rw [← ker_evalStarAlgHom_inter_adjoin_id s h0,
+    AlgHom.closure_ker_inter (φ := evalStarAlgHom 𝕜 𝕜 (X := s) ⟨0, h0⟩) (continuous_eval_const _) _]
+  convert (Set.univ_inter _).symm
+  rw [← Polynomial.toContinuousMapOn_X_eq_restrict_id, ← Polynomial.toContinuousMapOnAlgHom_apply,
+    ← polynomialFunctions.starClosure_eq_adjoin_X s]
+  congrm(($(polynomialFunctions.starClosure_topologicalClosure s) : Set C(s, 𝕜)))
+
+end ContinuousMap
+
+open ContinuousMapZero in
+/-- If `s : Set 𝕜` with `RCLike 𝕜` is compact and contains `0`, then the non-unital star subalgebra
+generated by the identity function in `C(s, 𝕜)₀` is dense. This can be seen as a version of the
+Weierstrass approximation theorem. -/
+lemma ContinuousMapZero.adjoin_id_dense {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
+    [CompactSpace s] : Dense (adjoin 𝕜 {(.id h0 : C(s, 𝕜)₀)} : Set C(s, 𝕜)₀) := by
+  have h0' : 0 ∈ s := h0 ▸ (0 : s).property
+  rw [dense_iff_closure_eq,
+    ← closedEmbedding_toContinuousMap.injective.preimage_image (closure _),
+    ← closedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
+    ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
+    toContinuousMapHom_apply, toContinuousMap_id h0,
+    ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']
+  apply Set.eq_univ_of_forall fun f ↦ ?_
+  simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
+    ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]
+  rw [show ⟨0, h0'⟩ = (0 : s) by ext; exact h0.symm, _root_.map_zero f]
+
+end ContinuousMapZero