Hilbert C⋆-modules #
A Hilbert C⋆-module is a complex module E together with a right A-module structure, where A
is a C⋆-algebra, and with an A-valued inner product. This inner product satisfies the
Cauchy-Schwarz inequality, and induces a norm that makes E a normed vector space over ℂ.
Main declarations #
CStarModule: The class containing the Hilbert C⋆-module structureCStarModule.normedSpaceCore: The proof that a Hilbert C⋆-module is a normed vector space. This can be used withNormedAddCommGroup.ofCoreandNormedSpace.ofCoreto create the relevant instances on a type of interest.CStarModule.inner_mul_inner_swap_le: The statement that⟪y, x⟫ * ⟪x, y⟫ ≤ ‖x‖ ^ 2 • ⟪y, y⟫, which can be viewed as a version of the Cauchy-Schwarz inequality for Hilbert C⋆-modules.CStarModule.norm_inner_le, which states that‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖, i.e. the Cauchy-Schwarz inequality.
Implementation notes #
The class CStarModule A E requires E to already have a Norm E instance on it, but
no other norm-related instances. We then include the fact that this norm agrees with the norm
induced by the inner product among the axioms of the class. Furthermore, instead of registering
NormedAddCommGroup E and NormedSpace ℂ E instances (which might already be present on the type,
and which would send the type class search algorithm on a chase for A), we provide a
NormedSpace.Core structure which enables downstream users of the class to easily register
these instances themselves on a particular type.
Although the Norm is passed as a parameter, it almost never coincides with the norm on the
underlying type, unless that it is a purpose built type, as with the standard Hilbert C⋆-module.
However, with generic types already equipped with a norm, the norm as a Hilbert C⋆-module almost
never coincides with the norm on the underlying type. The two notable exceptions to this are when
we view A as a C⋆-module over itself, or when A := ℂ. For this reason we will later use the
type synonym WithCStarModule.
As an example of just how different the norm can be, consider CStarModules E and F over A.
One would like to put a CStarModule structure on (a type synonym of) E × F, where the A-valued
inner product is given, for x y : E × F, ⟪x, y⟫_A := ⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A. The norm this
induces satisfies ‖x‖ ^ 2 = ‖⟪x.1, y.1⟫ + ⟪x.2, y.2⟫‖, but this doesn't coincide with any
natural norm on E × F unless A := ℂ, in which case it is WithLp 2 (E × F) because E × F is
then an InnerProductSpace over ℂ.
References #
- Erin Wittlich. Formalizing Hilbert Modules in C⋆-algebras with the Lean Proof Assistant, December 2022. Master's thesis, Southern Illinois University Edwardsville.
A Hilbert C⋆-module is a complex module E endowed with a right A-module structure
(where A is typically a C⋆-algebra) and an inner product ⟪x, y⟫_A which satisfies the
following properties.
- inner : E → E → A
Instances
Alias of CStarModule.
A Hilbert C⋆-module is a complex module E endowed with a right A-module structure
(where A is typically a C⋆-algebra) and an inner product ⟪x, y⟫_A which satisfies the
following properties.
Equations
Instances For
The function ⟨x, y⟩ ↦ ⟪x, y⟫ bundled as a sesquilinear map.
Equations
Instances For
The norm associated with a Hilbert C⋆-module. It is not registered as a norm, since a type might already have a norm defined on it.
Instances For
The C⋆-algebra-valued Cauchy-Schwarz inequality for Hilbert C⋆-modules.
The Cauchy-Schwarz inequality for Hilbert C⋆-modules.
This allows us to get NormedAddCommGroup and NormedSpace instances on E via
NormedAddCommGroup.ofCore and NormedSpace.ofCore.
This is not listed as an instance because we often want to replace the topology, uniformity and bornology instead of inheriting them from the norm.
Equations
- CStarModule.normedAddCommGroup = NormedAddCommGroup.ofCore ⋯
Instances For
The function ⟨x, y⟩ ↦ ⟪x, y⟫ bundled as a continuous sesquilinear map.
Equations
- CStarModule.innerSL = CStarModule.innerₛₗ.mkContinuous₂ 1 ⋯