English
The unitization of a nonunital C*-algebra inherits a C*-ring structure; in particular Unitization 𝕜 E is a C*-algebra.
Русский
Объединение единицы для неполной C*-алгебры наследует структуру C*-кольца; в частности Unitization 𝕜 E — это C*-алгебра.
LaTeX
$$$\text{Unitization } 𝕜 E \text{ is a } C^*\text{-algebra}$$$
Lean4
/-- This is the key lemma used to establish the instance `Unitization.instCStarRing`
(i.e., proving that the norm on `Unitization 𝕜 E` satisfies the C⋆-property). We split this one
out so that declaring the `CStarRing` instance doesn't time out. -/
theorem norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤ ‖(Unitization.splitMul 𝕜 E (star x * x)).snd‖ := by
/- The key idea is that we can use `sSup_unitClosedBall_eq_norm` to make this about
applying this linear map to elements of norm at most one. There is a bit of `sqrt` and `sq`
shuffling that needs to occur, which is primarily just an annoyance. -/
refine (Real.le_sqrt (norm_nonneg _) (norm_nonneg _)).mp ?_
simp only [Unitization.splitMul_apply]
rw [← sSup_unitClosedBall_eq_norm]
refine csSup_le ((Metric.nonempty_closedBall.2 zero_le_one).image _) ?_
rintro - ⟨b, hb, rfl⟩
simp only
-- rewrite to a more convenient form; this is where we use the C⋆-property
rw [← Real.sqrt_sq (norm_nonneg _), Real.sqrt_le_sqrt_iff (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self,
ContinuousLinearMap.add_apply, star_add, mul_apply', Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply,
ContinuousLinearMap.one_apply, star_mul, star_smul, add_mul, smul_mul_assoc, ← mul_smul_comm, mul_assoc, ← mul_add,
← sSup_unitClosedBall_eq_norm]
refine (norm_mul_le _ _).trans ?_
calc
_ ≤ ‖star x.fst • (x.fst • b + x.snd * b) + star x.snd * (x.fst • b + x.snd * b)‖ :=
by
nth_rewrite 2 [← one_mul ‖_ + _‖]
gcongr
exact (norm_star b).symm ▸ mem_closedBall_zero_iff.1 hb
_ ≤ sSup (_ '' Metric.closedBall 0 1) :=
le_csSup ?_
⟨b, hb, ?_⟩
-- now we just check the side conditions for `le_csSup`. There is nothing of interest here.
· refine ⟨‖(star x * x).fst‖ + ‖(star x * x).snd‖, ?_⟩
rintro _ ⟨y, hy, rfl⟩
refine (norm_add_le _ _).trans ?_
gcongr
· rw [Algebra.algebraMap_eq_smul_one]
refine (norm_smul _ _).trans_le ?_
simpa only [mul_one] using mul_le_mul_of_nonneg_left (mem_closedBall_zero_iff.1 hy) (norm_nonneg (star x * x).fst)
· exact (unit_le_opNorm _ y <| mem_closedBall_zero_iff.1 hy).trans (opNorm_mul_apply_le _ _ _)
· simp only [ContinuousLinearMap.add_apply, mul_apply', Unitization.snd_star, Unitization.snd_mul,
Unitization.fst_mul, Unitization.fst_star, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply, smul_add,
mul_add, add_mul]
simp only [smul_smul, smul_mul_assoc, ← add_assoc, ← mul_assoc, mul_smul_comm]
