Documentation

Mathlib.Analysis.CStarAlgebra.Module

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 "inner product" that takes values in A. This inner product satisfies the Cauchy-Schwarz inequality, and induces a norm that makes E a normed vector space.

Main declarations #

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.

References #

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 : EEA
  • 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
Instances
    @[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
    Instances For
      @[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

      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
        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, is, y i⟫_A = is, 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} :
        is, x i, y⟫_A = is, 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_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] :

        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
        Instances For
          theorem CStarModule.inner_self_eq_norm_sq {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, x⟫_A = x ^ 2
          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) :
          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.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.

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

          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}

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

          Equations
          • CStarModule.innerSL = CStarModule.innerₛₗ.mkContinuous₂ 1
          Instances For
            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