The convolution ⋆-algebra of a C⋆-dynamical system

For a point-norm continuous action α of a locally compact group G on a C⋆-algebra A and a left-invariant measure μ on G, the compactly supported continuous functions C_c(G, A) form a complex ⋆-algebra under the twisted convolution

(f ⋆ g) s = ∫ r, f r * α r (g (r⁻¹ * s)) ∂μ

and the twisted involution f* s = c(s) • α s (star (f s⁻¹)), where c is Mathlib's modular character. This is the dense ⋆-algebra whose completions in the universal and regular norms are the full and reduced crossed products of (A, G, α).

The essential identity is that the twisted involution reverses twisted convolution, (f ⋆ g)* = g* ⋆ f*, twistedInvolution_convolution. Its proof uses only left invariance of μ and multiplicativity of c, so no relation between μ and c is needed here. The modular character is matched with μ only when the involution is compared with the L¹ norm.

The ⋆-algebra is the type ConvolutionAlgebra α μ, a one-field structure wrapping C_c(G, A). A separate type is needed because C_c(G, A) already carries the pointwise product and star, and because the product and star depend on α and μ. The maps ConvolutionAlgebra.toConv and ConvolutionAlgebra.ofConv pass between the two types, following Mathlib's WithConv. Distributivity and the scalar compatibilities hold for any measure finite on compacts. Associativity, and hence the NonUnitalRing and StarRing structures, uses left invariance. No unit, separability, or σ-finiteness is assumed.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2.

Main definitions

• TauCeti.CStarAction.ConvolutionAlgebra: the convolution ⋆-algebra on C_c(G, A).

Main statements

• TauCeti.CStarAction.twistedInvolution_convolution: (f ⋆ g)* = g* ⋆ f*.
• TauCeti.CStarAction.ConvolutionAlgebra.instNonUnitalRing: twisted convolution makes ConvolutionAlgebra α μ a nonunital ring, and a complex algebra in the sense of IsScalarTower and SMulCommClass.
• TauCeti.CStarAction.ConvolutionAlgebra.instStarRing: the twisted involution makes it a ⋆-ring, and it is a ⋆-module over ℂ.
• TauCeti.CStarAction.ConvolutionAlgebra.ofConv_mul_smulRight_apply: the formula for the right product f ⋆ (φ ⊗ e) with an elementary function, after the substitution r = s * t⁻¹.

The involution reverses twisted convolution

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

The twisted involution reverses twisted convolution with respect to a left-invariant measure: (f ⋆ g)* = g* ⋆ f*.

The convolution algebra

structure TauCeti.CStarAction.ConvolutionAlgebra {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) : Type (max u_1 u_2)

The convolution ⋆-algebra of the C⋆-dynamical system (A, G, α) with respect to μ: the compactly supported continuous functions G → A, with twisted convolution as product and the twisted involution as star. Use ConvolutionAlgebra.toConv and ConvolutionAlgebra.ofConv to pass to and from C_c(G, A), whose own product and star are pointwise.

• toConv :: (
• ofConv : CompactlySupportedContinuousMap G A

  The compactly supported function underlying an element of the convolution algebra.

• )

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_toConv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : CompactlySupportedContinuousMap G A) : { ofConv := f }.ofConv = f

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_ofConv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : α.ConvolutionAlgebra μ) : { ofConv := f.ofConv } = f

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_injective {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : Function.Injective ofConv

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_injective {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : Function.Injective toConv

theorem TauCeti.CStarAction.ConvolutionAlgebra.ext {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} {f g : α.ConvolutionAlgebra μ} (h : f.ofConv = g.ofConv) : f = g

theorem TauCeti.CStarAction.ConvolutionAlgebra.ext_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} {f g : α.ConvolutionAlgebra μ} : f = g ↔ f.ofConv = g.ofConv

def TauCeti.CStarAction.ConvolutionAlgebra.equiv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) : α.ConvolutionAlgebra μ ≃ CompactlySupportedContinuousMap G A

ConvolutionAlgebra.ofConv and ConvolutionAlgebra.toConv as an equivalence.

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.equiv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : α.ConvolutionAlgebra μ) : (equiv α μ) f = f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.equiv_symm_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : CompactlySupportedContinuousMap G A) : (equiv α μ).symm f = { ofConv := f }

@[instance_reducible]

instance TauCeti.CStarAction.ConvolutionAlgebra.instAddCommGroup {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : AddCommGroup (α.ConvolutionAlgebra μ)

def TauCeti.CStarAction.ConvolutionAlgebra.addEquiv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) : α.ConvolutionAlgebra μ ≃+ CompactlySupportedContinuousMap G A

ConvolutionAlgebra.ofConv as an additive equivalence with C_c(G, A).

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.addEquiv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : α.ConvolutionAlgebra μ) : (addEquiv α μ) f = f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.addEquiv_symm_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : CompactlySupportedContinuousMap G A) : (addEquiv α μ).symm f = { ofConv := f }

@[instance_reducible]

instance TauCeti.CStarAction.ConvolutionAlgebra.instModuleComplex {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : Module ℂ (α.ConvolutionAlgebra μ)

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_zero {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : ofConv 0 = 0

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_add {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f g : α.ConvolutionAlgebra μ) : (f + g).ofConv = f.ofConv + g.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_neg {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : α.ConvolutionAlgebra μ) : (-f).ofConv = -f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_sub {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f g : α.ConvolutionAlgebra μ) : (f - g).ofConv = f.ofConv - g.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_smul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (c : ℂ) (f : α.ConvolutionAlgebra μ) : (c • f).ofConv = c • f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_zero {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} : { ofConv := 0 } = 0

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_add {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f g : CompactlySupportedContinuousMap G A) : { ofConv := f + g } = { ofConv := f } + { ofConv := g }

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_neg {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : CompactlySupportedContinuousMap G A) : { ofConv := -f } = -{ ofConv := f }

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_sub {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f g : CompactlySupportedContinuousMap G A) : { ofConv := f - g } = { ofConv := f } - { ofConv := g }

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_smul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (c : ℂ) (f : CompactlySupportedContinuousMap G A) : { ofConv := c • f } = c • { ofConv := f }

def TauCeti.CStarAction.ConvolutionAlgebra.linearEquiv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) : α.ConvolutionAlgebra μ ≃ₗ[ℂ] CompactlySupportedContinuousMap G A

ConvolutionAlgebra.ofConv as a complex linear equivalence with C_c(G, A).

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.linearEquiv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : α.ConvolutionAlgebra μ) : (linearEquiv α μ) f = f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.linearEquiv_symm_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (f : CompactlySupportedContinuousMap G A) : (linearEquiv α μ).symm f = { ofConv := f }

noncomputable def TauCeti.CStarAction.ConvolutionAlgebra.smulRight {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (φ : CompactlySupportedContinuousMap G ℝ) (e : A) : α.ConvolutionAlgebra μ

The elementary function s ↦ φ s • e of a real compactly supported function φ and a coefficient e, as an element of the convolution algebra.

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_smulRight_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} (φ : CompactlySupportedContinuousMap G ℝ) (e : A) (s : G) : (smulRight φ e).ofConv s = φ s • e

Convolution product

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instMul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : Mul (α.ConvolutionAlgebra μ)

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_mul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : α.ConvolutionAlgebra μ) : (f * g).ofConv = ((α.convolution μ) f.ofConv) g.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_convolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : CompactlySupportedContinuousMap G A) : { ofConv := ((α.convolution μ) f) g } = { ofConv := f } * { ofConv := g }

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instNonUnitalNonAssocRing {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : NonUnitalNonAssocRing (α.ConvolutionAlgebra μ)

instance TauCeti.CStarAction.ConvolutionAlgebra.instIsScalarTowerComplex {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : IsScalarTower ℂ (α.ConvolutionAlgebra μ) (α.ConvolutionAlgebra μ)

instance TauCeti.CStarAction.ConvolutionAlgebra.instSMulCommClassComplex {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : SMulCommClass ℂ (α.ConvolutionAlgebra μ) (α.ConvolutionAlgebra μ)

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instNonUnitalRing {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [OpensMeasurableSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasurableMul G] [μ.IsMulLeftInvariant] : NonUnitalRing (α.ConvolutionAlgebra μ)

Products with elementary functions

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_mul_smulRight_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] [BorelSpace G] [μ.IsHaarMeasure] (f : α.ConvolutionAlgebra μ) (φ : CompactlySupportedContinuousMap G ℝ) (e : A) (s : G) : (f * smulRight φ e).ofConv s = ∫ (t : G), φ t • ↑(MeasureTheory.Measure.modularCharacter t) • (f.ofConv (s * t⁻¹) * (α (s * t⁻¹)) e) ∂μ

The right product with an elementary function, after substituting r = s * t⁻¹: (f ⋆ (φ ⊗ e)) s = ∫ t, φ t • c(t) • (f (s * t⁻¹) * α (s * t⁻¹) e) ∂μ.

Twisted involution

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instStar {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] : Star (α.ConvolutionAlgebra μ)

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.ofConv_star {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] (f : α.ConvolutionAlgebra μ) : (star f).ofConv = α.twistedInvolution f.ofConv

@[simp]

theorem TauCeti.CStarAction.ConvolutionAlgebra.toConv_twistedInvolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] (f : CompactlySupportedContinuousMap G A) : { ofConv := α.twistedInvolution f } = star { ofConv := f }

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instInvolutiveStar {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] : InvolutiveStar (α.ConvolutionAlgebra μ)

instance TauCeti.CStarAction.ConvolutionAlgebra.instStarModuleComplex {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] : StarModule ℂ (α.ConvolutionAlgebra μ)

@[instance_reducible]

noncomputable instance TauCeti.CStarAction.ConvolutionAlgebra.instStarRing {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] {α : CStarAction G A} {μ : MeasureTheory.Measure G} [IsTopologicalGroup G] [LocallyCompactSpace G] [OpensMeasurableSpace G] [MeasurableMul G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsMulLeftInvariant] : StarRing (α.ConvolutionAlgebra μ)