mathlib documentation

analysis.normed_space.star.multiplier

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 #

theorem double_centralizer.ext_iff {π•œ : Type u} {A : Type v} {_inst_1 : nontrivially_normed_field π•œ} {_inst_2 : non_unital_normed_ring A} {_inst_3 : normed_space π•œ A} {_inst_4 : smul_comm_class π•œ A A} {_inst_5 : is_scalar_tower π•œ A A} (x y : double_centralizer π•œ A) :
theorem double_centralizer.ext {π•œ : Type u} {A : Type v} {_inst_1 : nontrivially_normed_field π•œ} {_inst_2 : non_unital_normed_ring A} {_inst_3 : normed_space π•œ A} {_inst_4 : smul_comm_class π•œ A A} {_inst_5 : is_scalar_tower π•œ A A} (x y : double_centralizer π•œ A) (h : x.to_prod = y.to_prod) :
x = y
@[ext]
structure double_centralizer (π•œ : Type u) (A : Type v) [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A 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$.

Instances for double_centralizer

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

theorem double_centralizer.range_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
set.range double_centralizer.to_prod = {lr : (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A) | βˆ€ (x y : A), ⇑(lr.snd) x * y = x * ⇑(lr.fst) y}
@[protected, instance]
def double_centralizer.has_add {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_zero {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_neg {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_sub {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_smul {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] :
Equations
@[simp]
theorem double_centralizer.smul_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] (s : S) (a : double_centralizer π•œ A) :
theorem double_centralizer.smul_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] (s : S) (a : double_centralizer π•œ A) :
theorem double_centralizer.smul_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] (s : S) (a : double_centralizer π•œ A) :
@[protected, instance]
def double_centralizer.is_scalar_tower {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] {T : Type u_4} [monoid T] [distrib_mul_action T A] [smul_comm_class π•œ T A] [has_continuous_const_smul T A] [is_scalar_tower T A A] [smul_comm_class T A A] [has_smul S T] [is_scalar_tower S T A] :
@[protected, instance]
def double_centralizer.smul_comm_class {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [monoid S] [distrib_mul_action S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] {T : Type u_4} [monoid T] [distrib_mul_action T A] [smul_comm_class π•œ T A] [has_continuous_const_smul T A] [is_scalar_tower T A A] [smul_comm_class T A A] [smul_comm_class S T A] :
@[protected, instance]
@[protected, instance]
def double_centralizer.has_one {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_mul {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_nat_cast {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.has_int_cast {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.nat.has_pow {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[protected, instance]
def double_centralizer.inhabited {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
Equations
@[simp]
theorem double_centralizer.add_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.zero_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
@[simp]
theorem double_centralizer.neg_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.sub_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.one_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
@[simp]
theorem double_centralizer.nat_cast_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) :
@[simp]
theorem double_centralizer.int_cast_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„€) :
@[simp]
theorem double_centralizer.pow_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) (a : double_centralizer π•œ A) :
(a ^ n).to_prod = a.to_prod ^ n
theorem double_centralizer.add_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
theorem double_centralizer.add_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
theorem double_centralizer.zero_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
theorem double_centralizer.zero_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
theorem double_centralizer.neg_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a : double_centralizer π•œ A) :
theorem double_centralizer.neg_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a : double_centralizer π•œ A) :
theorem double_centralizer.sub_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
theorem double_centralizer.sub_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
theorem double_centralizer.one_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
theorem double_centralizer.one_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
@[simp]
theorem double_centralizer.mul_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.mul_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a b : double_centralizer π•œ A) :
theorem double_centralizer.nat_cast_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) :
theorem double_centralizer.nat_cast_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) :
theorem double_centralizer.int_cast_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„€) :
theorem double_centralizer.int_cast_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„€) :
theorem double_centralizer.pow_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) (a : double_centralizer π•œ A) :
(a ^ n).to_prod.fst = a.to_prod.fst ^ n
theorem double_centralizer.pow_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (n : β„•) (a : double_centralizer π•œ A) :
(a ^ n).to_prod.snd = a.to_prod.snd ^ n
def double_centralizer.to_prod_mul_opposite {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
double_centralizer π•œ A β†’ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ

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
@[protected, instance]
def double_centralizer.ring {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :

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
def double_centralizer.to_prod_hom {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
double_centralizer π•œ A β†’+ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)

The canonical map double_centralizer.to_prod as an additive group homomorphism.

Equations
@[simp]
theorem double_centralizer.to_prod_hom_apply {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (self : double_centralizer π•œ A) :
@[protected, instance]
def double_centralizer.module {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] {S : Type u_3} [semiring S] [module S A] [smul_comm_class π•œ S A] [has_continuous_const_smul S A] [is_scalar_tower S A A] [smul_comm_class S A A] :
module S (double_centralizer π•œ A)

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
@[protected, instance]
def double_centralizer.algebra {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :
algebra π•œ (double_centralizer π•œ A)
Equations
@[simp]
theorem double_centralizer.algebra_map_to_prod {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (k : π•œ) :
(⇑(algebra_map π•œ (double_centralizer π•œ A)) k).to_prod = ⇑(algebra_map π•œ ((A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A))) k
theorem double_centralizer.algebra_map_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (k : π•œ) :
(⇑(algebra_map π•œ (double_centralizer π•œ A)) k).to_prod.fst = ⇑(algebra_map π•œ (A β†’L[π•œ] A)) k
theorem double_centralizer.algebra_map_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (k : π•œ) :
(⇑(algebra_map π•œ (double_centralizer π•œ A)) k).to_prod.snd = ⇑(algebra_map π•œ (A β†’L[π•œ] A)) k

Star structure #

@[protected, instance]
def double_centralizer.has_star {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] :

The star operation on a : π“œ(π•œ, A) is given by (star a).to_prod = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star).

Equations
@[simp]
theorem double_centralizer.star_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] (a : double_centralizer π•œ A) (b : A) :
@[simp]
theorem double_centralizer.star_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] (a : double_centralizer π•œ A) (b : A) :
@[protected, instance]
def double_centralizer.star_module {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] :
star_module π•œ (double_centralizer π•œ A)

Coercion from an algebra into its multiplier algebra #

@[protected, instance]
noncomputable def double_centralizer.has_coe_t {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ 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 algebra_map π•œ π“œ(π•œ, π•œ) coercion, but these are propositionally equal. See double_centralizer.coe_eq_algebra_map below.

Equations
@[simp, norm_cast]
theorem double_centralizer.coe_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a : A) :
@[simp, norm_cast]
theorem double_centralizer.coe_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] (a : A) :
theorem double_centralizer.coe_eq_algebra_map {π•œ : Type u_1} [nontrivially_normed_field π•œ] :
coe = ⇑(algebra_map π•œ (double_centralizer π•œ π•œ))
noncomputable def double_centralizer.coe_hom {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] :

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

Equations
@[simp]
theorem double_centralizer.coe_hom_apply {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring π•œ] [star_ring A] [star_module π•œ A] [normed_star_group A] (a : A) :

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β€–.

@[protected, instance]
noncomputable def double_centralizer.normed_ring {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] :

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
@[protected, instance]
def double_centralizer.complete_space {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [complete_space A] :
theorem double_centralizer.norm_fst_eq_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring A] [cstar_ring A] (a : double_centralizer π•œ A) :

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β€–).

@[simp]
theorem double_centralizer.norm_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring A] [cstar_ring A] (a : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.norm_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring A] [cstar_ring A] (a : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.nnnorm_fst {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring A] [cstar_ring A] (a : double_centralizer π•œ A) :
@[simp]
theorem double_centralizer.nnnorm_snd {π•œ : Type u_1} {A : Type u_2} [nontrivially_normed_field π•œ] [non_unital_normed_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_ring A] [cstar_ring A] (a : double_centralizer π•œ A) :
@[protected, instance]
def double_centralizer.cstar_ring {π•œ : Type u_1} {A : Type u_2} [densely_normed_field π•œ] [star_ring π•œ] [non_unital_normed_ring A] [star_ring A] [cstar_ring A] [normed_space π•œ A] [smul_comm_class π•œ A A] [is_scalar_tower π•œ A A] [star_module π•œ A] :