English
If a star subalgebra A of C(X, 𝕜) separates points, then the corresponding real subalgebra of its purely real elements also separates points.
Русский
Если звездная подалгебра A ⊂ C(X, 𝕜) разделяет точки, то соответствующая реальная подалгебра из чисто действительных элементов также разделяет точки.
LaTeX
$$$((A_{\mathbb{R}})^{\mathrm{comap}} \cdot {\text{ofReal}}) \;\text{separatesPoints}.$$$
Lean4
/-- If a star subalgebra of `C(X, 𝕜)` separates points, then the real subalgebra
of its purely real-valued elements also separates points. -/
theorem rclike_to_real {A : StarSubalgebra 𝕜 C(X, 𝕜)} (hA : A.SeparatesPoints) :
((A.restrictScalars ℝ).comap (ofRealAm.compLeftContinuous ℝ continuous_ofReal)).SeparatesPoints :=
by
intro x₁ x₂ hx
obtain ⟨_, ⟨f, hfA, rfl⟩, hf⟩ := hA hx
let F : C(X, 𝕜) :=
f -
const _
(f x₂)
-- Subtract the constant `f x₂` from `f`; this is still an element of the subalgebra
have hFA : F ∈ A :=
by
refine A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)
ext1
simp only [smul_apply, one_apply, Algebra.id.smul_eq_mul, mul_one, const_apply]
-- Consider now the function `fun x ↦ |f x - f x₂| ^ 2`
refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
· -- This is also an element of the subalgebra, and takes only real values
rw [SetLike.mem_coe, Subalgebra.mem_comap]
convert (A.restrictScalars ℝ).mul_mem hFA (star_mem hFA : star F ∈ A)
ext1
simp [← RCLike.mul_conj]
· -- And it also separates the points `x₁`, `x₂`
simpa [F] using sub_ne_zero.mpr hf
