English
For a morphism φ: A →⋆ₐ[ℂ] B, the naturality relation holds: composing the Gelfand transforms on A and B with φ commutes with the corresponding precomposition on spectra.
Русский
Для морфизма φ: A →⋆ₐ[ℂ] B справедлива натуральность: композиция преобразований Гельфанда с φ коммутирует с предкомпозицией на спектрах.
LaTeX
$$$(gelfandStarTransform B) \\\\circ φ = (compContinuousMap φ \\\\|> comp) \\\\circ (gelfandStarTransform A)$$$
Lean4
/-- A non-unital star algebra monomorphism of complex C⋆-algebras is isometric. -/
theorem norm_map (φ : F) (hφ : Function.Injective φ) (a : A) : ‖φ a‖ = ‖a‖ := by
/- Since passing to the unitization is functorial, and it is an isometric embedding, we may assume
that `φ` is a unital star algebra monomorphism and that `A` and `B` are unital C⋆-algebras. -/
suffices ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B} (_ : Function.Injective ψ) (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖
by simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a
intro ψ hψ a
rw [← sq_eq_sq₀ (by positivity) (by positivity)]
simp only [sq, ← CStarRing.norm_star_mul_self, ← map_star, ← map_mul]
/- since `star a * a` is selfadjoint, it has the same `ℝ`-spectrum as `ψ (star a * a)`.
Since the spectral radius over `ℝ` coincides with the norm, `‖ψ (star a * a)‖ = ‖star a * a‖`. -/
have ha : IsSelfAdjoint (star a * a) := .star_mul_self a
calc
‖ψ (star a * a)‖ = (spectralRadius ℝ (ψ (star a * a))).toReal := ha.map ψ |>.toReal_spectralRadius_eq_norm.symm
_ = (spectralRadius ℝ (star a * a)).toReal := by simp only [spectralRadius, ha.map_spectrum_real ψ hψ]
_ = ‖star a * a‖ := ha.toReal_spectralRadius_eq_norm
