The minimal unitization of a C⋆-algebra

This file shows that when E is a C⋆-algebra (over a densely normed field 𝕜), that the minimal Unitization is as well. In order to ensure that the norm structure is available, we must first show that every C⋆-algebra is a RegularNormedAlgebra.

In addition, we show that in a RegularNormedAlgebra which is a StarRing for which the involution is isometric, that multiplication on the right is also an isometry (i.e., Isometry (ContinuousLinearMap.mul 𝕜 E).flip).

theorem ContinuousLinearMap.opNorm_mul_flip_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [NormedStarGroup E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E] (a : E) : ‖(mul 𝕜 E).flip a‖ = ‖a‖

theorem ContinuousLinearMap.opNNNorm_mul_flip_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [NormedStarGroup E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E] (a : E) : ‖(mul 𝕜 E).flip a‖₊ = ‖a‖₊

theorem ContinuousLinearMap.isometry_mul_flip (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [NormedStarGroup E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E] : Isometry ⇑(mul 𝕜 E).flip

instance CStarRing.instRegularNormedAlgebra (𝕜 : Type u_1) (E : Type u_2) [DenselyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [CStarRing E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] : RegularNormedAlgebra 𝕜 E

A C⋆-algebra over a densely normed field is a regular normed algebra.

theorem Unitization.norm_splitMul_snd_sq (𝕜 : Type u_1) {E : Type u_2} [DenselyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [CStarRing E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] [StarRing 𝕜] [StarModule 𝕜 E] (x : Unitization 𝕜 E) : ‖((splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((splitMul 𝕜 E) (star x * x)).2‖

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.

instance Unitization.instCStarRing {𝕜 : Type u_1} {E : Type u_2} [DenselyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [CStarRing E] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] [StarRing 𝕜] [StarModule 𝕜 E] [CStarRing 𝕜] : CStarRing (Unitization 𝕜 E)

The norm on Unitization 𝕜 E satisfies the C⋆-property

def CStarAlgebra.«term_⁺¹» : Lean.TrailingParserDescr

The minimal unitization (over ℂ) of a C⋆-algebra, equipped with the C⋆-norm. When A is unital, A⁺¹ ≃⋆ₐ[ℂ] (ℂ × A).

noncomputable instance Unitization.instCStarAlgebra {A : Type u_3} [NonUnitalCStarAlgebra A] : CStarAlgebra (Unitization ℂ A)

noncomputable instance Unitization.instCommCStarAlgebra {A : Type u_3} [NonUnitalCommCStarAlgebra A] : CommCStarAlgebra (Unitization ℂ A)