Grace/Cumulus/Algebra/Ring/FiniteDoubleSum.g17

Open in Workbench Download source

Imports

DoubleSum

Declarations

Source

1-- Canonical finite-set iterated sums and their enumeration bridge (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.FiniteDoubleSum8import DoubleSum910defgraph finiteRowWeights (D E A w x : Set) (y ∈ E) : A := w((x, y))11requires matrix : w : D × E → A12requires row : x ∈ D13proof14  have pair := product.pair at x, y, D, E with *15  exact FunctionBetween.apply_closed at w, D × E, A, (x, y) with *1617defgraph finiteRowSums (D E A add zero neg mul one w : Set) (x ∈ D) : A :=18  finiteRingSum(E, A, add, zero, neg, mul, one, finiteRowWeights(D, E, A, w, x))19requires ring : IsCommRing(A, add, zero, neg, mul, one)20requires finiteE : Finite(E)21requires matrix : w : D × E → A22proof23  have weights := finiteRowWeights.function at D, E, A, w, x with *24  exact finiteRingSum.closed at E, A, add, zero, neg, mul, one, finiteRowWeights(D, E, A, w, x) with *2526def finiteDoubleSum (D E A add zero neg mul one w : Set) : Set :=27  finiteRingSum(D, A, add, zero, neg, mul, one, finiteRowSums(D, E, A, add, zero, neg, mul, one, w))2829defgraph enumeratedMatrix (m n D E A w f g : Set) (p ∈ m × n) : A :=30  w(productMap(f, g, m, n, D, E)(p))31requires matrix : w : D × E → A32requires rows : f : m → D33requires columns : g : n → E34proof35  have rectangle := productMap.function with rows, columns36  have pair := FunctionBetween.apply_closed at productMap(f, g, m, n, D, E), m × n, D × E, p with *37  exact FunctionBetween.apply_closed at w, D × E, A, productMap(f, g, m, n, D, E)(p) with *3839theorem enumeratedMatrix.pair (m n D E A w f g i j : Set)40  requires matrix : w : D × E → A41  requires rows : f : m → D42  requires columns : g : n → E43  requires row : i ∈ m44  requires column : j ∈ n45  shows enumeratedMatrix(m, n, D, E, A, w, f, g)((i, j)) = w((f(i), g(j)))46proof47  have pair := product.pair at i, j, m, n with *48  have value := enumeratedMatrix.value at m, n, D, E, A, w, f, g, (i, j) with *49  have mapped := productMap.apply at f, g, m, n, D, E, i, j with *50  cc5152theorem ringRowSum.as_indexed (w v f add zero x : Set, n : Nat)53  shows (∀ j ∈ n, w((x, j)) = v(f(j))) →54    ringRowSum(w, add, zero, x, n) = indexedRingSum(v, f, add, zero, n)55proof56  induction n57  | zero =>58    intro values59    simp [ringRowSum, indexedRingSum]60  | succ(k) using ih =>61    intro values62    have prefix : ∀ j ∈ k, w((x, j)) = v(f(j))63      intros j hj64      have included := membership.into_successor at j, k with *65      exact values with j, included66    have last := values with k, membership.self_successor at k with *67    have previous := ih with prefix68    rw [ringRowSum, indexedRingSum, previous, last]69    rfl7071theorem ringDoubleSum.as_indexed (w v f add zero : Set, m n : Nat)72  shows (∀ i ∈ m, ringRowSum(w, add, zero, i, n) = v(f(i))) →73    ringDoubleSum(w, add, zero, m, n) = indexedRingSum(v, f, add, zero, m)74proof75  induction m76  | zero =>77    intro values78    simp [ringDoubleSum, indexedRingSum]79  | succ(k) using ih =>80    intro values81    have prefix : ∀ i ∈ k, ringRowSum(w, add, zero, i, n) = v(f(i))82      intros i hi83      have included := membership.into_successor at i, k with *84      exact values with i, included85    have last := values with k, membership.self_successor at k with *86    have previous := ih with prefix87    rw [ringDoubleSum, indexedRingSum, previous, last]88    rfl8990theorem finiteDoubleSum.closed (D E A add zero neg mul one w : Set)91  requires ring : IsCommRing(A, add, zero, neg, mul, one)92  requires finiteD : Finite(D)93  requires finiteE : Finite(E)94  requires matrix : w : D × E → A95  shows finiteDoubleSum(D, E, A, add, zero, neg, mul, one, w) ∈ A96proof97  have rows := finiteRowSums.function at D, E, A, add, zero, neg, mul, one, w with *98  unfold finiteDoubleSum99  exact finiteRingSum.closed with *100101theorem finiteDoubleSum.enumerations (D E A add zero neg mul one w f g : Set, m n : Nat)102  requires ring : IsCommRing(A, add, zero, neg, mul, one)103  requires finiteE : Finite(E)104  requires matrix : w : D × E → A105  requires enumD : BijectiveBetween(f, m, D)106  requires enumE : BijectiveBetween(g, n, E)107  shows finiteDoubleSum(D, E, A, add, zero, neg, mul, one, w) = ringDoubleSum(enumeratedMatrix(m, n, D, E, A, w, f, g), add, zero, m, n)108proof109  have injD := Bijective.injective with enumD110  have injE := Bijective.injective with enumE111  have rows := Injective.function with injD112  have columns := Injective.function with injE113  have rowSums := finiteRowSums.function at D, E, A, add, zero, neg, mul, one, w with *114  have outer := finiteRingSum.enumeration at D, A, add, zero, neg, mul, one, finiteRowSums(D, E, A, add, zero, neg, mul, one, w), f, m with *115  have rowValues : ∀ i ∈ m, ringRowSum(enumeratedMatrix(m, n, D, E, A, w, f, g), add, zero, i, n) = finiteRowSums(D, E, A, add, zero, neg, mul, one, w)(f(i))116    intros i hi117    have row := FunctionBetween.apply_closed at f, m, D, i with *118    have weights := finiteRowWeights.function at D, E, A, w, f(i) with *119    have inner := finiteRingSum.enumeration at E, A, add, zero, neg, mul, one, finiteRowWeights(D, E, A, w, f(i)), g, n with *120    have values : ∀ j ∈ n, enumeratedMatrix(m, n, D, E, A, w, f, g)((i, j)) = finiteRowWeights(D, E, A, w, f(i))(g(j))121      intros j hj122      have column := FunctionBetween.apply_closed at g, n, E, j with *123      have left := enumeratedMatrix.pair at m, n, D, E, A, w, f, g, i, j with *124      have right := finiteRowWeights.value at D, E, A, w, f(i), g(j) with *125      cc126    have bridge := ringRowSum.as_indexed at enumeratedMatrix(m, n, D, E, A, w, f, g), finiteRowWeights(D, E, A, w, f(i)), g, add, zero, i, n with *127    have equal := bridge with values128    have value := finiteRowSums.value at D, E, A, add, zero, neg, mul, one, w, f(i) with *129    cc130  have bridge := ringDoubleSum.as_indexed at enumeratedMatrix(m, n, D, E, A, w, f, g), finiteRowSums(D, E, A, add, zero, neg, mul, one, w), f, add, zero, m, n with *131  have equal := bridge with rowValues132  unfold finiteDoubleSum133  cc134135theorem finiteDoubleSum.interchange (D E A add zero neg mul one w : Set)136  requires ring : IsCommRing(A, add, zero, neg, mul, one)137  requires finiteD : Finite(D)138  requires finiteE : Finite(E)139  requires matrix : w : D × E → A140  shows finiteDoubleSum(D, E, A, add, zero, neg, mul, one, w) =141    finiteDoubleSum(E, D, A, add, zero, neg, mul, one, transposedMatrix(D, E, A, w))142proof143  obtain ⟨m, naturalM, f, enumD⟩ := Finite.enumeration with finiteD144  obtain ⟨n, naturalN, g, enumE⟩ := Finite.enumeration with finiteE145  have injD := Bijective.injective with enumD146  have injE := Bijective.injective with enumE147  have rows := Injective.function with injD148  have columns := Injective.function with injE149  have transposed := transposedMatrix.function at D, E, A, w with *150  have first := enumeratedMatrix.function at m, n, D, E, A, w, f, g with *151  have second := enumeratedMatrix.function at n, m, E, D, A, transposedMatrix(D, E, A, w), g, f with *152  have valuesW := RingMatrixValues.of_function with first153  have valuesV := RingMatrixValues.of_function with second154  have entries : TransposedValues(enumeratedMatrix(m, n, D, E, A, w, f, g), enumeratedMatrix(n, m, E, D, A, transposedMatrix(D, E, A, w), g, f), m, n)155    intros i hi j hj156    have row := FunctionBetween.apply_closed at f, m, D, i with *157    have column := FunctionBetween.apply_closed at g, n, E, j with *158    have left := enumeratedMatrix.pair at m, n, D, E, A, w, f, g, i, j with *159    have right := enumeratedMatrix.pair at n, m, E, D, A, transposedMatrix(D, E, A, w), g, f, j, i with *160    have entry := transposedMatrix.pair at D, E, A, w, f(i), g(j) with *161    cc162  have interchange := ringDoubleSum.transpose at A, add, zero, neg, mul, one, enumeratedMatrix(m, n, D, E, A, w, f, g), enumeratedMatrix(n, m, E, D, A, transposedMatrix(D, E, A, w), g, f), m, n with *163  have equal := interchange with valuesW, valuesV, entries164  have left := finiteDoubleSum.enumerations at D, E, A, add, zero, neg, mul, one, w, f, g, m, n with *165  have right := finiteDoubleSum.enumerations at E, D, A, add, zero, neg, mul, one, transposedMatrix(D, E, A, w), g, f, n, m with *166  cc167