Grace/Cumulus/Algebra/Ring/PushforwardTransport.g17

Open in Workbench Download source

Imports

Pushforward · PushforwardComposition

Declarations

Source

1-- Reindexing and zero-extension for grouped finite ring sums (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.PushforwardTransport8import Pushforward9import PushforwardComposition1011theorem finitePushforward.reindex (D E C A add zero neg mul one h k w v f : Set)12  requires ring : IsCommRing(A, add, zero, neg, mul, one)13  requires finite : Finite(D)14  requires weightsW : w : D → A15  requires weightsV : v : E → A16  requires bijective : BijectiveBetween(f, D, E)17  requires indices : ∀ d ∈ D, h(d) = k(f(d))18  requires weights : ∀ d ∈ D, w(d) = v(f(d))19  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) =20    finitePushforward(E, C, A, add, zero, neg, mul, one, k, v)21proof22  have equivalent : Equipotent(D, E)23    unfold Equipotent24    refine ⟨f, bijective⟩25  have finiteE := Finite.of_equipotent with finite, equivalent26  have inj := Bijective.injective with bijective27  have functionF := Injective.function with inj28  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *29  have rightFunction := finitePushforward.function at E, C, A, add, zero, neg, mul, one, k, v with *30  apply FunctionBetween.ext with leftFunction, rightFunction31  intros c hc32  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *33  have selectedV := pushforwardWeights.function at E, A, add, zero, neg, mul, one, k, v, c with *34  have pointwise : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = pushforwardWeights(E, A, add, zero, neg, mul, one, k, v, c)(f(d))35    intros d hd36    have inE := FunctionBetween.apply_closed at f, D, E, d with *37    have index := indices with d, hd38    have weight := weights with d, hd39    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *40    have right := pushforwardWeights.value at E, A, add, zero, neg, mul, one, k, v, c, f(d) with *41    cc42  have same := finiteRingSum.reindex at D, E, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(E, A, add, zero, neg, mul, one, k, v, c), f with *43  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *44  have right := finitePushforward.value at E, C, A, add, zero, neg, mul, one, k, v, c with *45  cc4647theorem finitePushforward.restrict (D S C A add zero neg mul one h w : Set)48  requires ring : IsCommRing(A, add, zero, neg, mul, one)49  requires finite : Finite(D)50  requires weights : w : D → A51  requires subset : S ⊆ D52  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero53  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) =54    finitePushforward(S, C, A, add, zero, neg, mul, one, h, restrict(w, S))55proof56  have ordinary := IsCommRing.ring with ring57  have zeroIn := IsRing.zero_in_carrier with ordinary58  have finiteS := Finite.subset with finite, subset59  have closed : ∀ s ∈ S, w(s) ∈ A60    intros s hs61    have included := subset62    have member := included with s, hs63    exact FunctionBetween.apply_closed at w, D, A, s with *64  have restricted := restrict.function at w, D, A, S, A with *65  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *66  have rightFunction := finitePushforward.function at S, C, A, add, zero, neg, mul, one, h, restrict(w, S) with *67  apply FunctionBetween.ext with leftFunction, rightFunction68  intros c hc69  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *70  have selectedS := pushforwardWeights.function at S, A, add, zero, neg, mul, one, h, restrict(w, S), c with *71  have selectedClosed : ∀ s ∈ S, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(s) ∈ A72    intros s hs73    have included := subset74    have member := included with s, hs75    exact FunctionBetween.apply_closed at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, s with *76  have selectedRestriction := restrict.function at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, S, A with *77  have absent : ∀ d ∈ D, ¬(d ∈ S) → pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero78    intros d hd outside79    have sourceZero := vanishes with d, hd, outside80    have weight := FunctionBetween.apply_closed at w, D, A, d with *81    have value := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *82    have alternatives : c = h(d) ∨ c ≠ h(d) by tauto83    cases alternatives with same | different84    . have selected := singleValue.same at A, zero, w(d), h(d), c with *85      cc86    . have selected := singleValue.other at A, zero, w(d), h(d), c with *87      cc88  have sameWeights : restrict(pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), S) = pushforwardWeights(S, A, add, zero, neg, mul, one, h, restrict(w, S), c)89    apply FunctionBetween.ext with selectedRestriction, selectedS90    intros s hs91    have included := subset92    have member := included with s, hs93    have restriction := restrict.apply at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, S, A, s with *94    have source := restrict.apply at w, D, A, S, A, s with *95    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, s with *96    have right := pushforwardWeights.value at S, A, add, zero, neg, mul, one, h, restrict(w, S), c, s with *97    cc98  have sum := finiteRingSum.restrict at D, S, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *99  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *100  have right := finitePushforward.value at S, C, A, add, zero, neg, mul, one, h, restrict(w, S), c with *101  cc102103theorem finitePushforward.zero_extension (D S C A add zero neg mul one h w v : Set)104  requires ring : IsCommRing(A, add, zero, neg, mul, one)105  requires finite : Finite(D)106  requires weightsW : w : D → A107  requires weightsV : v : S → A108  requires subset : S ⊆ D109  requires agreement : ∀ s ∈ S, w(s) = v(s)110  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero111  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) = finitePushforward(S, C, A, add, zero, neg, mul, one, h, v)112proof113  have closed : ∀ s ∈ S, w(s) ∈ A114    intros s hs115    have value := FunctionBetween.apply_closed with *116    have equal := agreement with s, hs117    rwa equal118  have restricted := restrict.function with *119  have same : restrict(w, S) = v120    apply FunctionBetween.ext with restricted, weightsV121    intros s hs122    have value := restrict.apply with *123    have equal := agreement with s, hs124    cc125  have sum := finitePushforward.restrict at D, S, C, A, add, zero, neg, mul, one, h, w with *126  rwa same at sum127128theorem finitePushforward.singleton (C A add zero neg mul one h w x : Set)129  requires ring : IsCommRing(A, add, zero, neg, mul, one)130  requires weights : w : {x} → A131  shows finitePushforward({x}, C, A, add, zero, neg, mul, one, h, w) = coefficientSingle(C, A, zero, w(x), h(x))132proof133  have ordinary := IsCommRing.ring with ring134  have zeroIn := IsRing.zero_in_carrier with ordinary135  have finite := Finite.singleton at x136  have member := singleton.self at x137  have coefficient := FunctionBetween.apply_closed with *138  have pushed := finitePushforward.function at {x}, C, A, add, zero, neg, mul, one, h, w with *139  have single := coefficientSingle.function at C, A, zero, w(x), h(x) with *140  apply FunctionBetween.ext with pushed, single141  intros c hc142  have selected := pushforwardWeights.function at {x}, A, add, zero, neg, mul, one, h, w, c with *143  have sum := finiteRingSum.singleton at A, add, zero, neg, mul, one, pushforwardWeights({x}, A, add, zero, neg, mul, one, h, w, c), x with *144  have left := finitePushforward.value at {x}, C, A, add, zero, neg, mul, one, h, w, c with *145  have weight := pushforwardWeights.value at {x}, A, add, zero, neg, mul, one, h, w, c, x with *146  have right := coefficientSingle.value at C, A, zero, w(x), h(x), c with *147  cc148149-- Recover a sparse coefficient map from an injectively indexed finite domain.150-- The domain may include entries of weight zero.151theorem finitePushforward.reconstruct (D C A add zero neg mul one h w p : Set)152  requires ring : IsCommRing(A, add, zero, neg, mul, one)153  requires finite : Finite(D)154  requires weights : w : D → A155  requires target : p : C → A156  requires values : ∀ d ∈ D, w(d) = p(h(d))157  requires injective : ∀ d ∈ D, ∀ e ∈ D, h(d) = h(e) → d = e158  requires covers : ∀ c ∈ C, p(c) ≠ zero → ∃ d ∈ D, h(d) = c159  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) = p160proof161  have ordinary := IsCommRing.ring with ring162  have zeroIn := IsRing.zero_in_carrier with ordinary163  have pushed := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *164  apply FunctionBetween.ext with pushed, target165  intros c hc166  have coefficient := FunctionBetween.apply_closed at p, C, A, c with *167  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *168  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *169  have alternatives : p(c) = zero ∨ p(c) ≠ zero by tauto170  cases alternatives with vanishing | nonzero171  . have allZero : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero172      intros d hd173      have weight := FunctionBetween.apply_closed at w, D, A, d with *174      have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *175      have source := values with d, hd176      have cases : c = h(d) ∨ c ≠ h(d) by tauto177      cases cases with same | different178      . have chosen := singleValue.same at A, zero, w(d), h(d), c with *179        cc180      . have chosen := singleValue.other at A, zero, w(d), h(d), c with *181        cc182    have sum := finiteRingSum.zero at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *183    cc184  . obtain ⟨d, hd, image⟩ := covers with c, hc, nonzero185    have single := coefficientSingle.function at D, A, zero, p(c), d with *186    have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) = coefficientSingle(D, A, zero, p(c), d)187      apply FunctionBetween.ext with selected, single188      intros e he189      have weight := FunctionBetween.apply_closed at w, D, A, e with *190      have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, e with *191      have source := values with e, he192      have cases : e = d ∨ e ≠ d by tauto193      cases cases with same | different194      . have index : c = h(e)195          cc196        have chosen := singleValue.same at A, zero, w(e), h(e), c with *197        have point := coefficientSingle.same at D, A, zero, p(c), d with *198        cc199      . have differentImage : c ≠ h(e)200          intro equalImage201          have equalIndices : h(e) = h(d) by cc202          have equal := injective with e, he, d, hd, equalIndices203          exact different with equal204        have chosen := singleValue.other at A, zero, w(e), h(e), c with *205        have point := coefficientSingle.other at D, A, zero, p(c), d, e with *206        cc207    have sum := finiteRingSum.single at D, A, add, zero, neg, mul, one, p(c), d with *208    cc209210-- A group with exactly one source index has that source's coefficient.211theorem finitePushforward.unique_fiber (D C A add zero neg mul one h w d c : Set)212  requires ring : IsCommRing(A, add, zero, neg, mul, one)213  requires finite : Finite(D)214  requires weights : w : D → A215  requires source : d ∈ D216  requires target : c ∈ C217  requires image : h(d) = c218  requires unique : ∀ e ∈ D, h(e) = c → e = d219  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c) = w(d)220proof221  have ordinary := IsCommRing.ring with ring222  have zeroIn := IsRing.zero_in_carrier with ordinary223  have coefficient := FunctionBetween.apply_closed at w, D, A, d with *224  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *225  have single := coefficientSingle.function at D, A, zero, w(d), d with *226  have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) = coefficientSingle(D, A, zero, w(d), d)227    apply FunctionBetween.ext with selected, single228    intros e he229    have weight := FunctionBetween.apply_closed at w, D, A, e with *230    have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, e with *231    have alternatives : e = d ∨ e ≠ d by tauto232    cases alternatives with same | different233    . have index : c = h(e)234        cc235      have chosen := singleValue.same at A, zero, w(e), h(e), c with *236      have point := coefficientSingle.same at D, A, zero, w(d), d with *237      cc238    . have differentImage : c ≠ h(e)239        intro equality240        have forward : h(e) = c by cc241        have equal := unique with e, he, forward242        exact different with equal243      have chosen := singleValue.other at A, zero, w(e), h(e), c with *244      have point := coefficientSingle.other at D, A, zero, w(d), d, e with *245      cc246  have sum := finiteRingSum.single at D, A, add, zero, neg, mul, one, w(d), d with *247  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *248  cc249