Nondegenerate representations and their extension to multipliers

A representation π : A →⋆ₙₐ[ℂ] (H →L[ℂ] H) of a possibly nonunital C⋆-algebra on a Hilbert space is nondegenerate when the vectors π a ξ span a dense subspace of H. Equivalently, no nonzero vector is annihilated by every π a, and π e ξ → ξ along an increasing approximate unit.

A nondegenerate representation extends uniquely to a unital star-algebra homomorphism π' := π.multiplierExtension hπ : 𝓜(ℂ, A) →⋆ₐ[ℂ] (H →L[ℂ] H) of the multiplier algebra. It is characterized by π' m * π a = π (m * a), and it is the strong limit of π (m * e) along an increasing approximate unit e. This extension is how covariant pairs (π, U) with unitary multipliers U_s are obtained from nondegenerate representations of crossed products.

Main declarations

• NonUnitalStarAlgHom.IsNondegenerate: density of the span of the vectors π a ξ, unfolded by isNondegenerate_iff_dense.
• NonUnitalStarAlgHom.isNondegenerate_iff_forall_apply_eq_zero: nondegeneracy means that no nonzero vector is killed by the whole representation.
• NonUnitalStarAlgHom.isNondegenerate_iff_tendsto: nondegeneracy means that the representation of an increasing approximate unit converges strongly to the identity.
• NonUnitalStarAlgHom.multiplierExtension: the extension to the multiplier algebra, with its characterizing identities multiplierExtension_mul_eq_fst and mul_multiplierExtension_eq_snd, the uniqueness statement eq_multiplierExtension_of_apply_coe, and the strong-limit formula tendsto_multiplierExtension_apply.

References

• Dana Williams, Crossed Products of C-Algebras*, Section 1.1 and Proposition 2.39.
• Iain Raeburn and Dana Williams, Morita Equivalence and Continuous-Trace C-Algebras*, Corollary 2.51.

def NonUnitalStarAlgHom.IsNondegenerate {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₙₐ[ℂ] H →L[ℂ] H) : Prop

A representation of a C⋆-algebra on a Hilbert space is nondegenerate when the vectors π a ξ span a dense subspace.

theorem NonUnitalStarAlgHom.isNondegenerate_iff_dense {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} : π.IsNondegenerate ↔ Dense ↑(Submodule.span ℂ (⋃ (a : A), Set.range ⇑(π a)))

Unfolding lemma: nondegeneracy is density of the span of the vectors π a ξ.

theorem NonUnitalStarAlgHom.IsNondegenerate.ext {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) {S T : H →L[ℂ] H} (h : ∀ (a : A), S * π a = T * π a) : S = T

Operators agreeing after composition with every operator of a nondegenerate representation are equal.

theorem NonUnitalStarAlgHom.isNondegenerate_of_map_one {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {B : Type u_3} [CStarAlgebra B] {ρ : B →⋆ₙₐ[ℂ] H →L[ℂ] H} (hρ : ρ 1 = 1) : ρ.IsNondegenerate

A representation of a unital C⋆-algebra sending the identity to the identity operator is nondegenerate.

noncomputable def NonUnitalStarAlgHom.multiplierExtension {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) : DoubleCentralizer ℂ A →⋆ₐ[ℂ] H →L[ℂ] H

The extension of a nondegenerate representation to the multiplier algebra: the unique operator π' m with π' m * π a = π (m * a) for every a.

@[simp]

theorem NonUnitalStarAlgHom.multiplierExtension_mul_eq_fst {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) (m : DoubleCentralizer ℂ A) (a : A) : (multiplierExtension hπ) m * π a = π (m.toProd.1 a)

The defining identity π' m * π a = π (m * a) of the multiplier extension.

@[simp]

theorem NonUnitalStarAlgHom.mul_multiplierExtension_eq_snd {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) (m : DoubleCentralizer ℂ A) (a : A) : π a * (multiplierExtension hπ) m = π (m.toProd.2 a)

The right-handed identity π a * π' m = π (a * m) of the multiplier extension.

@[simp]

theorem NonUnitalStarAlgHom.multiplierExtension_apply_apply {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) (m : DoubleCentralizer ℂ A) (a : A) (ξ : H) : ((multiplierExtension hπ) m) ((π a) ξ) = (π (m.toProd.1 a)) ξ

The multiplier extension sends π a ξ to π (m * a) ξ.

theorem NonUnitalStarAlgHom.eq_multiplierExtension_iff {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) {m : DoubleCentralizer ℂ A} {T : H →L[ℂ] H} : T = (multiplierExtension hπ) m ↔ ∀ (a : A), T * π a = π (m.toProd.1 a)

An operator equals π' m exactly when it satisfies the defining identity.

@[simp]

theorem NonUnitalStarAlgHom.multiplierExtension_coe {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) (a : A) : (multiplierExtension hπ) (↑ℂ a) = π a

The multiplier extension restricts to π on A.

theorem NonUnitalStarAlgHom.eq_multiplierExtension_of_apply_coe {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) {F : Type u_3} [FunLike F (DoubleCentralizer ℂ A) (H →L[ℂ] H)] [MulHomClass F (DoubleCentralizer ℂ A) (H →L[ℂ] H)] (ψ : F) (hψ : ∀ (a : A), ψ (↑ℂ a) = π a) : ⇑ψ = ⇑(multiplierExtension hπ)

The multiplier extension is the only multiplicative map on 𝓜(ℂ, A) extending π.

theorem NonUnitalStarAlgHom.tendsto_multiplierExtension_apply {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) [PartialOrder A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) (m : DoubleCentralizer ℂ A) (ξ : H) : Filter.Tendsto (fun (e : A) => (π (m.toProd.1 e)) ξ) l (nhds (((multiplierExtension hπ) m) ξ))

Along an increasing approximate unit e, the operators π (m * e) converge strongly to the multiplier extension π' m.

theorem NonUnitalStarAlgHom.continuous_multiplierExtension_apply {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} (hπ : π.IsNondegenerate) {X : Type u_3} [TopologicalSpace X] {u : X → DoubleCentralizer ℂ A} (hu : ∀ (a : A), Continuous fun (x : X) => (u x).toProd.1 a) {C : ℝ} (hC : ∀ (x : X), ‖u x‖ ≤ C) (ξ : H) : Continuous fun (x : X) => ((multiplierExtension hπ) (u x)) ξ

Strict continuity of a norm-bounded family of multipliers gives strong continuity of its image under the multiplier extension: if x ↦ u x * a is norm continuous for every a and ‖u x‖ ≤ C, then x ↦ π' (u x) ξ is continuous for every vector ξ. Only the left half of strict continuity is needed. This applies to strictly continuous unitary multiplier groups.

theorem NonUnitalStarAlgHom.isNondegenerate_iff_tendsto {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} [PartialOrder A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : π.IsNondegenerate ↔ ∀ (ξ : H), Filter.Tendsto (fun (e : A) => (π e) ξ) l (nhds ξ)

A representation is nondegenerate exactly when the representation of an increasing approximate unit converges strongly to the identity.

theorem NonUnitalStarAlgHom.isNondegenerate_iff_forall_apply_eq_zero {A : Type u_1} {H : Type u_2} [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₙₐ[ℂ] H →L[ℂ] H} : π.IsNondegenerate ↔ ∀ (ξ : H), (∀ (a : A), (π a) ξ = 0) → ξ = 0

A representation is nondegenerate exactly when no nonzero vector is annihilated by every operator of the representation.