Grace/Cumulus/Algebra/Ring/Regrouping.g17

Open in Workbench Download source

Imports

FiniteDoubleSum · Pushforward

Declarations

Source

1-- Summing grouped coefficients recovers the original finite sum (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 Grace.Cumulus.Algebra.Ring.Regrouping8import FiniteDoubleSum9import Pushforward1011defunique groupingEntry (D C A zero h w t : Set) (a ∈ A) :=12  ∃ d ∈ D, ∃ c ∈ C, t = (d, c) ∧ a = singleValue(A, zero, w(d), h(d), c)13requires zeroIn : zero ∈ A14requires weights : w : D → A15requires pair : t ∈ D × C16proof17  obtain ⟨bound, d, hd, c, hc, shape⟩ := product.membership.forward at18    D, C, t with pair19  have coefficient := FunctionBetween.apply_closed at w, D, A, d with *20  have value := singleValue.closed at A, zero, w(d), h(d), c with *21  refine ⟨singleValue(A, zero, w(d), h(d), c), value, d, hd, c, hc, shape, rfl⟩22uniqueness23  intros u hu first v hv second24  obtain ⟨d, hd, c, hc, shapeU, valueU⟩ := first25  obtain ⟨e, he, b, hb, shapeV, valueV⟩ := second26  have equal : (d, c) = (e, b)27    cc28  have coordinates := orderedPair.injective at d, c, e, b with equal29  cc3031defgraph groupingMatrix (D C A zero h w : Set) (t ∈ D × C) : A := groupingEntry(D, C, A, zero, h, w, t)32requires zeroIn : zero ∈ A33requires weights : w : D → A34proof35  have selected := groupingEntry.selected at D, C, A, zero, h, w, t with *36  exact selected.left3738theorem groupingMatrix.pair (D C A zero h w d c : Set)39  requires zeroIn : zero ∈ A40  requires weights : w : D → A41  requires row : d ∈ D42  requires column : c ∈ C43  shows groupingMatrix(D, C, A, zero, h, w)((d, c)) = singleValue(A, zero, w(d), h(d), c)44proof45  have pair := product.pair at d, c, D, C with *46  have selected := groupingEntry.selected at D, C, A, zero, h, w, (d, c) with *47  obtain ⟨e, he, b, hb, shape, output⟩ := selected.right48  have coordinates := orderedPair.injective with shape49  have value := groupingMatrix.value at D, C, A, zero, h, w, (d, c) with *50  cc5152section Rings53variable (D C A add zero neg mul one h w : Set)54hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)55hypothesis weights : w : D → A5657theorem groupingMatrix.rows58  requires finiteC : Finite(C)59  requires indexMap : h : D → C60  shows finiteRowSums(D, C, A, add, zero, neg, mul, one, groupingMatrix(D, C, A, zero, h, w)) = w61proof62  have ordinary := IsCommRing.ring with ring63  have zeroIn := IsRing.zero_in_carrier with ordinary64  have matrix := groupingMatrix.function at D, C, A, zero, h, w with *65  have rows := finiteRowSums.function at D, C, A, add, zero, neg, mul, one, groupingMatrix(D, C, A, zero, h, w) with *66  apply FunctionBetween.ext with rows, weights67  intros d hd68  have coefficient := FunctionBetween.apply_closed at w, D, A, d with *69  have index := FunctionBetween.apply_closed at h, D, C, d with *70  have row := finiteRowWeights.function at D, C, A, groupingMatrix(D, C, A, zero, h, w), d with *71  have single := coefficientSingle.function at C, A, zero, w(d), h(d) with *72  have same : finiteRowWeights(D, C, A, groupingMatrix(D, C, A, zero, h, w), d) = coefficientSingle(C, A, zero, w(d), h(d))73    apply FunctionBetween.ext with row, single74    intros c hc75    have left := finiteRowWeights.value at D, C, A, groupingMatrix(D, C, A, zero, h, w), d, c with *76    have entry := groupingMatrix.pair at D, C, A, zero, h, w, d, c with *77    have right := coefficientSingle.value at C, A, zero, w(d), h(d), c with *78    cc79  have sum := finiteRingSum.single with ring, coefficient, index80  have value := finiteRowSums.value at D, C, A, add, zero, neg, mul, one, groupingMatrix(D, C, A, zero, h, w), d with *81  cc8283theorem groupingMatrix.columns84  requires finiteD : Finite(D)85  shows finiteRowSums(C, D, A, add, zero, neg, mul, one, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w))) = finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)86proof87  have ordinary := IsCommRing.ring with ring88  have zeroIn := IsRing.zero_in_carrier with ordinary89  have matrix := groupingMatrix.function at D, C, A, zero, h, w with *90  have transpose := transposedMatrix.function at D, C, A, groupingMatrix(D, C, A, zero, h, w) with *91  have rows := finiteRowSums.function at C, D, A, add, zero, neg, mul, one, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w)) with *92  have grouped := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *93  apply FunctionBetween.ext with rows, grouped94  intros c hc95  have row := finiteRowWeights.function at C, D, A, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w)), c with *96  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *97  have same : finiteRowWeights(C, D, A, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w)), c) = pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)98    apply FunctionBetween.ext with row, selected99    intros d hd100    have left := finiteRowWeights.value at C, D, A, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w)), c, d with *101    have swapped := transposedMatrix.pair with hd, hc102    have entry := groupingMatrix.pair at D, C, A, zero, h, w, d, c with *103    have right := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *104    cc105  have left := finiteRowSums.value at C, D, A, add, zero, neg, mul, one, transposedMatrix(D, C, A, groupingMatrix(D, C, A, zero, h, w)), c with *106  have right := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *107  cc108109theorem finitePushforward.sum110  requires finiteD : Finite(D)111  requires finiteC : Finite(C)112  requires indexMap : h : D → C113  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)114proof115  have ordinary := IsCommRing.ring with ring116  have zeroIn := IsRing.zero_in_carrier with ordinary117  have matrix := groupingMatrix.function at D, C, A, zero, h, w with *118  have rows := groupingMatrix.rows with ring, weights, finiteC, indexMap119  have columns := groupingMatrix.columns at D, C, A, add, zero, neg, mul, one, h, w with *120  have interchange := finiteDoubleSum.interchange with ring, finiteD, finiteC, matrix121  unfold finiteDoubleSum at interchange122  cc123124-- Only the finite image needs to be summed, even if C itself is infinite.125theorem finitePushforward.sum_image126  requires finiteD : Finite(D)127  requires indexMap : h : D → C128  shows finiteRingSum(functionImage(h, D, C), A, add, zero, neg, mul, one,129    finitePushforward(D, functionImage(h, D, C), A, add, zero, neg, mul, one, h, w)) =130    finiteRingSum(D, A, add, zero, neg, mul, one, w)131proof132  have reflexive : D ⊆ D by simp [Subset]133  have finiteImage := Finite.function_image at D, C, h, D with *134  have corestricted := functionImage.corestrict at h, D, C with *135  exact finitePushforward.sum with *136137end Rings138theorem finitePushforward.constant_index (D A add zero neg mul one w c : Set)139  requires ring : IsCommRing(A, add, zero, neg, mul, one)140  requires finite : Finite(D)141  requires weights : w : D → A142  shows finitePushforward(D, {c}, A, add, zero, neg, mul, one, constantFunction(D, {c}, c), w)(c) =143    finiteRingSum(D, A, add, zero, neg, mul, one, w)144proof145  have member : c ∈ {c} by simp [singleton.membership]146  have indexMap := constantFunction.function at D, {c}, c with member147  have finiteC := Finite.singleton at c148  have grouped := finitePushforward.function at D, {c}, A, add, zero, neg, mul, one, constantFunction(D, {c}, c), w with *149  have total := finitePushforward.sum at D, {c}, A, add, zero, neg, mul, one, constantFunction(D, {c}, c), w with *150  have singleton := finiteRingSum.singleton with *151  cc152