Documentation

Mathlib.Analysis.CStarAlgebra.Module.Defs

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 #

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 #

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.

Instances
    @[simp]
    theorem CStarModule.inner_add_right {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] {x y z : E}, inner x (y + z) = inner x y + inner x z
    theorem CStarModule.inner_self_nonneg {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] {x : E}, 0 inner x x
    theorem CStarModule.inner_self {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] {x : E}, inner x x = 0 x = 0
    @[simp]
    theorem CStarModule.inner_op_smul_right {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] {a : A} {x y : E}, inner x (MulOpposite.op a y) = inner x y * a
    @[simp]
    theorem CStarModule.inner_smul_right_complex {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] {z : } {x y : E}, inner x (z y) = z inner x y
    @[simp]
    theorem CStarModule.star_inner {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] (x y : E), star (inner x y) = inner y x
    theorem CStarModule.norm_eq_sqrt_norm_inner_self {A : outParam (Type u_1)} {E : Type u_2} :
    ∀ {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module A} {inst_3 : AddCommGroup E} {inst_4 : Module E} {inst_5 : PartialOrder A} {inst_6 : SMul Aᵐᵒᵖ E} {inst_7 : Norm A} {inst_8 : Norm E} [self : CStarModule A E] (x : E), x = inner x x
    @[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} :
      inner (x + y) z = inner x z + inner y z
      @[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} :
      @[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} :
      inner (z x) y = star z inner x y
      @[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} :
      inner (z x) y = z inner x y
      @[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} :
      inner x (z y) = z inner x y

      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
        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 = inner x y
        @[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} :
        inner x 0 = 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} :
        inner 0 x = 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} :
        inner x (-y) = -inner x y
        @[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} :
        inner (-x) y = -inner x y
        @[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} :
        inner x (y - z) = inner x y - inner x z
        @[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} :
        inner (x - y) z = inner x z - inner y z
        @[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} :
        inner x (∑ is, y i) = is, inner x (y i)
        @[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} :
        inner (∑ is, x i) y = is, inner (x i) y
        @[simp]
        noncomputable def CStarModule.norm (A : Type u_3) {E : Type u_4} [Norm A] [Inner 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.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) :

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

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

          @[reducible, inline]

          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
          Instances For
            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), inner w v = 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 = inner x y