Documentation

TauCeti.Analysis.CStarAlgebra.Action.Involution

The twisted involution on compactly supported coefficient functions #

For a point-norm continuous action α on a possibly nonunital C⋆-algebra, the twisted involution sends f to s ↦ c(s) • α s (star (f s⁻¹)), where c is Mathlib's modular character. It preserves continuity and compact support, is conjugate-linear, and squares to the identity. Its support is exactly the inverse of the original support.

The operation is named rather than installed as a Star instance: compactly supported continuous maps already carry a different, pointwise star operation. These functions and this involution are the dense coefficient space for crossed-product convolution algebras. Compatibility with twisted convolution is proved in TauCeti.Analysis.CStarAlgebra.Action.Convolution.Algebra; this file says nothing about the L¹ norm.

The convention follows Dana Williams, Crossed Products of C-Algebras*, Chapter 2: Mathlib's c(s) is Williams's Δ(s)⁻¹.

source
noncomputable def TauCeti.CStarAction.twistedInvolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) :
CompactlySupportedContinuousMap G A →ₗ⋆[ℂ] CompactlySupportedContinuousMap G A

The twisted, conjugate-linear involution on compactly supported coefficient functions.

Instances For
    source
    @[simp]
    theorem TauCeti.CStarAction.twistedInvolution_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) (s : G) :
    (α.twistedInvolution f) s = ↑↑(MeasureTheory.Measure.modularCharacter s) • (α s) (star (f s⁻¹))

    The pointwise formula, using the inverse of Williams's modular function.

    source
    @[simp]
    theorem TauCeti.CStarAction.twistedInvolution_twistedInvolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) :
    α.twistedInvolution (α.twistedInvolution f) = f

    Applying the twisted involution twice recovers the original coefficient function.

    source
    @[simp]
    theorem TauCeti.CStarAction.norm_twistedInvolution_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) (s : G) :
    ‖(α.twistedInvolution f) s‖ = ↑(MeasureTheory.Measure.modularCharacter s) * ‖f s⁻¹‖

    The norm of an involuted coefficient includes precisely the modular weight.

    source
    @[simp]
    theorem TauCeti.CStarAction.twistedInvolution_apply_eq_zero_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) (s : G) :
    (α.twistedInvolution f) s = 0 ↔ f s⁻¹ = 0

    Involution vanishes at s exactly when the original function vanishes at s⁻¹.

    source
    @[simp]
    theorem TauCeti.CStarAction.support_twistedInvolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) :
    Function.support ⇑(α.twistedInvolution f) = (Function.support ⇑f)⁻¹

    The support of the twisted involution is the inverse support.

    source
    @[simp]
    theorem TauCeti.CStarAction.tsupport_twistedInvolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f : CompactlySupportedContinuousMap G A) :
    tsupport ⇑(α.twistedInvolution f) = (tsupport ⇑f)⁻¹

    The topological support of the twisted involution is the inverse topological support.