Grace/Cumulus/Algebra/Ring/Adjugate.g17

Open in Workbench Download source

Imports

Cofactors · MatrixRows · PermutationSign

Declarations

Source

1-- The right-adjugate identity over arbitrary commutative rings (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.Adjugate8import Cofactors9import MatrixRows10import PermutationSign1112section CofactorIdentities13variable (A add zero neg mul one : Set)14notation ring R := (A, add, zero, neg, mul, one)15hypothesis ring : IsCommRing(R)1617theorem cofactorPairing.diagonal (n : Nat) (M i : Set)18  requires matrix : RingMatrix(n, R, M)19  requires row : i ∈ n20  shows cofactorPairing(n, R, M, M, i, i) = determinant(n, R, M)21proof22  have unchanged : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, M[k, j] = M[k, j]23    intros k hk different j hj24    rfl25  have expansion := determinant.row_expansion with *26  cc2728theorem cofactorPairing.off_diagonal (n : Nat) (M i r : Set)29  requires matrix : RingMatrix(n, R, M)30  requires row : i ∈ n31  requires source : r ∈ n32  requires distinct : i ≠ r33  shows cofactorPairing(n, R, M, M, i, r) = R[0]34proof35  have copied := matrixCopyRow.matrix at n, A, M, i, r with *36  have reverse : r ≠ i37    intro equal38    apply distinct39    cc40  have outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[k, j] = M[k, j]41    intros k hk different j hj42    exact matrixCopyRow.other with *43  have equalRows : ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[i, j] = matrixCopyRow(n, A, M, i, r)[r, j]44    intros j hj45    have left := matrixCopyRow.same at n, A, M, i, r, j with *46    have right := matrixCopyRow.other at n, A, M, i, r, r, j with *47    cc48  have vanishes := determinant.equal_rows with *49  have expansion := determinant.row_expansion with *50  have leftWeights := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, matrixCopyRow(n, A, M, i, r), i, i with *51  have rightWeights := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, M, i, r with *52  have entries : ∀ j ∈ n, cofactorPairWeights(n, R, M, matrixCopyRow(n, A, M, i, r), i, i)(j) = cofactorPairWeights(n, R, M, M, i, r)(j)53    intros j hj54    have left := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, matrixCopyRow(n, A, M, i, r), i, i, j with *55    have right := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, M, i, r, j with *56    have copy := matrixCopyRow.same at n, A, M, i, r, j with *57    cc58  have equal := finiteRingSum.congr with *59  unfold cofactorPairing at expansion60  unfold cofactorPairing61  cc6263end CofactorIdentities6465-- The adjugate transposes the cofactor array.66defunique adjugateEntry (I A add zero neg mul one M p : Set) (a ∈ A) :=67  ∃ i ∈ I, ∃ j ∈ I, p = (i, j) ∧ a = cofactorRow(I, A, add, zero, neg, mul, one, M, j)(i)68requires ring : IsCommRing(A, add, zero, neg, mul, one)69requires finite : Finite(I)70requires matrix : RingMatrix(I, A, M)71requires pair : p ∈ I × I72proof73  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at74    I, I, p with *75  have row := cofactorRow.function at I, A, add, zero, neg, mul, one, M, j with *76  have value := FunctionBetween.apply_closed at cofactorRow(I, A, add, zero, neg, mul, one, M, j), I, A, i with *77  refine ⟨cofactorRow(I, A, add, zero, neg, mul, one, M, j)(i), value, i, hi, j, hj, shape, rfl⟩78uniqueness79  intros u hu first v hv second80  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first81  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second82  have equal : (i, j) = (k, l)83    cc84  have coordinates := orderedPair.injective at i, j, k, l with equal85  cc8687defgraph adjugate (I A add zero neg mul one M : Set) (p ∈ I × I) : A :=88  adjugateEntry(I, A, add, zero, neg, mul, one, M, p)89requires ring : IsCommRing(A, add, zero, neg, mul, one)90requires finite : Finite(I)91requires matrix : RingMatrix(I, A, M)92proof93  have selected := adjugateEntry.selected at I, A, add, zero, neg, mul, one, M, p with *94  exact selected.left9596notation scoped adjugate(I, R, M) => adjugate(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)9798section Adjugates99variable (I A add zero neg mul one M : Set)100notation ring R := (A, add, zero, neg, mul, one)101hypothesis ring : IsCommRing(R)102hypothesis finite : Finite(I)103hypothesis matrix : RingMatrix(I, R, M)104105theorem adjugate.matrix106  shows RingMatrix(I, R, adjugate(I, R, M))107proof108  unfold RingMatrix109  exact adjugate.function with *110111theorem adjugate.entry (i j : Set)112  requires row : i ∈ I113  requires column : j ∈ I114  shows adjugate(I, R, M)[i, j] = cofactorRow(I, R, M, j)(i)115proof116  have pair := product.pair at i, j, I, I with *117  have selected := adjugateEntry.selected at I, A, add, zero, neg, mul, one, M, (i, j) with *118  obtain ⟨k, hk, l, hl, shape, result⟩ := selected.right119  have coordinates := orderedPair.injective with shape120  have value := adjugate.value at I, A, add, zero, neg, mul, one, M, (i, j) with *121  cc122123end Adjugates124125defgraph matrixProductWeights (I A add zero neg mul one M N i j : Set) (k ∈ I) : A :=126  call2(mul, M[i, k], N[k, j])127requires ring : IsCommRing(A, add, zero, neg, mul, one)128requires matrixM : RingMatrix(I, A, M)129requires matrixN : RingMatrix(I, A, N)130requires row : i ∈ I131requires column : j ∈ I132proof133  have left := RingMatrix.entry at I, A, M, i, k with *134  have right := RingMatrix.entry at I, A, N, k, j with *135  have ordinary := IsCommRing.ring with ring136  exact IsRing.mul_closed with ordinary, left, right137138notation scoped matrixProductWeights(I, R, M, N, i, j) => matrixProductWeights(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, N, i, j)139140def matrixProductEntry (I A add zero neg mul one M N i j : Set) : Set :=141  finiteRingSum(I, A, add, zero, neg, mul, one, matrixProductWeights(I, A, add, zero, neg, mul, one, M, N, i, j))142143notation scoped matrixProductEntry(I, R, M, N, i, j) => matrixProductEntry(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, N, i, j)144145section Identity146variable (A add zero neg mul one : Set)147notation ring R := (A, add, zero, neg, mul, one)148hypothesis ring : IsCommRing(R)149150theorem adjugate.right_identity (n : Nat) (M i j : Set)151  requires matrix : RingMatrix(n, R, M)152  requires row : i ∈ n153  requires column : j ∈ n154  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, j) =155    singleValue(A, zero, determinant(n, R, M), j, i)156proof157  have adj := adjugate.matrix at n, A, add, zero, neg, mul, one, M with *158  have products := matrixProductWeights.function at n, A, add, zero, neg, mul, one, M, adjugate(n, R, M), i, j with *159  have cofactors := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, M, j, i with *160  have entries : ∀ k ∈ n, matrixProductWeights(n, R, M, adjugate(n, R, M), i, j)(k) = cofactorPairWeights(n, R, M, M, j, i)(k)161    intros k hk162    have left := matrixProductWeights.value at n, A, add, zero, neg, mul, one, M, adjugate(n, R, M), i, j, k with *163    have right := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, M, j, i, k with *164    have entry := adjugate.entry at n, A, add, zero, neg, mul, one, M, k, j with *165    cc166  have sums := finiteRingSum.congr at n, A, add, zero, neg, mul, one, matrixProductWeights(n, R, M, adjugate(n, R, M), i, j), cofactorPairWeights(n, R, M, M, j, i) with *167  have ordinary := IsCommRing.ring with ring168  have zeroIn := IsRing.zero_in_carrier with ordinary169  have alternatives : i = j ∨ i ≠ j by tauto170  cases alternatives with same | different171  . have diagonal := cofactorPairing.diagonal at A, add, zero, neg, mul, one, n, M, i with *172    have single := singleValue.same at A, zero, determinant(n, R, M), j, i with *173    unfold matrixProductEntry174    unfold cofactorPairing at diagonal175    cc176  . have distinct : j ≠ i177      intro equal178      apply different179      cc180    have offDiagonal := cofactorPairing.off_diagonal at A, add, zero, neg, mul, one, n, M, j, i with *181    have single := singleValue.other at A, zero, determinant(n, R, M), j, i with *182    unfold matrixProductEntry183    unfold cofactorPairing at offDiagonal184    cc185186-- Ordinary applications need not expose the Kronecker-delta encoding.187theorem adjugate.right_diagonal (n : Nat) (M i : Set)188  requires matrix : RingMatrix(n, R, M)189  requires row : i ∈ n190  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, i) = determinant(n, R, M)191proof192  have identity := adjugate.right_identity with *193  have ordinary := IsCommRing.ring with ring194  have zeroIn := IsRing.zero_in_carrier with ordinary195  have same : i = i by rfl196  have value := singleValue.same at A, zero, determinant(n, R, M), i, i with *197  cc198199theorem adjugate.right_off_diagonal (n : Nat) (M i j : Set)200  requires matrix : RingMatrix(n, R, M)201  requires row : i ∈ n202  requires column : j ∈ n203  requires distinct : i ≠ j204  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, j) = R[0]205proof206  have identity := adjugate.right_identity at A, add, zero, neg, mul, one, n, M, i, j with *207  have ordinary := IsCommRing.ring with ring208  have zeroIn := IsRing.zero_in_carrier with ordinary209  have value := singleValue.other at A, zero, determinant(n, R, M), j, i with *210  cc211212end Identity213