English
The Gelfand transform induces a star-algebra isomorphism between a commutative unital C*-algebra over ℂ and the continuous functions on its spectrum.
Русский
Преобразование Гельфанда задаёт изоморфизм звёздных алгебр между коммутативной унилатной C*-алгеброй над ℂ и непрерывными функциями на её спектре.
LaTeX
$$$gelfandStarTransform: A \\\\cong_{*\\\\mathbb{C}} C(\\\\mathrm{CharacterSpace}(\\\\mathbb{C}, A), \\\\mathbb{C})$$$
Lean4
/-- The Gelfand transform as a `StarAlgEquiv` between a commutative unital C⋆-algebra over `ℂ`
and the continuous functions on its `characterSpace`. -/
@[simps!]
noncomputable def gelfandStarTransform : A ≃⋆ₐ[ℂ] C(characterSpace ℂ A, ℂ) :=
StarAlgEquiv.ofBijective
(show A →⋆ₐ[ℂ] C(characterSpace ℂ A, ℂ) from
{ gelfandTransform ℂ A with map_star' := fun x => gelfandTransform_map_star x })
(gelfandTransform_bijective A)
