Documentation

TauCeti.Analysis.CStarAlgebra.Action.Covariant.Regular

Regular covariant representations #

Let α be a point-norm continuous action of a topological group G on a possibly nonunital C⋆-algebra A, let ρ be a representation of A on a Hilbert space H, and let μ be a left-invariant measure on G, typically a left Haar measure. The regular covariant representation induced by ρ acts on L²(G, H) by

π(a) ξ (r) = ρ (α_{r⁻¹}(a)) (ξ r) and λ_s ξ (r) = ξ (s⁻¹ r).

The coefficient representation π is multiplication by the bounded continuous operator-valued function r ↦ ρ (α_{r⁻¹}(a)), so it is a ⋆-homomorphism; the group representation λ is the left regular representation, which is unitary and strongly continuous. The pair is covariant: λ_s π(a) λ_s⁻¹ = π(α_s(a)). Integrating it gives the regular representations of the convolution algebra, whose norms define the reduced crossed product.

The representation ρ need not be nondegenerate or faithful, and no separability, second countability, or σ-finiteness is assumed: the measure need only be left invariant, locally finite, and inner regular with respect to compact sets on sets of finite measure, as the Haar measure MeasureTheory.Measure.haar of a locally compact group is.

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

Main definitions #

If ρ is nondegenerate, so is the regular coefficient representation π, and conversely when μ is positive on nonempty open sets. Thus a nondegenerate representation of A induces a nondegenerate regular covariant pair, which is the kind of pair whose integrated form is a nondegenerate representation of the crossed product and extends to its multiplier algebra.

The integrated regular representation π ⋊ λ of C_c(G, A) has the matrix coefficients ⟪η, (π ⋊ λ)(f) ξ⟫ = ∫ s, ∫ r, ⟪η r, ρ (α_{r⁻¹}(f s)) (ξ (s⁻¹ r))⟫ dr ds. If ρ is faithful and μ is positive on nonempty open sets, then π ⋊ λ is injective on C_c(G, A): testing against scalar multiples of fixed vectors by continuous compactly supported functions recovers every matrix coefficient ⟪w, ρ (f s) v⟫. Hence integrated norms of regular representations are norms, not merely seminorms, on the convolution algebra.

Main statements #

source
noncomputable def TauCeti.CStarAction.CovariantRepresentation.regular {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (α : CStarAction G A) (ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H) (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] :
α.CovariantRepresentation ↥(MeasureTheory.Lp H 2 μ)

The regular covariant representation on L²(G, H) induced by a representation ρ of A on H: a acts by ξ ↦ (r ↦ ρ (α_{r⁻¹}(a)) (ξ r)) and s by left translation ξ ↦ (r ↦ ξ (s⁻¹ r)).

Instances For
    source
    @[simp]
    theorem TauCeti.CStarAction.CovariantRepresentation.regular_group {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (α : CStarAction G A) (ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H) (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] :
    (regular α ρ μ).group = MeasureTheory.Measure.leftRegular ℂ H μ 2

    The group representation of the regular covariant representation is the left regular representation.

    source
    theorem TauCeti.CStarAction.CovariantRepresentation.coeFn_regular_coefficient {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (α : CStarAction G A) (ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H) (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] (a : A) (ξ : ↥(MeasureTheory.Lp H 2 μ)) :
    ↑↑(((regular α ρ μ).coefficient a) ξ) =ᵐ[μ] fun (r : G) => (ρ ((α r⁻¹) a)) (↑↑ξ r)

    The coefficient representation of the regular covariant representation acts by π(a) ξ (r) = ρ (α_{r⁻¹}(a)) (ξ r) almost everywhere.

    source
    theorem TauCeti.CStarAction.CovariantRepresentation.regular_coefficient_eq_iff {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {α : CStarAction G A} {ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H} {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] {a : A} {ξ η : ↥(MeasureTheory.Lp H 2 μ)} :
    ((regular α ρ μ).coefficient a) ξ = η ↔ (fun (r : G) => (ρ ((α r⁻¹) a)) (↑↑ξ r)) =ᵐ[μ] ↑↑η

    The coefficient representation of the regular covariant representation is determined by its pointwise formula: an L² class equal almost everywhere to r ↦ ρ (α_{r⁻¹}(a)) (ξ r) is π(a) ξ.

    source
    theorem TauCeti.CStarAction.CovariantRepresentation.isNondegenerate_regular_coefficient {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {α : CStarAction G A} {ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H} {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] (hρ : ρ.IsNondegenerate) :
    (regular α ρ μ).coefficient.IsNondegenerate

    The regular coefficient representation induced by a nondegenerate representation ρ is nondegenerate.

    source
    @[simp]
    theorem TauCeti.CStarAction.CovariantRepresentation.isNondegenerate_regular_coefficient_iff {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {α : CStarAction G A} {ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H} {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] :
    (regular α ρ μ).coefficient.IsNondegenerate ↔ ρ.IsNondegenerate

    For a measure positive on nonempty open sets, such as a Haar measure, the regular coefficient representation induced by ρ is nondegenerate exactly when ρ is.

    source
    theorem TauCeti.CStarAction.CovariantRepresentation.inner_integratedOperator_regular_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {α : CStarAction G A} {ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H} {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] (f : CompactlySupportedContinuousMap G A) (η ξ : ↥(MeasureTheory.Lp H 2 μ)) :
    inner ℂ η ((((regular α ρ μ).integratedOperator μ) f) ξ) = ∫ (s : G), ∫ (r : G), inner ℂ (↑↑η r) ((ρ ((α r⁻¹) (f s))) (↑↑ξ (s⁻¹ * r))) ∂μ ∂μ

    Matrix coefficients of the integrated regular representation: for f ∈ C_c(G, A) and ξ, η ∈ L²(G, H), ⟪η, (π ⋊ λ)(f) ξ⟫ = ∫ s, ∫ r, ⟪η r, ρ (α_{r⁻¹}(f s)) (ξ (s⁻¹ r))⟫ dr ds.

    source
    theorem TauCeti.CStarAction.CovariantRepresentation.injective_integratedOperator_regular {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {α : CStarAction G A} {ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H} {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hρ : Function.Injective ⇑ρ) :
    Function.Injective ⇑((regular α ρ μ).integratedOperator μ)

    The integrated regular representation induced by a faithful representation ρ of A is injective on C_c(G, A), for a measure positive on nonempty open sets such as a Haar measure.