Grace/Cumulus/Algebra/Ring/DoubleSum.g17

Open in Workbench Download source

Imports

SumSupport · Cardinal.Product

Declarations

Source

1-- Interchange of arbitrary finite rectangular sums over a commutative ring (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.DoubleSum8import SumSupport9import Cardinal.Product1011predicate RingRowValues (w A x n : Set) := ∀ j ∈ n, w((x, j)) ∈ A12predicate RingMatrixValues (w A m n : Set) := ∀ i ∈ m, RingRowValues(w, A, i, n)13predicate TransposedValues (w v m n : Set) := ∀ i ∈ m, ∀ j ∈ n, w((i, j)) = v((j, i))1415def ringRowSum (w add z x : Set, n : Nat) → Set16  | w, add, z, x, zero => z17  | w, add, z, x, succ(k) => call2(add, ringRowSum(w, add, z, x, k), w((x, k)))1819def ringDoubleSum (w add z : Set, m n : Nat) → Set20  | w, add, z, zero, n => z21  | w, add, z, succ(k), n => call2(add, ringDoubleSum(w, add, z, k, n), ringRowSum(w, add, z, k, n))2223theorem RingRowValues.prefix (w A x : Set, n : Nat)24  requires values : RingRowValues(w, A, x, succ(n))25  shows RingRowValues(w, A, x, n)26proof27  intros j hj28  have included := membership.into_successor with *29  exact values with j, included3031theorem RingRowValues.last (w A x : Set, n : Nat)32  requires values : RingRowValues(w, A, x, succ(n))33  shows w((x, n)) ∈ A34proof35  exact values with n, membership.self_successor at n with *3637theorem RingMatrixValues.prefix (w A n : Set, m : Nat)38  requires values : RingMatrixValues(w, A, succ(m), n)39  shows RingMatrixValues(w, A, m, n)40proof41  intros i hi42  have included := membership.into_successor with *43  exact values with i, included4445theorem RingMatrixValues.last (w A n : Set, m : Nat)46  requires values : RingMatrixValues(w, A, succ(m), n)47  shows RingRowValues(w, A, m, n)48proof49  exact values with m, membership.self_successor at m with *5051section Rings52variable (A add zero neg mul one : Set)53hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)54notation ring R := (A, add, zero, neg, mul, one)5556theorem ringRowSum.closed (w x : Set, n : Nat)57  shows RingRowValues(w, A, x, n) → ringRowSum(w, add, zero, x, n) ∈ A58proof59  induction n60  | zero =>61    intro values62    have ordinary := IsCommRing.ring with ring63    rw ringRowSum64    exact IsRing.zero_in_carrier with ordinary65  | succ(k) using ih =>66    intro values67    have ordinary := IsCommRing.ring with ring68    have prefix := RingRowValues.prefix at w, A, x, k with *69    have last := RingRowValues.last at w, A, x, k with *70    have previous := ih with prefix71    rw ringRowSum72    exact IsRing.add_closed with ordinary, previous, last7374theorem ringDoubleSum.closed (w : Set, m n : Nat)75  shows RingMatrixValues(w, A, m, n) → ringDoubleSum(w, add, zero, m, n) ∈ A76proof77  induction m78  | zero =>79    intro values80    have ordinary := IsCommRing.ring with ring81    rw ringDoubleSum82    exact IsRing.zero_in_carrier with ordinary83  | succ(k) using ih =>84    intro values85    have ordinary := IsCommRing.ring with ring86    have prefix := RingMatrixValues.prefix at w, A, n, k with *87    have last := RingMatrixValues.last at w, A, n, k with *88    have previous := ih with prefix89    have rowClosed := ringRowSum.closed at A, add, zero, neg, mul, one, w, k, n with *90    have row := rowClosed with last91    rw ringDoubleSum92    exact IsRing.add_closed with ordinary, previous, row9394theorem ringDoubleSum.empty_columns (w : Set, m : Nat)95  shows ringDoubleSum(w, add, zero, m, (0:Nat)) = zero96proof97  induction m98  | zero =>99    rw ringDoubleSum100    rfl101  | succ(k) using ih =>102    rw [ringDoubleSum, ringRowSum, ih]103    ring104105-- A new column contributes one row of the transposed matrix.106theorem ringDoubleSum.extend_columns (w v : Set, m n : Nat)107  shows RingMatrixValues(w, A, m, succ(n)) → RingRowValues(v, A, n, m) →108    (∀ i ∈ m, w((i, n)) = v((n, i))) →109    ringDoubleSum(w, add, zero, m, succ(n)) = ringDoubleSum(w, add, zero, m, n) + ringRowSum(v, add, zero, n, m)110proof111  induction m112  | zero =>113    intros values rowValues transposed114    simp [ringDoubleSum, ringRowSum]115    ring116  | succ(k) using ih =>117    intros values rowValues transposed118    have prefix := RingMatrixValues.prefix at w, A, succ(n), k with *119    have last := RingMatrixValues.last at w, A, succ(n), k with *120    have rowPrefix := RingRowValues.prefix at v, A, n, k with *121    have rowLast := RingRowValues.last at v, A, n, k with *122    have prefixTranspose : ∀ i ∈ k, w((i, n)) = v((n, i))123      intros i hi124      have included := membership.into_successor at i, k with *125      exact transposed with i, included126    have lastTranspose := transposed with k, membership.self_successor at k with *127    have previous := ih with prefix, rowPrefix, prefixTranspose128    have shorter : RingMatrixValues(w, A, k, n)129      intros i hi130      have row := prefix with i, hi131      exact RingRowValues.prefix at w, A, i, n with *132    have lastPrefix := RingRowValues.prefix at w, A, k, n with *133    have totalClosed := ringDoubleSum.closed at A, add, zero, neg, mul, one, w, k, n with *134    have totalIn := totalClosed with shorter135    have columnClosed := ringRowSum.closed at A, add, zero, neg, mul, one, v, n, k with *136    have columnIn := columnClosed with rowPrefix137    have rowClosed := ringRowSum.closed at A, add, zero, neg, mul, one, w, k, n with *138    have rowIn := rowClosed with lastPrefix139    rw [ringDoubleSum, ringDoubleSum, ringRowSum, ringRowSum, previous, lastTranspose]140    ring141142theorem ringDoubleSum.transpose (w v : Set, m n : Nat)143  shows RingMatrixValues(w, A, m, n) → RingMatrixValues(v, A, n, m) → TransposedValues(w, v, m, n) →144    ringDoubleSum(w, add, zero, m, n) = ringDoubleSum(v, add, zero, n, m)145proof146  induction n147  | zero =>148    intros valuesW valuesV transposed149    have empty := ringDoubleSum.empty_columns at A, add, zero, neg, mul, one, w, m with *150    rw [empty, ringDoubleSum]151    rfl152  | succ(k) using ih =>153    intros valuesW valuesV transposed154    have prefixW : RingMatrixValues(w, A, m, k)155      have rows := valuesW156      intros i hi157      have row := rows with i, hi158      exact RingRowValues.prefix at w, A, i, k with *159    have prefixV := RingMatrixValues.prefix at v, A, m, k with *160    have lastV := RingMatrixValues.last at v, A, m, k with *161    have prefixTranspose : TransposedValues(w, v, m, k)162      intros i hi j hj163      have included := membership.into_successor at j, k with *164      exact transposed with i, hi, j, included165    have lastTranspose : ∀ i ∈ m, w((i, k)) = v((k, i))166      intros i hi167      exact transposed with i, hi, k, membership.self_successor at k with *168    have previous := ih with prefixW, prefixV, prefixTranspose169    have extension := ringDoubleSum.extend_columns at A, add, zero, neg, mul, one, w, v, m, k with *, valuesW, lastV, lastTranspose170    rw [extension, ringDoubleSum, previous]171    rfl172173end Rings174175-- A matrix is a function on a Cartesian rectangle.176theorem RingMatrixValues.of_function (w A m n : Set)177  requires function : w : m × n → A178  shows RingMatrixValues(w, A, m, n)179proof180  intros i hi j hj181  have pair := product.pair with hi, hj182  exact FunctionBetween.apply_closed with *183184defgraph transposedMatrix (m n A w : Set) (p ∈ n × m) : A := w(productSwap(n, m)(p))185requires matrix : w : m × n → A186proof187  have swap := productSwap.function at n, m188  have pair := FunctionBetween.apply_closed with *189  exact FunctionBetween.apply_closed with *190191theorem transposedMatrix.pair (m n A w i j : Set)192  requires matrix : w : m × n → A193  requires row : i ∈ m194  requires column : j ∈ n195  shows transposedMatrix(m, n, A, w)((j, i)) = w((i, j))196proof197  have pair := product.pair at j, i, n, m with *198  have swap := productSwap.pair at n, m, j, i with *199  have value := transposedMatrix.value at m, n, A, w, (j, i) with *200  cc201202theorem transposedMatrix.involution (m n A w : Set)203  requires matrix : w : m × n → A204  shows transposedMatrix(n, m, A, transposedMatrix(m, n, A, w)) = w205proof206  have once := transposedMatrix.function at m, n, A, w with *207  have twice := transposedMatrix.function at n, m, A, transposedMatrix(m, n, A, w) with *208  apply FunctionBetween.ext with twice, matrix209  intros p hp210  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with hp211  have first := transposedMatrix.pair at m, n, A, w, i, j with *212  have second := transposedMatrix.pair at n, m, A, transposedMatrix(m, n, A, w), j, i with *213  cc214215-- Public interface: one matrix graph, with all side conditions explicit.216theorem ringDoubleSum.interchange (A add zero neg mul one w : Set, m n : Nat)217  requires ring : IsCommRing(A, add, zero, neg, mul, one)218  requires matrix : w : m × n → A219  shows ringDoubleSum(w, add, zero, m, n) = ringDoubleSum(transposedMatrix(m, n, A, w), add, zero, n, m)220proof221  have transposed := transposedMatrix.function at m, n, A, w with *222  have valuesW := RingMatrixValues.of_function with matrix223  have valuesV := RingMatrixValues.of_function with transposed224  have entries : TransposedValues(w, transposedMatrix(m, n, A, w), m, n)225    intros i hi j hj226    symm227    exact transposedMatrix.pair with *228  have interchange := ringDoubleSum.transpose at A, add, zero, neg, mul, one, w, transposedMatrix(m, n, A, w), m, n with *229  exact interchange with valuesW, valuesV, entries230