Sums over a choice of representatives

Given a map π : α → β onto a finite type, a right inverse r of π chooses a representative r b of each fibre, and ∑ b, T (r b) sums a function T : α → A over these representatives. Such sums typically come with a proof that they do not depend on the choice, for instance when π is the projection onto a quotient such as the double cosets H \ G / K.

If they do not, and A is cancellative, then T itself is constant on the fibres of π: comparing a fixed choice with the one that replaces the representative of a single fibre leaves only the two terms at that fibre.

Main statements

• Function.RightInverse.eq_of_sum_eq: a function whose sums over the representatives chosen by the right inverses of π all agree is constant on the fibres of π.

theorem Function.RightInverse.eq_of_sum_eq {α : Type u_1} {β : Type u_2} {A : Type u_3} [Fintype β] [AddCancelCommMonoid A] {π : α → β} {r₀ : β → α} (hr₀ : RightInverse r₀ π) (T : α → A) (hT : ∀ (r : β → α), RightInverse r π → ∑ b : β, T (r b) = ∑ b : β, T (r₀ b)) {a a' : α} (h : π a = π a') : T a = T a'

A function is constant on fibres if its sums over representatives are: if the sum over a finite type β of the values of T at the representatives r b chosen by a right inverse r of π : α → β does not depend on r, then T a = T a' whenever π a = π a'.