Grace/Cumulus/Algebra/Ring/Cofactors.g17

Open in Workbench Download source

Imports

Determinant · WeightedRegrouping

Declarations

Source

1-- Cofactors from grouped Leibniz terms and expansion along a replaced row (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.Cofactors8import Determinant9import WeightedRegrouping1011defgraph permutationColumn (I i : Set) (p ∈ permutations(I)) : I := p(i)12requires row : i ∈ I13proof14  have permutation := permutations.mem_iff.forward at I, p with *15  have injective := Bijective.injective with permutation16  have function := Injective.function with injective17  exact FunctionBetween.apply_closed at p, I, I, i with *1819-- Delete just the distinguished factor, retaining its permutation sign.20defgraph cofactorTerms (I A add zero neg mul one M i : Set) (p ∈ permutations(I)) : A :=21  call2(mul, permutationSign(I, A, add, zero, neg, mul, one, p),22    finiteRingProduct(I ∖ {i}, A, add, zero, neg, mul, one, restrict(permutationEntries(I, A, M, p), I ∖ {i})))23requires ring : IsCommRing(A, add, zero, neg, mul, one)24requires finite : Finite(I)25requires matrix : RingMatrix(I, A, M)26proof27  have permutation := permutations.mem_iff.forward at I, p with *28  have entries := permutationEntries.function at I, A, M, p with *29  have subset := difference.subset_left at I, {i}30  have smaller := Finite.subset with finite, subset31  have restricted := restrict.domain_function at permutationEntries(I, A, M, p), I, A, I ∖ {i} with *32  have product := finiteRingProduct.closed at I ∖ {i}, A, add, zero, neg, mul, one, restrict(permutationEntries(I, A, M, p), I ∖ {i}) with *33  have sign := permutationSign.closed at A, add, zero, neg, mul, one, I, p with *34  have ordinary := IsCommRing.ring with ring35  exact IsRing.mul_closed with ordinary, sign, product3637notation scoped cofactorTerms(I, R, M, i) => cofactorTerms(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, i)3839-- Its j-th entry is the signed cofactor at (i,j), defined without reindexing minors.40def cofactorRow (I A add zero neg mul one M i : Set) : Set :=41  finitePushforward(permutations(I), I, A, add, zero, neg, mul, one,42    permutationColumn(I, i), cofactorTerms(I, A, add, zero, neg, mul, one, M, i))4344notation scoped cofactorRow(I, R, M, i) => cofactorRow(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, i)4546section Cofactors47variable (I A add zero neg mul one M i : Set)48notation ring R := (A, add, zero, neg, mul, one)49hypothesis ring : IsCommRing(R)50hypothesis finite : Finite(I)51hypothesis matrix : RingMatrix(I, R, M)5253theorem cofactorRow.function54  shows cofactorRow(I, R, M, i) : I → R55proof56  have permutationsFinite := permutations.finite with finite57  have weights := cofactorTerms.function at I, A, add, zero, neg, mul, one, M, i with *58  unfold cofactorRow59  exact finitePushforward.function with *6061theorem cofactorTerms.factor (N p : Set)62  requires matrixN : RingMatrix(I, R, N)63  requires row : i ∈ I64  requires permutation : BijectiveBetween(p, I, I)65  requires outside : ∀ k ∈ I, k ≠ i → ∀ j ∈ I, N[k, j] = M[k, j]66  shows determinantTerms(I, R, N)(p) = N[i, p(i)] * cofactorTerms(I, R, M, i)(p)67proof68  have member := permutations.mem_iff.backward with permutation69  have injective := Bijective.injective with permutation70  have function := Injective.function with injective71  have column := FunctionBetween.apply_closed at p, I, I, i with *72  have entryIn := RingMatrix.entry at I, A, N, i, p(i) with *73  have subset := difference.subset_left at I, {i}74  have smaller := Finite.subset with finite, subset75  have entriesM := permutationEntries.function at I, A, M, p with *76  have entriesN := permutationEntries.function at I, A, N, p with *77  have restrictedM := restrict.domain_function at permutationEntries(I, A, M, p), I, A, I ∖ {i} with *78  have restrictedN := restrict.domain_function at permutationEntries(I, A, N, p), I, A, I ∖ {i} with *79  have same : ∀ k ∈ I ∖ {i}, restrict(permutationEntries(I, A, N, p), I ∖ {i})(k) = restrict(permutationEntries(I, A, M, p), I ∖ {i})(k)80    intros k hk81    have inI : k ∈ I by simp [difference.membership]82    have different : k ≠ i by simp [difference.membership, singleton.membership]83    have image := FunctionBetween.apply_closed at p, I, I, k with *84    have restrictN := restrict.domain_apply at permutationEntries(I, A, N, p), I, A, I ∖ {i}, k with *85    have restrictM := restrict.domain_apply at permutationEntries(I, A, M, p), I, A, I ∖ {i}, k with *86    have valueN := permutationEntries.value at I, A, N, p, k with *87    have valueM := permutationEntries.value at I, A, M, p, k with *88    have equal := outside with k, inI, different, p(k), image89    cc90  have products := finiteRingProduct.congr at I ∖ {i}, A, add, zero, neg, mul, one, restrict(permutationEntries(I, A, N, p), I ∖ {i}), restrict(permutationEntries(I, A, M, p), I ∖ {i}) with *91  have removal := finiteRingProduct.remove at I, A, add, zero, neg, mul, one, permutationEntries(I, A, N, p), i with *92  have entry := permutationEntries.value at I, A, N, p, i with *93  have term := determinantTerms.value at I, A, add, zero, neg, mul, one, N, p with *94  have cofactor := cofactorTerms.value at I, A, add, zero, neg, mul, one, M, i, p with *95  have rest := finiteRingProduct.closed at I ∖ {i}, A, add, zero, neg, mul, one, restrict(permutationEntries(I, A, M, p), I ∖ {i}) with *96  have sign := permutationSign.closed at A, add, zero, neg, mul, one, I, p with *97  rw [term, cofactor, removal, products, entry]98  ring99100end Cofactors101102defgraph cofactorPairWeights (I A add zero neg mul one M N i r : Set) (j ∈ I) : A :=103  call2(mul, N[r, j], cofactorRow(I, A, add, zero, neg, mul, one, M, i)(j))104requires ring : IsCommRing(A, add, zero, neg, mul, one)105requires finite : Finite(I)106requires matrixM : RingMatrix(I, A, M)107requires matrixN : RingMatrix(I, A, N)108requires row : r ∈ I109proof110  have cofactors := cofactorRow.function at I, A, add, zero, neg, mul, one, M, i with *111  have cofactor := FunctionBetween.apply_closed at cofactorRow(I, A, add, zero, neg, mul, one, M, i), I, A, j with *112  have entry := RingMatrix.entry at I, A, N, r, j with *113  have ordinary := IsCommRing.ring with ring114  exact IsRing.mul_closed with ordinary, entry, cofactor115116notation scoped cofactorPairWeights(I, R, M, N, i, r) => cofactorPairWeights(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, N, i, r)117118def cofactorPairing (I A add zero neg mul one M N i r : Set) : Set :=119  finiteRingSum(I, A, add, zero, neg, mul, one, cofactorPairWeights(I, A, add, zero, neg, mul, one, M, N, i, r))120121notation scoped cofactorPairing(I, R, M, N, i, r) => cofactorPairing(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, N, i, r)122123section Expansion124variable (A add zero neg mul one : Set)125notation ring R := (A, add, zero, neg, mul, one)126hypothesis ring : IsCommRing(R)127128theorem determinant.row_expansion (n : Nat) (M N i : Set)129  requires matrixM : RingMatrix(n, R, M)130  requires matrixN : RingMatrix(n, R, N)131  requires row : i ∈ n132  requires outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, N[k, j] = M[k, j]133  shows determinant(n, R, N) = cofactorPairing(n, R, M, N, i, i)134proof135  have finite := Finite.natural with *136  have permutationsFinite := permutations.finite with finite137  have indexMap := permutationColumn.function at n, i with *138  have weights := cofactorTerms.function at n, A, add, zero, neg, mul, one, M, i with *139  have terms := determinantTerms.function at n, A, add, zero, neg, mul, one, N with *140  have functionN := matrixN141  have scalars := finiteRowWeights.function at n, n, A, N, i with *142  have outputs := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, N, i, i with *143  have factors : ∀ p ∈ permutations(n), determinantTerms(n, R, N)(p) = finiteRowWeights(n, n, A, N, i)(permutationColumn(n, i)(p)) * cofactorTerms(n, R, M, i)(p)144    intros p hp145    have permutation := permutations.mem_iff.forward with *146    have injective := Bijective.injective with permutation147    have function := Injective.function with injective148    have column := FunctionBetween.apply_closed with function149    have index := permutationColumn.value at n, i, p with *150    have value := finiteRowWeights.value at n, n, A, N, i, p(i) with *151    have factor := cofactorTerms.factor with *152    cc153  have values : ∀ j ∈ n, cofactorPairWeights(n, R, M, N, i, i)(j) = finiteRowWeights(n, n, A, N, i)(j) * finitePushforward(permutations(n), n, A, add, zero, neg, mul, one, permutationColumn(n, i), cofactorTerms(n, R, M, i))(j)154    intros j hj155    have value := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, N, i, i, j with *156    have entry := finiteRowWeights.value at n, n, A, N, i, j with *157    unfold cofactorRow at value158    cc159  have regroup := finitePushforward.weighted_sum with *160  simp [determinant, cofactorPairing]161162end Expansion163