Sums over ι → ZMod n along reduction and multiplication

For n = m * k, the coordinatewise reduction (ι → ZMod n) → (ι → ZMod k) is a surjective additive homomorphism whose fibers have m ^ #ι elements, so summing a function of the reduction over ι → ZMod n counts every value m ^ #ι times. Dually, the vectors of ι → ZMod n killed by m are exactly the images of ι → ZMod m under the coordinatewise multiplication by k (ZMod.mulCastHom), each attained once, so a sum restricted to them is a sum over ι → ZMod m.

These are the two reindexings by which a character sum modulo p ^ 2 * M is reduced to one modulo M.

Main results

• ZMod.sum_comp_castHom: summing a function of the reduction modulo k over ι → ZMod n.
• ZMod.sum_ite_natCast_smul_eq_zero: summing over the vectors of ι → ZMod n killed by m.

theorem ZMod.sum_comp_castHom {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m n : ℕ} (k : ℕ) (h : m * k = n) {R : Type u_2} [AddCommMonoid R] [NeZero k] [NeZero n] (F : (ι → ZMod k) → R) : (∑ w : ι → ZMod n, F fun (i : ι) => (castHom ⋯ (ZMod k)) (w i)) = m ^ Fintype.card ι • ∑ y : ι → ZMod k, F y

Summing a function of the reduction. For n = m * k, summing a function of the coordinatewise reduction modulo k over ι → ZMod n counts every value m ^ #ι times.

theorem ZMod.sum_ite_natCast_smul_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m n : ℕ} (k : ℕ) (h : m * k = n) {R : Type u_2} [AddCommMonoid R] [NeZero m] [NeZero n] (g : (ι → ZMod n) → R) : (∑ x : ι → ZMod n, if ↑m • x = 0 then g x else 0) = ∑ w : ι → ZMod m, g fun (i : ι) => (mulCastHom k h) (w i)

Summing over the vectors killed by m. For n = m * k, the vectors x ∈ (ℤ/n)^ι with m • x = 0 are exactly the images of the vectors w ∈ (ℤ/m)^ι under the coordinatewise multiplication by k, each attained once.