Documentation

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Constructions of Hilbert C⋆-modules #

In this file we define the following constructions of CStarModules where A denotes a C⋆-algebra. For some of the types listed below, the instance is declared on the type synonym WithCStarModule E (with the notation C⋆ᵐᵒᵈ E), instead of on E itself; we explain the reasoning behind each decision below.

  1. A as a CStarModule over itself.
  2. C⋆ᵐᵒᵈ (E × F) as a CStarModule over A, when E and F are themselves CStarModules over A.
  3. C⋆ᵐᵒᵈ (Π i : ι, E i) as a CStarModule over A, when each E i is a CStarModule over A and ι is a Fintype.
  4. E as a CStarModule over , when E is an InnerProductSpace over .

For E × F and Π i : ι, E i, we are required to declare the instance on a type synonym rather than on the product or pi-type itself because the existing norm on these types does not agree with the one induced by the C⋆-module structure. Moreover, the norm induced by the C⋆-module structure doesn't agree with any other natural norm on these types (e.g., WithLp 2 (E × F) unless A := ℂ), so we need a new synonym.

On A (a C⋆-algebra) and E (an inner product space), we declare the instances on the types themselves to ease the use of the C⋆-module structure. This does have the potential to cause inconvenience (as sometimes Lean will see terms of type A and apply lemmas pertaining to C⋆-modules to those terms, when the lemmas were actually intended for terms of some other C⋆-module in context, say F, in which case the arguments must be provided explicitly; see for instance the application of CStarModule.norm_eq_sqrt_norm_inner_self in the proof of WithCStarModule.max_le_prod_norm below). However, we believe that this, hopefully rare, inconvenience is outweighed by avoiding translating between type synonyms where possible.

For more details on the importance of the WithCStarModule type synonym, see the module documentation for Analysis.CStarAlgebra.Module.Synonym.

Implementation notes #

When A := ℂ and E := ℂ, then is both a C⋆-algebra (so it inherits a CStarModule instance via (1) above) and an inner product space (so it inherits a CStarModule instance via (4) above). We provide a sanity check ensuring that these two instances are definitionally equal. We also ensure that the Inner ℂ ℂ instance from InnerProductSpace is definitionally equal to the one inherited from the CStarModule instances.

Note that C⋆ᵐᵒᵈ E is already equipped with a bornology and uniformity whenever E is (namely, the pullback of the respective structures through WithCStarModule.equiv), so in each of the above cases, it is necessary to temporarily instantiate C⋆ᵐᵒᵈ E with CStarModule.normedAddCommGroup, show the resulting type is bilipschitz equivalent to E via WithCStarModule.equiv (in the first and last case, this map is actually trivially an isometry), and then replace the uniformity and bornology with the correct ones.

A C⋆-algebra as a C⋆-module over itself #

Reinterpret a C⋆-algebra A as a CStarModule over itself.

Equations
  • WithCStarModule.instCStarModule = CStarModule.mk

Products of C⋆-modules #

Equations
Equations
  • WithCStarModule.instCStarModuleProd = CStarModule.mk

Pi-types of C⋆-modules #

noncomputable instance WithCStarModule.instNormForall {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] :
Norm (WithCStarModule ((i : ι) → E i))
Equations
theorem WithCStarModule.pi_norm {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] (x : WithCStarModule ((i : ι) → E i)) :
x = i : ι, inner (x i) (x i)
theorem WithCStarModule.pi_norm_sq {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] (x : WithCStarModule ((i : ι) → E i)) :
x ^ 2 = i : ι, inner (x i) (x i)
theorem WithCStarModule.pi_norm_le_sum_norm {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] (x : WithCStarModule ((i : ι) → E i)) :
x i : ι, x i
noncomputable instance WithCStarModule.instCStarModuleForall {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] :
CStarModule A (WithCStarModule ((i : ι) → E i))
Equations
  • WithCStarModule.instCStarModuleForall = CStarModule.mk
theorem WithCStarModule.pi_inner {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] (x : WithCStarModule ((i : ι) → E i)) (y : WithCStarModule ((i : ι) → E i)) :
inner x y = i : ι, inner (x i) (y i)
@[simp]
theorem WithCStarModule.inner_single_left {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [DecidableEq ι] (x : WithCStarModule ((i : ι) → E i)) {i : ι} (y : E i) :
inner ((WithCStarModule.equiv ((j : ι) → E j)).symm (Pi.single i y)) x = inner y (x i)
@[simp]
theorem WithCStarModule.inner_single_right {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [DecidableEq ι] (x : WithCStarModule ((i : ι) → E i)) {i : ι} (y : E i) :
inner x ((WithCStarModule.equiv ((i : ι) → E i)).symm (Pi.single i y)) = inner (x i) y
@[simp]
theorem WithCStarModule.norm_single {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [CStarRing A] [SMulCommClass A A] [IsScalarTower A A] [CompleteSpace A] [DecidableEq ι] (i : ι) (y : E i) :
(WithCStarModule.equiv ((j : ι) → E j)).symm (Pi.single i y) = y
theorem WithCStarModule.norm_apply_le_norm {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [CStarRing A] [SMulCommClass A A] [IsScalarTower A A] [CompleteSpace A] (x : WithCStarModule ((i : ι) → E i)) (i : ι) :
theorem WithCStarModule.norm_equiv_le_norm_pi {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [CStarRing A] [SMulCommClass A A] [IsScalarTower A A] [CompleteSpace A] (x : WithCStarModule ((i : ι) → E i)) :
(WithCStarModule.equiv ((i : ι) → E i)) x x
noncomputable instance WithCStarModule.instNormedAddCommGroupForall {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [CStarRing A] [SMulCommClass A A] [IsScalarTower A A] [CompleteSpace A] :
NormedAddCommGroup (WithCStarModule ((i : ι) → E i))
Equations
instance WithCStarModule.instNormedSpaceComplexForall {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace A] [PartialOrder A] {ι : Type u_2} {E : ιType u_3} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module (E i)] [(i : ι) → SMul Aᵐᵒᵖ (E i)] [(i : ι) → CStarModule A (E i)] [StarModule A] [StarOrderedRing A] [CStarRing A] [SMulCommClass A A] [IsScalarTower A A] [CompleteSpace A] :
NormedSpace (WithCStarModule ((i : ι) → E i))
Equations

Inner product spaces as C⋆-modules #

Reinterpret an inner product space E over as a CStarModule over .

Note: this instance requires SMul ℂᵐᵒᵖ E and IsCentralScalar ℂ E instances to exist on E, which is unlikely to occur in practice. However, in practice one could either add those instances to the type E in question, or else supply them to this instance manually, which is reason behind the naming of these two instance arguments.

Equations
  • WithCStarModule.instCStarModuleComplex = CStarModule.mk