mathlib3 documentation

analysis.normed_space.star.multiplier

Multiplier Algebra of a C⋆-algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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) :
(s a).to_prod = s a.to_prod
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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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]
@[simp]
@[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.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) :
@[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.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

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]

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
@[protected, instance]

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]
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]

The star operation on a : 𝓜(𝕜, A) is given by (star a).to_prod = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star).

Equations
@[protected, instance]

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

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

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

@[protected, instance]