English
Let φ be a nonunital star-algebra homomorphism between complex C*-algebras A → B. Then for every a ∈ A, the norm is nonincreasing under φ: ∥φ(a)∥ ≤ ∥a∥.
Русский
Пусть φ — неглавный звездный однородный гомоморфизм между комплексными C*-алгебрами A и B. Тогда для любого a ∈ A выполняется нерастяжение норм: ∥φ(a)∥ ≤ ∥a∥.
LaTeX
$$$\|\phi(a)\| \leqslant \|a\|$$$
Lean4
/-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive. -/
theorem nnnorm_apply_le (φ : F) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊ :=
by
have h (ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B) (x : Unitization ℂ A) : ‖ψ x‖₊ ≤ ‖x‖₊ :=
by
suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊
by
refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
exact this <| .star_mul_self x
intro s hs
suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe] at this
exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)
simpa [nnnorm_inr] using h (starLift (inrNonUnitalStarAlgHom ℂ B |>.comp (φ : A →⋆ₙₐ[ℂ] B))) a
