Grace/Cumulus/Algebra/Ring/MatrixCramer.g17

Open in Workbench Download source

Imports

MatrixEntries

Declarations

Source

1-- Cramer's rule and the adjugate inverse over a bundled commutative ring:2-- for a solution x of the row system x · M = b, det(M) · x(i) is the3-- determinant of M with row i replaced by b, and when det(M) is a unit4-- the matrix det(M)⁻¹ · adj(M) is a right inverse of M; everything here5-- is ZF6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Ring.MatrixCramer12import MatrixEntries1314-- The scalar multiple a · M, entry by entry.15defgraph scalarMultiple (R n a M : Set) (p ∈ n × n) : Ring.carrier(R) :=16  call2(Ring.mul(R), a, M(p))17requires ring : Ring(R)18requires scalar : a ∈ Ring.carrier(R)19requires matrix : M : R ^ n × n20proof21  have function := Matrix.function with matrix22  have entry := FunctionBetween.apply_closed with function, member23  exact Ring.mul_mem with *2425-- The row vector x · M of a vector x : n → R.26defgraph rowProduct (R : Set, n : Nat, x M : Set) (j ∈ n) : Ring.carrier(R) :=27  rowVectorEntry(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),28    Ring.mul(R), Ring.one(R), x, M, j)29requires comm : CommRing(R)30requires vector : x : n → Ring.carrier(R)31requires matrix : M : R ^ n × n32proof33  have parts := CommRing.parts with comm34  have square := Matrix.square with matrix35  have shape := squareMatrices.membership.forward with square36  have finite := Finite.natural at n37  have weights := rowVectorWeights.function at n, Ring.carrier(R), Ring.add(R),38    Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), x, M, j with *39  unfold rowVectorEntry40  exact finiteRingSum.closed with *4142section Scalars43variable (R : Set) (n : Nat)44hypothesis comm : CommRing(R)4546theorem scalarMultiple.entry (a : R) (M : R ^ n × n) (i j : Set)47  requires row : i ∈ n48  requires column : j ∈ n49  shows scalarMultiple(R, n, a, M)[i, j] = a * M[i, j]50proof51  have pair := product.pair at i, j, n, n with *52  exact scalarMultiple.value at R, n, a, M, (i, j) with *5354instance scalarMultiple.matrix (a : R) (M : R ^ n × n)55  shows scalarMultiple(R, n, a, M) : R ^ n × n56proof57  have function := scalarMultiple.function at R, n, a, M with *58  exact Matrix.of_function with function5960theorem rowProduct.entry (x : Set) (M : R ^ n × n) (j : Set)61  requires vector : x : n → R.carrier62  requires column : j ∈ n63  shows rowProduct(R, n, x, M)(j) = rowVectorEntry(n, R.carrier, R.add, R.zero,64    R.neg, R.mul, R.one, x, M, j)65proof66  exact rowProduct.value with *6768end Scalars6970-- The terms x(k) · M[k, j] · C(j), C the cofactor row, as an array over71-- n × n indexed by (j, k).72defunique cramerWeightValue (R : Set, n : Nat, x M i q : Set) (a ∈ Ring.carrier(R)) :=73  ∃ j ∈ n, ∃ k ∈ n, q = (j, k) ∧74    a = call2(Ring.mul(R), x(k), call2(Ring.mul(R), M[k, j],75      cofactorRow(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),76        Ring.mul(R), Ring.one(R), M, i)(j)))77requires comm : CommRing(R)78requires vector : x : n → Ring.carrier(R)79requires matrix : M : R ^ n × n80requires row : i ∈ n81requires pair : q ∈ n × n82proof83  obtain ⟨bound, j, hj, k, hk, shape⟩ := product.membership.forward at84    n, n, q with *85  have parts := CommRing.parts with comm86  have square := Matrix.square with matrix87  have shapeM := squareMatrices.membership.forward with square88  have finite := Finite.natural at n89  have cofactors := cofactorRow.function at n, Ring.carrier(R), Ring.add(R),90    Ring.zero(R), Ring.neg(R), Ring.mul(R), Ring.one(R), M, i with *91  have cofactor := FunctionBetween.apply_closed with cofactors, hj92  have coordinate := FunctionBetween.apply_closed with vector, hk93  have entry := Matrix.entry at M, R, n, k, j with *94  have ordinary := IsCommRing.ring with parts95  have inner := IsRing.mul_closed with ordinary, entry, cofactor96  have value := IsRing.mul_closed with ordinary, coordinate, inner97  refine ⟨call2(Ring.mul(R), x(k), call2(Ring.mul(R), M[k, j],98    cofactorRow(n, Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R),99      Ring.mul(R), Ring.one(R), M, i)(j))), value, j, hj, k, hk, shape, rfl⟩100uniqueness101  intros u hu first v hv second102  obtain ⟨j, hj, k, hk, shapeU, valueU⟩ := first103  obtain ⟨a, ha, b, hb, shapeV, valueV⟩ := second104  have equal : (j, k) = (a, b)105    cc106  have coordinates := orderedPair.injective at j, k, a, b with equal107  cc108109defgraph cramerWeights (R : Set, n : Nat, x M i : Set) (q ∈ n × n) : Ring.carrier(R) :=110  cramerWeightValue(R, n, x, M, i, q)111requires comm : CommRing(R)112requires vector : x : n → Ring.carrier(R)113requires matrix : M : R ^ n × n114requires row : i ∈ n115proof116  have selected := cramerWeightValue.selected at R, n, x, M, i, q with *117  exact selected.left118119theorem cramerWeights.pair (R : Set, n : Nat, x M i j k : Set)120  requires comm : CommRing(R)121  requires vector : x : n → Ring.carrier(R)122  requires matrix : M : R ^ n × n123  requires row : i ∈ n124  requires hj : j ∈ n125  requires hk : k ∈ n126  shows cramerWeights(R, n, x, M, i)((j, k)) =127    x(k) * (M[k, j] * cofactorRow(n, R.carrier, R.add, R.zero, R.neg, R.mul,128      R.one, M, i)(j))129proof130  have pair := product.pair at j, k, n, n with *131  have selected := cramerWeightValue.selected at R, n, x, M, i, (j, k) with *132  obtain ⟨a, ha, b, hb, shape, result⟩ := selected.right133  have coordinates := orderedPair.injective with shape134  have value := cramerWeights.value at R, n, x, M, i, (j, k) with *135  cc136137section Cramer138variable (R : Set) (n : Nat)139hypothesis comm : CommRing(R)140141-- Cramer's rule: a solution x of x · M = b has det(M) · x(i) equal to the142-- determinant of the matrix N obtained from M by replacing row i by b.143theorem Matrix.cramer (M N : R ^ n × n) (x b i : Set)144  requires vector : x : n → R.carrier145  requires solution : ∀ j ∈ n, rowProduct(R, n, x, M)(j) = b(j)146  requires row : i ∈ n147  requires replaced : ∀ j ∈ n, N[i, j] = b(j)148  requires outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, N[k, j] = M[k, j]149  shows det(M) * x(i) = det(N)150proof151  have parts := CommRing.parts with comm152  have squareM := Matrix.square at M, R, n with assumption153  have squareN := Matrix.square at N, R, n with assumption154  have shapeM := squareMatrices.membership.forward with squareM155  have shapeN := squareMatrices.membership.forward with squareN156  have finite := Finite.natural at n157  have adjugateShape := adjugate.matrix at n, R.carrier, R.add, R.zero, R.neg,158    R.mul, R.one, M with *159  have determinantIn := Matrix.det_mem at R, n, M with *160  have coordinate := FunctionBetween.apply_closed with vector, row161  have cofactors := cofactorRow.function at n, R.carrier, R.add, R.zero, R.neg,162    R.mul, R.one, M, i with *163  have array := cramerWeights.function at R, n, x, M, i with *164  have transposed := transposedMatrix.function at n, n, R.carrier,165    cramerWeights(R, n, x, M, i) with *166  have rowsL := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,167    R.mul, R.one, cramerWeights(R, n, x, M, i) with *168  have rowsR := finiteRowSums.function at n, n, R.carrier, R.add, R.zero, R.neg,169    R.mul, R.one, transposedMatrix(n, n, R.carrier, cramerWeights(R, n, x, M, i)) with *170  have pairWeights := cofactorPairWeights.function at n, R.carrier, R.add,171    R.zero, R.neg, R.mul, R.one, M, N, i, i with *172  have selector := coefficientSingle.function at n, R.carrier, R.zero,173    det(M) * x(i), i with *174  -- Row expansion of det(N) along the replaced row, as a double sum.175  have expansion := determinant.row_expansion at R.carrier, R.add, R.zero, R.neg,176    R.mul, R.one, n, M, N, i with *177  have leftRows : ∀ j ∈ n, cofactorPairWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, M, N, i, i)(j) =178      finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, cramerWeights(R, n, x, M, i))(j)179    intros j hj180    have cofactor := FunctionBetween.apply_closed with cofactors, hj181    have rowWeights := finiteRowWeights.function at n, n, R.carrier,182      cramerWeights(R, n, x, M, i), j with *183    have inner := rowVectorWeights.function at n, R.carrier, R.add, R.zero,184      R.neg, R.mul, R.one, x, M, j with *185    have scaled : ∀ k ∈ n, finiteRowWeights(n, n, Ring.carrier(R), cramerWeights(R, n, x, M, i), j)(k) =186        cofactorRow(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, M, i)(j) * rowVectorWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, x, M, j)(k)187      intros k hk188      have entry := Matrix.entry at M, R, n, k, j with *189      have coordinateK := FunctionBetween.apply_closed with vector, hk190      have rowWeight := finiteRowWeights.value at n, n, R.carrier,191        cramerWeights(R, n, x, M, i), j, k with *192      have cell := cramerWeights.pair at R, n, x, M, i, j, k with *193      have weight := rowVectorWeights.value at n, R.carrier, R.add, R.zero,194        R.neg, R.mul, R.one, x, M, j, k with *195      rw [rowWeight, cell, weight]196      ring197    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,198      R.mul, R.one, rowVectorWeights(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, x, M, j),199      finiteRowWeights(n, n, R.carrier, cramerWeights(R, n, x, M, i), j),200      cofactorRow(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, i)(j) with *201    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,202      R.mul, R.one, cramerWeights(R, n, x, M, i), j with *203    have weight := cofactorPairWeights.value at n, R.carrier, R.add, R.zero,204      R.neg, R.mul, R.one, M, N, i, i, j with *205    have entryN := replaced with j, hj206    have solved := solution with j, hj207    have product := rowProduct.entry at R, n, x, M, j with *208    have closed := finiteRingSum.closed at n, R.carrier, R.add, R.zero, R.neg,209      R.mul, R.one, rowVectorWeights(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, x, M, j) with *210    unfold rowVectorEntry at product211    rw [weight, rowSum, scale, entryN, ← solved, product]212    ring213  -- After interchanging, the inner sums are the entries of M · adj(M).214  have rightRows : ∀ k ∈ n, finiteRowSums(n, n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, transposedMatrix(n, n, Ring.carrier(R), cramerWeights(R, n, x, M, i)))(k) =215      coefficientSingle(n, Ring.carrier(R), R.zero, det(M) * x(i), i)(k)216    intros k hk217    have coordinateK := FunctionBetween.apply_closed with vector, hk218    have rowWeights := finiteRowWeights.function at n, n, R.carrier,219      transposedMatrix(n, n, R.carrier, cramerWeights(R, n, x, M, i)), k with *220    have inner := matrixProductWeights.function at n, R.carrier, R.add, R.zero,221      R.neg, R.mul, R.one, M, adj(M), k, i with *222    have scaled : ∀ j ∈ n, finiteRowWeights(n, n, Ring.carrier(R), transposedMatrix(n, n, Ring.carrier(R), cramerWeights(R, n, x, M, i)), k)(j) =223        x(k) * matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, M, adj(M), k, i)(j)224      intros j hj225      have rowWeight := finiteRowWeights.value at n, n, R.carrier,226        transposedMatrix(n, n, R.carrier, cramerWeights(R, n, x, M, i)), k, j with *227      have swap := transposedMatrix.pair at n, n, R.carrier,228        cramerWeights(R, n, x, M, i), j, k with *229      have cell := cramerWeights.pair at R, n, x, M, i, j, k with *230      have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,231        R.neg, R.mul, R.one, M, adj(M), k, i, j with *232      have entry := Matrix.adj_entry at R, n, M, j, i with *233      rw [rowWeight, swap, cell, weight, entry]234      rfl235    have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,236      R.mul, R.one, matrixProductWeights(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, adj(M), k, i),237      finiteRowWeights(n, n, R.carrier, transposedMatrix(n, n, R.carrier, cramerWeights(R, n, x, M, i)), k),238      x(k) with *239    have rowSum := finiteRowSums.value at n, n, R.carrier, R.add, R.zero, R.neg,240      R.mul, R.one, transposedMatrix(n, n, R.carrier, cramerWeights(R, n, x, M, i)), k with *241    have identity := adjugate.right_identity at R.carrier, R.add, R.zero, R.neg,242      R.mul, R.one, n, M, k, i with *243    have zeroIn : R[0] ∈ R := Ring.zero_mem with *244    unfold matrixProductEntry at identity245    rw [rowSum, scale, identity]246    have alternatives : k = i ∨ k ≠ i by tauto247    cases alternatives with same | different248    . have delta := singleValue.same at R.carrier, R.zero, det(M), i, k with *249      have selected := coefficientSingle.same at n, R.carrier, R.zero, det(M) * x(i), i with *250      rw [delta, same, selected]251      ring252    . have reverse : i ≠ k253        intro equal254        apply different255        cc256      have delta := singleValue.other at R.carrier, R.zero, det(M), i, k with *257      have selected := coefficientSingle.other at n, R.carrier, R.zero, det(M) * x(i), i, k with *258      rw [delta, selected]259      ring260  have sameL := finiteRingSum.congr with leftRows261  have sameR := finiteRingSum.congr with rightRows262  have interchange := finiteDoubleSum.interchange at n, n, R.carrier, R.add, R.zero,263    R.neg, R.mul, R.one, cramerWeights(R, n, x, M, i) with *264  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,265    R.mul, R.one, det(M) * x(i), i with *266  unfold finiteDoubleSum at interchange267  unfold cofactorPairing at expansion268  cc269270end Cramer271272section Inverse273variable (R : Set) (n : Nat)274hypothesis comm : CommRing(R)275276-- The adjugate identity in the matrix ring.277theorem Matrix.mul_adj (M : R ^ n × n)278  shows M * adj(M) = scalarMultiple(R, n, det(M), matrixRing(R, n)[1])279proof280  have parts := CommRing.parts with comm281  have square := Matrix.square at M, R, n with assumption282  have shape := squareMatrices.membership.forward with square283  have finite := Finite.natural at n284  have determinantIn := Matrix.det_mem at R, n, M with *285  have adjugate := Matrix.adj_matrix at R, n, M with *286  have one := Matrix.of_mem at matrixRing(R, n)[1], R, n with (Ring.one_mem with *)287  have product := Matrix.of_mem at M * adj(M), R, n with (Ring.mul_mem with *)288  have scaled := scalarMultiple.matrix at R, n, det(M), matrixRing(R, n)[1] with *289  apply Matrix.ext with product, scaled290  intros i hi j hj291  have entry := matrixRing.mul_entry at R, n, M, adj(M), i, j with *292  have identity := adjugate.right_identity at R.carrier, R.add, R.zero, R.neg,293    R.mul, R.one, n, M, i, j with *294  have scale := scalarMultiple.entry at R, n, det(M), matrixRing(R, n)[1], i, j with *295  have unit := matrixRing.one_entry at R, n, i, j with *296  have zeroIn : R[0] ∈ R := Ring.zero_mem with *297  have oneIn : R[1] ∈ R := Ring.one_mem with *298  rw [entry, identity, scale, unit]299  have alternatives : i = j ∨ i ≠ j by tauto300  cases alternatives with same | different301  . have deltaD := singleValue.same at R.carrier, R.zero, det(M), j, i with *302    have deltaO := singleValue.same at R.carrier, R.zero, R.one, j, i with *303    rw [deltaD, deltaO]304    ring305  . have deltaD := singleValue.other at R.carrier, R.zero, det(M), j, i with *306    have deltaO := singleValue.other at R.carrier, R.zero, R.one, j, i with *307    rw [deltaD, deltaO]308    ring309310-- When det(M) has an inverse u, the matrix u · adj(M) is a right inverse.311theorem Matrix.mul_inverse (M : R ^ n × n) (u : R)312  requires inverse : u * det(M) = R[1]313  shows M * scalarMultiple(R, n, u, adj(M)) = matrixRing(R, n)[1]314proof315  have parts := CommRing.parts with comm316  have square := Matrix.square at M, R, n with assumption317  have shape := squareMatrices.membership.forward with square318  have finite := Finite.natural at n319  have determinantIn := Matrix.det_mem at R, n, M with *320  have adjugate := Matrix.adj_matrix at R, n, M with *321  have adjugateShape := adjugate.matrix at n, R.carrier, R.add, R.zero, R.neg,322    R.mul, R.one, M with *323  have scaled := scalarMultiple.matrix at R, n, u, adj(M) with *324  have scaledSquare := Matrix.square at scalarMultiple(R, n, u, adj(M)), R, n with *325  have scaledShape := squareMatrices.membership.forward with scaledSquare326  have one := Matrix.of_mem at matrixRing(R, n)[1], R, n with (Ring.one_mem with *)327  have product := Matrix.of_mem at M * scalarMultiple(R, n, u, adj(M)), R, n with (Ring.mul_mem with *)328  have uIn : u ∈ R by assumption329  apply Matrix.ext with product, one330  intros i hi j hj331  have entry := matrixRing.mul_entry at R, n, M, scalarMultiple(R, n, u, adj(M)), i, j with *332  have weightsA := matrixProductWeights.function at n, R.carrier, R.add, R.zero,333    R.neg, R.mul, R.one, M, adj(M), i, j with *334  have weightsS := matrixProductWeights.function at n, R.carrier, R.add, R.zero,335    R.neg, R.mul, R.one, M, scalarMultiple(R, n, u, adj(M)), i, j with *336  have scaledWeights : ∀ k ∈ n, matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, M, scalarMultiple(R, n, u, adj(M)), i, j)(k) =337      u * matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, M, adj(M), i, j)(k)338    intros k hk339    have entryM := Matrix.entry at M, R, n, i, k with *340    have entryA := Matrix.entry at adj(M), R, n, k, j with *341    have weightA := matrixProductWeights.value at n, R.carrier, R.add, R.zero,342      R.neg, R.mul, R.one, M, adj(M), i, j, k with *343    have weightS := matrixProductWeights.value at n, R.carrier, R.add, R.zero,344      R.neg, R.mul, R.one, M, scalarMultiple(R, n, u, adj(M)), i, j, k with *345    have scale := scalarMultiple.entry at R, n, u, adj(M), k, j with *346    rw [weightA, weightS, scale]347    ring348  have scale := finiteRingSum.scale_eq at n, R.carrier, R.add, R.zero, R.neg,349    R.mul, R.one, matrixProductWeights(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, adj(M), i, j),350    matrixProductWeights(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, scalarMultiple(R, n, u, adj(M)), i, j), u with *351  have identity := adjugate.right_identity at R.carrier, R.add, R.zero, R.neg,352    R.mul, R.one, n, M, i, j with *353  have unit := matrixRing.one_entry at R, n, i, j with *354  have zeroIn : R[0] ∈ R := Ring.zero_mem with *355  have oneIn : R[1] ∈ R := Ring.one_mem with *356  unfold matrixProductEntry at identity357  unfold matrixProductEntry at entry358  rw [entry, unit, scale, identity]359  have alternatives : i = j ∨ i ≠ j by tauto360  cases alternatives with same | different361  . have deltaD := singleValue.same at R.carrier, R.zero, det(M), j, i with *362    have deltaO := singleValue.same at R.carrier, R.zero, R.one, j, i with *363    rw [deltaD, deltaO]364    exact inverse365  . have deltaD := singleValue.other at R.carrier, R.zero, det(M), j, i with *366    have deltaO := singleValue.other at R.carrier, R.zero, R.one, j, i with *367    rw [deltaD, deltaO]368    ring369370end Inverse371