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 #

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

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

x = y ↔ x.to_prod = y.to_prod

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

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

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

has_add (double_centralizer 𝕜 A)

Equations

double_centralizer.has_add = {add := λ (a b : double_centralizer 𝕜 A), {to_prod := a.to_prod + b.to_prod, central := _}}

@[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] :

has_zero (double_centralizer 𝕜 A)

Equations

double_centralizer.has_zero = {zero := {to_prod := 0, central := _}}

@[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] :

has_neg (double_centralizer 𝕜 A)

Equations

double_centralizer.has_neg = {neg := λ (a : double_centralizer 𝕜 A), {to_prod := -a.to_prod, central := _}}

@[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] :

has_sub (double_centralizer 𝕜 A)

Equations

double_centralizer.has_sub = {sub := λ (a b : double_centralizer 𝕜 A), {to_prod := a.to_prod - b.to_prod, central := _}}

@[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] :

has_smul S (double_centralizer 𝕜 A)

Equations

double_centralizer.has_smul = {smul := λ (s : S) (a : double_centralizer 𝕜 A), {to_prod := s • a.to_prod, central := _}}

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

(s • a).to_prod.fst = s • a.to_prod.fst

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

(s • a).to_prod.snd = s • a.to_prod.snd

@[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] :

is_scalar_tower S T (double_centralizer 𝕜 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] :

smul_comm_class S T (double_centralizer 𝕜 A)

@[protected, instance]

def double_centralizer.is_central_scalar {𝕜 : 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] {R : Type u_3} [semiring R] [module R A] [smul_comm_class 𝕜 R A] [has_continuous_const_smul R A] [is_scalar_tower R A A] [smul_comm_class R A A] [module Rᵐᵒᵖ A] [is_central_scalar R A] :

is_central_scalar R (double_centralizer 𝕜 A)

@[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] :

has_one (double_centralizer 𝕜 A)

Equations

double_centralizer.has_one = {one := {to_prod := 1, central := _}}

@[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] :

has_mul (double_centralizer 𝕜 A)

Equations

double_centralizer.has_mul = {mul := λ (a b : double_centralizer 𝕜 A), {to_prod := (a.to_prod.fst.comp b.to_prod.fst, b.to_prod.snd.comp a.to_prod.snd), central := _}}

@[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] :

has_nat_cast (double_centralizer 𝕜 A)

Equations

double_centralizer.has_nat_cast = {nat_cast := λ (n : ℕ), {to_prod := ↑n, central := _}}

@[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] :

has_int_cast (double_centralizer 𝕜 A)

Equations

double_centralizer.has_int_cast = {int_cast := λ (n : ℤ), {to_prod := ↑n, central := _}}

@[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] :

has_pow (double_centralizer 𝕜 A) ℕ

Equations

double_centralizer.nat.has_pow = {pow := λ (a : double_centralizer 𝕜 A) (n : ℕ), {to_prod := a.to_prod ^ n, central := _}}

@[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] :

inhabited (double_centralizer 𝕜 A)

Equations

double_centralizer.inhabited = {default := 0}

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

(a + b).to_prod = a.to_prod + b.to_prod

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

(-a).to_prod = -a.to_prod

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

(a - b).to_prod = a.to_prod - b.to_prod

@[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 : ℕ) :

↑n.to_prod = ↑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 : ℤ) :

↑n.to_prod = ↑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) :

(a + b).to_prod.fst = a.to_prod.fst + b.to_prod.fst

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

(a + b).to_prod.snd = a.to_prod.snd + b.to_prod.snd

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

0.to_prod.fst = 0

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

0.to_prod.snd = 0

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

(-a).to_prod.fst = -a.to_prod.fst

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

(-a).to_prod.snd = -a.to_prod.snd

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

(a - b).to_prod.fst = a.to_prod.fst - b.to_prod.fst

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

(a - b).to_prod.snd = a.to_prod.snd - b.to_prod.snd

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

1.to_prod.fst = 1

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

1.to_prod.snd = 1

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

(a * b).to_prod.fst = a.to_prod.fst * b.to_prod.fst

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

(a * b).to_prod.snd = b.to_prod.snd * a.to_prod.snd

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

↑n.to_prod.fst = ↑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 : ℕ) :

↑n.to_prod.snd = ↑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 : ℤ) :

↑n.to_prod.fst = ↑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 : ℤ) :

↑n.to_prod.snd = ↑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

double_centralizer.to_prod_mul_opposite = λ (a : double_centralizer 𝕜 A), (a.to_prod.fst, mul_opposite.op a.to_prod.snd)

theorem double_centralizer.to_prod_mul_opposite_injective {𝕜 : 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] :

function.injective double_centralizer.to_prod_mul_opposite

theorem double_centralizer.range_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] :

set.range double_centralizer.to_prod_mul_opposite = {lr : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ | ∀ (x y : A), ⇑(mul_opposite.unop lr.snd) x * y = x * ⇑(lr.fst) y}

@[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] :

ring (double_centralizer 𝕜 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

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

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

double_centralizer.to_prod_hom = {to_fun := double_centralizer.to_prod _inst_5, map_zero' := _, map_add' := _}

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

⇑double_centralizer.to_prod_hom self = self.to_prod

def double_centralizer.to_prod_mul_opposite_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_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' := _}

@[simp]

theorem double_centralizer.to_prod_mul_opposite_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] (ᾰ : double_centralizer 𝕜 A) :

⇑double_centralizer.to_prod_mul_opposite_hom ᾰ = ᾰ.to_prod_mul_opposite

@[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

double_centralizer.module = function.injective.module S double_centralizer.to_prod_hom double_centralizer.ext double_centralizer.module._proof_3

@[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

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' := _}

@[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] :

has_star (double_centralizer 𝕜 A)

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 := _}}

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

⇑((has_star.star a).to_prod.fst) b = has_star.star (⇑(a.to_prod.snd) (has_star.star b))

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

⇑((has_star.star a).to_prod.snd) b = has_star.star (⇑(a.to_prod.fst) (has_star.star b))

@[protected, instance]

def double_centralizer.star_add_monoid {𝕜 : 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_add_monoid (double_centralizer 𝕜 A)

Equations

double_centralizer.star_add_monoid = {to_has_involutive_star := {to_has_star := {star := has_star.star double_centralizer.has_star}, star_involutive := _}, star_add := _}

@[protected, instance]

def double_centralizer.star_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] [star_ring 𝕜] [star_ring A] [star_module 𝕜 A] [normed_star_group A] :

star_ring (double_centralizer 𝕜 A)

Equations

double_centralizer.star_ring = {to_star_semigroup := {to_has_involutive_star := star_add_monoid.to_has_involutive_star double_centralizer.star_add_monoid, star_mul := _}, star_add := _}

@[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] :

has_coe_t A (double_centralizer 𝕜 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

double_centralizer.has_coe_t = {coe := λ (a : A), {to_prod := (⇑(continuous_linear_map.mul 𝕜 A) a, ⇑((continuous_linear_map.mul 𝕜 A).flip) a), central := _}}

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

↑a.to_prod.fst = ⇑(continuous_linear_map.mul 𝕜 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) :

↑a.to_prod.snd = ⇑((continuous_linear_map.mul 𝕜 A).flip) 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] :

A →⋆ₙₐ[𝕜] double_centralizer 𝕜 A

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

Equations

double_centralizer.coe_hom = {to_fun := λ (a : A), ↑a, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

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

⇑double_centralizer.coe_hom 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] :

normed_ring (double_centralizer 𝕜 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

double_centralizer.normed_ring = normed_ring.induced (double_centralizer 𝕜 A) ((A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) double_centralizer.to_prod_mul_opposite_hom double_centralizer.to_prod_mul_opposite_injective

theorem double_centralizer.norm_def {𝕜 : 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) :

‖a‖ = ‖⇑double_centralizer.to_prod_hom a‖

theorem double_centralizer.nnnorm_def {𝕜 : 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) :

‖a‖₊ = ‖⇑double_centralizer.to_prod_hom a‖₊

theorem double_centralizer.norm_def' {𝕜 : 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) :

‖a‖ = ‖⇑double_centralizer.to_prod_mul_opposite_hom a‖

theorem double_centralizer.nnnorm_def' {𝕜 : 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) :

‖a‖₊ = ‖⇑double_centralizer.to_prod_mul_opposite_hom a‖₊

@[protected, instance]

def double_centralizer.normed_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] :

normed_space 𝕜 (double_centralizer 𝕜 A)

Equations

double_centralizer.normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action double_centralizer.module, add_smul := _, zero_smul := _}, norm_smul_le := _}

@[protected, instance]

def double_centralizer.normed_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] :

normed_algebra 𝕜 (double_centralizer 𝕜 A)

Equations

double_centralizer.normed_algebra = {to_algebra := {to_has_smul := algebra.to_has_smul double_centralizer.algebra, to_ring_hom := algebra.to_ring_hom double_centralizer.algebra, commutes' := _, smul_def' := _}, norm_smul_le := _}

theorem double_centralizer.uniform_embedding_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] :

uniform_embedding double_centralizer.to_prod_mul_opposite

@[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] :

complete_space (double_centralizer 𝕜 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) :

‖a.to_prod.fst ‖ = ‖a.to_prod.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 double_centralizer.nnnorm_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) :

‖a.to_prod.fst ‖₊ = ‖a.to_prod.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) :

‖a.to_prod.fst ‖ = ‖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) :

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

‖a.to_prod.fst ‖₊ = ‖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) :

‖a.to_prod.snd ‖₊ = ‖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] :

cstar_ring (double_centralizer 𝕜 A)