English
Let A be a commutative complex C*-algebra. The Gelfand transform maps A onto the algebra of continuous complex-valued functions on its spectrum, hence is a bijection.
Русский
Пусть A — коммутативная комплексная C*-алгебра над ℂ. Преобразование Гельфанда отображает A в алгебру непрерывных комплекснозначных функций на спектре A и является биекцией.
LaTeX
$$$\\\\mathcal{G}_{A}: A \\\\to C(\\\\mathrm{Char}(A), \\\\mathbb{C}) \\\\text{ is bijective}$$$
Lean4
/-- The Gelfand transform is bijective when the algebra is a C⋆-algebra over `ℂ`. -/
theorem gelfandTransform_bijective : Function.Bijective (gelfandTransform ℂ A) :=
by
refine
⟨(gelfandTransform_isometry A).injective, ?_⟩
/- The range of `gelfandTransform ℂ A` is actually a `StarSubalgebra`. The key lemma below may be
hard to spot; it's `map_star` coming from `WeakDual.Complex.instStarHomClass`, which is a
nontrivial result. -/
let rng : StarSubalgebra ℂ C(characterSpace ℂ A, ℂ) :=
{ toSubalgebra := (gelfandTransform ℂ A).range
star_mem' := by
rintro - ⟨a, rfl⟩
use star a
ext1 φ
dsimp
simp only [map_star, RCLike.star_def] }
suffices rng = ⊤ from fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top
have h : rng.topologicalClosure = rng :=
le_antisymm
(StarSubalgebra.topologicalClosure_minimal le_rfl (gelfandTransform_isometry A).isClosedEmbedding.isClosed_range)
(StarSubalgebra.le_topologicalClosure _)
refine
h ▸
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
(fun _ _ => ?_)
/- Separating points just means that elements of the `characterSpace` which agree at all points
of `A` are the same functional, which is just extensionality. -/
contrapose!
exact fun h =>
Subtype.ext (ContinuousLinearMap.ext fun a => h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)
