Functoriality of multiplier algebras of C⋆-algebras

Mathlib's multiplier algebra 𝓜(𝕜, A) consists of double centralizers (L, R). This file proves that, when A has a proper involution (for example, when it is a C⋆-ring), the left and right centralizers are module maps for right and left multiplication respectively, so that the products of a multiplier with an element of A are again elements of A, and the canonical map A → 𝓜(𝕜, A) is injective. For regular normed algebras (RegularNormedAlgebra), including real and complex C⋆-algebras, this map is isometric.

With a proper involution a multiplier is determined by its left centralizer, DoubleCentralizer.ext_fst. Conversely, a bounded operator L with an adjoint L' for the pairing (x, y) ↦ star x * y is the left centralizer of the multiplier DoubleCentralizer.ofAdjoint L L', whose right centralizer is star ∘ L' ∘ star. This is how multipliers are built from left actions on a dense subalgebra, such as the canonical multipliers of a crossed product.

A star-algebra equivalence e : A ≃⋆ₐ[ℂ] B of complex C⋆-algebras extends to a star-algebra equivalence DoubleCentralizer.congr e : 𝓜(ℂ, A) ≃⋆ₐ[ℂ] 𝓜(ℂ, B), sending (L, R) to (e ∘ L ∘ e⁻¹, e ∘ R ∘ e⁻¹). It is compatible with the inclusions of A and B, and it is the only multiplicative map with this property. Applied to the automorphisms of a C⋆-dynamical system, this gives the induced action on the multiplier algebra; DoubleCentralizer.congrAut records that e ↦ congr e is a monoid homomorphism of automorphism groups.

Since A is an ideal of 𝓜(ℂ, A), conjugation a ↦ u * a * u⋆ by a unitary multiplier u maps A to itself; DoubleCentralizer.conjStarAlgAut records it as a monoid homomorphism from the unitary multipliers to the automorphisms of A. As the inclusion of A is a linear isometry, a real path in A has derivative v exactly when its image in 𝓜(ℂ, A) has derivative ↑v, DoubleCentralizer.hasDerivAt_coe_iff, so derivatives may be computed in the multiplier algebra. Consequently, conjugating a path in A by a path of multipliers U with U 0 = 1 and U' 0 = i Q, for self-adjoint Q ∈ A, adds i[Q, ·] to its derivative at 0, DoubleCentralizer.hasDerivAt_conj_zero.

References

• Iain Raeburn and Dana Williams, Morita Equivalence and Continuous-Trace C-Algebras*, Section 2.3, for multiplier algebras.
• Dana Williams, Crossed Products of C-Algebras*, Chapter 2, for the extension of automorphisms to multiplier algebras.

theorem DoubleCentralizer.ext_fst_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] {m n : DoubleCentralizer 𝕜 A} (h₁ : ∀ (a : A), m.toProd.1 a = n.toProd.1 a) (h₂ : ∀ (a : A), m.toProd.2 a = n.toProd.2 a) : m = n

Two multipliers are equal if their left and right centralizers agree pointwise.

@[simp]

theorem DoubleCentralizer.coe_zero {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] : ↑𝕜 0 = 0

The inclusion of A into its multiplier algebra sends 0 to 0.

@[simp]

theorem DoubleCentralizer.coe_add {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : A) : ↑𝕜 (a + b) = ↑𝕜 a + ↑𝕜 b

The inclusion of A into its multiplier algebra commutes with addition.

@[simp]

theorem DoubleCentralizer.coe_mul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : A) : ↑𝕜 (a * b) = ↑𝕜 a * ↑𝕜 b

The inclusion of A into its multiplier algebra commutes with multiplication.

@[simp]

theorem DoubleCentralizer.coe_neg {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a : A) : ↑𝕜 (-a) = -↑𝕜 a

The inclusion of A into its multiplier algebra commutes with negation.

@[simp]

theorem DoubleCentralizer.coe_sub {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : A) : ↑𝕜 (a - b) = ↑𝕜 a - ↑𝕜 b

The inclusion of A into its multiplier algebra commutes with subtraction.

@[simp]

theorem DoubleCentralizer.coe_smul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (c : 𝕜) (a : A) : ↑𝕜 (c • a) = c • ↑𝕜 a

The inclusion of A into its multiplier algebra commutes with scalar multiplication.

@[simp]

theorem DoubleCentralizer.coe_star {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] (a : A) : ↑𝕜 (star a) = star (↑𝕜 a)

The inclusion of A into its multiplier algebra commutes with the star operation.

@[simp]

theorem DoubleCentralizer.coe_one {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] : ↑𝕜 1 = 1

The inclusion of a unital algebra into its multiplier algebra sends 1 to 1.

theorem DoubleCentralizer.fst_mul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [Star A] [IsProperStar A] (m : DoubleCentralizer 𝕜 A) (a b : A) : m.toProd.1 (a * b) = m.toProd.1 a * b

The left centralizer of a multiplier commutes with right multiplication.

@[simp]

theorem DoubleCentralizer.mul_coe_eq_coe_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [Star A] [IsProperStar A] (m : DoubleCentralizer 𝕜 A) (a : A) : m * ↑𝕜 a = ↑𝕜 (m.toProd.1 a)

A multiplier times an element of A is the element obtained from the left centralizer.

theorem DoubleCentralizer.coe_injective {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [Star A] [IsProperStar A] : Function.Injective ↑𝕜

The canonical map of A into its multiplier algebra is injective.

@[simp]

theorem DoubleCentralizer.coe_inj {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [Star A] [IsProperStar A] {a b : A} : ↑𝕜 a = ↑𝕜 b ↔ a = b

theorem DoubleCentralizer.snd_mul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [InvolutiveStar A] [IsProperStar A] (m : DoubleCentralizer 𝕜 A) (a b : A) : m.toProd.2 (a * b) = a * m.toProd.2 b

The right centralizer of a multiplier commutes with left multiplication.

@[simp]

theorem DoubleCentralizer.coe_mul_eq_coe_snd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [InvolutiveStar A] [IsProperStar A] (a : A) (m : DoubleCentralizer 𝕜 A) : ↑𝕜 a * m = ↑𝕜 (m.toProd.2 a)

An element of A times a multiplier is the element obtained from the right centralizer.

theorem DoubleCentralizer.ext_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [InvolutiveStar A] [IsProperStar A] {m n : DoubleCentralizer 𝕜 A} (h : ∀ (a : A), m.toProd.1 a = n.toProd.1 a) : m = n

A multiplier is determined by its left centralizer.

def DoubleCentralizer.ofAdjoint {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedStarGroup A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A] (L L' : A →L[𝕜] A) (h : ∀ (x y : A), star (L' x) * y = star x * L y) : DoubleCentralizer 𝕜 A

A bounded operator L on A with an adjoint L' for the pairing (x, y) ↦ star x * y, that is star (L' x) * y = star x * L y, is the left centralizer of the multiplier (L, star ∘ L' ∘ star).

@[simp]

theorem DoubleCentralizer.ofAdjoint_fst {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedStarGroup A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A] {L L' : A →L[𝕜] A} {h : ∀ (x y : A), star (L' x) * y = star x * L y} : (ofAdjoint L L' h).toProd.1 = L

@[simp]

theorem DoubleCentralizer.ofAdjoint_snd_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedStarGroup A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A] {L L' : A →L[𝕜] A} {h : ∀ (x y : A), star (L' x) * y = star x * L y} (x : A) : (ofAdjoint L L' h).toProd.2 x = star (L' (star x))

@[simp]

theorem DoubleCentralizer.star_ofAdjoint {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedStarGroup A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [StarModule 𝕜 A] {L L' : A →L[𝕜] A} {h : ∀ (x y : A), star (L' x) * y = star x * L y} : star (ofAdjoint L L' h) = ofAdjoint L' L ⋯

The adjoint of the multiplier with left centralizer L has left centralizer L'.

@[simp]

theorem DoubleCentralizer.norm_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (a : A) : ‖↑𝕜 a‖ = ‖a‖

The inclusion of a regular normed algebra into its multiplier algebra preserves the norm.

theorem DoubleCentralizer.isometry_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [RegularNormedAlgebra 𝕜 A] : Isometry ↑𝕜

The inclusion of a regular normed algebra into its multiplier algebra is isometric.

noncomputable def DoubleCentralizer.congr {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) : DoubleCentralizer ℂ A ≃⋆ₐ[ℂ] DoubleCentralizer ℂ B

A star-algebra equivalence of C⋆-algebras extends to their multiplier algebras: the pair (L, R) is sent to (e ∘ L ∘ e⁻¹, e ∘ R ∘ e⁻¹).

@[simp]

theorem DoubleCentralizer.congr_apply_fst {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) (m : DoubleCentralizer ℂ A) (b : B) : ((congr e) m).toProd.1 b = e (m.toProd.1 (e.symm b))

@[simp]

theorem DoubleCentralizer.congr_apply_snd {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) (m : DoubleCentralizer ℂ A) (b : B) : ((congr e) m).toProd.2 b = e (m.toProd.2 (e.symm b))

@[simp]

theorem DoubleCentralizer.congr_symm {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) : (congr e).symm = congr e.symm

@[simp]

theorem DoubleCentralizer.congr_refl {A : Type u_1} [NonUnitalCStarAlgebra A] : congr (StarAlgEquiv.refl ℂ A) = StarAlgEquiv.refl ℂ (DoubleCentralizer ℂ A)

@[simp]

theorem DoubleCentralizer.congr_trans {A : Type u_1} {B : Type u_2} {C : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] (e : A ≃⋆ₐ[ℂ] B) (f : B ≃⋆ₐ[ℂ] C) : congr (e.trans f) = (congr e).trans (congr f)

noncomputable def DoubleCentralizer.congrAut {A : Type u_1} [NonUnitalCStarAlgebra A] : (A ≃⋆ₐ[ℂ] A) →* DoubleCentralizer ℂ A ≃⋆ₐ[ℂ] DoubleCentralizer ℂ A

Extension to multiplier algebras, as a monoid homomorphism of automorphism groups.

@[simp]

theorem DoubleCentralizer.congrAut_apply {A : Type u_1} [NonUnitalCStarAlgebra A] (e : A ≃⋆ₐ[ℂ] A) : congrAut e = congr e

@[simp]

theorem DoubleCentralizer.congr_coe {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) (a : A) : (congr e) (↑ℂ a) = ↑ℂ (e a)

The extension of e to multiplier algebras restricts to e on A.

theorem DoubleCentralizer.eq_congr_of_apply_coe {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {F : Type u_4} [FunLike F (DoubleCentralizer ℂ A) (DoubleCentralizer ℂ B)] [MulHomClass F (DoubleCentralizer ℂ A) (DoubleCentralizer ℂ B)] (e : A ≃⋆ₐ[ℂ] B) (φ : F) (hφ : ∀ (a : A), φ (↑ℂ a) = ↑ℂ (e a)) : ⇑φ = ⇑(congr e)

congr e is the unique multiplicative map of multiplier algebras extending e.

noncomputable def DoubleCentralizer.conjStarAlgAut {A : Type u_4} [NonUnitalCStarAlgebra A] : ↥(unitary (DoubleCentralizer ℂ A)) →* A ≃⋆ₐ[ℂ] A

Conjugation a ↦ u * a * u⋆ of A by a unitary multiplier u, as a star-algebra automorphism of A. Since A is an ideal of 𝓜(ℂ, A), this is the restriction to A of the inner automorphism Unitary.conjStarAlgAut ℂ 𝓜(ℂ, A) u of the multiplier algebra.

@[simp]

theorem DoubleCentralizer.coe_conjStarAlgAut_apply {A : Type u_4} [NonUnitalCStarAlgebra A] (u : ↥(unitary (DoubleCentralizer ℂ A))) (a : A) : ↑ℂ ((conjStarAlgAut u) a) = ↑u * ↑ℂ a * star ↑u

Conjugation by a unitary multiplier u sends a to u * a * u⋆, computed in the multiplier algebra.

theorem DoubleCentralizer.hasDerivAt_coe_iff {A : Type u_4} [NonUnitalCStarAlgebra A] {f : ℝ → A} {v : A} {x : ℝ} : HasDerivAt (fun (t : ℝ) => ↑ℂ (f t)) (↑ℂ v) x ↔ HasDerivAt f v x

A real path in A has derivative v exactly when its image in the multiplier algebra has derivative v: the inclusion A → 𝓜(ℂ, A) is a linear isometry.

theorem DoubleCentralizer.hasDerivAt_conj_zero {A : Type u_4} [NonUnitalCStarAlgebra A] {Q : A} (hQ : IsSelfAdjoint Q) {U : ℝ → DoubleCentralizer ℂ A} (hU₀ : U 0 = 1) (hU : HasDerivAt U (Complex.I • ↑ℂ Q) 0) {f g : ℝ → A} (hfg : ∀ (t : ℝ), ↑ℂ (g t) = U t * ↑ℂ (f t) * star (U t)) {v : A} (hf : HasDerivAt f v 0) : HasDerivAt g (v + Complex.I • (Q * f 0 - f 0 * Q)) 0

Conjugating a differentiable path in A by a path of multipliers U with U 0 = 1 and U' 0 = i Q, for self-adjoint Q ∈ A, adds the commutator i[Q, ·] to its derivative at 0.