bijective_characterSpaceToSpectrum

English

The map from the character space to the spectrum is bijective.

Русский

Отображение между пространством характеров и спектром является биективным.

LaTeX

$$Function.Bijective (characterSpaceToSpectrum a)$$

Lean4

theorem bijective_characterSpaceToSpectrum : Function.Bijective (characterSpaceToSpectrum a) :=
  by
  refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
  · exact (map_continuous φ)
  · exact (map_continuous ψ)
  · simpa only [characterSpaceToSpectrum, Subtype.mk_eq_mk, ContinuousMap.coe_mk] using h
  · rintro ⟨z, hz⟩
    have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a) (a := ⟨a, self_mem ℂ a⟩) ▸ hz)
    rw [CharacterSpace.mem_spectrum_iff_exists] at hz'
    obtain ⟨φ, rfl⟩ := hz'
    exact ⟨φ, rfl⟩

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