Type synonym for types with a CStarModule structure

It is often the case that we want to construct a CStarModule instance on a type that is already endowed with a norm, but this norm is not the one associated to its CStarModule structure. For this reason, we create a type synonym WithCStarModule which is endowed with the requisite CStarModule instance. We also introduce the scoped notation C⋆ᵐᵒᵈ for this type synonym.

The common use cases are, when A is a C⋆-algebra:

• E × F where E and F are CStarModules over A
• Π i, E i where E i is a CStarModule over A and i : ι with ι a Fintype

In this way, the set up is very similar to the WithLp type synonym, although there is no way to reuse WithLp because the norms do not coincide in general.

The WithCStarModule synonym is of vital importance, especially because the CStarModule class marks A as an outParam. Indeed, we want to infer A from the type of E, but, as with modules, a type E can be a CStarModule over different C⋆-algebras. For example, note that if A is a C⋆-algebra, then so is A × A, and therefore we may consider both A and A × A as CStarModules over themselves, respectively. However, we may also consider A × A as a CStarModule over A. However, by utilizing the type synonym, these actually correspond to different types, namely:

• A as a CStarModule over A corresponds to A
• A × A as a CStarModule over A × A corresponds to A × A
• A × A as a CStarModule over A corresponds to C⋆ᵐᵒᵈ (A × A)

Main definitions

• WithCStarModule E: a copy of E to be equipped with a CStarModule A structure. Note that A is an outParam in the class CStarModule, so it can be inferred from the type of E.
• WithCStarModule.equiv E: the canonical equivalence between WithCStarModule E and E.
• WithCStarModule.linearEquiv ℂ A E: the canonical ℂ-module isomorphism between WithCStarModule E and E.

Implementation notes

The pattern here is the same one as is used by Lex for order structures; it avoids having a separate synonym for each type, and allows all the structure-copying code to be shared.

def WithCStarModule (E : Type u_1) : Type u_1

A type synonym for endowing a given type with a CStarModule structure. This has the scoped notation C⋆ᵐᵒᵈ.

Note: because the C⋆-algebra A over which E is a CStarModule is listed as an outParam in that class, we don't pass it as an unused argument to WithCStarModule, unlike the p parameter in WithLp, which can vary.

Equations

• WithCStarModule E = E

def WithCStarModule.«termC⋆ᵐᵒᵈ» : Lean.ParserDescr

A type synonym for endowing a given type with a CStarModule structure. This has the scoped notation C⋆ᵐᵒᵈ.

Note: because the C⋆-algebra A over which E is a CStarModule is listed as an outParam in that class, we don't pass it as an unused argument to WithCStarModule, unlike the p parameter in WithLp, which can vary.

Equations

• WithCStarModule.«termC⋆ᵐᵒᵈ» = Lean.ParserDescr.node `WithCStarModule.termC⋆ᵐᵒᵈ 1024 (Lean.ParserDescr.symbol "C⋆ᵐᵒᵈ")

def WithCStarModule.equiv (E : Type u_3) : WithCStarModule E ≃ E

The canonical equivalence between WithCStarModule E and E. This should always be used to convert back and forth between the representations.

Equations

• WithCStarModule.equiv E = Equiv.refl (WithCStarModule E)

instance WithCStarModule.instNontrivial (E : Type u_3) [Nontrivial E] : Nontrivial (WithCStarModule E)

Equations

• ⋯ = inst

instance WithCStarModule.instInhabited (E : Type u_3) [Inhabited E] : Inhabited (WithCStarModule E)

Equations

• WithCStarModule.instInhabited E = inst

instance WithCStarModule.instNonempty (E : Type u_3) [Nonempty E] : Nonempty (WithCStarModule E)

Equations

• ⋯ = inst

instance WithCStarModule.instUnique (E : Type u_3) [Unique E] : Unique (WithCStarModule E)

Equations

• WithCStarModule.instUnique E = inst

WithCStarModule E inherits various module-adjacent structures from E.

instance WithCStarModule.instAddCommGroup (E : Type u_3) [AddCommGroup E] : AddCommGroup (WithCStarModule E)

Equations

• WithCStarModule.instAddCommGroup E = inst

instance WithCStarModule.instSMul (E : Type u_3) {R : Type u_4} [SMul R E] : SMul R (WithCStarModule E)

Equations

• WithCStarModule.instSMul E = inst

instance WithCStarModule.instModule (E : Type u_3) {R : Type u_4} [Semiring R] [AddCommGroup E] [Module R E] : Module R (WithCStarModule E)

Equations

• WithCStarModule.instModule E = inst

instance WithCStarModule.instIsScalarTower (R : Type u_1) (R' : Type u_2) (E : Type u_3) [SMul R R'] [SMul R E] [SMul R' E] [IsScalarTower R R' E] : IsScalarTower R R' (WithCStarModule E)

Equations

• ⋯ = inst

instance WithCStarModule.instSMulCommClass (R : Type u_1) (R' : Type u_2) (E : Type u_3) [SMul R E] [SMul R' E] [SMulCommClass R R' E] : SMulCommClass R R' (WithCStarModule E)

Equations

• ⋯ = inst

instance WithCStarModule.instModuleFinite (R : Type u_1) (E : Type u_3) [Semiring R] [AddCommGroup E] [Module R E] [Module.Finite R E] : Module.Finite R (WithCStarModule E)

Equations

• ⋯ = inst

WithCStarModule.equiv preserves the module structure.

@[simp]

theorem WithCStarModule.equiv_zero {E : Type u_3} [AddCommGroup E] : (WithCStarModule.equiv E) 0 = 0

@[simp]

theorem WithCStarModule.equiv_symm_zero {E : Type u_3} [AddCommGroup E] : (WithCStarModule.equiv E).symm 0 = 0

@[simp]

theorem WithCStarModule.equiv_add {E : Type u_3} (x : WithCStarModule E) (y : WithCStarModule E) [AddCommGroup E] : (WithCStarModule.equiv E) (x + y) = (WithCStarModule.equiv E) x + (WithCStarModule.equiv E) y

@[simp]

theorem WithCStarModule.equiv_symm_add {E : Type u_3} (x' : E) (y' : E) [AddCommGroup E] : (WithCStarModule.equiv E).symm (x' + y') = (WithCStarModule.equiv E).symm x' + (WithCStarModule.equiv E).symm y'

@[simp]

theorem WithCStarModule.equiv_sub {E : Type u_3} (x : WithCStarModule E) (y : WithCStarModule E) [AddCommGroup E] : (WithCStarModule.equiv E) (x - y) = (WithCStarModule.equiv E) x - (WithCStarModule.equiv E) y

@[simp]

theorem WithCStarModule.equiv_symm_sub {E : Type u_3} (x' : E) (y' : E) [AddCommGroup E] : (WithCStarModule.equiv E).symm (x' - y') = (WithCStarModule.equiv E).symm x' - (WithCStarModule.equiv E).symm y'

@[simp]

theorem WithCStarModule.equiv_neg {E : Type u_3} (x : WithCStarModule E) [AddCommGroup E] : (WithCStarModule.equiv E) (-x) = -(WithCStarModule.equiv E) x

@[simp]

theorem WithCStarModule.equiv_symm_neg {E : Type u_3} (x' : E) [AddCommGroup E] : (WithCStarModule.equiv E).symm (-x') = -(WithCStarModule.equiv E).symm x'

@[simp]

theorem WithCStarModule.equiv_smul {R : Type u_1} {E : Type u_3} [SMul R E] (c : R) (x : WithCStarModule E) : (WithCStarModule.equiv E) (c • x) = c • (WithCStarModule.equiv E) x

@[simp]

theorem WithCStarModule.equiv_symm_smul {R : Type u_1} {E : Type u_3} [SMul R E] (c : R) (x' : E) : (WithCStarModule.equiv E).symm (c • x') = c • (WithCStarModule.equiv E).symm x'

@[simp]

theorem WithCStarModule.linearEquiv_apply (R : Type u_1) (E : Type u_3) [Semiring R] [AddCommGroup E] [Module R E] : ⇑(WithCStarModule.linearEquiv R E) = ⇑(WithCStarModule.equiv E)

@[simp]

theorem WithCStarModule.linearEquiv_symm_apply (R : Type u_1) (E : Type u_3) [Semiring R] [AddCommGroup E] [Module R E] : ⇑(WithCStarModule.linearEquiv R E).symm = ⇑(WithCStarModule.equiv E).symm

def WithCStarModule.linearEquiv (R : Type u_1) (E : Type u_3) [Semiring R] [AddCommGroup E] [Module R E] : WithCStarModule E ≃ₗ[R] E

WithCStarModule.equiv as a linear equivalence.

Equations

• WithCStarModule.linearEquiv R E = { toFun := ⇑(WithCStarModule.equiv E), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(WithCStarModule.equiv E).symm, left_inv := ⋯, right_inv := ⋯ }

WithCStarModule E inherits the uniformity and bornology from E.

instance WithCStarModule.instUniformSpace {E : Type u_3} [u : UniformSpace E] : UniformSpace (WithCStarModule E)

Equations

• WithCStarModule.instUniformSpace = UniformSpace.comap (⇑(WithCStarModule.equiv E)) u

instance WithCStarModule.instBornology {E : Type u_3} [Bornology E] : Bornology (WithCStarModule E)

Equations

• WithCStarModule.instBornology = Bornology.induced ⇑(WithCStarModule.equiv E)

def WithCStarModule.uniformEquiv {E : Type u_3} [UniformSpace E] : WithCStarModule E ≃ᵤ E

WithCStarModule.equiv as a uniform equivalence between C⋆ᵐᵒᵈ E and E.

Equations

• WithCStarModule.uniformEquiv = (WithCStarModule.equiv E).toUniformEquivOfUniformInducing ⋯

instance WithCStarModule.instCompleteSpace {E : Type u_3} [UniformSpace E] [CompleteSpace E] : CompleteSpace (WithCStarModule E)

Equations

• ⋯ = ⋯

Prod

Register simplification lemmas for the applications of WithCStarModule (E × F) elements, as the usual lemmas for Prod will not trigger.

@[simp]

theorem WithCStarModule.zero_fst {E : Type u_2} {F : Type u_3} [AddCommGroup E] [AddCommGroup F] : 0.1 = 0

@[simp]

theorem WithCStarModule.zero_snd {E : Type u_2} {F : Type u_3} [AddCommGroup E] [AddCommGroup F] : 0.2 = 0

@[simp]

theorem WithCStarModule.add_fst {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) (y : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (x + y).1 = x.1 + y.1

@[simp]

theorem WithCStarModule.add_snd {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) (y : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (x + y).2 = x.2 + y.2

@[simp]

theorem WithCStarModule.sub_fst {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) (y : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (x - y).1 = x.1 - y.1

@[simp]

theorem WithCStarModule.sub_snd {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) (y : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (x - y).2 = x.2 - y.2

@[simp]

theorem WithCStarModule.neg_fst {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (-x).1 = -x.1

@[simp]

theorem WithCStarModule.neg_snd {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) [AddCommGroup E] [AddCommGroup F] : (-x).2 = -x.2

@[simp]

theorem WithCStarModule.smul_fst {R : Type u_1} {E : Type u_2} {F : Type u_3} [SMul R E] [SMul R F] (x : WithCStarModule (E × F)) (c : R) : (c • x).1 = c • x.1

@[simp]

theorem WithCStarModule.smul_snd {R : Type u_1} {E : Type u_2} {F : Type u_3} [SMul R E] [SMul R F] (x : WithCStarModule (E × F)) (c : R) : (c • x).2 = c • x.2

Note that the unapplied versions of these lemmas are deliberately omitted, as they break the use of the type synonym.

@[simp]

theorem WithCStarModule.equiv_fst {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) : ((WithCStarModule.equiv (E × F)) x).1 = x.1

@[simp]

theorem WithCStarModule.equiv_snd {E : Type u_2} {F : Type u_3} (x : WithCStarModule (E × F)) : ((WithCStarModule.equiv (E × F)) x).2 = x.2

@[simp]

theorem WithCStarModule.equiv_symm_fst {E : Type u_2} {F : Type u_3} (x : E × F) : ((WithCStarModule.equiv (E × F)).symm x).1 = x.1

@[simp]

theorem WithCStarModule.equiv_symm_snd {E : Type u_2} {F : Type u_3} (x : E × F) : ((WithCStarModule.equiv (E × F)).symm x).2 = x.2

Pi

Register simplification lemmas for the applications of WithCStarModule (Π i, E i) elements, as the usual lemmas for Pi will not trigger.

We also provide a CoeFun instance for WithCStarModule (Π i, E i).

instance WithCStarModule.instCoeFunForall {ι : Type u_1} (E : ι → Type u_2) : CoeFun (WithCStarModule ((i : ι) → E i)) fun (x : WithCStarModule ((i : ι) → E i)) => (i : ι) → E i

Equations

• WithCStarModule.instCoeFunForall E = { coe := ⇑(WithCStarModule.equiv ((i : ι) → E i)) }

theorem WithCStarModule.ext_iff {ι : Type u_1} {E : ι → Type u_2} {x : WithCStarModule ((i : ι) → E i)} {y : WithCStarModule ((i : ι) → E i)} : x = y ↔ ∀ (i : ι), x i = y i

theorem WithCStarModule.ext {ι : Type u_1} {E : ι → Type u_2} {x : WithCStarModule ((i : ι) → E i)} {y : WithCStarModule ((i : ι) → E i)} (h : ∀ (i : ι), x i = y i) : x = y

@[simp]

theorem WithCStarModule.zero_apply {ι : Type u_2} {E : ι → Type u_3} (i : ι) [(i : ι) → AddCommGroup (E i)] : 0 i = 0

@[simp]

theorem WithCStarModule.add_apply {ι : Type u_2} {E : ι → Type u_3} (x : WithCStarModule ((i : ι) → E i)) (y : WithCStarModule ((i : ι) → E i)) (i : ι) [(i : ι) → AddCommGroup (E i)] : (x + y) i = x i + y i

@[simp]

theorem WithCStarModule.sub_apply {ι : Type u_2} {E : ι → Type u_3} (x : WithCStarModule ((i : ι) → E i)) (y : WithCStarModule ((i : ι) → E i)) (i : ι) [(i : ι) → AddCommGroup (E i)] : (x - y) i = x i - y i

@[simp]

theorem WithCStarModule.neg_apply {ι : Type u_2} {E : ι → Type u_3} (x : WithCStarModule ((i : ι) → E i)) (i : ι) [(i : ι) → AddCommGroup (E i)] : (-x) i = -x i

@[simp]

theorem WithCStarModule.smul_apply {R : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → SMul R (E i)] (c : R) (x : WithCStarModule ((i : ι) → E i)) (i : ι) : (c • x) i = c • x i

Note that the unapplied versions of these lemmas are deliberately omitted, as they break the use of the type synonym.

@[simp]

theorem WithCStarModule.equiv_pi_apply {ι : Type u_2} {E : ι → Type u_3} (x : WithCStarModule ((i : ι) → E i)) (i : ι) : (WithCStarModule.equiv ((i : ι) → E i)) x i = x i

@[simp]

theorem WithCStarModule.equiv_symm_pi_apply {ι : Type u_2} {E : ι → Type u_3} (x : (i : ι) → E i) (i : ι) : (WithCStarModule.equiv ((i : ι) → E i)).symm x i = x i