Constructions of Hilbert C⋆-modules #
In this file we define the following constructions of CStarModules where A denotes a C⋆-algebra.
For some of the types listed below, the instance is declared on the type synonym WithCStarModule E
(with the notation C⋆ᵐᵒᵈ E), instead of on E itself; we explain the reasoning behind each
decision below.
Aas aCStarModuleover itself.C⋆ᵐᵒᵈ (E × F)as aCStarModuleoverA, whenEandFare themselvesCStarModules overA.C⋆ᵐᵒᵈ (Π i : ι, E i)as aCStarModuleoverA, when eachE iis aCStarModuleoverAandιis aFintype.Eas aCStarModuleoverℂ, whenEis anInnerProductSpaceoverℂ.
For E × F and Π i : ι, E i, we are required to declare the instance on a type synonym rather
than on the product or pi-type itself because the existing norm on these types does not agree with
the one induced by the C⋆-module structure. Moreover, the norm induced by the C⋆-module structure
doesn't agree with any other natural norm on these types (e.g., WithLp 2 (E × F) unless A := ℂ),
so we need a new synonym.
On A (a C⋆-algebra) and E (an inner product space), we declare the instances on the types
themselves to ease the use of the C⋆-module structure. This does have the potential to cause
inconvenience (as sometimes Lean will see terms of type A and apply lemmas pertaining to
C⋆-modules to those terms, when the lemmas were actually intended for terms of some other
C⋆-module in context, say F, in which case the arguments must be provided explicitly; see for
instance the application of CStarModule.norm_eq_sqrt_norm_inner_self in the proof of
WithCStarModule.max_le_prod_norm below). However, we believe that this, hopefully rare,
inconvenience is outweighed by avoiding translating between type synonyms where possible.
For more details on the importance of the WithCStarModule type synonym, see the module
documentation for Analysis.CStarAlgebra.Module.Synonym.
Implementation notes #
When A := ℂ and E := ℂ, then ℂ is both a C⋆-algebra (so it inherits a CStarModule instance
via (1) above) and an inner product space (so it inherits a CStarModule instance via (4) above).
We provide a sanity check ensuring that these two instances are definitionally equal. We also ensure
that the Inner ℂ ℂ instance from InnerProductSpace is definitionally equal to the one inherited
from the CStarModule instances.
Note that C⋆ᵐᵒᵈ E is already equipped with a bornology and uniformity whenever E is (namely,
the pullback of the respective structures through WithCStarModule.equiv), so in each of the above
cases, it is necessary to temporarily instantiate C⋆ᵐᵒᵈ E with CStarModule.normedAddCommGroup,
show the resulting type is bilipschitz equivalent to E via WithCStarModule.equiv (in the first
and last case, this map is actually trivially an isometry), and then replace the uniformity and
bornology with the correct ones.
A C⋆-algebra as a C⋆-module over itself #
Reinterpret a C⋆-algebra A as a CStarModule over itself.
Equations
- WithCStarModule.instCStarModule = CStarModule.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Products of C⋆-modules #
Equations
- WithCStarModule.instCStarModuleProd = CStarModule.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- WithCStarModule.instNormedAddCommGroupProd = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯
Equations
- WithCStarModule.instNormedSpaceComplexProd = NormedSpace.ofCore ⋯
Pi-types of C⋆-modules #
Equations
- WithCStarModule.instCStarModuleForall = CStarModule.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- WithCStarModule.instNormedAddCommGroupForall = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯
Equations
- WithCStarModule.instNormedSpaceComplexForall = NormedSpace.ofCore ⋯
Inner product spaces as C⋆-modules #
Reinterpret an inner product space E over ℂ as a CStarModule over ℂ.
Note: this instance requires SMul ℂᵐᵒᵖ E and IsCentralScalar ℂ E instances to exist on E,
which is unlikely to occur in practice. However, in practice one could either add those instances
to the type E in question, or else supply them to this instance manually, which is reason behind
the naming of these two instance arguments.
Equations
- WithCStarModule.instCStarModuleComplex = CStarModule.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯