# 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) [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] extends :

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.

Instances For
theorem DoubleCentralizer.central {π : Type u} {A : Type v} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (self : DoubleCentralizer π A) (x : A) (y : A) :
self.toProd.2 x * y = x * self.toProd.1 y

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

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.
Instances For
theorem DoubleCentralizer.ext (π : Type u) (A : Type v) [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) (b : DoubleCentralizer π A) (h : a.toProd = b.toProd) :
a = b

### 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Set.range DoubleCentralizer.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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Equations
• DoubleCentralizer.instAdd = { add := fun (a b : DoubleCentralizer π A) => { toProd := a.toProd + b.toProd, central := β― } }
instance DoubleCentralizer.instZero {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Zero (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instZero = { zero := { toProd := 0, central := β― } }
instance DoubleCentralizer.instNeg {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Neg (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instNeg = { neg := fun (a : DoubleCentralizer π A) => { toProd := -a.toProd, central := β― } }
instance DoubleCentralizer.instSub {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Sub (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instSub = { sub := fun (a b : DoubleCentralizer π A) => { toProd := a.toProd - b.toProd, central := β― } }
instance DoubleCentralizer.instSMul {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S A] [] [] [] :
SMul S (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instSMul = { smul := fun (s : S) (a : DoubleCentralizer π A) => { toProd := s β’ a.toProd, central := β― } }
@[simp]
theorem DoubleCentralizer.smul_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S A] [] [] [] (s : S) (a : DoubleCentralizer π A) :
(s β’ a).toProd = s β’ a.toProd
theorem DoubleCentralizer.smul_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S A] [] [] [] (s : S) (a : DoubleCentralizer π A) :
(s β’ a).toProd.2 = s β’ a.toProd.2
instance DoubleCentralizer.instIsScalarTower {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S A] [] [] [] {T : Type u_4} [] [] [SMulCommClass π T A] [] [] [] [SMul S T] [] :
Equations
• β― = β―
instance DoubleCentralizer.instSMulCommClass {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [] [SMulCommClass π S A] [] [] [] {T : Type u_4} [] [] [SMulCommClass π T A] [] [] [] [] :
Equations
• β― = β―
instance DoubleCentralizer.instIsCentralScalar {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {R : Type u_5} [] [Module R A] [SMulCommClass π R A] [] [] [] [] [] :
Equations
• β― = β―
instance DoubleCentralizer.instOne {π : Type u_1} {A : Type u_2} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Mul (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instMul = { mul := fun (a b : DoubleCentralizer π A) => { toProd := (a.toProd.1.comp b.toProd.1, b.toProd.2.comp a.toProd.2), central := β― } }
instance DoubleCentralizer.instNatCast {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Equations
• DoubleCentralizer.instNatCast = { natCast := fun (n : β) => { toProd := βn, central := β― } }
instance DoubleCentralizer.instIntCast {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Equations
• DoubleCentralizer.instIntCast = { intCast := fun (n : β€) => { toProd := βn, central := β― } }
instance DoubleCentralizer.instPow {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Equations
• DoubleCentralizer.instInhabited = { default := 0 }
@[simp]
theorem DoubleCentralizer.add_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) (b : DoubleCentralizer π A) :
(a + b).toProd = a.toProd + b.toProd
@[simp]
theorem DoubleCentralizer.zero_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
@[simp]
theorem DoubleCentralizer.neg_toProd {π : Type u_1} {A : Type u_2} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) (b : DoubleCentralizer π A) :
(a - b).toProd = a.toProd - b.toProd
@[simp]
theorem DoubleCentralizer.one_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
@[simp]
theorem DoubleCentralizer.natCast_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd = βn
@[deprecated DoubleCentralizer.natCast_toProd]
theorem DoubleCentralizer.nat_cast_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd = βn

Alias of DoubleCentralizer.natCast_toProd.

@[simp]
theorem DoubleCentralizer.intCast_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd = βn
@[deprecated DoubleCentralizer.intCast_toProd]
theorem DoubleCentralizer.int_cast_toProd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd = βn

Alias of DoubleCentralizer.intCast_toProd.

@[simp]
theorem DoubleCentralizer.pow_toProd {π : Type u_1} {A : Type u_2} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
.1 = 0
theorem DoubleCentralizer.zero_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
.2 = 0
theorem DoubleCentralizer.neg_fst {π : Type u_1} {A : Type u_2} [] [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} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
.1 = 1
theorem DoubleCentralizer.one_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
.2 = 1
@[simp]
theorem DoubleCentralizer.mul_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd.1 = βn
@[deprecated DoubleCentralizer.natCast_fst]
theorem DoubleCentralizer.nat_cast_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd.1 = βn

Alias of DoubleCentralizer.natCast_fst.

theorem DoubleCentralizer.natCast_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd.2 = βn
@[deprecated DoubleCentralizer.natCast_snd]
theorem DoubleCentralizer.nat_cast_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β) :
(βn).toProd.2 = βn

Alias of DoubleCentralizer.natCast_snd.

theorem DoubleCentralizer.intCast_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd.1 = βn
@[deprecated DoubleCentralizer.intCast_fst]
theorem DoubleCentralizer.int_cast_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd.1 = βn

Alias of DoubleCentralizer.intCast_fst.

theorem DoubleCentralizer.intCast_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd.2 = βn
@[deprecated DoubleCentralizer.intCast_snd]
theorem DoubleCentralizer.int_cast_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (n : β€) :
(βn).toProd.2 = βn

Alias of DoubleCentralizer.intCast_snd.

theorem DoubleCentralizer.pow_fst {π : Type u_1} {A : Type u_2} [] [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} [] [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} [] [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
Instances For
theorem DoubleCentralizer.toProdMulOpposite_injective {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Function.Injective DoubleCentralizer.toProdMulOpposite
theorem DoubleCentralizer.range_toProdMulOpposite {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
Set.range DoubleCentralizer.toProdMulOpposite = {lr : (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅ | β (x y : A), lr.2.unop x * y = x * lr.1 y}
instance DoubleCentralizer.instRing {π : Type u_1} {A : Type u_2} [] [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 β― β― β― β― β― β― β― β― β― β― β― β―
@[simp]
theorem DoubleCentralizer.toProdHom_apply {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (self : DoubleCentralizer π A) :
DoubleCentralizer.toProdHom self = self.toProd
def DoubleCentralizer.toProdHom {π : Type u_1} {A : Type u_2} [] [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' := β― }
Instances For
@[simp]
theorem DoubleCentralizer.toProdMulOppositeHom_apply {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
β (a : DoubleCentralizer π A), DoubleCentralizer.toProdMulOppositeHom a = a.toProdMulOpposite
def DoubleCentralizer.toProdMulOppositeHom {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :

The canonical map DoubleCentralizer.toProdMulOpposite as a ring homomorphism.

Equations
• DoubleCentralizer.toProdMulOppositeHom = { toFun := DoubleCentralizer.toProdMulOpposite, map_one' := β―, map_mul' := β―, map_zero' := β―, map_add' := β― }
Instances For
instance DoubleCentralizer.instModule {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] {S : Type u_3} [] [Module S A] [SMulCommClass π S 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
instance DoubleCentralizer.instAlgebra {π : Type u_1} {A : Type u_2} [] [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} [] [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} [] [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} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π A] [] :
Equations
• DoubleCentralizer.instStarAddMonoid = let __src := DoubleCentralizer.instStar;
instance DoubleCentralizer.instStarRing {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π A] [] :
Equations
• DoubleCentralizer.instStarRing = let __src := DoubleCentralizer.instStarAddMonoid; StarRing.mk β―
instance DoubleCentralizer.instStarModule {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π A] [] :
StarModule π (DoubleCentralizer π A)
Equations
• β― = β―

### Coercion from an algebra into its multiplier algebra #

noncomputable def DoubleCentralizer.coe (π : Type u_1) {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : 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 = { toProd := (() a, ().flip a), central := β― }
Instances For
noncomputable instance DoubleCentralizer.instCoeTC {π : Type u_1} {A : Type u_2} [] [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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : A) :
(βπ a).toProd.1 = () a
@[simp]
theorem DoubleCentralizer.coe_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : A) :
(βπ a).toProd.2 = ().flip a
theorem DoubleCentralizer.coe_eq_algebraMap {π : Type u_1} [] :
βπ = β(algebraMap π (DoubleCentralizer π π))
@[simp]
theorem DoubleCentralizer.coeHom_apply {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π A] [] (a : A) :
DoubleCentralizer.coeHom a = βπ a
noncomputable def DoubleCentralizer.coeHom {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarRing π] [] [StarModule π 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' := β― }
Instances For

### 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :

The normed group structure is inherited as the pullback under the ring monomorphism DoubleCentralizer.toProdMulOppositeHom : π(π, A) β+* (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅.

Equations
theorem DoubleCentralizer.norm_def {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) :
= βDoubleCentralizer.toProdHom aβ
theorem DoubleCentralizer.nnnorm_def {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) :
= βDoubleCentralizer.toProdHom aββ
theorem DoubleCentralizer.norm_def' {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) :
= βDoubleCentralizer.toProdMulOppositeHom aβ
theorem DoubleCentralizer.nnnorm_def' {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] (a : DoubleCentralizer π A) :
= βDoubleCentralizer.toProdMulOppositeHom aββ
instance DoubleCentralizer.instNormedSpace {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
NormedSpace π (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instNormedSpace = let __src := DoubleCentralizer.instModule;
instance DoubleCentralizer.instNormedAlgebra {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
NormedAlgebra π (DoubleCentralizer π A)
Equations
• DoubleCentralizer.instNormedAlgebra = let __src := DoubleCentralizer.instAlgebra; let __src_1 := DoubleCentralizer.instNormedSpace;
theorem DoubleCentralizer.uniformEmbedding_toProdMulOpposite {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] :
UniformEmbedding DoubleCentralizer.toProdMulOpposite
instance DoubleCentralizer.instCompleteSpace {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] :
Equations
• β― = β―
theorem DoubleCentralizer.norm_fst_eq_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A 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} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] [] (a : DoubleCentralizer π A) :
@[simp]
theorem DoubleCentralizer.norm_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] [] (a : DoubleCentralizer π A) :
βa.toProd.1β =
@[simp]
theorem DoubleCentralizer.norm_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] [] (a : DoubleCentralizer π A) :
βa.toProd.2β =
@[simp]
theorem DoubleCentralizer.nnnorm_fst {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] [] (a : DoubleCentralizer π A) :
@[simp]
theorem DoubleCentralizer.nnnorm_snd {π : Type u_1} {A : Type u_2} [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [] [] (a : DoubleCentralizer π A) :
instance DoubleCentralizer.instCstarRing {π : Type u_1} {A : Type u_2} [] [StarRing π] [] [] [NormedSpace π A] [SMulCommClass π A A] [IsScalarTower π A A] [StarModule π A] :
Equations
• β― = β―