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 structure
• CStarModule.normedSpaceCore: The proof that a Hilbert C⋆-module is a normed vector space. This can be used with NormedAddCommGroup.ofCore and NormedSpace.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 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.

class CStarModule (A : outParam (Type u_1)) (E : Type u_2) [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] extends Inner : Type (max u_1 u_2)

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_add_right : ∀ {x y z : E}, ⟪x, y + z⟫_A = ⟪x, y⟫_A + ⟪x, z⟫_A
• inner_self_nonneg : ∀ {x : E}, 0 ≤ ⟪x, x⟫_A
• inner_self : ∀ {x : E}, ⟪x, x⟫_A = 0 ↔ x = 0
• inner_op_smul_right : ∀ {a : A} {x y : E}, ⟪x, MulOpposite.op a • y⟫_A = ⟪x, y⟫_A * a
• inner_smul_right_complex : ∀ {z : ℂ} {x y : E}, ⟪x, z • y⟫_A = z • ⟪x, y⟫_A
• star_inner : ∀ (x y : E), star ⟪x, y⟫_A = ⟪y, x⟫_A
• norm_eq_sqrt_norm_inner_self : ∀ (x : E), ‖x‖ = √‖⟪x, x⟫_A‖

@[simp]

theorem CStarModule.inner_add_right {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] {x : E} {y : E} {z : E} : ⟪x, y + z⟫_A = ⟪x, y⟫_A + ⟪x, z⟫_A

theorem CStarModule.inner_self_nonneg {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] {x : E} : 0 ≤ ⟪x, x⟫_A

theorem CStarModule.inner_self {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] {x : E} : ⟪x, x⟫_A = 0 ↔ x = 0

@[simp]

theorem CStarModule.inner_op_smul_right {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] {a : A} {x : E} {y : E} : ⟪x, MulOpposite.op a • y⟫_A = ⟪x, y⟫_A * a

@[simp]

theorem CStarModule.inner_smul_right_complex {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] {z : ℂ} {x : E} {y : E} : ⟪x, z • y⟫_A = z • ⟪x, y⟫_A

@[simp]

theorem CStarModule.star_inner {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] (x : E) (y : E) : star ⟪x, y⟫_A = ⟪y, x⟫_A

theorem CStarModule.norm_eq_sqrt_norm_inner_self {A : outParam (Type u_1)} {E : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [self : CStarModule A E] (x : E) : ‖x‖ = √‖⟪x, x⟫_A‖

@[deprecated CStarModule]

def CstarModule (A : outParam (Type u_1)) (E : Type u_2) [NonUnitalSemiring A] [StarRing A] [Module ℂ A] [AddCommGroup E] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] : Type (max u_1 u_2)

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

• CstarModule = CStarModule

@[simp]

theorem CStarModule.inner_add_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] {x : E} {y : E} {z : E} : ⟪x + y, z⟫_A = ⟪x, z⟫_A + ⟪y, z⟫_A

@[simp]

theorem CStarModule.inner_op_smul_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] {a : A} {x : E} {y : E} : ⟪MulOpposite.op a • x, y⟫_A = star a * ⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_smul_left_complex {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {z : ℂ} {x : E} {y : E} : ⟪z • x, y⟫_A = star z • ⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_smul_left_real {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {z : ℝ} {x : E} {y : E} : ⟪z • x, y⟫_A = z • ⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_smul_right_real {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {z : ℝ} {x : E} {y : E} : ⟪x, z • y⟫_A = z • ⟪x, y⟫_A

def CStarModule.innerₛₗ {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] : E →ₗ⋆[ℂ] E →ₗ[ℂ] A

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' := ⋯ }

theorem CStarModule.innerₛₗ_apply {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} {y : E} : (CStarModule.innerₛₗ x) y = ⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_zero_right {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} : ⟪x, 0⟫_A = 0

@[simp]

theorem CStarModule.inner_zero_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} : ⟪0, x⟫_A = 0

@[simp]

theorem CStarModule.inner_neg_right {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} {y : E} : ⟪x, -y⟫_A = -⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_neg_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} {y : E} : ⟪-x, y⟫_A = -⟪x, y⟫_A

@[simp]

theorem CStarModule.inner_sub_right {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} {y : E} {z : E} : ⟪x, y - z⟫_A = ⟪x, y⟫_A - ⟪x, z⟫_A

@[simp]

theorem CStarModule.inner_sub_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {x : E} {y : E} {z : E} : ⟪x - y, z⟫_A = ⟪x, z⟫_A - ⟪y, z⟫_A

@[simp]

theorem CStarModule.inner_sum_right {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {ι : Type u_3} {s : Finset ι} {x : E} {y : ι → E} : ⟪x, ∑ i ∈ s, y i⟫_A = ∑ i ∈ s, ⟪x, y i⟫_A

@[simp]

theorem CStarModule.inner_sum_left {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] [StarModule ℂ A] {ι : Type u_3} {s : Finset ι} {x : ι → E} {y : E} : ⟪∑ i ∈ s, x i, y⟫_A = ∑ i ∈ s, ⟪x i, y⟫_A

@[simp]

theorem CStarModule.isSelfAdjoint_inner_self {A : Type u_1} {E : Type u_2} [NonUnitalRing A] [StarRing A] [AddCommGroup E] [Module ℂ A] [Module ℂ E] [PartialOrder A] [SMul Aᵐᵒᵖ E] [Norm A] [Norm E] [CStarModule A E] {x : E} : IsSelfAdjoint ⟪x, x⟫_A

noncomputable def CStarModule.norm (A : Type u_3) {E : Type u_4} [Norm A] [Inner A E] : Norm E

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‖ }

theorem CStarModule.norm_sq_eq {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] {x : E} : ‖x‖ ^ 2 = ‖⟪x, x⟫_A‖

theorem CStarModule.norm_nonneg {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] {x : E} : 0 ≤ ‖x‖

theorem CStarModule.norm_pos {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] {x : E} (hx : x ≠ 0) : 0 < ‖x‖

theorem CStarModule.norm_zero {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [StarModule ℂ A] : ‖0‖ = 0

theorem CStarModule.norm_zero_iff {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [StarModule ℂ A] (x : E) : ‖x‖ = 0 ↔ x = 0

theorem CStarModule.inner_mul_inner_swap_le {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] {x : E} {y : E} : ⟪y, x⟫_A * ⟪x, y⟫_A ≤ ‖x‖ ^ 2 • ⟪y, y⟫_A

The C⋆-algebra-valued Cauchy-Schwarz inequality for Hilbert C⋆-modules.

theorem CStarModule.norm_inner_le {A : Type u_1} (E : Type u_2) [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] {x : E} {y : E} : ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖

The Cauchy-Schwarz inequality for Hilbert C⋆-modules.

theorem CStarModule.norm_triangle {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] (x : E) (y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

theorem CStarModule.normedSpaceCore {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] : NormedSpace.Core ℂ E

This allows us to get NormedAddCommGroup and NormedSpace instances on E via NormedAddCommGroup.ofCore and NormedSpace.ofCore.

@[reducible, inline]

abbrev CStarModule.normedAddCommGroup {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] : NormedAddCommGroup E

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 ⋯

theorem CStarModule.norm_eq_csSup {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [PartialOrder A] [AddCommGroup E] [NormedSpace ℂ A] [Module ℂ E] [SMul Aᵐᵒᵖ E] [Norm E] [CStarModule A E] [CStarRing A] [StarOrderedRing A] [StarModule ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] (v : E) : ‖v‖ = sSup {x : ℝ | ∃ (w : E) (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

noncomputable def CStarModule.innerSL {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [PartialOrder A] [StarOrderedRing A] [NormedSpace ℂ A] [SMul Aᵐᵒᵖ E] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [StarModule ℂ A] [CStarModule A E] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] : E →L⋆[ℂ] E →L[ℂ] A

The function ⟨x, y⟩ ↦ ⟪x, y⟫ bundled as a continuous sesquilinear map.

Equations

• CStarModule.innerSL = CStarModule.innerₛₗ.mkContinuous₂ 1 ⋯

theorem CStarModule.innerSL_apply {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [PartialOrder A] [StarOrderedRing A] [NormedSpace ℂ A] [SMul Aᵐᵒᵖ E] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [StarModule ℂ A] [CStarModule A E] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {x : E} {y : E} : (CStarModule.innerSL x) y = ⟪x, y⟫_A

theorem CStarModule.continuous_inner {A : Type u_1} {E : Type u_2} [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [PartialOrder A] [StarOrderedRing A] [NormedSpace ℂ A] [SMul Aᵐᵒᵖ E] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [StarModule ℂ A] [CStarModule A E] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] : Continuous fun (x : E × E) => ⟪x.1, x.2⟫_A