English
The Gelfand transform is an isometry for commutative C*-algebras over ℂ.
Русский
Гельфанд-преобразование является изометрией для коммутативных C*-алгебр над ℂ.
LaTeX
$$$$\text{Isometry}(\mathrm{gelfandTransform}(\mathbb{C},A))$$$$
Lean4
/-- The Gelfand transform is an isometry when the algebra is a C⋆-algebra over `ℂ`. -/
theorem gelfandTransform_isometry : Isometry (gelfandTransform ℂ A) :=
by
nontriviality A
refine
AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a =>
?_
/- By `spectrum.gelfandTransform_eq`, the spectra of `star a * a` and its
`gelfandTransform` coincide. Therefore, so do their spectral radii, and since they are
self-adjoint, so also do their norms. Applying the C⋆-property of the norm and taking square
roots shows that the norm is preserved. -/
have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
(IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this
simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this
simpa only [Function.comp_apply, NNReal.sqrt_sq] using congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this
