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⋆ᵐᵒᵈ(A, E × F) as a CStarModule over A, when E and F are themselves CStarModules over A.
3. C⋆ᵐᵒᵈ (A, Π 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⋆ᵐᵒᵈ(A, 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⋆ᵐᵒᵈ(A, 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

instance WithCStarModule.instCStarModule {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : CStarModule A A

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

Equations

• One or more equations did not get rendered due to their size.

theorem WithCStarModule.inner_def {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (x y : A) : inner A x y = y * star x

Products of C⋆-modules

noncomputable instance WithCStarModule.instNormProd {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] : Norm (WithCStarModule A (E × F))

Equations

• WithCStarModule.instNormProd = { norm := fun (x : WithCStarModule A (E × F)) => √‖inner A x.1 x.1 + inner A x.2 x.2‖ }

theorem WithCStarModule.prod_norm {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] (x : WithCStarModule A (E × F)) : ‖x‖ = √‖inner A x.1 x.1 + inner A x.2 x.2‖

theorem WithCStarModule.prod_norm_sq {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] (x : WithCStarModule A (E × F)) : ‖x‖ ^ 2 = ‖inner A x.1 x.1 + inner A x.2 x.2‖

theorem WithCStarModule.prod_norm_le_norm_add {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] (x : WithCStarModule A (E × F)) : ‖x‖ ≤ ‖x.1‖ + ‖x.2‖

noncomputable instance WithCStarModule.instCStarModuleProd {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] : CStarModule A (WithCStarModule A (E × F))

Equations

• One or more equations did not get rendered due to their size.

theorem WithCStarModule.prod_inner {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] (x y : WithCStarModule A (E × F)) : inner A x y = inner A x.1 y.1 + inner A x.2 y.2

theorem WithCStarModule.max_le_prod_norm {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] (x : WithCStarModule A (E × F)) : max ‖x.1‖ ‖x.2‖ ≤ ‖x‖

theorem WithCStarModule.norm_equiv_le_norm_prod {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] (x : WithCStarModule A (E × F)) : ‖(equiv A (E × F)) x‖ ≤ ‖x‖

noncomputable def WithCStarModule.normedAddCommGroupProdAux {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] : NormedAddCommGroup (WithCStarModule A (E × F))

A normed additive commutative group structure on C⋆ᵐᵒᵈ(A, E × F) with the wrong topology, uniformity and bornology. This is only used to build the instance with the correct forgetful inheritance data.

Equations

• WithCStarModule.normedAddCommGroupProdAux = NormedAddCommGroup.ofCore ⋯

noncomputable instance WithCStarModule.instNormedAddCommGroupProd {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] : NormedAddCommGroup (WithCStarModule A (E × F))

Equations

• WithCStarModule.instNormedAddCommGroupProd = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯

noncomputable instance WithCStarModule.instNormedSpaceComplexProd {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [Module ℂ E] [SMul A E] [NormedAddCommGroup F] [Module ℂ F] [SMul A F] [CStarModule A E] [CStarModule A F] [StarOrderedRing A] : NormedSpace ℂ (WithCStarModule A (E × F))

Equations

• WithCStarModule.instNormedSpaceComplexProd = NormedSpace.ofCore ⋯

Pi-types of C⋆-modules

noncomputable instance WithCStarModule.instNormForall {A : Type u_1} [NonUnitalCStarAlgebra 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 A ((i : ι) → E i))

Equations

• WithCStarModule.instNormForall = { norm := fun (x : WithCStarModule A ((i : ι) → E i)) => √‖∑ i : ι, inner A (x i) (x i)‖ }

theorem WithCStarModule.pi_norm {A : Type u_1} [NonUnitalCStarAlgebra 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 A ((i : ι) → E i)) : ‖x‖ = √‖∑ i : ι, inner A (x i) (x i)‖

theorem WithCStarModule.pi_norm_sq {A : Type u_1} [NonUnitalCStarAlgebra 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 A ((i : ι) → E i)) : ‖x‖ ^ 2 = ‖∑ i : ι, inner A (x i) (x i)‖

theorem WithCStarModule.pi_norm_le_sum_norm {A : Type u_1} [NonUnitalCStarAlgebra 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 A ((i : ι) → E i)) : ‖x‖ ≤ ∑ i : ι, ‖x i‖

noncomputable instance WithCStarModule.instCStarModuleForall {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] : CStarModule A (WithCStarModule A ((i : ι) → E i))

Equations

• One or more equations did not get rendered due to their size.

theorem WithCStarModule.pi_inner {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] (x y : WithCStarModule A ((i : ι) → E i)) : inner A x y = ∑ i : ι, inner A (x i) (y i)

@[simp]

theorem WithCStarModule.inner_single_left {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] [DecidableEq ι] (x : WithCStarModule A ((i : ι) → E i)) {i : ι} (y : E i) : inner A ((equiv A ((j : ι) → E j)).symm (Pi.single i y)) x = inner A y (x i)

@[simp]

theorem WithCStarModule.inner_single_right {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] [DecidableEq ι] (x : WithCStarModule A ((i : ι) → E i)) {i : ι} (y : E i) : inner A x ((equiv A ((i : ι) → E i)).symm (Pi.single i y)) = inner A (x i) y

@[simp]

theorem WithCStarModule.norm_single {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] [DecidableEq ι] (i : ι) (y : E i) : ‖(equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

theorem WithCStarModule.norm_apply_le_norm {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] (x : WithCStarModule A ((i : ι) → E i)) (i : ι) : ‖x i‖ ≤ ‖x‖

theorem WithCStarModule.norm_equiv_le_norm_pi {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] (x : WithCStarModule A ((i : ι) → E i)) : ‖(equiv A ((i : ι) → E i)) x‖ ≤ ‖x‖

noncomputable def WithCStarModule.normedAddCommGroupPiAux {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] : NormedAddCommGroup (WithCStarModule A ((i : ι) → E i))

A normed additive commutative group structure on C⋆ᵐᵒᵈ(A, Π i, E i) with the wrong topology, uniformity and bornology. This is only used to build the instance with the correct forgetful inheritance data.

Equations

• WithCStarModule.normedAddCommGroupPiAux = NormedAddCommGroup.ofCore ⋯

noncomputable instance WithCStarModule.instNormedAddCommGroupForall {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] : NormedAddCommGroup (WithCStarModule A ((i : ι) → E i))

Equations

• WithCStarModule.instNormedAddCommGroupForall = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯

noncomputable instance WithCStarModule.instNormedSpaceComplexForall {A : Type u_1} [NonUnitalCStarAlgebra 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)] [StarOrderedRing A] : NormedSpace ℂ (WithCStarModule A ((i : ι) → E i))

Equations

• WithCStarModule.instNormedSpaceComplexForall = NormedSpace.ofCore ⋯

Inner product spaces as C⋆-modules

instance WithCStarModule.instCStarModuleComplex {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : CStarModule ℂ E

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

• One or more equations did not get rendered due to their size.