The Stone-Weierstrass theorem

If a subalgebra A of C(X, ℝ), where X is a compact topological space, separates points, then it is dense.

We argue as follows.

• In any subalgebra A of C(X, ℝ), if f ∈ A, then abs f ∈ A.topologicalClosure. This follows from the Weierstrass approximation theorem on [-‖f‖, ‖f‖] by approximating abs uniformly thereon by polynomials.
• This ensures that A.topologicalClosure is actually a sublattice: if it contains f and g, then it contains the pointwise supremum f ⊔ g and the pointwise infimum f ⊓ g.
• Any nonempty sublattice L of C(X, ℝ) which separates points is dense, by a nice argument approximating a given f above and below using separating functions. For each x y : X, we pick a function g x y ∈ L so g x y x = f x and g x y y = f y. By continuity these functions remain close to f on small patches around x and y. We use compactness to identify a certain finitely indexed infimum of finitely indexed supremums which is then close to f everywhere, obtaining the desired approximation.
• Finally we put these pieces together. L = A.topologicalClosure is a nonempty sublattice which separates points since A does, and so is dense (in fact equal to ⊤).

We then prove the complex version for star subalgebras A, by separately approximating the real and imaginary parts using the real subalgebra of real-valued functions in A (which still separates points, by taking the norm-square of a separating function).

Future work

Extend to cover the case of subalgebras of the continuous functions vanishing at infinity, on non-compact spaces.

def ContinuousMap.attachBound {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, ℝ)) : C(X, ↑(Set.Icc (-‖f‖) ‖f‖))

Turn a function f : C(X, ℝ) into a continuous map into Set.Icc (-‖f‖) (‖f‖), thereby explicitly attaching bounds.

Equations

• f.attachBound = { toFun := fun (x : X) => ⟨f x, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.attachBound_apply_coe {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, ℝ)) (x : X) : ↑(f.attachBound x) = f x

theorem ContinuousMap.polynomial_comp_attachBound {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A) (g : Polynomial ℝ) : (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound = ↑((Polynomial.aeval f) g)

theorem ContinuousMap.polynomial_comp_attachBound_mem {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A) (g : Polynomial ℝ) : (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A

Given a continuous function f in a subalgebra of C(X, ℝ), postcomposing by a polynomial gives another function in A.

This lemma proves something slightly more subtle than this: we take f, and think of it as a function into the restricted target Set.Icc (-‖f‖) ‖f‖), and then postcompose with a polynomial function on that interval. This is in fact the same situation as above, and so also gives a function in A.

theorem ContinuousMap.comp_attachBound_mem_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A) (p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) : p.comp (↑f).attachBound ∈ A.topologicalClosure

theorem ContinuousMap.abs_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A) : |↑f| ∈ A.topologicalClosure

theorem ContinuousMap.inf_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f g : ↥A) : ↑f ⊓ ↑g ∈ A.topologicalClosure

theorem ContinuousMap.inf_mem_closed_subalgebra {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed ↑A) (f g : ↥A) : ↑f ⊓ ↑g ∈ A

theorem ContinuousMap.sup_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f g : ↥A) : ↑f ⊔ ↑g ∈ A.topologicalClosure

theorem ContinuousMap.sup_mem_closed_subalgebra {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed ↑A) (f g : ↥A) : ↑f ⊔ ↑g ∈ A

theorem ContinuousMap.sublattice_closure_eq_top {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (L : Set C(X, ℝ)) (nA : L.Nonempty) (inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L) (sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L) (sep : L.SeparatesPointsStrongly) : closure L = ⊤

theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) : A.topologicalClosure = ⊤

The Stone-Weierstrass Approximation Theorem, that a subalgebra A of C(X, ℝ), where X is a compact topological space, is dense if it separates points.

theorem ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) (f : C(X, ℝ)) : f ∈ A.topologicalClosure

An alternative statement of the Stone-Weierstrass theorem.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is a uniform limit of elements of A.

theorem ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) (f : C(X, ℝ)) (ε : ℝ) (pos : 0 < ε) : ∃ (g : ↥A), ‖↑g - f‖ < ε

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is within any ε > 0 of some element of A.

theorem ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) (f : X → ℝ) (c : Continuous f) (ε : ℝ) (pos : 0 < ε) : ∃ (g : ↥A), ∀ (x : X), ‖↑g x - f x‖ < ε

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons and don't like bundled continuous functions.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is within any ε > 0 of some element of A.

theorem Subalgebra.SeparatesPoints.rclike_to_real {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [TopologicalSpace X] {A : StarSubalgebra 𝕜 C(X, 𝕜)} (hA : A.SeparatesPoints) : (Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)).SeparatesPoints

If a star subalgebra of C(X, 𝕜) separates points, then the real subalgebra of its purely real-valued elements also separates points.

theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] (A : StarSubalgebra 𝕜 C(X, 𝕜)) (hA : A.SeparatesPoints) : A.topologicalClosure = ⊤

The Stone-Weierstrass approximation theorem, RCLike version, that a star subalgebra A of C(X, 𝕜), where X is a compact topological space and RCLike 𝕜, is dense if it separates points.

theorem polynomialFunctions.topologicalClosure (s : Set ℝ) [CompactSpace ↑s] : (polynomialFunctions s).topologicalClosure = ⊤

Polynomial functions in are dense in C(s, ℝ) when s is compact.

See polynomialFunctions_closure_eq_top for the special case s = Set.Icc a b which does not use the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as well.

theorem polynomialFunctions.starClosure_topologicalClosure {𝕜 : Type u_1} [RCLike 𝕜] (s : Set 𝕜) [CompactSpace ↑s] : (polynomialFunctions s).starClosure.topologicalClosure = ⊤

The star subalgebra generated by polynomials functions is dense in C(s, 𝕜) when s is compact and 𝕜 is either ℝ or ℂ.

theorem ContinuousMap.induction_on {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} {p : C(↑s, 𝕜) → Prop} (const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) (id : p (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) (star_id : p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))) (add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) (mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) (closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f) (f : C(↑s, 𝕜)) : p f

An induction principle for C(s, 𝕜).

theorem ContinuousMap.induction_on_of_compact {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [CompactSpace ↑s] {p : C(↑s, 𝕜) → Prop} (const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) (id : p (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) (star_id : p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))) (add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) (mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) (frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in nhds f, p g) → p f) (f : C(↑s, 𝕜)) : p f

theorem ContinuousMap.algHom_ext_map_X {A : Type u_1} [Ring A] [Algebra ℝ A] [TopologicalSpace A] [T2Space A] {s : Set ℝ} [CompactSpace ↑s] {φ ψ : C(↑s, ℝ) →ₐ[ℝ] A} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : φ = ψ

Continuous algebra homomorphisms from C(s, ℝ) into an ℝ-algebra A which agree at X : 𝕜[X] (interpreted as a continuous map) are, in fact, equal.

theorem ContinuousMap.starAlgHom_ext_map_X {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace ↑s] {φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : φ = ψ

Continuous star algebra homomorphisms from C(s, 𝕜) into a star 𝕜-algebra A which agree at X : 𝕜[X] (interpreted as a continuous map) are, in fact, equal.

Continuous maps sending zero to zero

theorem ContinuousMap.adjoin_id_eq_span_one_union {𝕜 : Type u_1} [RCLike 𝕜] (s : Set 𝕜) : ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) = ↑(Submodule.span 𝕜 ({1} ∪ ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})))

theorem ContinuousMap.adjoin_id_eq_span_one_add {𝕜 : Type u_1} [RCLike 𝕜] (s : Set 𝕜) : ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) = ↑(Submodule.span 𝕜 {1}) + ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})

theorem ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} (h0 : 0 ∈ s) : ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ⊆ ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

theorem ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id {𝕜 : Type u_1} [RCLike 𝕜] (s : Set 𝕜) (h0 : 0 ∈ s) : ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})

theorem ContinuousMap.AlgHom.closure_ker_inter {F : Type u_2} {S : Type u_3} {K : Type u_4} {A : Type u_5} [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 ∩ ↑(RingHom.ker φ)

theorem ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id {𝕜 : Type u_1} [RCLike 𝕜] (s : Set 𝕜) (h0 : 0 ∈ s) [CompactSpace ↑s] : ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = closure ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})

theorem ContinuousMapZero.adjoin_id_dense {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero ↑s] (h0 : ↑0 = 0) [CompactSpace ↑s] : Dense ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id h0})

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.

theorem ContinuousMapZero.induction_on {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero ↑s] (h0 : ↑0 = 0) {p : ContinuousMapZero (↑s) 𝕜 → Prop} (zero : p 0) (id : p (ContinuousMapZero.id h0)) (star_id : p (star (ContinuousMapZero.id h0))) (add : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f + g)) (mul : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f * g)) (smul : ∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p f → p (r • f)) (closure : (∀ f ∈ NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : ContinuousMapZero (↑s) 𝕜), p f) (f : ContinuousMapZero (↑s) 𝕜) : p f

An induction principle for C(s, 𝕜)₀.

theorem ContinuousMapZero.induction_on_of_compact {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero ↑s] (h0 : ↑0 = 0) [CompactSpace ↑s] {p : ContinuousMapZero (↑s) 𝕜 → Prop} (zero : p 0) (id : p (ContinuousMapZero.id h0)) (star_id : p (star (ContinuousMapZero.id h0))) (add : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f + g)) (mul : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f * g)) (smul : ∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p f → p (r • f)) (frequently : ∀ (f : ContinuousMapZero (↑s) 𝕜), (∃ᶠ (g : ContinuousMapZero (↑s) 𝕜) in nhds f, p g) → p f) (f : ContinuousMapZero (↑s) 𝕜) : p f

theorem ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [TopologicalSemiring A] [T2Space A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] {s : Set 𝕜} [Zero ↑s] [CompactSpace ↑s] (h0 : ↑0 = 0) (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : φ (ContinuousMapZero.id h0) * a = 0) (hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0) (hφ : Continuous ⇑φ) (f : ContinuousMapZero (↑s) 𝕜) : φ f * a = 0

theorem ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [TopologicalSemiring A] [T2Space A] [Module 𝕜 A] [SMulCommClass 𝕜 A A] {s : Set 𝕜} [Zero ↑s] [CompactSpace ↑s] (h0 : ↑0 = 0) (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : a * φ (ContinuousMapZero.id h0) = 0) (hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0) (hφ : Continuous ⇑φ) (f : ContinuousMapZero (↑s) 𝕜) : a * φ f = 0