Constructions of Hilbert C⋆-modules #
In this file we define the following constructions of CStarModule
s 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.
A
as aCStarModule
over itself.C⋆ᵐᵒᵈ (E × F)
as aCStarModule
overA
, whenE
andF
are themselvesCStarModule
s overA
.C⋆ᵐᵒᵈ (Π i : ι, E i)
as aCStarModule
overA
, when eachE i
is aCStarModule
overA
andι
is aFintype
.E
as aCStarModule
overℂ
, whenE
is anInnerProductSpace
overℂ
.
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.instNormForall = { norm := fun (x : WithCStarModule ((i : ι) → E i)) => √‖∑ i : ι, ⟪x i, x i⟫_A‖ }
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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯