Regrouping a finite sum by the fibres of a map

A sum over a finite type can be taken fibrewise along any map out of it: sum over the values the map actually takes, and within each value over the indices sent there.

Mathlib's Fintype.sum_fiberwise says this with the outer sum ranging over the whole codomain, which needs the codomain finite. The version here indexes the outer sum by the image instead, so it applies to a map into an arbitrary type — the situation whenever the codomain is a quotient or a subtype with no finiteness available.

Main results

• TauCeti.sum_eq_sum_image_fiber: ∑ i, F i is the sum, over the values g takes, of the sums of F over the fibres of g.

theorem TauCeti.sum_eq_sum_image_fiber {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq κ] [AddCommMonoid M] (g : ι → κ) (F : ι → M) : ∑ i : ι, F i = ∑ k ∈ Finset.image g Finset.univ, ∑ i : { i : ι // g i = k }, F ↑i

A finite sum is the sum over the values actually taken of the sums over their fibres. Summing F over all of ι is summing, over each k in the image of g, the contribution of the indices g sends to k.

The outer index is Finset.univ.image g rather than all of κ, so no finiteness of κ is needed; that is the difference from Fintype.sum_fiberwise.