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 normed_algebra
structure (and everything contained therein) through the
ring (even algebra) homomorphism
double_centralizer.to_prod_mul_opposite_hom : π(π, A) β+* (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅
which
sends a : π(π, A)
to (a.fst, mul_opposite.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)
.
- to_prod : (A βL[π] A) Γ (A βL[π] A)
- central : β (x y : A), β(self.to_prod.snd) x * y = x * β(self.to_prod.fst) y
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$.
Instances for double_centralizer
- double_centralizer.has_sizeof_inst
- double_centralizer.has_add
- double_centralizer.has_zero
- double_centralizer.has_neg
- double_centralizer.has_sub
- double_centralizer.has_smul
- double_centralizer.is_scalar_tower
- double_centralizer.smul_comm_class
- double_centralizer.is_central_scalar
- double_centralizer.has_one
- double_centralizer.has_mul
- double_centralizer.has_nat_cast
- double_centralizer.has_int_cast
- double_centralizer.nat.has_pow
- double_centralizer.inhabited
- double_centralizer.ring
- double_centralizer.module
- double_centralizer.algebra
- double_centralizer.has_star
- double_centralizer.star_add_monoid
- double_centralizer.star_ring
- double_centralizer.star_module
- double_centralizer.has_coe_t
- double_centralizer.normed_ring
- double_centralizer.normed_space
- double_centralizer.normed_algebra
- double_centralizer.complete_space
- double_centralizer.cstar_ring
Algebraic structure #
Because the multiplier algebra is defined as the algebra of double centralizers, there is a natural
injection double_centralizer.to_prod_mul_opposite : π(π, A) β (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅
defined by Ξ» a, (a.fst, mul_opposite.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
- double_centralizer.has_neg = {neg := Ξ» (a : double_centralizer π A), {to_prod := -a.to_prod, central := _}}
Equations
- double_centralizer.has_smul = {smul := Ξ» (s : S) (a : double_centralizer π A), {to_prod := s β’ a.to_prod, central := _}}
Equations
The natural injection from double_centralizer.to_prod
except the second coordinate inherits
mul_opposite.op
. The ring structure on π(π, A)
is the pullback under this map.
Equations
- double_centralizer.to_prod_mul_opposite = Ξ» (a : double_centralizer π A), (a.to_prod.fst, mul_opposite.op a.to_prod.snd)
The ring structure is inherited as the pullback under the injective map
double_centralizer.to_prod_mul_opposite : π(π, A) β (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅
Equations
- double_centralizer.ring = function.injective.ring double_centralizer.to_prod_mul_opposite double_centralizer.to_prod_mul_opposite_injective double_centralizer.ring._proof_10 double_centralizer.ring._proof_11 double_centralizer.ring._proof_12 double_centralizer.ring._proof_13 double_centralizer.ring._proof_14 double_centralizer.ring._proof_15 double_centralizer.ring._proof_16 double_centralizer.ring._proof_17 double_centralizer.ring._proof_18 double_centralizer.ring._proof_19 double_centralizer.ring._proof_20
The canonical map double_centralizer.to_prod
as an additive group homomorphism.
Equations
- double_centralizer.to_prod_hom = {to_fun := double_centralizer.to_prod _inst_5, map_zero' := _, map_add' := _}
The canonical map double_centralizer.to_prod_mul_opposite
as a ring homomorphism.
Equations
- double_centralizer.to_prod_mul_opposite_hom = {to_fun := double_centralizer.to_prod_mul_opposite _inst_5, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
The module structure is inherited as the pullback under the additive group monomorphism
double_centralizer.to_prod : π(π, A) β+ (A βL[π] A) Γ (A βL[π] A)
Equations
- double_centralizer.module = function.injective.module S double_centralizer.to_prod_hom double_centralizer.ext double_centralizer.module._proof_3
Equations
- double_centralizer.algebra = {to_has_smul := double_centralizer.has_smul _inst_4, to_ring_hom := {to_fun := Ξ» (k : π), {to_prod := β(algebra_map π ((A βL[π] A) Γ (A βL[π] A))) k, central := _}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Star structure #
The star operation on a : π(π, A)
is given by
(star a).to_prod = (star β a.snd β star, star β a.fst β star)
.
Equations
- double_centralizer.has_star = {star := Ξ» (a : double_centralizer π A), {to_prod := ((β(starβα΅’ π).comp a.to_prod.snd).comp β(starβα΅’ π), (β(starβα΅’ π).comp a.to_prod.fst).comp β(starβα΅’ π)), central := _}}
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
algebra_map π π(π, π)
coercion, but these are propositionally equal. See
double_centralizer.coe_eq_algebra_map
below.
Equations
- double_centralizer.has_coe_t = {coe := Ξ» (a : A), {to_prod := (β(continuous_linear_map.mul π A) a, β((continuous_linear_map.mul π A).flip) a), central := _}}
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
double_centralizer.to_prod_mul_opposite_hom : π(π, 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 monomoprhism
double_centralizer.to_prod_mul_opposite_hom : π(π, A) β+* (A βL[π] A) Γ (A βL[π] A)α΅α΅α΅
.
Equations
Equations
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β)
.