Grace/Cumulus/Algebra/Ring/MatrixRows.g17

Open in Workbench Download source

Imports

Determinant

Declarations

Source

1-- Copying a matrix row as a function graph, with coordinate equations (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.MatrixRows8import Determinant910defunique matrixCopyRowEntry (I A M i r p : Set) (a ∈ A) :=11  ∃ k ∈ I, ∃ j ∈ I, p = (k, j) ∧12    (k = i → a = M[r, j]) ∧ (k ≠ i → a = M[k, j])13requires matrix : RingMatrix(I, A, M)14requires source : r ∈ I15requires pair : p ∈ I × I16proof17  obtain ⟨bound, k, hk, j, hj, shape⟩ := product.membership.forward at18    I, I, p with pair19  have original := RingMatrix.entry at I, A, M, k, j with *20  have copied := RingMatrix.entry at I, A, M, r, j with *21  have alternatives : k = i ∨ k ≠ i22    tauto23  cases alternatives with same | different24  . refine ⟨M[r, j], copied, k, hk, j, hj, shape, ?_⟩25    constructor26    . intro equal27      rfl28    . intro unequal29      exfalso30      exact unequal with same31  . refine ⟨M[k, j], original, k, hk, j, hj, shape, ?_⟩32    constructor33    . intro equal34      exfalso35      exact different with equal36    . intro unequal37      rfl38uniqueness39  intros u hu first v hv second40  obtain ⟨k, hk, j, hj, shapeU, sameU, otherU⟩ := first41  obtain ⟨l, hl, s, hs, shapeV, sameV, otherV⟩ := second42  have pairs : (k, j) = (l, s)43    cc44  have coordinates := orderedPair.injective at k, j, l, s with pairs45  have alternatives : k = i ∨ k ≠ i46    tauto47  cases alternatives with same | different48  . have left : u = M[r, j]49      exact sameU with same50    have right : v = M[r, s]51      apply sameV52      cc53    cc54  . have left : u = M[k, j]55      exact otherU with different56    have distinct : l ≠ i57      intro equal58      apply different59      cc60    have right := otherV with distinct61    cc6263defgraph matrixCopyRow (I A M i r : Set) (p ∈ I × I) : A := matrixCopyRowEntry(I, A, M, i, r, p)64requires matrix : RingMatrix(I, A, M)65requires source : r ∈ I66proof67  have selected := matrixCopyRowEntry.selected at I, A, M, i, r, p with *68  exact selected.left6970theorem matrixCopyRow.matrix (I A M i r : Set)71  requires matrix : RingMatrix(I, A, M)72  requires source : r ∈ I73  shows RingMatrix(I, A, matrixCopyRow(I, A, M, i, r))74proof75  unfold RingMatrix76  exact matrixCopyRow.function with *7778theorem matrixCopyRow.entry (I A M i r k j : Set)79  requires matrix : RingMatrix(I, A, M)80  requires source : r ∈ I81  requires row : k ∈ I82  requires column : j ∈ I83  shows (k = i → matrixCopyRow(I, A, M, i, r)[k, j] = M[r, j]) ∧84    (k ≠ i → matrixCopyRow(I, A, M, i, r)[k, j] = M[k, j])85proof86  have pair := product.pair at k, j, I, I with *87  have value := matrixCopyRow.value at I, A, M, i, r, (k, j) with *88  have selected := matrixCopyRowEntry.selected at I, A, M, i, r, (k, j) with *89  obtain ⟨l, hl, s, hs, shape, same, other⟩ := selected.right90  have coordinates := orderedPair.injective with shape91  rw value92  constructor93  . intro equal94    have match : l = i by cc95    have result := same with match96    cc97  . intro different98    have distinct : l ≠ i99      intro equal100      apply different101      cc102    have result := other with distinct103    cc104105-- Public rewrite lemmas avoid unpacking the conditional specification.106theorem matrixCopyRow.same (I A M i r j : Set)107  requires matrix : RingMatrix(I, A, M)108  requires source : r ∈ I109  requires row : i ∈ I110  requires column : j ∈ I111  shows matrixCopyRow(I, A, M, i, r)[i, j] = M[r, j]112proof113  have entry := matrixCopyRow.entry at I, A, M, i, r, i, j with *114  have equal : i = i by rfl115  exact entry.left with equal116117theorem matrixCopyRow.other (I A M i r k j : Set)118  requires matrix : RingMatrix(I, A, M)119  requires source : r ∈ I120  requires row : k ∈ I121  requires column : j ∈ I122  requires different : k ≠ i123  shows matrixCopyRow(I, A, M, i, r)[k, j] = M[k, j]124proof125  have entry := matrixCopyRow.entry at I, A, M, i, r, k, j with *126  exact entry.right with different127