English
There is a canonical complex-amplified C*-algebra structure on 𝓜(𝕜,A) when A is a nonunital C*-algebra.
Русский
Для 𝓜(𝕜,A) существует каноническая структура C*-алгебры над Complex, если A — неполная C*-алгебра.
LaTeX
$$$\mathcal{M}(\mathbb{K},A) \text{ is a } C^*\text{-algebra under complex structure}$$$
Lean4
instance instCStarRing : CStarRing 𝓜(𝕜, A) where
norm_mul_self_le := fun (a : 𝓜(𝕜, A)) =>
le_of_eq <|
Eq.symm <|
congr_arg ((↑) : ℝ≥0 → ℝ) <|
show ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊ by
/- The essence of the argument is this: let `a = (L,R)` and recall `‖a‖ = ‖L‖`.
`star a = (star ∘ R ∘ star, star ∘ L ∘ star)`. Then for any `x y : A`, we have
`‖star a * a‖ = ‖(star a * a).snd‖ = ‖R (star (L (star x))) * y‖ = ‖star (L (star x)) * L y‖`
Now, on the one hand,
`‖star (L (star x)) * L y‖ ≤ ‖star (L (star x))‖ * ‖L y‖ = ‖L (star x)‖ * ‖L y‖ ≤ ‖L‖ ^ 2`
whenever `‖x‖, ‖y‖ ≤ 1`, so the supremum over all such `x, y` is at most `‖L‖ ^ 2`.
On the other hand, for any `‖z‖ ≤ 1`, we may choose `x := star z` and `y := z` to get:
`‖star (L (star x)) * L y‖ = ‖star (L z) * (L z)‖ = ‖L z‖ ^ 2`, and taking the supremum over
all such `z` yields that the supremum is at least `‖L‖ ^ 2`. It is the latter part of the
argument where `DenselyNormedField 𝕜` is required (for `sSup_unitClosedBall_eq_nnnorm`). -/
have hball : (Metric.closedBall (0 : A) 1).Nonempty := Metric.nonempty_closedBall.2 zero_le_one
have key : ∀ x y, ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.snd (star (a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊ :=
by
intro x y hx hy
rw [a.central]
calc
‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
_ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
(mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx)) (a.fst.le_opNorm_of_le hy))
_ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
rw [← nnnorm_snd]
simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply]
simp only [← @opNNNorm_mul_apply 𝕜 _ A]
simp only [← sSup_unitClosedBall_eq_nnnorm, mul_apply']
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_
· rintro - ⟨x, hx, rfl⟩
refine csSup_le (hball.image _) ?_
rintro - ⟨y, hy, rfl⟩
exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)
· simp only [Set.mem_image, exists_exists_and_eq_and]
have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt.2 hr
simp_rw [← nnnorm_fst, ← sSup_unitClosedBall_eq_nnnorm] at hr'
obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'
have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx
refine ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), ?_⟩
refine lt_csSup_of_lt ?_ ⟨x, hx, rfl⟩ ?_
· refine ⟨‖a‖₊ * ‖a‖₊, ?_⟩
rintro - ⟨y, hy, rfl⟩
exact key (star x) y ((nnnorm_star x).trans_le hx') (mem_closedBall_zero_iff.1 hy)
·
simpa only [a.central, star_star, CStarRing.nnnorm_star_mul_self, NNReal.sq_sqrt, ← sq] using
pow_lt_pow_left₀ hxr zero_le' two_ne_zero
