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 #
- 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
Ain𝓜(𝕜, 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 → Asatisfying the centrality condition∀ x y, R x * y = x * L y. - Show that if
Ais unital, thenA ≃⋆ₐ[𝕜] 𝓜(𝕜, 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) :
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] :
Type v
- 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).
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] :
@[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)
@[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)
@[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)
@[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) :
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] :
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)
@[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)
@[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] :
@[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] :
@[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) ℕ
@[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
@[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) :
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) :
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) :
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] :
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] :
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] :
@[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] :
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] :
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) :
@[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).
@[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] :
Equations
@[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)
@[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) :
@[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] :
A →⋆ₙₐ[𝕜] double_centralizer 𝕜 A
The coercion of an algebra into its multiplier algebra as a non-unital star algebra homomorphism.
@[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)ᵐᵒᵖ.
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) :
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) :
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) :
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) :
@[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
@[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
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] :
@[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‖).
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) :
@[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] :
cstar_ring (double_centralizer 𝕜 A)