-- The right-adjugate identity over arbitrary commutative rings (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.Adjugate
import Cofactors
import MatrixRows
import PermutationSign

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

theorem cofactorPairing.diagonal (n : Nat) (M i : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  shows cofactorPairing(n, R, M, M, i, i) = determinant(n, R, M)
proof
  have unchanged : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, M[k, j] = M[k, j]
    intros k hk different j hj
    rfl
  have expansion := determinant.row_expansion with *
  cc

theorem cofactorPairing.off_diagonal (n : Nat) (M i r : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  requires source : r ∈ n
  requires distinct : i ≠ r
  shows cofactorPairing(n, R, M, M, i, r) = R[0]
proof
  have copied := matrixCopyRow.matrix at n, A, M, i, r with *
  have reverse : r ≠ i
    intro equal
    apply distinct
    cc
  have outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[k, j] = M[k, j]
    intros k hk different j hj
    exact matrixCopyRow.other with *
  have equalRows : ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[i, j] = matrixCopyRow(n, A, M, i, r)[r, j]
    intros j hj
    have left := matrixCopyRow.same at n, A, M, i, r, j with *
    have right := matrixCopyRow.other at n, A, M, i, r, r, j with *
    cc
  have vanishes := determinant.equal_rows with *
  have expansion := determinant.row_expansion with *
  have leftWeights := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, matrixCopyRow(n, A, M, i, r), i, i with *
  have rightWeights := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, M, i, r with *
  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)
    intros j hj
    have left := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, matrixCopyRow(n, A, M, i, r), i, i, j with *
    have right := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, M, i, r, j with *
    have copy := matrixCopyRow.same at n, A, M, i, r, j with *
    cc
  have equal := finiteRingSum.congr with *
  unfold cofactorPairing at expansion
  unfold cofactorPairing
  cc

end CofactorIdentities

-- The adjugate transposes the cofactor array.
defunique adjugateEntry (I A add zero neg mul one M p : Set) (a ∈ A) :=
  ∃ i ∈ I, ∃ j ∈ I, p = (i, j) ∧ a = cofactorRow(I, A, add, zero, neg, mul, one, M, j)(i)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(I)
requires matrix : RingMatrix(I, A, M)
requires pair : p ∈ I × I
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward at
    I, I, p with *
  have row := cofactorRow.function at I, A, add, zero, neg, mul, one, M, j with *
  have value := FunctionBetween.apply_closed at cofactorRow(I, A, add, zero, neg, mul, one, M, j), I, A, i with *
  refine ⟨cofactorRow(I, A, add, zero, neg, mul, one, M, j)(i), value, i, hi, j, hj, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨i, hi, j, hj, shapeU, valueU⟩ := first
  obtain ⟨k, hk, l, hl, shapeV, valueV⟩ := second
  have equal : (i, j) = (k, l)
    cc
  have coordinates := orderedPair.injective at i, j, k, l with equal
  cc

defgraph adjugate (I A add zero neg mul one M : Set) (p ∈ I × I) : A :=
  adjugateEntry(I, A, add, zero, neg, mul, one, M, p)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(I)
requires matrix : RingMatrix(I, A, M)
proof
  have selected := adjugateEntry.selected at I, A, add, zero, neg, mul, one, M, p with *
  exact selected.left

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

section Adjugates
variable (I A add zero neg mul one M : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)
hypothesis finite : Finite(I)
hypothesis matrix : RingMatrix(I, R, M)

theorem adjugate.matrix
  shows RingMatrix(I, R, adjugate(I, R, M))
proof
  unfold RingMatrix
  exact adjugate.function with *

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

end Adjugates

defgraph matrixProductWeights (I A add zero neg mul one M N i j : Set) (k ∈ I) : A :=
  call2(mul, M[i, k], N[k, j])
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires matrixM : RingMatrix(I, A, M)
requires matrixN : RingMatrix(I, A, N)
requires row : i ∈ I
requires column : j ∈ I
proof
  have left := RingMatrix.entry at I, A, M, i, k with *
  have right := RingMatrix.entry at I, A, N, k, j with *
  have ordinary := IsCommRing.ring with ring
  exact IsRing.mul_closed with ordinary, left, right

notation 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)

def matrixProductEntry (I A add zero neg mul one M N i j : Set) : Set :=
  finiteRingSum(I, A, add, zero, neg, mul, one, matrixProductWeights(I, A, add, zero, neg, mul, one, M, N, i, j))

notation 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)

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

theorem adjugate.right_identity (n : Nat) (M i j : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  requires column : j ∈ n
  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, j) =
    singleValue(A, zero, determinant(n, R, M), j, i)
proof
  have adj := adjugate.matrix at n, A, add, zero, neg, mul, one, M with *
  have products := matrixProductWeights.function at n, A, add, zero, neg, mul, one, M, adjugate(n, R, M), i, j with *
  have cofactors := cofactorPairWeights.function at n, A, add, zero, neg, mul, one, M, M, j, i with *
  have entries : ∀ k ∈ n, matrixProductWeights(n, R, M, adjugate(n, R, M), i, j)(k) = cofactorPairWeights(n, R, M, M, j, i)(k)
    intros k hk
    have left := matrixProductWeights.value at n, A, add, zero, neg, mul, one, M, adjugate(n, R, M), i, j, k with *
    have right := cofactorPairWeights.value at n, A, add, zero, neg, mul, one, M, M, j, i, k with *
    have entry := adjugate.entry at n, A, add, zero, neg, mul, one, M, k, j with *
    cc
  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 *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . have diagonal := cofactorPairing.diagonal at A, add, zero, neg, mul, one, n, M, i with *
    have single := singleValue.same at A, zero, determinant(n, R, M), j, i with *
    unfold matrixProductEntry
    unfold cofactorPairing at diagonal
    cc
  . have distinct : j ≠ i
      intro equal
      apply different
      cc
    have offDiagonal := cofactorPairing.off_diagonal at A, add, zero, neg, mul, one, n, M, j, i with *
    have single := singleValue.other at A, zero, determinant(n, R, M), j, i with *
    unfold matrixProductEntry
    unfold cofactorPairing at offDiagonal
    cc

-- Ordinary applications need not expose the Kronecker-delta encoding.
theorem adjugate.right_diagonal (n : Nat) (M i : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, i) = determinant(n, R, M)
proof
  have identity := adjugate.right_identity with *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have same : i = i by rfl
  have value := singleValue.same at A, zero, determinant(n, R, M), i, i with *
  cc

theorem adjugate.right_off_diagonal (n : Nat) (M i j : Set)
  requires matrix : RingMatrix(n, R, M)
  requires row : i ∈ n
  requires column : j ∈ n
  requires distinct : i ≠ j
  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, j) = R[0]
proof
  have identity := adjugate.right_identity at A, add, zero, neg, mul, one, n, M, i, j with *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have value := singleValue.other at A, zero, determinant(n, R, M), j, i with *
  cc

end Identity