Grace/Cumulus/Algebra/Ring/DeterminantKernel.g17

Open in Workbench Download source

Imports

Adjugate

Declarations

Source

1-- The determinant annihilates every vector in the left kernel (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.DeterminantKernel8import Adjugate910defgraph rowVectorWeights (I A add zero neg mul one v M j : Set) (i ∈ I) : A :=11  call2(mul, v(i), M[i, j])12requires ring : IsCommRing(A, add, zero, neg, mul, one)13requires vector : v : I → A14requires matrix : RingMatrix(I, A, M)15requires column : j ∈ I16proof17  have value := FunctionBetween.apply_closed at v, I, A, i with *18  have entry := RingMatrix.entry at I, A, M, i, j with *19  have ordinary := IsCommRing.ring with ring20  exact IsRing.mul_closed with ordinary, value, entry2122notation scoped rowVectorWeights(I, R, v, M, j) => rowVectorWeights(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)2324def rowVectorEntry (I A add zero neg mul one v M j : Set) : Set :=25  finiteRingSum(I, A, add, zero, neg, mul, one, rowVectorWeights(I, A, add, zero, neg, mul, one, v, M, j))2627notation scoped rowVectorEntry(I, R, v, M, j) => rowVectorEntry(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)2829predicate LeftKernelVector (I A add zero neg mul one M v : Set) :=30  FunctionBetween(v, I, A) ∧ ∀ j ∈ I, rowVectorEntry(I, A, add, zero, neg, mul, one, v, M, j) = zero3132notation scoped LeftKernelVector(I, R, M, v) => LeftKernelVector(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, v)3334-- This finite double sum contracts v, M, and a column of adj(M).35defunique adjugateContractionEntry (I A add zero neg mul one v M j p : Set) (a ∈ A) :=36  ∃ i ∈ I, ∃ k ∈ I, p = (i, k) ∧37    a = call2(mul, v(i), call2(mul, M[i, k], adjugate(I, A, add, zero, neg, mul, one, M)[k, j]))38requires ring : IsCommRing(A, add, zero, neg, mul, one)39requires finite : Finite(I)40requires vector : v : I → A41requires matrix : RingMatrix(I, A, M)42requires column : j ∈ I43requires pair : p ∈ I × I44proof45  obtain ⟨bound, i, hi, k, hk, shape⟩ := product.membership.forward at46    I, I, p with *47  have adj := adjugate.matrix at I, A, add, zero, neg, mul, one, M with *48  have coefficient := FunctionBetween.apply_closed at v, I, A, i with *49  have left := RingMatrix.entry at I, A, M, i, k with *50  have right := RingMatrix.entry at I, A, adjugate(I, A, add, zero, neg, mul, one, M), k, j with *51  have ordinary := IsCommRing.ring with ring52  have product := IsRing.mul_closed with ordinary, left, right53  have value := IsRing.mul_closed with ordinary, coefficient, product54  refine ⟨call2(mul, v(i), call2(mul, M[i, k], adjugate(I, A, add, zero, neg, mul, one, M)[k, j])), value, i, hi, k, hk, shape, rfl⟩55uniqueness56  intros u hu first w hw second57  obtain ⟨i, hi, k, hk, shapeU, valueU⟩ := first58  obtain ⟨l, hl, r, hr, shapeW, valueW⟩ := second59  have equal : (i, k) = (l, r)60    cc61  have coordinates := orderedPair.injective at i, k, l, r with equal62  cc6364defgraph adjugateContraction (I A add zero neg mul one v M j : Set) (p ∈ I × I) : A :=65  adjugateContractionEntry(I, A, add, zero, neg, mul, one, v, M, j, p)66requires ring : IsCommRing(A, add, zero, neg, mul, one)67requires finite : Finite(I)68requires vector : v : I → A69requires matrix : RingMatrix(I, A, M)70requires column : j ∈ I71proof72  have selected := adjugateContractionEntry.selected at I, A, add, zero, neg, mul, one, v, M, j, p with *73  exact selected.left7475notation scoped adjugateContraction(I, R, v, M, j) => adjugateContraction(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)7677section Contraction78variable (I A add zero neg mul one v M j : Set)79notation ring R := (A, add, zero, neg, mul, one)80hypothesis ring : IsCommRing(R)81hypothesis finite : Finite(I)82hypothesis vector : v : I → R83hypothesis matrix : RingMatrix(I, R, M)84hypothesis column : j ∈ I8586theorem adjugateContraction.pair (i k : Set)87  requires row : i ∈ I88  requires index : k ∈ I89  shows adjugateContraction(I, R, v, M, j)[i, k] = v(i) * (M[i, k] * adjugate(I, R, M)[k, j])90proof91  have pair := product.pair at i, k, I, I with *92  have selected := adjugateContractionEntry.selected at I, A, add, zero, neg, mul, one, v, M, j, (i, k) with *93  obtain ⟨l, hl, r, hr, shape, result⟩ := selected.right94  have coordinates := orderedPair.injective with shape95  have value := adjugateContraction.value at I, A, add, zero, neg, mul, one, v, M, j, (i, k) with *96  cc9798theorem adjugateContraction.row (i : Set)99  requires row : i ∈ I100  shows finiteRowSums(I, I, A, add, zero, neg, mul, one, adjugateContraction(I, R, v, M, j))(i) =101    v(i) * matrixProductEntry(I, R, M, adjugate(I, R, M), i, j)102proof103  have contraction := adjugateContraction.function at I, A, add, zero, neg, mul, one, v, M, j with *104  have rows := finiteRowWeights.function at I, I, A, adjugateContraction(I, R, v, M, j), i with *105  have adj := adjugate.matrix with *106  have products := matrixProductWeights.function at I, A, add, zero, neg, mul, one, M, adjugate(I, R, M), i, j with *107  have scalar := FunctionBetween.apply_closed at v, I, A, i with *108  have entries : ∀ k ∈ I, finiteRowWeights(I, I, A, adjugateContraction(I, R, v, M, j), i)(k) = v(i) * matrixProductWeights(I, R, M, adjugate(I, R, M), i, j)(k)109    intros k hk110    have left := finiteRowWeights.value at I, I, A, adjugateContraction(I, R, v, M, j), i, k with *111    have right := matrixProductWeights.value at I, A, add, zero, neg, mul, one, M, adjugate(I, R, M), i, j, k with *112    have pair := adjugateContraction.pair at I, A, add, zero, neg, mul, one, v, M, j, i, k with *113    cc114  have scale := finiteRingSum.scale_eq with *115  have value := finiteRowSums.value at I, I, A, add, zero, neg, mul, one, adjugateContraction(I, R, v, M, j), i with *116  unfold matrixProductEntry117  cc118119theorem adjugateContraction.column_zero (k : Set)120  requires index : k ∈ I121  requires vanishes : rowVectorEntry(I, R, v, M, k) = R[0]122  shows finiteRowSums(I, I, A, add, zero, neg, mul, one, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)))(k) = R[0]123proof124  have contraction := adjugateContraction.function at I, A, add, zero, neg, mul, one, v, M, j with *125  have transposed := transposedMatrix.function at I, I, A, adjugateContraction(I, R, v, M, j) with *126  have columns := finiteRowWeights.function at I, I, A, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k with *127  have weights := rowVectorWeights.function at I, A, add, zero, neg, mul, one, v, M, k with *128  have adj := adjugate.matrix with *129  have scalar := RingMatrix.entry at I, A, adjugate(I, R, M), k, j with *130  have entries : ∀ i ∈ I, finiteRowWeights(I, I, A, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k)(i) = adjugate(I, R, M)[k, j] * rowVectorWeights(I, R, v, M, k)(i)131    intros i hi132    have left := finiteRowWeights.value at I, I, A, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k, i with *133    have transpose := transposedMatrix.pair at I, I, A, adjugateContraction(I, R, v, M, j), i, k with *134    have pair := adjugateContraction.pair at I, A, add, zero, neg, mul, one, v, M, j, i, k with *135    have right := rowVectorWeights.value at I, A, add, zero, neg, mul, one, v, M, k, i with *136    have coefficient := FunctionBetween.apply_closed at v, I, A, i with *137    have entry := RingMatrix.entry at I, A, M, i, k with *138    rw [left, transpose, pair, right]139    ring140  have scale := finiteRingSum.scale_eq with *141  have value := finiteRowSums.value at I, I, A, add, zero, neg, mul, one, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k with *142  unfold rowVectorEntry at vanishes143  rw [value, scale, vanishes]144  ring145146end Contraction147148section Annihilation149variable (A add zero neg mul one : Set)150notation ring R := (A, add, zero, neg, mul, one)151hypothesis ring : IsCommRing(R)152153theorem determinant.annihilates_left_kernel (n : Nat) (M v j : Set)154  requires matrix : RingMatrix(n, R, M)155  requires kernel : LeftKernelVector(n, R, M, v)156  requires index : j ∈ n157  shows determinant(n, R, M) * v(j) = R[0]158proof159  have vector := kernel.left160  have annihilates := kernel.right161  have contraction := adjugateContraction.function at n, A, add, zero, neg, mul, one, v, M, j with *162  have rows := finiteRowSums.function at n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j) with *163  have transposed := transposedMatrix.function at n, n, A, adjugateContraction(n, R, v, M, j) with *164  have columns := finiteRowSums.function at n, n, A, add, zero, neg, mul, one, transposedMatrix(n, n, A, adjugateContraction(n, R, v, M, j)) with *165  have zeros : ∀ k ∈ n, finiteRowSums(n, n, A, add, zero, neg, mul, one, transposedMatrix(n, n, A, adjugateContraction(n, R, v, M, j)))(k) = R[0]166    intros k hk167    have vanishes := annihilates with k, hk168    exact adjugateContraction.column_zero with *169  have zeroSum := finiteRingSum.zero at n, A, add, zero, neg, mul, one, finiteRowSums(n, n, A, add, zero, neg, mul, one, transposedMatrix(n, n, A, adjugateContraction(n, R, v, M, j))) with *170  have ordinary := IsCommRing.ring with ring171  have zeroIn := IsRing.zero_in_carrier with ordinary172  have determinantIn := determinant.closed at A, add, zero, neg, mul, one, M, n with *173  have valueIn := FunctionBetween.apply_closed at v, n, A, j with *174  have productIn := IsRing.mul_closed with ordinary, determinantIn, valueIn175  have single := coefficientSingle.function at n, A, zero, determinant(n, R, M) * v(j), j with *176  have rowEntries : ∀ i ∈ n, finiteRowSums(n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j))(i) = coefficientSingle(n, A, zero, determinant(n, R, M) * v(j), j)(i)177    intros i hi178    have row := adjugateContraction.row at n, A, add, zero, neg, mul, one, v, M, j, i with *179    have identity := adjugate.right_identity at A, add, zero, neg, mul, one, n, M, i, j with *180    have coefficient := FunctionBetween.apply_closed at v, n, A, i with *181    have alternatives : i = j ∨ i ≠ j by tauto182    cases alternatives with same | different183    . have delta := singleValue.same at A, zero, determinant(n, R, M), j, i with *184      have selected := coefficientSingle.same at n, A, zero, determinant(n, R, M) * v(j), j with *185      rw [row, identity, delta, same, selected]186      ring187    . have delta := singleValue.other at A, zero, determinant(n, R, M), j, i with *188      have selected := coefficientSingle.other at n, A, zero, determinant(n, R, M) * v(j), j, i with *189      rw [row, identity, delta, selected]190      ring191  have rowSum := finiteRingSum.congr at n, A, add, zero, neg, mul, one, finiteRowSums(n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j)), coefficientSingle(n, A, zero, determinant(n, R, M) * v(j), j) with *192  have selectedSum := finiteRingSum.single at n, A, add, zero, neg, mul, one, determinant(n, R, M) * v(j), j with *193  have interchange := finiteDoubleSum.interchange at n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j) with *194  unfold finiteDoubleSum at interchange195  cc196197theorem determinant.zero_of_nonzero_left_kernel (n : Nat) (M v j : Set)198  requires domain : IsIntegralDomain(R)199  requires matrix : RingMatrix(n, R, M)200  requires kernel : LeftKernelVector(n, R, M, v)201  requires index : j ∈ n202  requires nonzero : v(j) ≠ R[0]203  shows determinant(n, R, M) = R[0]204proof205  have annihilates := determinant.annihilates_left_kernel with *206  have vector := kernel.left207  have value := FunctionBetween.apply_closed with *208  have noZero := IsIntegralDomain.no_zero_divisors with domain209  have alternatives := noZero with determinant(n, R, M), v(j), value, annihilates210  tauto211212end Annihilation213