FiniteRegrouping

Interchange and regroup finite-set sums, with arbitrary fibers (ZF)

Open in Workbench View on GitHub

1-- Interchange and regroup finite-set sums, with arbitrary fibers (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module FiniteRegrouping8import Grace.Cumulus.Algebra.Ring.Regrouping910section Rings11variable (A add zero neg mul one : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)1314theorem rows_equal_columns (D E w : Set)15  requires finiteD : Finite(D)16  requires finiteE : Finite(E)17  requires matrix : w : D × E → A18  shows finiteDoubleSum(D, E, A, add, zero, neg, mul, one, w) = finiteDoubleSum(E, D, A, add, zero, neg, mul, one, transposedMatrix(D, E, A, w))19proof20  exact finiteDoubleSum.interchange with ring, finiteD, finiteE, matrix2122-- No injectivity is assumed: different inputs may go to the same group.23theorem regroup (D C h w : Set)24  requires finiteD : Finite(D)25  requires finiteC : Finite(C)26  requires weights : w : D → A27  requires indexMap : h : D → C28  shows finiteRingSum(C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)) = finiteRingSum(D, A, add, zero, neg, mul, one, w)29proof30  exact finitePushforward.sum with ring, weights, finiteD, finiteC, indexMap3132-- All collisions are allowed, even when every input has the same output.33theorem one_group (D w c : Set)34  requires finite : Finite(D)35  requires weights : w : D → A36  shows finitePushforward(D, {c}, A, add, zero, neg, mul, one, constantFunction(D, {c}, c), w)(c) = finiteRingSum(D, A, add, zero, neg, mul, one, w)37proof38  exact finitePushforward.constant_index at D, A, add, zero, neg, mul, one, w, c with *3940-- The ambient codomain need not be finite: sum over the finite image.41theorem regroup_image (D C h w : Set)42  requires finite : Finite(D)43  requires weights : w : D → A44  requires indexMap : h : D → C45  shows finiteRingSum(functionImage(h, D, C), A, add, zero, neg, mul, one, finitePushforward(D, functionImage(h, D, C), A, add, zero, neg, mul, one, h, w)) = finiteRingSum(D, A, add, zero, neg, mul, one, w)46proof47  exact finitePushforward.sum_image with ring, weights, finite, indexMap4849end Rings50