starSubalgebra_topologicalClosure_eq_top_of_separatesPoints

English

If A is a star subalgebra of C(X, 𝕜) with X compact and separates points, then its topological closure is the whole space of star-preserving continuous functions.

Русский

Если A — звездная подалгебра C(X, 𝕜) на компактном X, которая разделяет точки, то её топологическое замыкание равно всей пространству непрерывных функций со звездо-структурой.

LaTeX

$$$A^{\star\text{-closure}} = \top.$$$

Lean4

/-- 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 starSubalgebra_topologicalClosure_eq_top_of_separatesPoints (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, ℝ) →L[ℝ] C(X, 𝕜) := ofRealCLM.compLeftContinuous ℝ X
  have key : LinearMap.range I ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
    -- Let `A₀` be the subalgebra of `C(X, ℝ)` consisting of `A`'s purely real elements; it is the
        -- preimage of `A` under `I`.  In this argument we only need its submodule structure.

    let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I
    have SW : A₀.topologicalClosure = ⊤ :=
      haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
      congr_arg Subalgebra.toSubmodule this
    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 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
            -- closure of `A`

  intro f
  let f_re : C(X, ℝ) := (⟨RCLike.re, RCLike.reCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  let f_im : C(X, ℝ) := (⟨RCLike.im, RCLike.imCLM.continuous⟩ : C(𝕜, ℝ)).comp f
  have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩
  have h_f_im : I f_im ∈ A.topologicalClosure :=
    key
      ⟨f_im, rfl⟩
        -- So `f_re + I • f_im` is in the closure of `A`

  have := A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im RCLike.I)
  rw [StarSubalgebra.mem_toSubalgebra] at this
  convert this
  ext
  apply Eq.symm
  simp [I, f_re, f_im, mul_comm RCLike.I _]

Похожие утверждения