Documentation

Mathlib.Analysis.CStarAlgebra.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).

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) :
@[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) :

Alias of ContinuousLinearMap.opNorm_mul_flip_apply.

@[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) :

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

Equations
  • ā‹Æ = ā‹Æ
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) :

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

Equations
  • ā‹Æ = ā‹Æ