-- The determinant annihilates every vector in the left kernel (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.DeterminantKernel
import Adjugate

defgraph rowVectorWeights (I A add zero neg mul one v M j : Set) (i ∈ I) : A :=
  call2(mul, v(i), M[i, j])
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires vector : v : I → A
requires matrix : RingMatrix(I, A, M)
requires column : j ∈ I
proof
  have value := FunctionBetween.apply_closed at v, I, A, i with *
  have entry := RingMatrix.entry at I, A, M, i, j with *
  have ordinary := IsCommRing.ring with ring
  exact IsRing.mul_closed with ordinary, value, entry

notation scoped rowVectorWeights(I, R, v, M, j) => rowVectorWeights(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)

def rowVectorEntry (I A add zero neg mul one v M j : Set) : Set :=
  finiteRingSum(I, A, add, zero, neg, mul, one, rowVectorWeights(I, A, add, zero, neg, mul, one, v, M, j))

notation scoped rowVectorEntry(I, R, v, M, j) => rowVectorEntry(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)

predicate LeftKernelVector (I A add zero neg mul one M v : Set) :=
  FunctionBetween(v, I, A) ∧ ∀ j ∈ I, rowVectorEntry(I, A, add, zero, neg, mul, one, v, M, j) = zero

notation scoped LeftKernelVector(I, R, M, v) => LeftKernelVector(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M, v)

-- This finite double sum contracts v, M, and a column of adj(M).
defunique adjugateContractionEntry (I A add zero neg mul one v M j p : Set) (a ∈ A) :=
  ∃ i ∈ I, ∃ k ∈ I, p = (i, k) ∧
    a = call2(mul, v(i), call2(mul, M[i, k], adjugate(I, A, add, zero, neg, mul, one, M)[k, j]))
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(I)
requires vector : v : I → A
requires matrix : RingMatrix(I, A, M)
requires column : j ∈ I
requires pair : p ∈ I × I
proof
  obtain ⟨bound, i, hi, k, hk, shape⟩ := product.membership.forward at
    I, I, p with *
  have adj := adjugate.matrix at I, A, add, zero, neg, mul, one, M with *
  have coefficient := FunctionBetween.apply_closed at v, I, A, i with *
  have left := RingMatrix.entry at I, A, M, i, k with *
  have right := RingMatrix.entry at I, A, adjugate(I, A, add, zero, neg, mul, one, M), k, j with *
  have ordinary := IsCommRing.ring with ring
  have product := IsRing.mul_closed with ordinary, left, right
  have value := IsRing.mul_closed with ordinary, coefficient, product
  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⟩
uniqueness
  intros u hu first w hw second
  obtain ⟨i, hi, k, hk, shapeU, valueU⟩ := first
  obtain ⟨l, hl, r, hr, shapeW, valueW⟩ := second
  have equal : (i, k) = (l, r)
    cc
  have coordinates := orderedPair.injective at i, k, l, r with equal
  cc

defgraph adjugateContraction (I A add zero neg mul one v M j : Set) (p ∈ I × I) : A :=
  adjugateContractionEntry(I, A, add, zero, neg, mul, one, v, M, j, p)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(I)
requires vector : v : I → A
requires matrix : RingMatrix(I, A, M)
requires column : j ∈ I
proof
  have selected := adjugateContractionEntry.selected at I, A, add, zero, neg, mul, one, v, M, j, p with *
  exact selected.left

notation scoped adjugateContraction(I, R, v, M, j) => adjugateContraction(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v, M, j)

section Contraction
variable (I A add zero neg mul one v M j : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)
hypothesis finite : Finite(I)
hypothesis vector : v : I → R
hypothesis matrix : RingMatrix(I, R, M)
hypothesis column : j ∈ I

theorem adjugateContraction.pair (i k : Set)
  requires row : i ∈ I
  requires index : k ∈ I
  shows adjugateContraction(I, R, v, M, j)[i, k] = v(i) * (M[i, k] * adjugate(I, R, M)[k, j])
proof
  have pair := product.pair at i, k, I, I with *
  have selected := adjugateContractionEntry.selected at I, A, add, zero, neg, mul, one, v, M, j, (i, k) with *
  obtain ⟨l, hl, r, hr, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := adjugateContraction.value at I, A, add, zero, neg, mul, one, v, M, j, (i, k) with *
  cc

theorem adjugateContraction.row (i : Set)
  requires row : i ∈ I
  shows finiteRowSums(I, I, A, add, zero, neg, mul, one, adjugateContraction(I, R, v, M, j))(i) =
    v(i) * matrixProductEntry(I, R, M, adjugate(I, R, M), i, j)
proof
  have contraction := adjugateContraction.function at I, A, add, zero, neg, mul, one, v, M, j with *
  have rows := finiteRowWeights.function at I, I, A, adjugateContraction(I, R, v, M, j), i with *
  have adj := adjugate.matrix with *
  have products := matrixProductWeights.function at I, A, add, zero, neg, mul, one, M, adjugate(I, R, M), i, j with *
  have scalar := FunctionBetween.apply_closed at v, I, A, i with *
  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)
    intros k hk
    have left := finiteRowWeights.value at I, I, A, adjugateContraction(I, R, v, M, j), i, k with *
    have right := matrixProductWeights.value at I, A, add, zero, neg, mul, one, M, adjugate(I, R, M), i, j, k with *
    have pair := adjugateContraction.pair at I, A, add, zero, neg, mul, one, v, M, j, i, k with *
    cc
  have scale := finiteRingSum.scale_eq with *
  have value := finiteRowSums.value at I, I, A, add, zero, neg, mul, one, adjugateContraction(I, R, v, M, j), i with *
  unfold matrixProductEntry
  cc

theorem adjugateContraction.column_zero (k : Set)
  requires index : k ∈ I
  requires vanishes : rowVectorEntry(I, R, v, M, k) = R[0]
  shows finiteRowSums(I, I, A, add, zero, neg, mul, one, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)))(k) = R[0]
proof
  have contraction := adjugateContraction.function at I, A, add, zero, neg, mul, one, v, M, j with *
  have transposed := transposedMatrix.function at I, I, A, adjugateContraction(I, R, v, M, j) with *
  have columns := finiteRowWeights.function at I, I, A, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k with *
  have weights := rowVectorWeights.function at I, A, add, zero, neg, mul, one, v, M, k with *
  have adj := adjugate.matrix with *
  have scalar := RingMatrix.entry at I, A, adjugate(I, R, M), k, j with *
  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)
    intros i hi
    have left := finiteRowWeights.value at I, I, A, transposedMatrix(I, I, A, adjugateContraction(I, R, v, M, j)), k, i with *
    have transpose := transposedMatrix.pair at I, I, A, adjugateContraction(I, R, v, M, j), i, k with *
    have pair := adjugateContraction.pair at I, A, add, zero, neg, mul, one, v, M, j, i, k with *
    have right := rowVectorWeights.value at I, A, add, zero, neg, mul, one, v, M, k, i with *
    have coefficient := FunctionBetween.apply_closed at v, I, A, i with *
    have entry := RingMatrix.entry at I, A, M, i, k with *
    rw [left, transpose, pair, right]
    ring
  have scale := finiteRingSum.scale_eq with *
  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 *
  unfold rowVectorEntry at vanishes
  rw [value, scale, vanishes]
  ring

end Contraction

section Annihilation
variable (A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)

theorem determinant.annihilates_left_kernel (n : Nat) (M v j : Set)
  requires matrix : RingMatrix(n, R, M)
  requires kernel : LeftKernelVector(n, R, M, v)
  requires index : j ∈ n
  shows determinant(n, R, M) * v(j) = R[0]
proof
  have vector := kernel.left
  have annihilates := kernel.right
  have contraction := adjugateContraction.function at n, A, add, zero, neg, mul, one, v, M, j with *
  have rows := finiteRowSums.function at n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j) with *
  have transposed := transposedMatrix.function at n, n, A, adjugateContraction(n, R, v, M, j) with *
  have columns := finiteRowSums.function at n, n, A, add, zero, neg, mul, one, transposedMatrix(n, n, A, adjugateContraction(n, R, v, M, j)) with *
  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]
    intros k hk
    have vanishes := annihilates with k, hk
    exact adjugateContraction.column_zero with *
  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 *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have determinantIn := determinant.closed at A, add, zero, neg, mul, one, M, n with *
  have valueIn := FunctionBetween.apply_closed at v, n, A, j with *
  have productIn := IsRing.mul_closed with ordinary, determinantIn, valueIn
  have single := coefficientSingle.function at n, A, zero, determinant(n, R, M) * v(j), j with *
  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)
    intros i hi
    have row := adjugateContraction.row at n, A, add, zero, neg, mul, one, v, M, j, i with *
    have identity := adjugate.right_identity at A, add, zero, neg, mul, one, n, M, i, j with *
    have coefficient := FunctionBetween.apply_closed at v, n, A, i with *
    have alternatives : i = j ∨ i ≠ j by tauto
    cases alternatives with same | different
    . have delta := singleValue.same at A, zero, determinant(n, R, M), j, i with *
      have selected := coefficientSingle.same at n, A, zero, determinant(n, R, M) * v(j), j with *
      rw [row, identity, delta, same, selected]
      ring
    . have delta := singleValue.other at A, zero, determinant(n, R, M), j, i with *
      have selected := coefficientSingle.other at n, A, zero, determinant(n, R, M) * v(j), j, i with *
      rw [row, identity, delta, selected]
      ring
  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 *
  have selectedSum := finiteRingSum.single at n, A, add, zero, neg, mul, one, determinant(n, R, M) * v(j), j with *
  have interchange := finiteDoubleSum.interchange at n, n, A, add, zero, neg, mul, one, adjugateContraction(n, R, v, M, j) with *
  unfold finiteDoubleSum at interchange
  cc

theorem determinant.zero_of_nonzero_left_kernel (n : Nat) (M v j : Set)
  requires domain : IsIntegralDomain(R)
  requires matrix : RingMatrix(n, R, M)
  requires kernel : LeftKernelVector(n, R, M, v)
  requires index : j ∈ n
  requires nonzero : v(j) ≠ R[0]
  shows determinant(n, R, M) = R[0]
proof
  have annihilates := determinant.annihilates_left_kernel with *
  have vector := kernel.left
  have value := FunctionBetween.apply_closed with *
  have noZero := IsIntegralDomain.no_zero_divisors with domain
  have alternatives := noZero with determinant(n, R, M), v(j), value, annihilates
  tauto

end Annihilation