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.ofCore
andNormedSpace.ofCore
to 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 CStarModule
s 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
- inner_self_nonneg : ∀ {x : E}, 0 ≤ ⟪x, x⟫_A
- inner_op_smul_right : ∀ {a : A} {x y : E}, ⟪x, MulOpposite.op a • y⟫_A = ⟪x, y⟫_A * 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) => ⟪x, y⟫_A, 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.
Equations
- CStarModule.norm A = { norm := fun (x : E) => √‖⟪x, x⟫_A‖ }
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 ⋯