Grace/Cumulus/Algebra/Ring/SumSupport.g17

Open in Workbench Download source

Imports

SumExtension

Declarations

Source

1-- Removing zero summands from finite ring sums, 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.SumSupport8import SumExtension910section Rings11variable (A add zero neg mul one w : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)13notation ring R := (A, add, zero, neg, mul, one)1415theorem matchingRingRow.zero (f x : Set, n : Nat)16  requires vanishes : w(x) = zero17  shows matchingRingRow(A, zero, add, w, f, x, n) = zero18proof19  induction n20  | zero =>21    rw matchingRingRow22    rfl23  | succ(k) using ih =>24    have ordinary := IsCommRing.ring with ring25    have zeroIn := IsRing.zero_in_carrier with ordinary26    have value : w(x) ∈ A27      rwa vanishes28    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto29    have entry : singleValue(A, zero, w(x), x, f(k)) = zero30      cases alternatives with same | different31      . have selected := singleValue.same at A, zero, w(x), x, f(k) with *32        cc33      . exact singleValue.other at A, zero, w(x), x, f(k) with *34    rw [matchingRingRow, ih, entry]35    ring3637theorem matchingRingRow.covered_or_zero (f x : Set, n : Nat)38  requires value : w(x) ∈ A39  requires distinct : DistinctValues(f, n)40  requires covered : Occurs(f, n, x) ∨ w(x) = zero41  shows matchingRingRow(A, zero, add, w, f, x, n) = w(x)42proof43  cases covered with occurs | vanishes44  . have unique := matchingRingRow.unique at A, add, zero, neg, mul, one, w, f, x, n with *45    exact unique with distinct, occurs46  . have empty := matchingRingRow.zero at A, add, zero, neg, mul, one, w, f, x, n with *47    cc4849theorem matchingRingTotal.support_sum (f g : Set, n m : Nat)50  requires distinct : DistinctValues(f, n)51  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = zero) →52    matchingRingTotal(A, zero, add, w, f, g, n, m) = indexedRingSum(w, g, add, zero, m)53proof54  induction m55  | zero =>56    intros values covered57    simp [matchingRingTotal, indexedRingSum]58  | succ(k) using ih =>59    intros values covered60    have prefix : ∀ j ∈ k, Occurs(f, n, g(j)) ∨ w(g(j)) = zero61      intros j before62      have included := membership.into_successor at j, k with *63      exact covered with j, included64    have last := covered with k, membership.self_successor at k with *65    have valuePrefix := WeightedValues.prefix at w, g, A, k with *66    have valueLast := WeightedValues.last at w, g, A, k with *67    have row := matchingRingRow.covered_or_zero at A, add, zero, neg, mul, one, w, f, g(k), n with *68    have previous := ih with valuePrefix, prefix69    rw [matchingRingTotal, indexedRingSum, previous, row]70    rfl7172theorem indexedRingSum.same_nonzero_entries (f g : Set, n m : Nat)73  requires valuesF : WeightedValues(w, f, A, n)74  requires valuesG : WeightedValues(w, g, A, m)75  requires distinctF : DistinctValues(f, n)76  requires distinctG : DistinctValues(g, m)77  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = zero78  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = zero79  shows indexedRingSum(w, f, add, zero, n) = indexedRingSum(w, g, add, zero, m)80proof81  have left := matchingRingTotal.support_sum at A, add, zero, neg, mul, one, w, g, f, m, n with *, valuesF, coveredF82  have right := matchingRingTotal.support_sum at A, add, zero, neg, mul, one, w, f, g, n, m with *, valuesG, coveredG83  have transpose := matchingRingTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *84  rw [← left, ← right]85  symm86  exact transpose with valuesF8788end Rings8990theorem finiteRingSum.restrict (V S A add zero neg mul one w : Set)91  requires ring : IsCommRing(A, add, zero, neg, mul, one)92  requires finite : Finite(V)93  requires weights : w : V → A94  requires subset : S ⊆ V95  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = zero96  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) =97    finiteRingSum(S, A, add, zero, neg, mul, one, restrict(w, S))98proof99  have finiteS := Finite.subset with finite, subset100  have closed : ∀ x ∈ S, w(x) ∈ A101    intros x hx102    have included := subset103    have member := included with x, hx104    exact FunctionBetween.apply_closed with *105  have restricted := restrict.function with *106  have selectedV := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *107  have selectedS := finiteRingSum.selected at S, A, add, zero, neg, mul, one, restrict(w, S) with *108  obtain ⟨n, naturalN, f, enumerationF, equationV⟩ := selectedV.right109  obtain ⟨m, naturalM, g, enumerationG, equationS⟩ := selectedS.right110  have injF := Bijective.injective with enumerationF111  have injG := Bijective.injective with enumerationG112  have surjF := Bijective.surjective with enumerationF113  have surjG := Bijective.surjective with enumerationG114  have functionF := Injective.function with injF115  have functionG := Injective.function with injG116  have distinctF := Injective.distinct_values with injF117  have distinctG := Injective.distinct_values with injG118  have valuesF := WeightedValues.of_functions with weights, functionF119  have valuesG : WeightedValues(w, g, A, m)120    intros i hi121    have member := FunctionBetween.apply_closed with *122    exact closed with g(i), member123  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = zero124    intros i hi125    have member := FunctionBetween.apply_closed with *126    have alternatives : f(i) ∈ S ∨ ¬(f(i) ∈ S) by tauto127    cases alternatives with inside | outside128    . left129      exact Surjective.occurs with *130    . right131      exact vanishes with f(i), member, outside132  have coveredG : ∀ i ∈ m, Occurs(f, n, g(i)) ∨ w(g(i)) = zero133    intros i hi134    have inS := FunctionBetween.apply_closed with *135    have included := subset136    have inV := included with g(i), inS137    left138    exact Surjective.occurs with *139  have same := indexedRingSum.same_nonzero_entries with valuesF, valuesG, distinctF, distinctG, coveredF, coveredG140  have pointwise : ∀ i ∈ m, w(g(i)) = restrict(w, S)(g(i))141    intros i hi142    have inS := FunctionBetween.apply_closed with *143    symm144    exact restrict.apply with *145  have congr := indexedRingSum.congr at w, restrict(w, S), g, g, add, zero, m with naturalM146  have equal := congr with pointwise147  cc148149theorem finiteRingSum.reindex (D E A add zero neg mul one w v f : Set)150  requires ring : IsCommRing(A, add, zero, neg, mul, one)151  requires finite : Finite(D)152  requires weightsW : w : D → A153  requires weightsV : v : E → A154  requires bijective : BijectiveBetween(f, D, E)155  requires values : ∀ d ∈ D, w(d) = v(f(d))156  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = finiteRingSum(E, A, add, zero, neg, mul, one, v)157proof158  have selected := finiteRingSum.selected at D, A, add, zero, neg, mul, one, w with *159  obtain ⟨n, natural, g, enumeration, equation⟩ := selected.right160  have composed := compose.bijective at f, g, n, D, E with *161  have injF := Bijective.injective with bijective162  have injG := Bijective.injective with enumeration163  have functionF := Injective.function with injF164  have functionG := Injective.function with injG165  have equationV := finiteRingSum.enumeration at E, A, add, zero, neg, mul, one, v, compose(f, g, n, D, E), n with *166  have pointwise : ∀ i ∈ n, w(g(i)) = v(compose(f, g, n, D, E)(i))167    intros i hi168    have member := FunctionBetween.apply_closed at g, n, D, i with *169    have value := values with g(i), member170    have composite := compose.apply at f, g, n, D, E, i with *171    cc172  have congr := indexedRingSum.congr at w, v, g, compose(f, g, n, D, E), add, zero, n with natural173  have same := congr with pointwise174  cc175176-- The smaller-domain weights may be represented by any agreeing graph.177theorem finiteRingSum.zero_extension (D S A add zero neg mul one w v : Set)178  requires ring : IsCommRing(A, add, zero, neg, mul, one)179  requires finite : Finite(D)180  requires weightsW : w : D → A181  requires weightsV : v : S → A182  requires subset : S ⊆ D183  requires agreement : ∀ s ∈ S, w(s) = v(s)184  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero185  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = finiteRingSum(S, A, add, zero, neg, mul, one, v)186proof187  have closed : ∀ s ∈ S, w(s) ∈ A188    intros s hs189    have value := FunctionBetween.apply_closed with *190    have equal := agreement with s, hs191    rwa equal192  have restricted := restrict.function with *193  have same : restrict(w, S) = v194    apply FunctionBetween.ext with restricted, weightsV195    intros s hs196    have value := restrict.apply with *197    have equal := agreement with s, hs198    cc199  have sum := finiteRingSum.restrict with *200  rwa same at sum201202theorem finiteRingSum.singleton (A add zero neg mul one w x : Set)203  requires ring : IsCommRing(A, add, zero, neg, mul, one)204  requires weights : w : {x} → A205  shows finiteRingSum({x}, A, add, zero, neg, mul, one, w) = w(x)206proof207  have same : insert(x, ∅) = {x}208    ext y209    simp210  have empty := Finite.empty211  have fresh : ¬(x ∈ ∅) by exact set.empty at x212  have extended : w : insert(x, ∅) → A by rwa same213  have subset : ∅ ⊆ insert(x, ∅) by simp [Subset, set.empty]214  have closed : ∀ y ∈ ∅, w(y) ∈ A215    intros y hy216    exfalso217    exact set.empty with hy218  have restricted := restrict.function with *219  have emptySum := finiteRingSum.empty with *220  have inserted := finiteRingSum.insert with *221  have member : x ∈ {x} by simp [singleton.membership]222  have value := FunctionBetween.apply_closed with *223  rw same at inserted224  rw [inserted, emptySum]225  ring226227theorem finiteRingSum.single (C A add zero neg mul one a c : Set)228  requires ring : IsCommRing(A, add, zero, neg, mul, one)229  requires finite : Finite(C)230  requires coefficient : a ∈ A231  requires index : c ∈ C232  shows finiteRingSum(C, A, add, zero, neg, mul, one, coefficientSingle(C, A, zero, a, c)) = a233proof234  have ordinary := IsCommRing.ring with ring235  have zeroIn := IsRing.zero_in_carrier with ordinary236  have weights := coefficientSingle.function at C, A, zero, a, c with *237  have small := coefficientSingle.function at {c}, A, zero, a, c with *238  have singletonMember : c ∈ {c}239    settle with singleton.membership240  have subset : {c} ⊆ C241    settle with Subset, singleton.membership242  have agreement : ∀ x ∈ {c}, coefficientSingle(C, A, zero, a, c)(x) = coefficientSingle({c}, A, zero, a, c)(x)243    intros x hx244    have equal := singleton.membership.forward at x, c with hx245    have left := coefficientSingle.same at C, A, zero, a, c with *246    have right := coefficientSingle.same at {c}, A, zero, a, c with *247    cc248  have vanishes : ∀ x ∈ C, ¬(x ∈ {c}) → coefficientSingle(C, A, zero, a, c)(x) = zero249    intros x hx outside250    have different : x ≠ c251      settle with singleton.membership252    exact coefficientSingle.other at C, A, zero, a, c, x with *253  have reduced := finiteRingSum.zero_extension at C, {c}, A, add, zero, neg, mul, one, coefficientSingle(C, A, zero, a, c), coefficientSingle({c}, A, zero, a, c) with *254  have singleton := finiteRingSum.singleton at A, add, zero, neg, mul, one, coefficientSingle({c}, A, zero, a, c), c with *255  have value := coefficientSingle.same at {c}, A, zero, a, c with *256  cc257258-- A fixed equality selector commutes with a finite sum.259theorem finiteRingSum.select (D A add zero neg mul one w v j i : Set)260  requires ring : IsCommRing(A, add, zero, neg, mul, one)261  requires finite : Finite(D)262  requires weightsW : w : D → A263  requires weightsV : v : D → A264  requires values : ∀ d ∈ D, v(d) = singleValue(A, zero, w(d), j, i)265  shows finiteRingSum(D, A, add, zero, neg, mul, one, v) =266    singleValue(A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i)267proof268  have ordinary := IsCommRing.ring with ring269  have zeroIn := IsRing.zero_in_carrier with ordinary270  have alternatives : i = j ∨ i ≠ j by tauto271  cases alternatives with same | different272  . have equal : v = w273      apply FunctionBetween.ext with weightsV, weightsW274      intros d hd275      have coefficient := FunctionBetween.apply_closed at w, D, A, d with *276      have selected := singleValue.same at A, zero, w(d), j, i with *277      have value := values with d, hd278      cc279    have selected := singleValue.same at A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i with *280    cc281  . have vanishes : ∀ d ∈ D, v(d) = zero282      intros d hd283      have coefficient := FunctionBetween.apply_closed at w, D, A, d with *284      have selected := singleValue.other at A, zero, w(d), j, i with *285      have value := values with d, hd286      cc287    have sum := finiteRingSum.zero at D, A, add, zero, neg, mul, one, v with *288    have selected := singleValue.other at A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i with *289    cc290