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 Prod : Type v

• fst : A →L[𝕜] A
• snd : A →L[𝕜] A
• central : ∀ (x y : A), ↑s.snd x * y = x * ↑s.fst 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$.

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$.

theorem DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [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 λ 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 DoubleCentralizer.toProd = {lr | ∀ (x y : A), ↑lr.snd x * y = x * ↑lr.fst 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)

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

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

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

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)

@[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).fst = s • a.fst

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).snd = s • a.snd

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)

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

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

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

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

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

@[simp]

theorem DoubleCentralizer.add_toProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [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} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : 0.toProd = 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 : DoubleCentralizer 𝕜 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] : 1.toProd = 1

@[simp]

theorem DoubleCentralizer.nat_cast_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.int_cast_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 : DoubleCentralizer 𝕜 A) (b : DoubleCentralizer 𝕜 A) : (a + b).fst = a.fst + b.fst

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

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

theorem DoubleCentralizer.zero_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : 0.snd = 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).fst = -a.fst

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).snd = -a.snd

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

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

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

theorem DoubleCentralizer.one_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : 1.snd = 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 : DoubleCentralizer 𝕜 A) (b : DoubleCentralizer 𝕜 A) : (a * b).fst = a.fst * b.fst

@[simp]

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

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

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

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

theorem DoubleCentralizer.int_cast_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (n : ℤ) : (↑n).toProd.snd = ↑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).fst = a.fst ^ 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).snd = a.snd ^ 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.

theorem DoubleCentralizer.toProdMulOpposite_injective {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : Function.Injective DoubleCentralizer.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 DoubleCentralizer.toProdMulOpposite = {lr | ∀ (x y : A), ↑(MulOpposite.unop lr.snd) x * y = x * ↑lr.fst 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)ᵐᵒᵖ

@[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) : ↑DoubleCentralizer.toProdHom self = self.toProd

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 double_centralizer.to_prod as an additive group homomorphism.

@[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), ↑DoubleCentralizer.toProdMulOppositeHom a = DoubleCentralizer.toProdMulOpposite a

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.

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)

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

@[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).fst = ↑(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).snd = ↑(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).

@[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).fst b = star (↑a.snd (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).snd b = star (↑a.fst (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)

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)

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.

noncomputable instance DoubleCentralizer.instCoeTCDoubleCentralizer {𝕜 : 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.

@[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.fst = ↑(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.snd = ↑(ContinuousLinearMap.flip (ContinuousLinearMap.mul 𝕜 A)) a

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

@[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) : ↑DoubleCentralizer.coeHom a = ↑𝕜 a

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.

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.instNormedRingDoubleCentralizer {𝕜 : 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)ᵐᵒᵖ.

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‖ = ‖↑DoubleCentralizer.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‖₊ = ‖↑DoubleCentralizer.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‖ = ‖↑DoubleCentralizer.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‖₊ = ‖↑DoubleCentralizer.toProdMulOppositeHom a‖₊

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

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

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

instance DoubleCentralizer.instCompleteSpaceDoubleCentralizerToUniformSpaceToPseudoMetricSpaceToSeminormedRingInstNormedRingDoubleCentralizer {𝕜 : 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.fst‖ = ‖a.snd‖

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.fst‖₊ = ‖a.snd‖₊

@[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.fst‖ = ‖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.snd‖ = ‖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.fst‖₊ = ‖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.snd‖₊ = ‖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)