Grace/Cumulus/Algebra/Ring/Pushforward.g17

Open in Workbench Download source

Imports

SumExtension · Cardinal.FiniteImage

Declarations

Source

1-- Group finite ring sums along a function, without Choice.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.Pushforward8import SumExtension9import Cardinal.FiniteImage1011defgraph pushforwardWeights (D A add zero neg mul one h w c : Set) (d ∈ D) : A :=12  singleValue(A, zero, w(d), h(d), c)13requires ring : IsCommRing(A, add, zero, neg, mul, one)14requires weights : w : D → A15proof16  have ordinary := IsCommRing.ring with ring17  have zeroIn := IsRing.zero_in_carrier with ordinary18  have value := FunctionBetween.apply_closed at w, D, A, d with *19  exact singleValue.closed at A, zero, w(d), h(d), c with *2021defgraph finitePushforward (D C A add zero neg mul one h w : Set) (c ∈ C) : A :=22  finiteRingSum(D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c))23requires ring : IsCommRing(A, add, zero, neg, mul, one)24requires finite : Finite(D)25requires weights : w : D → A26proof27  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *28  exact finiteRingSum.closed at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *2930theorem finitePushforward.outside (D C A add zero neg mul one h w c : Set)31  requires ring : IsCommRing(A, add, zero, neg, mul, one)32  requires finite : Finite(D)33  requires weights : w : D → A34  requires index : c ∈ C35  requires absent : ¬(c ∈ functionImage(h, D, C))36  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c) = zero37proof38  have ordinary := IsCommRing.ring with ring39  have zeroIn := IsRing.zero_in_carrier with ordinary40  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *41  have vanishes : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero42    intros d hd43    have coefficient := FunctionBetween.apply_closed at w, D, A, d with *44    have different : c ≠ h(d)45      intro equal46      have inImage : c ∈ functionImage(h, D, C) := functionImage.membership.backward with ⟨index, d, hd, equal⟩47      exact absent with inImage48    have term := singleValue.other with zeroIn, coefficient, different49    have value := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *50    cc51  have sumZero := finiteRingSum.zero with *52  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *53  cc5455theorem finitePushforward.support (D C A add zero neg mul one h w : Set)56  requires ring : IsCommRing(A, add, zero, neg, mul, one)57  requires finite : Finite(D)58  requires weights : w : D → A59  shows functionSupport(finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), C, zero) ⊆ functionImage(h, D, C)60proof61  intros c hc62  have data := functionSupport.membership.forward with hc63  have alternatives : c ∈ functionImage(h, D, C) ∨ ¬(c ∈ functionImage(h, D, C)) by tauto64  cases alternatives with present | absent65  . exact present66  . have vanishes := finitePushforward.outside with absent67    exfalso68    exact data.right with vanishes6970theorem finitePushforward.map (D C A add zero neg mul one h w E : Set)71  requires ring : IsCommRing(A, add, zero, neg, mul, one)72  requires finite : Finite(D)73  requires weights : w : D → A74  requires indexMap : h : E → C75  requires domain : D ⊆ E76  shows CoefficientMap(finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), C, A, zero)77proof78  have function := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *79  have finiteImage := Finite.function_image with *80  have subset := finitePushforward.support at D, C, A, add, zero, neg, mul, one, h, w with *81  have supportFinite := Finite.subset with finiteImage, subset82  unfold CoefficientMap83  refine ⟨function, supportFinite⟩8485section Linearity86variable (A add zero neg mul one : Set)87hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)88notation ring R := (A, add, zero, neg, mul, one)8990theorem singleValue.add (a b j i : Set)91  requires valueA : a ∈ A92  requires valueB : b ∈ A93  shows singleValue(A, zero, a + b, j, i) = singleValue(A, zero, a, j, i) + singleValue(A, zero, b, j, i)94proof95  have ordinary := IsCommRing.ring with ring96  have zeroIn := IsRing.zero_in_carrier with ordinary97  have sumIn := IsRing.add_closed at A, add, zero, neg, mul, one, a, b with *98  have alternatives : i = j ∨ i ≠ j by tauto99  cases alternatives with same | different100  . have sum := singleValue.same at A, zero, a + b, j, i with *101    have left := singleValue.same at A, zero, a, j, i with *102    have right := singleValue.same at A, zero, b, j, i with *103    cc104  . have sum := singleValue.other at A, zero, a + b, j, i with *105    have left := singleValue.other at A, zero, a, j, i with *106    have right := singleValue.other at A, zero, b, j, i with *107    rw [sum, left, right]108    ring109110theorem pushforwardWeights.add (D h w v c : Set)111  requires weightsW : w : D → A112  requires weightsV : v : D → A113  shows pushforwardWeights(D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c) =114    coefficientAdd(D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c))115proof116  have sumFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, w, v with *117  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *118  have selectedV := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, v, c with *119  have leftFunction := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c with *120  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c) with *121  apply FunctionBetween.ext with leftFunction, rightFunction122  intros d hd123  have wIn := FunctionBetween.apply_closed at w, D, A, d with *124  have vIn := FunctionBetween.apply_closed at v, D, A, d with *125  have source := coefficientAdd.value at D, A, add, zero, neg, mul, one, w, v, d with *126  have selectedSum := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c, d with *127  have valueW := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *128  have valueV := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, v, c, d with *129  have target := coefficientAdd.value at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c), d with *130  have distribute := singleValue.add at A, add, zero, neg, mul, one, w(d), v(d), h(d), c with *131  cc132133theorem finitePushforward.add (D C h w v : Set)134  requires finite : Finite(D)135  requires weightsW : w : D → A136  requires weightsV : v : D → A137  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v)) =138    coefficientAdd(C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v))139proof140  have sumFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, w, v with *141  have pushW := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *142  have pushV := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, v with *143  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v) with *144  have rightFunction := coefficientAdd.function at C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v) with *145  apply FunctionBetween.ext with leftFunction, rightFunction146  intros c hc147  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *148  have selectedV := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, v, c with *149  have weightSum := pushforwardWeights.add at A, add, zero, neg, mul, one, D, h, w, v, c with *150  have distribute := finiteRingSum.add at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c) with *151  have leftValue := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c with *152  have valueW := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *153  have valueV := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, v, c with *154  have rightValue := coefficientAdd.value at C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v), c with *155  cc156157end Linearity158