English
If A is a nonunital commutative C*-algebra, then the unitization of A over ℂ is a commutative C*-algebra.
Русский
Если A — неполная коммутативная C*-алгебра, то ее единичное расширение над ℂ является коммутативной C*-алгеброй.
LaTeX
$$$\text{Unitization } \mathbb{C} A \text{ is a CommCStarAlgebra}$$$
Lean4
/-- The norm on `Unitization 𝕜 E` satisfies the C⋆-property -/
instance instCStarRing : CStarRing (Unitization 𝕜 E) where
norm_mul_self_le
x := by
-- rewrite both sides as a `⊔`
simp only [Unitization.norm_def, Prod.norm_def]
-- Show that `(Unitization.splitMul 𝕜 E x).snd` satisfies the C⋆-property, in two stages:
have h₁ : ∀ x : Unitization 𝕜 E, ‖(Unitization.splitMul 𝕜 E x).snd‖ ≤ ‖(Unitization.splitMul 𝕜 E (star x)).snd‖ :=
by
simp only [Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_star]
intro x
by_cases h : algebraMap 𝕜 (E →L[𝕜] E) x.fst + mul 𝕜 E x.snd = 0
· simp only [h, norm_zero]
exact norm_nonneg _
· have :
‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤
‖(Unitization.splitMul 𝕜 E (star x)).snd‖ * ‖(Unitization.splitMul 𝕜 E x).snd‖ :=
(norm_splitMul_snd_sq 𝕜 x).trans <| by
rw [map_mul, Prod.snd_mul]
exact norm_mul_le _ _
rw [sq] at this
rw [← Ne, ← norm_pos_iff] at h
simp only [Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_star] at this
exact (mul_le_mul_iff_left₀ h).mp this
have h₂ : ‖(Unitization.splitMul 𝕜 E (star x * x)).snd‖ = ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 :=
by
refine le_antisymm ?_ (norm_splitMul_snd_sq 𝕜 x)
rw [map_mul, Prod.snd_mul]
exact
(norm_mul_le _ _).trans <| by
rw [sq]
gcongr
simpa only [star_star] using
h₁
(star x)
-- Show that `(Unitization.splitMul 𝕜 E x).fst` satisfies the C⋆-property
have h₃ : ‖(Unitization.splitMul 𝕜 E (star x * x)).fst‖ = ‖(Unitization.splitMul 𝕜 E x).fst‖ ^ 2 := by
simp only [Unitization.splitMul_apply, Unitization.fst_mul, Unitization.fst_star, norm_mul, norm_star, sq]
rw [h₂, h₃]
/- use the definition of the norm, and split into cases based on whether the norm in the first
coordinate is bigger or smaller than the norm in the second coordinate. -/
by_cases h : ‖(Unitization.splitMul 𝕜 E x).fst‖ ≤ ‖(Unitization.splitMul 𝕜 E x).snd‖
· rw [sq, sq, sup_eq_right.mpr h, sup_eq_right.mpr (mul_self_le_mul_self (norm_nonneg _) h)]
· replace h := (not_le.mp h).le
rw [sq, sq, sup_eq_left.mpr h, sup_eq_left.mpr (mul_self_le_mul_self (norm_nonneg _) h)]
