Documentation

TauCeti.Analysis.CStarAlgebra.UnitaryCharacter

Characters from unitary multipliers #

A unitary representation need not be continuous in the norm of a C⋆-algebra. Nevertheless, a character of a subalgebra detects a continuous circle-valued character whenever it is nonzero on an operator whose translates are norm continuous and belong to the subalgebra. The resulting character describes every translate that belongs to the subalgebra, so it is independent of the operator used to detect it.

This is the character-identification step in the spectral representation of a strongly continuous unitary representation, applied to a nonzero integrated operator.

References #

theorem MonoidHom.existsUnique_pontryaginDual_of_unitary_translate {G : Type u_1} {B : Type u_2} [Monoid G] [TopologicalSpace G] [CStarAlgebra B] (ρ : G →* B) (hρ : ∀ (g : G), ρ g ∈ unitary B) (A : StarSubalgebra ℂ B) [CompleteSpace ↥A] (a : ↥A) (hcomm : ∀ (g : G), Commute (ρ g) ↑a) (hmem : ∀ (g : G), ρ g * ↑a ∈ A) (hcont : Continuous fun (g : G) => ρ g * ↑a) (ω : ↑(WeakDual.characterSpace ℂ ↥A)) (ha : ω a ≠ 0) :
∃! χ : PontryaginDual G, ∀ (g : G) (b : ↥A) (hb : ρ g * ↑b ∈ A), ω ⟨ρ g * ↑b, hb⟩ = ↑(χ g) * ω b

A character nonzero on a commuting operator with norm-continuous unitary translates induces a unique continuous circle-valued character. It describes every translate in the subalgebra, not just the translates of the witnessing operator.