Representations on functions and averaging with a cutoff function

Let a group G act on a type X and linearly on a module A through ρ. Then G acts on the functions X → A by translating the argument and acting on the values, $$(g \cdot \varphi)(x) = \rho(g)\bigl(\varphi(g^{-1} \cdot x)\bigr),$$ the representation Representation.funLeft ρ X. For the trivial action on A this is the translation of functions on a G-space. Through Finsupp.lift it is isomorphic to Representation.linHom (Representation.ofMulAction k G X) ρ; the function model is the one on which a weight c : X → k acts pointwise. A function is invariant exactly when φ (g • x) = ρ g (φ x) for all g and x (Representation.mem_invariants_funLeft_iff).

A function c : X → k whose translates sum to one, ∑ᶠ g, c (g • x) = 1 for every x, such as a cutoff function of a proper action of a discrete group, replaces the normalized group sum of a finite group. The cutoff average $$(Q\varphi)(x) = \sum_{g \in G} c(g \cdot x)\, \rho(g)^{-1}\bigl(\varphi(g \cdot x)\bigr)$$ is a projection onto the invariants (Representation.isProj_cutoffAverage). The group G need not be finite and the action need not be faithful; every element of G is counted. For a finite group and the constant function |G|⁻¹ it is the average over the group, the analogue of Representation.averageMap. The hypothesis on c forces each sum to have finitely many nonzero terms (hasFiniteSupport_of_finsum_eq_one).

Main declarations

• Representation.funLeft ρ X: the representation of G on X → A.
• Representation.mem_invariants_funLeft_iff: the invariant functions.
• Representation.cutoffAverage: the average of a function against a function c whose translates sum to one.
• Representation.isProj_cutoffAverage: the cutoff average is a projection onto the invariants.
• Representation.cutoffAverage_comp: naturality for pullback along equivariant maps.

References

• M. Crainic, Differentiable and algebroid cohomology, van Est isomorphisms, and characteristic classes, Comment. Math. Helv. 78 (2003), Section 2, for averaging with cutoff functions of proper groupoids.

def Representation.funLeft {k : Type u_1} {G : Type u_2} {A : Type u_3} [Semiring k] [Group G] [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (X : Type u_4) [MulAction G X] : Representation k G (X → A)

The representation of G on functions X → A that translates the argument and acts on the values: (g • φ) x = ρ g (φ (g⁻¹ • x)).

@[simp]

theorem Representation.funLeft_apply {k : Type u_1} {G : Type u_2} {A : Type u_3} [Semiring k] [Group G] [AddCommMonoid A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] (g : G) (φ : X → A) (x : X) : ((ρ.funLeft X) g) φ x = (ρ g) (φ (g⁻¹ • x))

noncomputable def Representation.cutoffAverage {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : (X → A) →ₗ[k] X → A

The average x ↦ ∑ᶠ g, c (g • x) • ρ g⁻¹ (φ (g • x)) of a function φ : X → A against a function c whose translates sum to one. It is a projection onto the invariants of Representation.funLeft ρ X (Representation.isProj_cutoffAverage).

@[simp]

theorem Representation.cutoffAverage_apply {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (φ : X → A) (x : X) : (ρ.cutoffAverage hc) φ x = ∑ᶠ (g : G), c (g • x) • (ρ g⁻¹) (φ (g • x))

theorem Representation.cutoffAverage_comp {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] {c : X → k} {Y : Type u_5} [MulAction G Y] (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (π : Y →ₑ[id] X) (hc' : ∀ (y : Y), ∑ᶠ (g : G), (c ∘ ⇑π) (g • y) = 1) (φ : X → A) : (ρ.cutoffAverage hc') (φ ∘ ⇑π) = (ρ.cutoffAverage hc) φ ∘ ⇑π

Naturality of the cutoff average for pullback. Pulling a function back along an equivariant map π : Y → X commutes with the cutoff average, for the pulled-back weight c ∘ π.

theorem Representation.mem_invariants_funLeft_iff {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommRing k] [Group G] [AddCommGroup A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] {φ : X → A} : φ ∈ (ρ.funLeft X).invariants ↔ ∀ (g : G) (x : X), φ (g • x) = (ρ g) (φ x)

A function φ : X → A is invariant under Representation.funLeft ρ X exactly when it is equivariant, φ (g • x) = ρ g (φ x).

theorem Representation.isProj_cutoffAverage {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommRing k] [Group G] [AddCommGroup A] [Module k A] (ρ : Representation k G A) {X : Type u_4} [MulAction G X] {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : LinearMap.IsProj (ρ.funLeft X).invariants (ρ.cutoffAverage hc)

The cutoff average is a projection onto the invariants. Its values are invariant functions, and it fixes every invariant function.