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 #
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, thenA βββ[π] π(π, A)
.
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$.
The centrality condition that the maps linear maps intertwine one another.
Instances For
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
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)
.
Equations
- DoubleCentralizer.instAdd = { add := fun (a b : DoubleCentralizer π A) => { toProd := a.toProd + b.toProd, central := β― } }
Equations
- DoubleCentralizer.instZero = { zero := { toProd := 0, central := β― } }
Equations
- DoubleCentralizer.instNeg = { neg := fun (a : DoubleCentralizer π A) => { toProd := -a.toProd, central := β― } }
Equations
- DoubleCentralizer.instSub = { sub := fun (a b : DoubleCentralizer π A) => { toProd := a.toProd - b.toProd, central := β― } }
Equations
- DoubleCentralizer.instSMul = { smul := fun (s : S) (a : DoubleCentralizer π A) => { toProd := s β’ a.toProd, central := β― } }
Equations
- β― = β―
Equations
- β― = β―
Equations
- β― = β―
Equations
- DoubleCentralizer.instOne = { one := { toProd := 1, central := β― } }
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 := β― } }
Equations
- DoubleCentralizer.instPow = { pow := fun (a : DoubleCentralizer π A) (n : β) => { toProd := a.toProd ^ n, central := β― } }
Equations
- DoubleCentralizer.instInhabited = { default := 0 }
Alias of DoubleCentralizer.natCast_toProd
.
Alias of DoubleCentralizer.intCast_toProd
.
Alias of DoubleCentralizer.natCast_fst
.
Alias of DoubleCentralizer.natCast_snd
.
Alias of DoubleCentralizer.intCast_fst
.
Alias of DoubleCentralizer.intCast_snd
.
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)
Instances For
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 β― β― β― β― β― β― β― β― β― β― β― β―
The canonical map DoubleCentralizer.toProd
as an additive group homomorphism.
Equations
- DoubleCentralizer.toProdHom = { toFun := DoubleCentralizer.toProd, map_zero' := β―, map_add' := β― }
Instances For
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
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 β― β―
Equations
- One or more equations did not get rendered due to their size.
Star structure #
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.
Equations
- DoubleCentralizer.instStarAddMonoid = StarAddMonoid.mk β―
Equations
- DoubleCentralizer.instStarRing = StarRing.mk β―
Equations
- β― = β―
Coercion from an algebra into its multiplier algebra #
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 := ((ContinuousLinearMap.mul π A) a, (ContinuousLinearMap.mul π A).flip a), central := β― }
Instances For
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 := βπ }
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β
.
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 β―
Equations
- DoubleCentralizer.instNormedSpace = NormedSpace.mk β―
Equations
- DoubleCentralizer.instNormedAlgebra = NormedAlgebra.mk β―
Alias of DoubleCentralizer.isUniformEmbedding_toProdMulOpposite
.
Equations
- β― = β―
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β)
.
Equations
- β― = β―