English
Let A be a star-subalgebra of bounded 𝕜-valued functions on a space E. The two natural ways of restricting scalars to ℝ and applying the real-linear realization are equal to first mapping via the star-structure and then restricting scalars; i.e., two canonical constructions yield the same real subalgebra of bounded real-valued maps.
Русский
Пусть A — подалгебра со знаком-звезда в пространстве ограниченно-непрерывных функций с значениямии в 𝕜 на E. Два естественных способа ограничивать скаляры до ℝ и рассматривать реальную реализацию дают одну и ту же подалгебру ограниченно вещественных отображений: два канонических построения совпадают.
LaTeX
$$$((A_{\\mathbb{R}})^{\\mathrm{comap}}(\\mathrm{AlgHom}_{\\mathbb{R}}(\\mathrm{ofRealAm}, \\mathrm{lipschitzWith\\_ofReal}))) = ((A^{\\mathrm{map}}(\\mathrm{toContinuousMapStar}_{\\mathbb{𝕜}}))_{\\mathbb{R}})^{\\mathrm{comap}}(\\mathrm{ofRealAm} \\circ \\mathrm{continuous\\_ofReal})$$$
Lean4
/-- On a star subalgebra of bounded continuous functions, the operations "restrict scalars to ℝ"
and "forget that a bounded continuous function is a bounded" commute. -/
theorem restrict_toContinuousMap_eq_toContinuousMapStar_restrict {A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)} :
((A.restrictScalars ℝ).comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm lipschitzWith_ofReal)).map
(toContinuousMapₐ ℝ) =
((A.map (toContinuousMapStarₐ 𝕜)).restrictScalars ℝ).comap (ofRealAm.compLeftContinuous ℝ continuous_ofReal) :=
by
ext g
simp only [Subalgebra.mem_map, Subalgebra.mem_comap, Subalgebra.mem_restrictScalars, StarSubalgebra.mem_toSubalgebra,
toContinuousMapₐ_apply, StarSubalgebra.mem_map]
constructor
· intro ⟨x, hxA, hxg⟩
use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA
ext a
simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuousBounded_apply_apply, ofRealAm_coe,
AlgHom.compLeftContinuous_apply_apply, algebraMap.coe_inj]
exact DFunLike.congr_fun hxg a
· intro ⟨x, hxA, hxg⟩
have hg_apply (a : E) := DFunLike.congr_fun hxg a
simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuous_apply_apply, ofRealAm_coe] at hg_apply
have h_comp_eq :
(@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal (x.comp reCLM (@reCLM 𝕜 _).lipschitz) = x :=
by
ext a
simp [hg_apply]
use x.comp reCLM (@reCLM 𝕜 _).lipschitz
refine ⟨by rwa [h_comp_eq], ?_⟩
ext a
simp [hg_apply]
