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
).
A Cā-algebra over a densely normed field is a regular normed algebra.
Equations
- āÆ = āÆ
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.
The norm on Unitization š E
satisfies the Cā-property
Equations
- āÆ = āÆ