English
There is a star-algebra isomorphism between continuous complex-valued functions on the spectrum of a and the unital C*-subalgebra generated by a, extending the polynomial calculus.
Русский
Существует изоморфизм по звездной алгебре между непрерывными комплекс-значными функциями на спектре a и единичной C*-подалгеброй, порождаемой a, продолжающий полинейный функциональный калькулялс.
LaTeX
$$$\\mathrm{continuousFunctionalCalculus}(a) : C(\\mathrm{spec}_{\\mathbb{C}} a, \\mathbb{C}) \\cong_*^{\\mathbb{C}} \\mathrm{elemental} \\mathbb{C} a$$$
Lean4
/-- **Continuous functional calculus.** Given a normal element `a : A` of a unital C⋆-algebra,
the continuous functional calculus is a `StarAlgEquiv` from the complex-valued continuous
functions on the spectrum of `a` to the unital C⋆-subalgebra generated by `a`. Moreover, this
equivalence identifies `(ContinuousMap.id ℂ).restrict (spectrum ℂ a))` with `a`; see
`continuousFunctionalCalculus_map_id`. As such it extends the polynomial functional calculus. -/
noncomputable def continuousFunctionalCalculus : C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elemental ℂ a :=
((characterSpaceHomeo a).compStarAlgEquiv' ℂ ℂ).trans (gelfandStarTransform (elemental ℂ a)).symm
