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

theorem ContinuousLinearMap.op_norm_mul_flip_apply (𝕜 : Type u_1) {E : Type u_2} [] [] [] [] [] [] (a : E) :
theorem ContinuousLinearMap.op_nnnorm_mul_flip_apply (𝕜 : Type u_1) {E : Type u_2} [] [] [] [] [] [] (a : E) :
theorem ContinuousLinearMap.isometry_mul_flip (𝕜 : Type u_1) (E : Type u_2) [] [] [] [] [] [] :
instance CstarRing.instRegularNormedAlgebra (𝕜 : Type u_1) (E : Type u_2) [] [] [] [] [] :

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} [] [] [] [] [] [] [] (x : ) :
(↑() x).snd ^ 2 (↑() (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} [] [] [] [] [] [] [] [] :

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