Grace/Cumulus/Algebra/Ring/PushforwardComposition.g17

Imports

Declarations

finitePushforward.filter_composition theorem derivation
finitePushforward.compose theorem derivation
finitePushforward.identity theorem derivation
finitePushforward.index_congr theorem derivation
Source

1-- Grouping in two stages equals grouping along the composite map (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.PushforwardComposition8import Regrouping910section Grouping11variable (D C B A add zero neg mul one h k w : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)13hypothesis finiteD : Finite(D)14hypothesis weights : w : D → A15hypothesis firstMap : h : D → C16hypothesis secondMap : k : C → B1718-- Pointwise filtering can move across the first grouping operation.19theorem finitePushforward.filter_composition (b : Set)20  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h,21    pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b)) =22    pushforwardWeights(C, A, add, zero, neg, mul, one, k,23      finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), b)24proof25  have ordinary := IsCommRing.ring with ring26  have zeroIn := IsRing.zero_in_carrier with ordinary27  have filtered := pushforwardWeights.function at D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b with *28  have grouped := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *29  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b) with *30  have rightFunction := pushforwardWeights.function at C, A, add, zero, neg, mul, one, k, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), b with *31  apply FunctionBetween.ext with leftFunction, rightFunction32  intros c hc33  have rowW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *34  have rowV := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b), c with *35  have entries : ∀ d ∈ D,36    pushforwardWeights(D, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b), c)(d) =37    singleValue(A, zero, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d), k(c), b)38    intros d hd39    have coefficient := FunctionBetween.apply_closed at w, D, A, d with *40    have composite := compose.apply at k, h, D, C, B, d with *41    have selected := pushforwardWeights.value at D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b, d with *42    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b), c, d with *43    have row := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *44    have iteration := singleValue.iterated at A, zero, w(d), k, h(d), c, b with *45    cc46  have selection := finiteRingSum.select with *47  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b), c with *48  have row := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *49  have right := pushforwardWeights.value at C, A, add, zero, neg, mul, one, k, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), b, c with *50  cc5152theorem finitePushforward.compose53  requires finiteC : Finite(C)54  shows finitePushforward(C, B, A, add, zero, neg, mul, one, k,55    finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)) =56    finitePushforward(D, B, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w)57proof58  have grouped := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *59  have leftFunction := finitePushforward.function at C, B, A, add, zero, neg, mul, one, k, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) with *60  have rightFunction := finitePushforward.function at D, B, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w with *61  apply FunctionBetween.ext with leftFunction, rightFunction62  intros b hb63  have filtered := pushforwardWeights.function at D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b with *64  have commuted := finitePushforward.filter_composition at D, C, B, A, add, zero, neg, mul, one, h, k, w, b with *65  have regrouped := finitePushforward.sum at D, C, A, add, zero, neg, mul, one, h, pushforwardWeights(D, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b) with *66  have left := finitePushforward.value at C, B, A, add, zero, neg, mul, one, k, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), b with *67  have right := finitePushforward.value at D, B, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w, b with *68  cc6970end Grouping71theorem finitePushforward.identity (D A add zero neg mul one w : Set)72  requires ring : IsCommRing(A, add, zero, neg, mul, one)73  requires finite : Finite(D)74  requires weights : w : D → A75  shows finitePushforward(D, D, A, add, zero, neg, mul, one, identity(D), w) = w76proof77  have ordinary := IsCommRing.ring with ring78  have zeroIn := IsRing.zero_in_carrier with ordinary79  have grouped := finitePushforward.function at D, D, A, add, zero, neg, mul, one, identity(D), w with *80  apply FunctionBetween.ext with grouped, weights81  intros b hb82  have coefficient := FunctionBetween.apply_closed at w, D, A, b with *83  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, identity(D), w, b with *84  have single := coefficientSingle.function at D, A, zero, w(b), b with *85  have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, identity(D), w, b) = coefficientSingle(D, A, zero, w(b), b)86    apply FunctionBetween.ext with selected, single87    intros d hd88    have coefficientD := FunctionBetween.apply_closed at w, D, A, d with *89    have id := identity.apply at d, D with *90    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, identity(D), w, b, d with *91    have right := coefficientSingle.value at D, A, zero, w(b), b, d with *92    have alternatives : d = b ∨ d ≠ b by tauto93    cases alternatives with same | different94    . cc95    . have reversed : b ≠ d96        intro equal97        have reverseEqual : d = b98          symm99          exact equal100        exact different with reverseEqual101      have leftZero := singleValue.other at A, zero, w(d), d, b with *102      have rightZero := singleValue.other at A, zero, w(b), b, d with *103      cc104  have sum := finiteRingSum.single at D, A, add, zero, neg, mul, one, w(b), b with *105  have value := finitePushforward.value at D, D, A, add, zero, neg, mul, one, identity(D), w, b with *106  cc107108theorem finitePushforward.index_congr (D C A add zero neg mul one h k w : Set)109  requires ring : IsCommRing(A, add, zero, neg, mul, one)110  requires finite : Finite(D)111  requires weights : w : D → A112  requires indices : ∀ d ∈ D, h(d) = k(d)113  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) = finitePushforward(D, C, A, add, zero, neg, mul, one, k, w)114proof115  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *116  have rightFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, k, w with *117  apply FunctionBetween.ext with leftFunction, rightFunction118  intros c hc119  have leftWeights := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *120  have rightWeights := pushforwardWeights.function at D, A, add, zero, neg, mul, one, k, w, c with *121  have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) = pushforwardWeights(D, A, add, zero, neg, mul, one, k, w, c)122    apply FunctionBetween.ext with leftWeights, rightWeights123    intros d hd124    have index := indices with d, hd125    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *126    have right := pushforwardWeights.value at D, A, add, zero, neg, mul, one, k, w, c, d with *127    cc128  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *129  have right := finitePushforward.value at D, C, A, add, zero, neg, mul, one, k, w, c with *130  cc131