Documentation

Mathlib.Analysis.NormedSpace.Star.Unitization

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).

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] :

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) :
ā€–(ā†‘(Unitization.splitMul š•œ E) x).sndā€– ^ 2 ā‰¤ ā€–(ā†‘(Unitization.splitMul š•œ E) (star x * x)).sndā€–

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