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) : ‖(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 E)) a‖ = ‖a‖

@[deprecated ContinuousLinearMap.opNorm_mul_flip_apply]

theorem ContinuousLinearMap.op_norm_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) : ‖(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 E)) a‖ = ‖a‖

Alias of ContinuousLinearMap.opNorm_mul_flip_apply.

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) : ‖(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 E)) a‖₊ = ‖a‖₊

@[deprecated ContinuousLinearMap.opNNNorm_mul_flip_apply]

theorem ContinuousLinearMap.op_nnnorm_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) : ‖(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 E)) a‖₊ = ‖a‖₊

Alias of ContinuousLinearMap.opNNNorm_mul_flip_apply.

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 ⇑(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 E))

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.

Equations

• (_ : RegularNormedAlgebra 𝕜 E) = (_ : RegularNormedAlgebra 𝕜 E)

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) : ‖((Unitization.splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((Unitization.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 𝕜] [CstarRing 𝕜] [StarModule 𝕜 E] : CstarRing (Unitization 𝕜 E)

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

Equations

• (_ : CstarRing (Unitization 𝕜 E)) = (_ : CstarRing (Unitization 𝕜 E))