Grace/Cumulus/Algebra/Ring/IndexedSum.g17

Open in Workbench Download source

Imports

CoefficientSingle · Cardinal.Enumeration

Declarations

Source

1-- Ring-valued finite sums independent of a bijective enumeration (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.IndexedSum8import CoefficientSingle9import Cardinal.Enumeration1011predicate WeightedValues (w f A n : Set) := ∀ i ∈ n, w(f(i)) ∈ A1213def indexedRingSum (w f add z0 : Set, n : Nat) → Set14  | w, f, add, z0, zero => z015  | w, f, add, z0, succ(k) => call2(add, indexedRingSum(w, f, add, z0, k), w(f(k)))1617def matchingRingRow (A z0 add w f x : Set, n : Nat) → Set18  | A, z0, add, w, f, x, zero => z019  | A, z0, add, w, f, x, succ(k) => call2(add, matchingRingRow(A, z0, add, w, f, x, k), singleValue(A, z0, w(x), x, f(k)))2021def matchingRingTotal (A z0 add w f g : Set, n m : Nat) → Set22  | A, z0, add, w, f, g, n, zero => z023  | A, z0, add, w, f, g, n, succ(k) => call2(add, matchingRingTotal(A, z0, add, w, f, g, n, k), matchingRingRow(A, z0, add, w, f, g(k), n))24  descends m2526theorem WeightedValues.prefix (w f A : Set, n : Nat)27  requires values : WeightedValues(w, f, A, succ(n))28  shows WeightedValues(w, f, A, n)29proof30  intros i hi31  have next := membership.into_successor with *32  exact values with i, next3334theorem WeightedValues.last (w f A : Set, n : Nat)35  requires values : WeightedValues(w, f, A, succ(n))36  shows w(f(n)) ∈ A37proof38  have last := membership.self_successor with *39  exact values with n, last4041section Rings42variable (A add zero neg mul one w : Set)43hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)44notation ring R := (A, add, zero, neg, mul, one)4546theorem indexedRingSum.closed (f : Set, n : Nat)47  shows WeightedValues(w, f, A, n) → indexedRingSum(w, f, add, zero, n) ∈ A48proof49  induction n50  | zero =>51    have ordinary := IsCommRing.ring with ring52    intro values53    rw indexedRingSum54    exact IsRing.zero_in_carrier with ordinary55  | succ(k) using ih =>56    have ordinary := IsCommRing.ring with ring57    intro values58    have prefix := WeightedValues.prefix at w, f, A, k with *59    have last := WeightedValues.last at w, f, A, k with *60    have previous := ih with prefix61    rw indexedRingSum62    exact IsRing.add_closed with ordinary, previous, last6364theorem matchingRingRow.closed (f x : Set, n : Nat)65  requires value : w(x) ∈ A66  shows matchingRingRow(A, zero, add, w, f, x, n) ∈ A67proof68  induction n69  | zero =>70    have ordinary := IsCommRing.ring with ring71    have zeroIn := IsRing.zero_in_carrier with ordinary72    rwa matchingRingRow73  | succ(k) using ih =>74    have ordinary := IsCommRing.ring with ring75    have zeroIn := IsRing.zero_in_carrier with ordinary76    have last := singleValue.closed at A, zero, w(x), x, f(k) with *77    rw matchingRingRow78    exact IsRing.add_closed with ordinary, ih, last7980theorem matchingRingTotal.closed (f g : Set, n m : Nat)81  shows WeightedValues(w, g, A, m) → matchingRingTotal(A, zero, add, w, f, g, n, m) ∈ A82proof83  induction m84  | zero =>85    have ordinary := IsCommRing.ring with ring86    intro values87    rw matchingRingTotal88    exact IsRing.zero_in_carrier with ordinary89  | succ(k) using ih =>90    have ordinary := IsCommRing.ring with ring91    intro values92    have prefix := WeightedValues.prefix at w, g, A, k with *93    have last := WeightedValues.last at w, g, A, k with *94    have previous := ih with prefix95    have row := matchingRingRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *96    rw matchingRingTotal97    exact IsRing.add_closed with ordinary, previous, row9899theorem matchingRingRow.absent (f x : Set, n : Nat)100  requires value : w(x) ∈ A101  shows (∀ i ∈ n, f(i) ≠ x) → matchingRingRow(A, zero, add, w, f, x, n) = zero102proof103  induction n104  | zero =>105    have ordinary := IsCommRing.ring with ring106    have zeroIn := IsRing.zero_in_carrier with ordinary107    intro absent108    rw matchingRingRow109    rfl110  | succ(k) using ih =>111    have ordinary := IsCommRing.ring with ring112    have zeroIn := IsRing.zero_in_carrier with ordinary113    intro absent114    have prefix : ∀ i ∈ k, f(i) ≠ x115      intros i before116      have included := membership.into_successor at i, k with *117      exact absent with i, included118    have last := absent with k, membership.self_successor at k with *119    have previous := ih with prefix120    have entry := singleValue.other at A, zero, w(x), x, f(k) with *121    rw [matchingRingRow, previous, entry]122    ring123124theorem matchingRingRow.unique (f x : Set, n : Nat)125  requires value : w(x) ∈ A126  shows DistinctValues(f, n) → Occurs(f, n, x) → matchingRingRow(A, zero, add, w, f, x, n) = w(x)127proof128  induction n129  | zero =>130    have ordinary := IsCommRing.ring with ring131    have zeroIn := IsRing.zero_in_carrier with ordinary132    intros distinct occurs133    rcases occurs with ⟨i, impossible, same⟩134    exfalso135    simp [nat.zero, set.empty]136  | succ(k) using ih =>137    have ordinary := IsCommRing.ring with ring138    have zeroIn := IsRing.zero_in_carrier with ordinary139    intros distinct occurs140    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto141    cases alternatives with last | other142    . have fresh := DistinctValues.last_fresh at f, k with *143      have absent : ∀ i ∈ k, f(i) ≠ x144        intros i before equal145        have different := fresh with i, before146        rw ← last at equal147        exact different with equal148      have previous := matchingRingRow.absent at A, add, zero, neg, mul, one, w, f, x, k with *149      have entry := singleValue.same at A, zero, w(x), x, f(k) with *150      rw [matchingRingRow, previous, entry]151      ring152    . obtain ⟨position, before, equal⟩ := Occurs.forward at f, succ(k), x with occurs153      have shape := membership.successor_forward{n := k} with before154      have earlier : position ∈ k155        cases shape with inside | atLast156        . exact inside157        . exfalso158          rw atLast at equal159          exact other with equal160      have prefix := DistinctValues.prefix at f, k with *161      have occurrence : Occurs(f, k, x)162        unfold Occurs163        refine ⟨position, earlier, equal⟩164      have previous := ih with prefix, occurrence165      have entry := singleValue.other at A, zero, w(x), x, f(k) with *166      rw [matchingRingRow, previous, entry]167      ring168169theorem matchingRingWeight.symmetric (x y : Set)170  requires xValue : w(x) ∈ A171  requires yValue : w(y) ∈ A172  shows singleValue(A, zero, w(x), x, y) = singleValue(A, zero, w(y), y, x)173proof174  have ordinary := IsCommRing.ring with ring175  have zeroIn := IsRing.zero_in_carrier with ordinary176  have alternatives : x = y ∨ x ≠ y by tauto177  cases alternatives with same | different178  . rw same179    rfl180  . have reverse : y ≠ x181      intro equal182      have impossible : x = y by cc183      exact different with impossible184    have left := singleValue.other at A, zero, w(x), x, y with *185    have right := singleValue.other at A, zero, w(y), y, x with *186    cc187188theorem matchingRingTotal.empty_left (f g : Set, m : Nat)189  shows matchingRingTotal(A, zero, add, w, f, g, (0:Nat), m) = zero190proof191  induction m192  | zero =>193    rw matchingRingTotal194    rfl195  | succ(k) using ih =>196    rw [matchingRingTotal, matchingRingRow, ih]197    ring198199theorem matchingRingTotal.extend_left (f g : Set, n m : Nat)200  requires value : w(f(n)) ∈ A201  shows WeightedValues(w, g, A, m) →202    matchingRingTotal(A, zero, add, w, f, g, succ(n), m) =203    matchingRingTotal(A, zero, add, w, f, g, n, m) + matchingRingRow(A, zero, add, w, g, f(n), m)204proof205  induction m206  | zero =>207    have ordinary := IsCommRing.ring with ring208    have zeroIn := IsRing.zero_in_carrier with ordinary209    intro values210    simp [matchingRingTotal, matchingRingRow]211    ring212  | succ(k) using ih =>213    have ordinary := IsCommRing.ring with ring214    have zeroIn := IsRing.zero_in_carrier with ordinary215    intro values216    have prefix := WeightedValues.prefix at w, g, A, k with *217    have last := WeightedValues.last at w, g, A, k with *218    have previous := ih with prefix219    have symmetric := matchingRingWeight.symmetric at A, add, zero, neg, mul, one, w, g(k), f(n) with *220    have totalBound := matchingRingTotal.closed at A, add, zero, neg, mul, one, w, f, g, n, k with *221    have totalIn := totalBound with prefix222    have rowLeftIn := matchingRingRow.closed at A, add, zero, neg, mul, one, w, g, f(n), k with *223    have rowRightIn := matchingRingRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *224    have entryIn := singleValue.closed at A, zero, w(f(n)), f(n), g(k) with *225    rw [matchingRingTotal, matchingRingTotal, matchingRingRow, matchingRingRow, previous, symmetric]226    ring227228theorem matchingRingTotal.transpose (f g : Set, m n : Nat)229  requires valuesG : WeightedValues(w, g, A, m)230  shows WeightedValues(w, f, A, n) →231    matchingRingTotal(A, zero, add, w, f, g, n, m) = matchingRingTotal(A, zero, add, w, g, f, m, n)232proof233  induction n234  | zero =>235    intro valuesF236    have empty := matchingRingTotal.empty_left at A, add, zero, neg, mul, one, w, f, g, m with *237    rw [empty, matchingRingTotal]238    rfl239  | succ(k) using ih =>240    intro valuesF241    have prefix := WeightedValues.prefix at w, f, A, k with *242    have last := WeightedValues.last at w, f, A, k with *243    have previous := ih with prefix244    have extended := matchingRingTotal.extend_left at A, add, zero, neg, mul, one, w, f, g, k, m with *245    rw [extended, matchingRingTotal, previous]246    rfl247248theorem matchingRingTotal.sum (f g : Set, n m : Nat)249  requires distinct : DistinctValues(f, n)250  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j))) →251    matchingRingTotal(A, zero, add, w, f, g, n, m) = indexedRingSum(w, g, add, zero, m)252proof253  induction m254  | zero =>255    intros values covered256    simp [matchingRingTotal, indexedRingSum]257  | succ(k) using ih =>258    intros values covered259    have prefix : ∀ j ∈ k, Occurs(f, n, g(j))260      intros j before261      have included := membership.into_successor at j, k with *262      exact covered with j, included263    have last := covered with k, membership.self_successor at k with *264    have valuePrefix := WeightedValues.prefix at w, g, A, k with *265    have valueLast := WeightedValues.last at w, g, A, k with *266    have row := matchingRingRow.unique at A, add, zero, neg, mul, one, w, f, g(k), n with *267    have previous := ih with valuePrefix, prefix268    rw [matchingRingTotal, indexedRingSum, previous, row]269    rfl270271theorem indexedRingSum.same_entries (f g : Set, n m : Nat)272  requires valuesF : WeightedValues(w, f, A, n)273  requires valuesG : WeightedValues(w, g, A, m)274  requires distinctF : DistinctValues(f, n)275  requires distinctG : DistinctValues(g, m)276  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i))277  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j))278  shows indexedRingSum(w, f, add, zero, n) = indexedRingSum(w, g, add, zero, m)279proof280  have left := matchingRingTotal.sum at A, add, zero, neg, mul, one, w, g, f, m, n with *281  have right := matchingRingTotal.sum at A, add, zero, neg, mul, one, w, f, g, n, m with *282  have transpose := matchingRingTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *283  rw [← left, ← right]284  symm285  exact transpose with valuesF286287theorem indexedRingSum.reindex (V f g : Set, n m : Nat)288  requires weights : w : V → A289  requires enumerationF : BijectiveBetween(f, n, V)290  requires enumerationG : BijectiveBetween(g, m, V)291  shows indexedRingSum(w, f, add, zero, n) = indexedRingSum(w, g, add, zero, m)292proof293  have injF := Bijective.injective with enumerationF294  have injG := Bijective.injective with enumerationG295  have surjF := Bijective.surjective with enumerationF296  have surjG := Bijective.surjective with enumerationG297  have fnF := Injective.function with injF298  have fnG := Injective.function with injG299  have distinctF := Injective.distinct_values with injF300  have distinctG := Injective.distinct_values with injG301  have valuesF : WeightedValues(w, f, A, n)302    intros i hi303    have member := FunctionBetween.apply_closed with *304    exact FunctionBetween.apply_closed with *305  have valuesG : WeightedValues(w, g, A, m)306    intros j hj307    have member := FunctionBetween.apply_closed with *308    exact FunctionBetween.apply_closed with *309  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i))310    intros i hi311    have member := FunctionBetween.apply_closed with *312    exact Surjective.occurs with *313  have coveredG : ∀ j ∈ m, Occurs(f, n, g(j))314    intros j hj315    have member := FunctionBetween.apply_closed with *316    exact Surjective.occurs with *317  exact indexedRingSum.same_entries with *318319theorem indexedRingSum.add (v h f : Set, n : Nat)320  shows WeightedValues(w, f, A, n) → WeightedValues(v, f, A, n) →321    (∀ i ∈ n, h(f(i)) = w(f(i)) + v(f(i))) →322    indexedRingSum(h, f, add, zero, n) = indexedRingSum(w, f, add, zero, n) + indexedRingSum(v, f, add, zero, n)323proof324  induction n325  | zero =>326    intros valuesW valuesV equations327    simp [indexedRingSum]328    ring329  | succ(k) using ih =>330    intros valuesW valuesV equations331    have prefixW := WeightedValues.prefix at w, f, A, k with *332    have prefixV := WeightedValues.prefix at v, f, A, k with *333    have lastW := WeightedValues.last at w, f, A, k with *334    have lastV := WeightedValues.last at v, f, A, k with *335    have prefix : ∀ i ∈ k, h(f(i)) = w(f(i)) + v(f(i))336      intros i hi337      have next := membership.into_successor at i, k with *338      exact equations with i, next339    have last := equations with k, membership.self_successor at k with *340    have previous := ih with prefixW, prefixV, prefix341    have closureW := indexedRingSum.closed at A, add, zero, neg, mul, one, w, f, k with *342    have sumW := closureW with prefixW343    have closureV := indexedRingSum.closed at A, add, zero, neg, mul, one, v, f, k with *344    have sumV := closureV with prefixV345    rw [indexedRingSum, indexedRingSum, indexedRingSum, previous, last]346    ring347348theorem indexedRingSum.scale (a v f : Set, n : Nat)349  requires scalar : a ∈ A350  shows WeightedValues(w, f, A, n) → (∀ i ∈ n, v(f(i)) = a * w(f(i))) →351    indexedRingSum(v, f, add, zero, n) = a * indexedRingSum(w, f, add, zero, n)352proof353  induction n354  | zero =>355    intros values equations356    simp [indexedRingSum]357    ring358  | succ(k) using ih =>359    intros values equations360    have prefixW := WeightedValues.prefix at w, f, A, k with *361    have lastW := WeightedValues.last at w, f, A, k with *362    have prefix : ∀ i ∈ k, v(f(i)) = a * w(f(i))363      intros i hi364      have next := membership.into_successor at i, k with *365      exact equations with i, next366    have last := equations with k, membership.self_successor at k with *367    have previous := ih with prefixW, prefix368    have closure := indexedRingSum.closed at A, add, zero, neg, mul, one, w, f, k with *369    have sumW := closure with prefixW370    rw [indexedRingSum, indexedRingSum, previous, last]371    ring372373end Rings374