Coset sums of coinduced invariants

For a continuous representation π of G on V, Mathlib's coinduced representation π.coind₁ acts on C(G, V) by (g • f) x = π g (f (g⁻¹ * x)), so an invariant f satisfies π g (f x) = f (g * x). Evaluation at a point does not carry invariants of π.coind₁ to invariants of π, but a sum of evaluations over a transversal of a finite-index subgroup U does, as soon as f is invariant under right translation by U: left multiplication by g permutes the cosets of U, and right translation by U absorbs the change of representatives.

Main results

• ContRepresentation.sum_apply_out_mem_invariants: summing an invariant element of the coinduced representation C(G, V) over a transversal of a finite-index subgroup stabilizing it under right translation gives an invariant element of V.

theorem ContRepresentation.sum_apply_out_mem_invariants {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul R V] {π : ContRepresentation R G V} {f : C(G, V)} (hf : f ∈ π.coind₁.invariants) {U : Subgroup G} [Fintype (G ⧸ U)] (hU : U ≤ TauCeti.rightTranslationStabilizer ⇑f) : ∑ q : G ⧸ U, f (Quotient.out q) ∈ π.invariants

Coset sums of coinduced invariants are invariant. Let f : C(G, V) be invariant for the coinduced representation π.coind₁ and invariant under right translation by a finite-index subgroup U. Then the sum of f over the transversal of U given by Quotient.out is invariant for π.