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 A E: a copy of E to be equipped with a CStarModule A structure.
• WithCStarModule.equiv A E: the canonical equivalence between WithCStarModule A E and E.
• WithCStarModule.linearEquiv ℂ A E: the canonical ℂ-module isomorphism between WithCStarModule A 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 (A : Type u_1) (E : Type u_2) : Type u_2

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

def WithCStarModule.«termC⋆ᵐᵒᵈ(_,_)» : Lean.ParserDescr

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

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

The canonical equivalence between C⋆ᵐᵒᵈ(A, E) and E. This should always be used to convert back and forth between the representations.

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

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

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

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

C⋆ᵐᵒᵈ(A, E) inherits various module-adjacent structures from E.

instance WithCStarModule.instZero (A : Type u_3) (E : Type u_4) [Zero E] : Zero (WithCStarModule A E)

instance WithCStarModule.instAdd (A : Type u_3) (E : Type u_4) [Add E] : Add (WithCStarModule A E)

instance WithCStarModule.instSub (A : Type u_3) (E : Type u_4) [Sub E] : Sub (WithCStarModule A E)

instance WithCStarModule.instNeg (A : Type u_3) (E : Type u_4) [Neg E] : Neg (WithCStarModule A E)

instance WithCStarModule.instAddMonoid (A : Type u_3) (E : Type u_4) [AddMonoid E] : AddMonoid (WithCStarModule A E)

instance WithCStarModule.instSubNegMonoid (A : Type u_3) (E : Type u_4) [SubNegMonoid E] : SubNegMonoid (WithCStarModule A E)

instance WithCStarModule.instSubNegZeroMonoid (A : Type u_3) (E : Type u_4) [SubNegZeroMonoid E] : SubNegZeroMonoid (WithCStarModule A E)

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

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

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

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

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

WithCStarModule.equiv preserves the module structure.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def WithCStarModule.addEquiv (A : Type u_3) (E : Type u_4) [AddCommGroup E] : WithCStarModule A E ≃+ E

WithCStarModule.equiv as an additive equivalence.

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

WithCStarModule.equiv as a linear equivalence.

@[simp]

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

@[simp]

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

theorem WithCStarModule.map_top_submodule (A : Type u_3) (E : Type u_4) {R : Type u_5} [Semiring R] [AddCommGroup E] [Module R E] : Submodule.map (linearEquiv R A E).symm ⊤ = ⊤

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

C⋆ᵐᵒᵈ(A, E) inherits the uniformity and bornology from E.

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

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

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

WithCStarModule.equiv as a uniform equivalence between C⋆ᵐᵒᵈ(A, E) and E.

def WithCStarModule.equivL (R : Type u_1) {A : Type u_3} {E : Type u_4} [Semiring R] [AddCommGroup E] [UniformSpace E] [Module R E] : WithCStarModule A E ≃L[R] E

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

@[simp]

theorem WithCStarModule.equivL_apply (R : Type u_1) {A : Type u_3} {E : Type u_4} [Semiring R] [AddCommGroup E] [UniformSpace E] [Module R E] (a : WithCStarModule A E) : (equivL R) a = (equiv A E) a

@[simp]

theorem WithCStarModule.equivL_symm_apply (R : Type u_1) {A : Type u_3} {E : Type u_4} [Semiring R] [AddCommGroup E] [UniformSpace E] [Module R E] (a : E) : (equivL R).symm a = (equiv A E).symm a

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

instance WithCStarModule.instContinuousAdd {A : Type u_3} {E : Type u_4} [AddCommGroup E] [UniformSpace E] [ContinuousAdd E] : ContinuousAdd (WithCStarModule A E)

instance WithCStarModule.instIsUniformAddGroup {A : Type u_3} {E : Type u_4} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] : IsUniformAddGroup (WithCStarModule A E)

instance WithCStarModule.instContinuousSMul (R : Type u_1) {A : Type u_3} {E : Type u_4} [Semiring R] [TopologicalSpace R] [AddCommGroup E] [UniformSpace E] [Module R E] [ContinuousSMul R E] : ContinuousSMul R (WithCStarModule A E)

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 {A : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] : 0.1 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WithCStarModule.smul_snd {R : Type u_1} {A : Type u_2} {E : Type u_3} {F : Type u_4} [SMul R E] [SMul R F] (x : WithCStarModule A (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 {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : WithCStarModule A (E × F)) : ((equiv A (E × F)) x).1 = x.1

@[simp]

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

@[simp]

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

@[simp]

theorem WithCStarModule.equiv_symm_snd {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : E × F) : ((equiv A (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 {A : Type u_1} {ι : Type u_2} (E : ι → Type u_3) : CoeFun (WithCStarModule A ((i : ι) → E i)) fun (x : WithCStarModule A ((i : ι) → E i)) => (i : ι) → E i

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem WithCStarModule.smul_apply {R : Type u_1} {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} [(i : ι) → SMul R (E i)] (c : R) (x : WithCStarModule A ((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 {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x : WithCStarModule A ((i : ι) → E i)) (i : ι) : (equiv A ((i : ι) → E i)) x i = x i

@[simp]

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