English
Matrices with entries in a nonunital C*-algebra A form a NonUnitalCStarAlgebra.
Русский
Матрицы с элементами из ненулевой C*-алгебры A образуют ненулевую C*-алгебру.
LaTeX
$$$$\\mathrm{NonUnitalCStarAlgebra}(\\mathrm{CStarMatrix}(n,n,A)).$$$$
Lean4
/-- Matrices with entries in a C⋆-algebra form a C⋆-algebra. -/
instance instCStarRing : CStarRing (CStarMatrix n n A) :=
.of_le_norm_mul_star_self fun M ↦
by
have hmain : ‖M‖ ≤ √‖M * star M‖ := by
change ‖toCLM M‖ ≤ √‖M * star M‖
rw [opNorm_le_iff (by positivity)]
intro v
rw [norm_eq_sqrt_norm_inner_self (A := A), ← inner_toCLM_conjTranspose_right]
have h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2 :=
calc
_ ≤ ‖v‖ * ‖(toCLM Mᴴ) (toCLM M v)‖ := norm_inner_le (C⋆ᵐᵒᵈ(A, n → A))
_ ≤ ‖v‖ * ‖(toCLM Mᴴ).comp (toCLM M)‖ * ‖v‖ := by
rw [mul_assoc]
gcongr
rw [← ContinuousLinearMap.comp_apply]
exact le_opNorm ((toCLM Mᴴ).comp (toCLM M)) v
_ = ‖(toCLM Mᴴ).comp (toCLM M)‖ * ‖v‖ ^ 2 := by ring
_ = ‖M * star M‖ * ‖v‖ ^ 2 := by
congr
apply MulOpposite.op_injective
simp only [← toCLMNonUnitalAlgHom_eq_toCLM, map_mul]
rfl
have h₂ : ‖v‖ = √(‖v‖ ^ 2) := by simp
rw [h₂, ← Real.sqrt_mul]
gcongr
positivity
rw [← Real.sqrt_le_sqrt_iff (by positivity)]
simp [hmain]
