Multiplier Algebra of a C⋆-algebra

Define the multiplier algebra of a C⋆-algebra as the algebra (over 𝕜) of double centralizers, for which we provide the localized notation 𝓜(𝕜, A). A double centralizer is a pair of continuous linear maps L R : A →L[𝕜] A satisfying the intertwining condition R x * y = x * L y.

There is a natural embedding A → 𝓜(𝕜, A) which sends a : A to the continuous linear maps L R : A →L[𝕜] A given by left and right multiplication by a, and we provide this map as a coercion.

The multiplier algebra corresponds to a non-commutative Stone–Čech compactification in the sense that when the algebra A is commutative, it can be identified with C₀(X, ℂ) for some locally compact Hausdorff space X, and in that case 𝓜(𝕜, A) can be identified with C(β X, ℂ).

Implementation notes

We make the hypotheses on 𝕜 as weak as possible so that, in particular, this construction works for both 𝕜 = ℝ and 𝕜 = ℂ.

The reader familiar with C⋆-algebra theory may recognize that one only needs L and R to be functions instead of continuous linear maps, at least when A is a C⋆-algebra. Our intention is simply to eventually provide a constructor for this situation.

We pull back the NormedAlgebra structure (and everything contained therein) through the ring (even algebra) homomorphism DoubleCentralizer.toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ which sends a : 𝓜(𝕜, A) to (a.fst, MulOpposite.op a.snd). The star structure is provided separately.

References

• https://en.wikipedia.org/wiki/Multiplier_algebra

TODO

• Define a type synonym for 𝓜(𝕜, A) which is equipped with the strict uniform space structure and show it is complete
• Show that the image of A in 𝓜(𝕜, A) is an essential ideal
• Prove the universal property of 𝓜(𝕜, A)
• Construct a double centralizer from a pair of maps (not necessarily linear or continuous) L : A → A, R : A → A satisfying the centrality condition ∀ x y, R x * y = x * L y.
• Show that if A is unital, then A ≃⋆ₐ[𝕜] 𝓜(𝕜, A).

structure DoubleCentralizer (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] extends (A →L[𝕜] A) × (A →L[𝕜] A) : Type v

The type of double centralizers, also known as the multiplier algebra and denoted by 𝓜(𝕜, A), of a non-unital normed algebra.

If x : 𝓜(𝕜, A), then x.fst and x.snd are what is usually referred to as $L$ and $R$.

• fst : A →L[𝕜] A
• snd : A →L[𝕜] A
• central (x y : A) : self.toProd.2 x * y = x * self.toProd.1 y

  The centrality condition that the maps linear maps intertwine one another.

def MultiplierAlgebra.«term𝓜(_,_)» : Lean.ParserDescr

The type of double centralizers, also known as the multiplier algebra and denoted by 𝓜(𝕜, A), of a non-unital normed algebra.

If x : 𝓜(𝕜, A), then x.fst and x.snd are what is usually referred to as $L$ and $R$.

Equations

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

theorem DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) (h : a.toProd = b.toProd) : a = b

theorem DoubleCentralizer.ext_iff {𝕜 : Type u} {A : Type v} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {a b : DoubleCentralizer 𝕜 A} : a = b ↔ a.toProd = b.toProd

Algebraic structure

Because the multiplier algebra is defined as the algebra of double centralizers, there is a natural injection DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ defined by fun a ↦ (a.fst, MulOpposite.op a.snd). We use this map to pull back the ring, module and algebra structure from (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ to 𝓜(𝕜, A).

theorem DoubleCentralizer.range_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Set.range toProd = {lr : (A →L[𝕜] A) × (A →L[𝕜] A) | ∀ (x y : A), lr.2 x * y = x * lr.1 y}

instance DoubleCentralizer.instAdd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Add (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instAdd = { add := fun (a b : DoubleCentralizer 𝕜 A) => let __Prod := a.toProd + b.toProd; { toProd := __Prod, central := ⋯ } }

instance DoubleCentralizer.instZero {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Zero (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instZero = { zero := let __Prod := 0; { toProd := __Prod, central := ⋯ } }

instance DoubleCentralizer.instNeg {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Neg (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instNeg = { neg := fun (a : DoubleCentralizer 𝕜 A) => let __Prod := -a.toProd; { toProd := __Prod, central := ⋯ } }

instance DoubleCentralizer.instSub {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Sub (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instSub = { sub := fun (a b : DoubleCentralizer 𝕜 A) => let __Prod := a.toProd - b.toProd; { toProd := __Prod, central := ⋯ } }

instance DoubleCentralizer.instSMul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] : SMul S (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instSMul = { smul := fun (s : S) (a : DoubleCentralizer 𝕜 A) => let __Prod := s • a.toProd; { toProd := __Prod, central := ⋯ } }

@[simp]

theorem DoubleCentralizer.smul_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A) : (s • a).toProd = s • a.toProd

theorem DoubleCentralizer.smul_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A) : (s • a).toProd.1 = s • a.toProd.1

theorem DoubleCentralizer.smul_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A) : (s • a).toProd.2 = s • a.toProd.2

instance DoubleCentralizer.instIsScalarTower {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] {T : Type u_4} [Monoid T] [DistribMulAction T A] [SMulCommClass 𝕜 T A] [ContinuousConstSMul T A] [IsScalarTower T A A] [SMulCommClass T A A] [SMul S T] [IsScalarTower S T A] : IsScalarTower S T (DoubleCentralizer 𝕜 A)

instance DoubleCentralizer.instSMulCommClass {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] {T : Type u_4} [Monoid T] [DistribMulAction T A] [SMulCommClass 𝕜 T A] [ContinuousConstSMul T A] [IsScalarTower T A A] [SMulCommClass T A A] [SMulCommClass S T A] : SMulCommClass S T (DoubleCentralizer 𝕜 A)

instance DoubleCentralizer.instIsCentralScalar {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {R : Type u_5} [Semiring R] [Module R A] [SMulCommClass 𝕜 R A] [ContinuousConstSMul R A] [IsScalarTower R A A] [SMulCommClass R A A] [Module Rᵐᵒᵖ A] [IsCentralScalar R A] : IsCentralScalar R (DoubleCentralizer 𝕜 A)

instance DoubleCentralizer.instOne {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : One (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instOne = { one := { toProd := 1, central := ⋯ } }

instance DoubleCentralizer.instMul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Mul (DoubleCentralizer 𝕜 A)

Equations

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

instance DoubleCentralizer.instNatCast {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : NatCast (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instNatCast = { natCast := fun (n : ℕ) => { toProd := ↑n, central := ⋯ } }

instance DoubleCentralizer.instIntCast {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : IntCast (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instIntCast = { intCast := fun (n : ℤ) => { toProd := ↑n, central := ⋯ } }

instance DoubleCentralizer.instPow {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Pow (DoubleCentralizer 𝕜 A) ℕ

Equations

• DoubleCentralizer.instPow = { pow := fun (a : DoubleCentralizer 𝕜 A) (n : ℕ) => { toProd := a.toProd ^ n, central := ⋯ } }

instance DoubleCentralizer.instInhabited {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Inhabited (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instInhabited = { default := 0 }

@[simp]

theorem DoubleCentralizer.add_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a + b).toProd = a.toProd + b.toProd

@[simp]

theorem DoubleCentralizer.zero_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : toProd 0 = 0

@[simp]

theorem DoubleCentralizer.neg_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : (-a).toProd = -a.toProd

@[simp]

theorem DoubleCentralizer.sub_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a - b).toProd = a.toProd - b.toProd

@[simp]

theorem DoubleCentralizer.one_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : toProd 1 = 1

@[simp]

theorem DoubleCentralizer.natCast_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) : (↑n).toProd = ↑n

@[simp]

theorem DoubleCentralizer.intCast_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℤ) : (↑n).toProd = ↑n

@[simp]

theorem DoubleCentralizer.pow_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) (a : DoubleCentralizer 𝕜 A) : (a ^ n).toProd = a.toProd ^ n

theorem DoubleCentralizer.add_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a + b).toProd.1 = a.toProd.1 + b.toProd.1

theorem DoubleCentralizer.add_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a + b).toProd.2 = a.toProd.2 + b.toProd.2

theorem DoubleCentralizer.zero_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : (toProd 0).1 = 0

theorem DoubleCentralizer.zero_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : (toProd 0).2 = 0

theorem DoubleCentralizer.neg_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : (-a).toProd.1 = -a.toProd.1

theorem DoubleCentralizer.neg_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : (-a).toProd.2 = -a.toProd.2

theorem DoubleCentralizer.sub_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a - b).toProd.1 = a.toProd.1 - b.toProd.1

theorem DoubleCentralizer.sub_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a - b).toProd.2 = a.toProd.2 - b.toProd.2

theorem DoubleCentralizer.one_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : (toProd 1).1 = 1

theorem DoubleCentralizer.one_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : (toProd 1).2 = 1

@[simp]

theorem DoubleCentralizer.mul_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a * b).toProd.1 = a.toProd.1 * b.toProd.1

@[simp]

theorem DoubleCentralizer.mul_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : DoubleCentralizer 𝕜 A) : (a * b).toProd.2 = b.toProd.2 * a.toProd.2

theorem DoubleCentralizer.natCast_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) : (↑n).toProd.1 = ↑n

theorem DoubleCentralizer.natCast_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) : (↑n).toProd.2 = ↑n

theorem DoubleCentralizer.intCast_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℤ) : (↑n).toProd.1 = ↑n

theorem DoubleCentralizer.intCast_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℤ) : (↑n).toProd.2 = ↑n

theorem DoubleCentralizer.pow_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) (a : DoubleCentralizer 𝕜 A) : (a ^ n).toProd.1 = a.toProd.1 ^ n

theorem DoubleCentralizer.pow_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℕ) (a : DoubleCentralizer 𝕜 A) : (a ^ n).toProd.2 = a.toProd.2 ^ n

def DoubleCentralizer.toProdMulOpposite {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : DoubleCentralizer 𝕜 A → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ

The natural injection from DoubleCentralizer.toProd except the second coordinate inherits MulOpposite.op. The ring structure on 𝓜(𝕜, A) is the pullback under this map.

Equations

• a.toProdMulOpposite = (a.toProd.1, MulOpposite.op a.toProd.2)

theorem DoubleCentralizer.toProdMulOpposite_injective {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Function.Injective toProdMulOpposite

theorem DoubleCentralizer.range_toProdMulOpposite {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Set.range toProdMulOpposite = {lr : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ | ∀ (x y : A), (MulOpposite.unop lr.2) x * y = x * lr.1 y}

instance DoubleCentralizer.instRing {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Ring (DoubleCentralizer 𝕜 A)

The ring structure is inherited as the pullback under the injective map DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ

Equations

• DoubleCentralizer.instRing = Function.Injective.ring DoubleCentralizer.toProdMulOpposite ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def DoubleCentralizer.toProdHom {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : DoubleCentralizer 𝕜 A →+ (A →L[𝕜] A) × (A →L[𝕜] A)

The canonical map DoubleCentralizer.toProd as an additive group homomorphism.

Equations

• DoubleCentralizer.toProdHom = { toFun := DoubleCentralizer.toProd, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DoubleCentralizer.toProdHom_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (self : DoubleCentralizer 𝕜 A) : toProdHom self = self.toProd

def DoubleCentralizer.toProdMulOppositeHom {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : DoubleCentralizer 𝕜 A →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ

The canonical map DoubleCentralizer.toProdMulOpposite as a ring homomorphism.

Equations

• DoubleCentralizer.toProdMulOppositeHom = { toFun := DoubleCentralizer.toProdMulOpposite, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DoubleCentralizer.toProdMulOppositeHom_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a✝ : DoubleCentralizer 𝕜 A) : toProdMulOppositeHom a✝ = a✝.toProdMulOpposite

noncomputable instance DoubleCentralizer.instModule {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {S : Type u_3} [Semiring S] [Module S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] : Module S (DoubleCentralizer 𝕜 A)

The module structure is inherited as the pullback under the additive group monomorphism DoubleCentralizer.toProd : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)

Equations

• DoubleCentralizer.instModule = Function.Injective.module S DoubleCentralizer.toProdHom ⋯ ⋯

instance DoubleCentralizer.instAlgebra {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Algebra 𝕜 (DoubleCentralizer 𝕜 A)

Equations

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

@[simp]

theorem DoubleCentralizer.algebraMap_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (k : 𝕜) : ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd = (algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k

theorem DoubleCentralizer.algebraMap_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (k : 𝕜) : ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd.1 = (algebraMap 𝕜 (A →L[𝕜] A)) k

theorem DoubleCentralizer.algebraMap_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (k : 𝕜) : ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd.2 = (algebraMap 𝕜 (A →L[𝕜] A)) k

Star structure

instance DoubleCentralizer.instStar {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] : Star (DoubleCentralizer 𝕜 A)

The star operation on a : 𝓜(𝕜, A) is given by (star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star).

Equations

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

@[simp]

theorem DoubleCentralizer.star_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] (a : DoubleCentralizer 𝕜 A) (b : A) : (star a).toProd.1 b = star (a.toProd.2 (star b))

@[simp]

theorem DoubleCentralizer.star_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] (a : DoubleCentralizer 𝕜 A) (b : A) : (star a).toProd.2 b = star (a.toProd.1 (star b))

instance DoubleCentralizer.instStarAddMonoid {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] : StarAddMonoid (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instStarAddMonoid = { toStar := DoubleCentralizer.instStar, star_involutive := ⋯, star_add := ⋯ }

instance DoubleCentralizer.instStarRing {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] : StarRing (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instStarRing = { toInvolutiveStar := DoubleCentralizer.instStarAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

instance DoubleCentralizer.instStarModule {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] : StarModule 𝕜 (DoubleCentralizer 𝕜 A)

Coercion from an algebra into its multiplier algebra

noncomputable def DoubleCentralizer.coe (𝕜 : Type u_1) {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : A) : DoubleCentralizer 𝕜 A

The natural coercion of A into 𝓜(𝕜, A) given by sending a : A to the pair of linear maps Lₐ Rₐ : A →L[𝕜] A given by left- and right-multiplication by a, respectively.

Warning: if A = 𝕜, then this is a coercion which is not definitionally equal to the algebraMap 𝕜 𝓜(𝕜, 𝕜) coercion, but these are propositionally equal. See DoubleCentralizer.coe_eq_algebraMap below.

Equations

• ↑𝕜 a = { fst := (ContinuousLinearMap.mul 𝕜 A) a, snd := (ContinuousLinearMap.mul 𝕜 A).flip a, central := ⋯ }

noncomputable instance DoubleCentralizer.instCoeTC {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : CoeTC A (DoubleCentralizer 𝕜 A)

The natural coercion of A into 𝓜(𝕜, A) given by sending a : A to the pair of linear maps Lₐ Rₐ : A →L[𝕜] A given by left- and right-multiplication by a, respectively.

Warning: if A = 𝕜, then this is a coercion which is not definitionally equal to the algebraMap 𝕜 𝓜(𝕜, 𝕜) coercion, but these are propositionally equal. See DoubleCentralizer.coe_eq_algebraMap below.

Equations

• DoubleCentralizer.instCoeTC = { coe := ↑𝕜 }

@[simp]

theorem DoubleCentralizer.coe_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : A) : (↑𝕜 a).toProd.1 = (ContinuousLinearMap.mul 𝕜 A) a

@[simp]

theorem DoubleCentralizer.coe_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : A) : (↑𝕜 a).toProd.2 = (ContinuousLinearMap.mul 𝕜 A).flip a

theorem DoubleCentralizer.coe_eq_algebraMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : ↑𝕜 = ⇑(algebraMap 𝕜 (DoubleCentralizer 𝕜 𝕜))

noncomputable def DoubleCentralizer.coeHom {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] : A →⋆ₙₐ[𝕜] DoubleCentralizer 𝕜 A

The coercion of an algebra into its multiplier algebra as a non-unital star algebra homomorphism.

Equations

• DoubleCentralizer.coeHom = { toFun := fun (a : A) => ↑𝕜 a, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem DoubleCentralizer.coeHom_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] (a : A) : coeHom a = ↑𝕜 a

Norm structures

We define the norm structure on 𝓜(𝕜, A) as the pullback under DoubleCentralizer.toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ, which provides a definitional isometric embedding. Consequently, completeness of 𝓜(𝕜, A) is obtained by proving that the range of this map is closed.

In addition, we prove that 𝓜(𝕜, A) is a normed algebra, and, when A is a C⋆-algebra, we show that 𝓜(𝕜, A) is also a C⋆-algebra. Moreover, in this case, for a : 𝓜(𝕜, A), ‖a‖ = ‖a.fst‖ = ‖a.snd‖.

noncomputable instance DoubleCentralizer.instNormedRing {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : NormedRing (DoubleCentralizer 𝕜 A)

The normed group structure is inherited as the pullback under the ring monomorphism DoubleCentralizer.toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ.

Equations

• DoubleCentralizer.instNormedRing = NormedRing.induced (DoubleCentralizer 𝕜 A) ((A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) DoubleCentralizer.toProdMulOppositeHom ⋯

theorem DoubleCentralizer.norm_def {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : ‖a‖ = ‖toProdHom a‖

theorem DoubleCentralizer.nnnorm_def {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : ‖a‖₊ = ‖toProdHom a‖₊

theorem DoubleCentralizer.norm_def' {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : ‖a‖ = ‖toProdMulOppositeHom a‖

theorem DoubleCentralizer.nnnorm_def' {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A) : ‖a‖₊ = ‖toProdMulOppositeHom a‖₊

noncomputable instance DoubleCentralizer.instNormedSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : NormedSpace 𝕜 (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instNormedSpace = { toModule := DoubleCentralizer.instModule, norm_smul_le := ⋯ }

noncomputable instance DoubleCentralizer.instNormedAlgebra {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : NormedAlgebra 𝕜 (DoubleCentralizer 𝕜 A)

Equations

• DoubleCentralizer.instNormedAlgebra = { toAlgebra := DoubleCentralizer.instAlgebra, norm_smul_le := ⋯ }

theorem DoubleCentralizer.isUniformEmbedding_toProdMulOpposite {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : IsUniformEmbedding toProdMulOpposite

instance DoubleCentralizer.instCompleteSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [CompleteSpace A] : CompleteSpace (DoubleCentralizer 𝕜 A)

theorem DoubleCentralizer.norm_fst_eq_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.1‖ = ‖a.toProd.2‖

For a : 𝓜(𝕜, A), the norms of a.fst and a.snd coincide, and hence these also coincide with ‖a‖ which is max (‖a.fst‖) (‖a.snd‖).

theorem DoubleCentralizer.nnnorm_fst_eq_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.1‖₊ = ‖a.toProd.2‖₊

@[simp]

theorem DoubleCentralizer.norm_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.1‖ = ‖a‖

@[simp]

theorem DoubleCentralizer.norm_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.2‖ = ‖a‖

@[simp]

theorem DoubleCentralizer.nnnorm_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.1‖₊ = ‖a‖₊

@[simp]

theorem DoubleCentralizer.nnnorm_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing A] [CStarRing A] (a : DoubleCentralizer 𝕜 A) : ‖a.toProd.2‖₊ = ‖a‖₊

instance DoubleCentralizer.instCStarRing {𝕜 : Type u_1} {A : Type u_2} [DenselyNormedField 𝕜] [StarRing 𝕜] [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A] : CStarRing (DoubleCentralizer 𝕜 A)

noncomputable instance DoubleCentralizer.instCStarAlgebraComplex {A : Type u_1} [NonUnitalCStarAlgebra A] : CStarAlgebra (DoubleCentralizer ℂ A)

Equations

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