Coefficient and group multipliers of twisted convolution

Let α be a point-norm continuous action of a topological group G on a C⋆-algebra A. The coefficient algebra and the group act on C_c(G, A) on the left by

(a • f) s = a * f s and (r • f) s = α r (f (r⁻¹ * s)),

the second being CStarAction.translate. These are the formulas of Williams's canonical maps i_A(a) and i_G(r) into the multiplier algebra of the crossed product, evaluated on the dense subalgebra C_c(G, A). Both commute with twisted convolution in the first variable, (a • f) ⋆ g = a • (f ⋆ g) and (r • f) ⋆ g = r • (f ⋆ g); the second identity needs a left-invariant measure. The coefficient action is Mathlib's pointwise scalar action of A on C_c(G, A), and its identity TauCeti.CStarAction.smul_convolution lives beside the convolution itself, so only the group action and its identity are developed here.

An integrated covariant representation turns these multipliers into its coefficient and group operators; this is how a covariant pair is recovered from its integrated form.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2, where these are the maps i_A and i_G.

Main definitions

• TauCeti.CStarAction.translate: the left action (r • f) s = α r (f (r⁻¹ * s)) of G on C_c(G, A).

Main statements

• TauCeti.CStarAction.translate_convolution: (r • f) ⋆ g = r • (f ⋆ g).

noncomputable def TauCeti.CStarAction.translate {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) [ContinuousMul G] (r : G) : CompactlySupportedContinuousMap G A →ₗ[ℂ] CompactlySupportedContinuousMap G A

The left action of G on C_c(G, A) twisted by α: (r • f) s = α r (f (r⁻¹ * s)).

@[simp]

theorem TauCeti.CStarAction.translate_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) [ContinuousMul G] (r : G) (f : CompactlySupportedContinuousMap G A) (s : G) : ((α.translate r) f) s = (α r) (f (r⁻¹ * s))

@[simp]

theorem TauCeti.CStarAction.translate_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) [ContinuousMul G] (f : CompactlySupportedContinuousMap G A) : (α.translate 1) f = f

The identity translates trivially.

theorem TauCeti.CStarAction.translate_mul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) [ContinuousMul G] (r t : G) (f : CompactlySupportedContinuousMap G A) : (α.translate (r * t)) f = (α.translate r) ((α.translate t) f)

The twisted translations form a left action of G.

theorem TauCeti.CStarAction.translate_convolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasurableMul G] [μ.IsMulLeftInvariant] (r : G) (f g : CompactlySupportedContinuousMap G A) : ((α.convolution μ) ((α.translate r) f)) g = (α.translate r) (((α.convolution μ) f) g)

The twisted left translation commutes with twisted convolution with respect to a left-invariant measure.