characterSpaceHomeo — Mathlib

English

There is a homeomorphism between the character space of the unital subalgebra generated by a and the spectrum of a.

Русский

Существует гомеоморфизм между пространством характеров единичной подпалгебры, порождаемой a, и спектром a.

LaTeX

$$$\\text{characterSpaceHomeo } a : \\mathrm{characterSpace}(\\mathbb{C}, \\mathrm{elemental}(\\mathbb{C}, a)) \\simeq_t \\mathrm{ spectrum}(\\mathbb{C}, a)$$$

Lean4

/-- The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
single normal element `a : A` and `spectrum ℂ a`. -/
noncomputable def characterSpaceHomeo : characterSpace ℂ (elemental ℂ a) ≃ₜ spectrum ℂ a :=
  @Continuous.homeoOfEquivCompactToT2 _ _ _ _ _ _
    (Equiv.ofBijective (characterSpaceToSpectrum a) (bijective_characterSpaceToSpectrum a))
    (continuous_characterSpaceToSpectrum a)

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