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
- CStarModule.innerₛₗ = { toFun := fun (x : E) => { toFun := fun (y : E) => inner x y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
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.
Instances For
The function ⟨x, y⟩ ↦ ⟪x, y⟫ bundled as a continuous sesquilinear map.
Equations
- CStarModule.innerSL = CStarModule.innerₛₗ.mkContinuous₂ 1 ⋯