Documentation

TauCeti.RepresentationTheory.Compact.BiregularRepresentation

The biregular representation of a compact group on L²(G) #

A compact group G acts on L²(G) from both sides, by TauCeti.leftRegularLp and TauCeti.rightRegularLp. The two actions commute, and this file bundles them into the biregular representation of G × G,

((g, h) · f) x = f (g⁻¹ * x * h).

Bi-translation preserves normalized Haar measure, so the action is unitary. It is also strongly continuous: the orbit map is continuous at every L² function, although for an infinite compact group the representation need not be continuous in the operator norm. This is the G × G-action used by the equivariant form of the Peter-Weyl decomposition.

Main definitions #

Main statements #

source
theorem TauCeti.measurePreserving_biTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g h : G) :
MeasureTheory.MeasurePreserving (fun (x : G) => g⁻¹ * x * h) (haarProb G) (haarProb G)

Bi-translation x ↦ g⁻¹ * x * h preserves normalized Haar measure.

source
noncomputable def TauCeti.biRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
ContRepresentation 𝕜 (G × G) ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The biregular representation of G × G on L²(G): (g, h) acts by f ↦ (x ↦ f (g⁻¹ * x * h)).

The two factors are ordered so that restricting along g ↦ (g, 1) gives TauCeti.leftRegularLp, while restricting along h ↦ (1, h) gives TauCeti.rightRegularLp.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.biRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (p : G × G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ((biRegularLp 𝕜 G) p) f = (MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => p.1⁻¹ * x * p.2) ⋯) f

    Bi-translation on L²(G), unfolded to the underlying Lp.compMeasurePreserving. The body of biRegularLp is not exposed, so this is the lemma that moves a statement between the representation and its raw Lp.compMeasurePreserving form.

    source
    theorem TauCeti.coeFn_biRegularLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (p : G × G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ↑↑(((biRegularLp 𝕜 G) p) f) =ᵐ[haarProb G] fun (x : G) => ↑↑f (p.1⁻¹ * x * p.2)

    Bi-translation on L²(G) is represented by bi-translation of functions.

    source
    @[simp]
    theorem TauCeti.biRegularLp_toLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (F : C(G, 𝕜)) (p : G × G) :
    ((biRegularLp 𝕜 G) p) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) F) = (ContinuousMap.toLp 2 (haarProb G) 𝕜) (F.comp { toFun := fun (x : G) => p.1⁻¹ * x * p.2, continuous_toFun := ⋯ })

    On a continuous function, the biregular representation is bi-translation.

    source
    @[simp]
    theorem TauCeti.biRegularLp_apply_mk_one {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ((biRegularLp 𝕜 G) (g, 1)) f = ((leftRegularLp 𝕜 G) g) f

    The first factor of the biregular representation is the left regular representation.

    source
    @[simp]
    theorem TauCeti.biRegularLp_apply_one_mk {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (h : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ((biRegularLp 𝕜 G) (1, h)) f = ((rightRegularLp 𝕜 G) h) f

    The second factor of the biregular representation is the right regular representation.

    source
    theorem TauCeti.biRegularLp_apply_eq_left_right {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (p : G × G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ((biRegularLp 𝕜 G) p) f = ((leftRegularLp 𝕜 G) p.1) (((rightRegularLp 𝕜 G) p.2) f)

    The biregular action is left translation after right translation.

    source
    theorem TauCeti.biRegularLp_apply_eq_right_left {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (p : G × G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    ((biRegularLp 𝕜 G) p) f = ((rightRegularLp 𝕜 G) p.2) (((leftRegularLp 𝕜 G) p.1) f)

    The biregular action is also right translation after left translation; in particular, its two factors commute.

    source
    theorem TauCeti.isUnitary_biRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (biRegularLp 𝕜 G).IsUnitary

    The biregular representation is unitary, because every bi-translation preserves normalized Haar measure.

    source
    theorem TauCeti.continuous_biRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) :
    Continuous fun (p : G × G) => ((biRegularLp 𝕜 G) p) f

    The biregular representation is strongly continuous: every orbit map (g, h) ↦ (g, h) · f is continuous.