Sums over the orbits of a free action

Let a finite group G act on a type α, and let B be a finite G-stable set of points, each with trivial stabilizer. Let M be an additive commutative monoid with scalar multiplication by G preserving addition and zero. A function f : α → M satisfying f (g • a) = g • f a on B then sums over B to a "trace":

∑_{a ∈ B} f a = ∑_{g ∈ G} g • w,

where w is the sum of f over a set of representatives of the orbits in B. Only the existence of w is recorded, together with the fact that it lies in the additive submonoid generated by the values of f on B, which is all a consumer needs to bound w. The proof peels off one free orbit at a time: the orbit of a is the image of g ↦ g • a, which is injective because the stabilizer of a is trivial, so the sum over it is ∑_{g} g • f a.

The application in mind is the expansion of a norm ∏_{g} (1 + g • x) for a group G of prime order acting on a ring: the subsets of G with at least two elements, other than G itself, form a free G-set under translation, and this lemma is what makes the corresponding terms of the expansion a trace.

Main results

• TauCeti.MulAction.exists_sum_eq_sum_smul_of_stabilizer_eq_bot: the sum of an equivariant function over a stable finite set of points with trivial stabilizers is the orbit sum of an element of the additive submonoid generated by its values.

theorem TauCeti.MulAction.exists_sum_eq_sum_smul_of_stabilizer_eq_bot {G : Type u_1} {α : Type u_2} {M : Type u_3} [Group G] [Fintype G] [MulAction G α] [AddCommMonoid M] [DistribSMul G M] {B : Finset α} (hB : ∀ (g : G), ∀ a ∈ B, g • a ∈ B) (hfree : ∀ a ∈ B, MulAction.stabilizer G a = ⊥) {f : α → M} (hf : ∀ (g : G), ∀ a ∈ B, f (g • a) = g • f a) : ∃ w ∈ AddSubmonoid.closure (f '' ↑B), ∑ a ∈ B, f a = ∑ g : G, g • w

A sum over a free G-set is a trace. Let B be a finite set of points stable under the finite group G, each with trivial stabilizer. Suppose scalar multiplication on the additive commutative monoid M preserves addition and zero, and f : α → M satisfies f (g • a) = g • f a on B. Then there is w in the additive submonoid generated by the values of f on B, with ∑_{a ∈ B} f a = ∑_{g ∈ G} g • w.