Adjugate matrix and M * adjugate M = det M • 1

The local adjugate matrix is the transpose of the cofactor matrix. The defining property is (M * adjugate M)[i][j] = det M * δᵢⱼ, which we prove entrywise via Laplace expansion. The off-diagonal case uses the "alien cofactor" identity: expanding row i against the cofactors of a different row j collapses to the determinant of a matrix with two equal rows. These are the Mathlib-free local analogues of Mathlib's Matrix.adjugate and Matrix.mul_adjugate needed by the Desnanot-Jacobi assembly.

theorem Hex.Matrix.deleteRowCol_setRow_self {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) (dst col : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow dst v).deleteRowCol dst col = M.deleteRowCol dst col

Deleting the destination row of setRow M dst v gives the same minor as deleting the destination row of M: the replaced row is removed anyway, so the new entries are invisible.

theorem Hex.Matrix.cofactor_setRow_self {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (dst col : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow dst v).cofactor dst col = M.cofactor dst col

The cofactor expansion of setRow M dst v along the replaced row dst uses the same minors as the cofactor expansion of M along that row, because the deleted row never contributes to the minor.

def Hex.Matrix.cofactorRowPairing {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) (v : Vector R (n + 1)) : R

Pair a row vector with a cofactor row of M. This is the scalar that appears in Laplace expansion after replacing the expanded row.

Equations

• M.cofactorRowPairing row v = Fin.foldl (n + 1) (fun (acc : R) (col : Fin (n + 1)) => acc + v[col] * M.cofactor row col) 0

theorem Hex.Matrix.det_setRow_eq_cofactorRowPairing {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow row v).det = M.cofactorRowPairing row v

Replacing row row by v makes the determinant the pairing of v against the original cofactor row.

theorem Hex.Matrix.cofactorRowPairing_self {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : M.cofactorRowPairing row M[row] = M.det

Pairing the original row against its own cofactor row recovers det M.

theorem Hex.Matrix.foldl_alien_cofactor_eq_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) (hij : i ≠ j) : Fin.foldl (n + 1) (fun (acc : R) (k : Fin (n + 1)) => acc + M[i][k] * M.cofactor j k) 0 = 0

The "alien cofactor" identity: expanding row i of M against the cofactors of a different row j produces zero. This is the characteristic vanishing identity that makes the adjugate work.

theorem Hex.Matrix.cofactorRowPairing_alien_eq_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) (hij : i ≠ j) : M.cofactorRowPairing j M[i] = 0

Pairing an unreplaced row of M against a different cofactor row is zero.

def Hex.Matrix.adjugate {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : Matrix R (n + 1) (n + 1)

The local adjugate matrix: entry (i, j) is the cofactor at row j, column i of M. This is the transpose of the cofactor matrix.

Equations

• M.adjugate = Hex.Matrix.ofFn fun (i j : Fin (n + 1)) => M.cofactor j i

theorem Hex.Matrix.adjugate_get {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : M.adjugate[i][j] = M.cofactor j i

Entry (i, j) of the adjugate is the cofactor of M at row j, column i (the transpose of the cofactor matrix).

theorem Hex.Matrix.mul_adjugate_apply {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : (M * M.adjugate)[i][j] = if i = j then M.det else 0

Entrywise version of M * adjugate M = det M • 1. On the diagonal this is Laplace expansion of det M; off the diagonal it is the alien cofactor identity.

theorem Hex.Matrix.mul_adjugate {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M * M.adjugate = M.det • Matrix.identity (n + 1)

The adjugate identity M * adjugate M = det M • identity.

theorem Hex.Matrix.adjugate_mul_apply {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : (M.adjugate * M)[i][j] = if i = j then M.det else 0

Entrywise version of adjugate M * M = det M • 1.

This is the transpose-side companion to mul_adjugate_apply; it is useful when cofactor identities are consumed columnwise rather than rowwise.

theorem Hex.Matrix.mul_adjugate_apply_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i : Fin (n + 1)) : (M * M.adjugate)[i][0] = if i = 0 then M.det else 0

Column-0 view of M * adjugate M.

theorem Hex.Matrix.mul_adjugate_apply_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i : Fin (n + 1)) : (M * M.adjugate)[i][Fin.last n] = if i = Fin.last n then M.det else 0

Last-column view of M * adjugate M.

theorem Hex.Matrix.adjugate_eq_cofactorSign_mul_deleteRowCol {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : M.adjugate[i][j] = cofactorSign j i * (M.deleteRowCol j i).det

Cofactor-minor representation of an adjugate entry.

theorem Hex.Matrix.adjugate_zero_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.adjugate[0][0] = (M.deleteRowCol 0 0).det

The (0, 0) adjugate entry equals the determinant of the minor obtained by deleting row 0 and column 0.

theorem Hex.Matrix.adjugate_last_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.adjugate[Fin.last n][Fin.last n] = (M.principalSubmatrix n ⋯).det

The (Fin.last, Fin.last) adjugate entry equals the determinant of the leading prefix minor obtained by deleting the last row and column.

Multiplicativity helpers

These private helpers prove determinant multiplicativity for Hex.det.

theorem Hex.Matrix.det_mul {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M N : Matrix R n n) : (M * N).det = M.det * N.det

Determinant of a product of square matrices.

This is the Mathlib-free Cauchy-Binet specialization already used by the Desnanot-Jacobi auxiliary proof.

Two-row replacement determinant Plucker kernel

The square-matrix two-row determinant Plucker identity: replacing distinct rows a and b of an (n+1) × (n+1) matrix M by vectors u and v is controlled by the cofactor-row pairings of u and v against the original cofactors of rows a and b. The proof routes through the single-column adjugate identity, computed by expanding the (c, s) entry of adjugate (setRow M r u) * (setRow M r u * adjugate M) in two ways.

theorem Hex.Matrix.cofactorRowPairing_setRow_plucker {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : M.det * (M.setRow a u).cofactorRowPairing b v = M.cofactorRowPairing a u * M.cofactorRowPairing b v - M.cofactorRowPairing a v * M.cofactorRowPairing b u

Two-row replacement determinant Plucker kernel.

For matrix M : Matrix R (n+1) (n+1), distinct rows a and b, and replacement vectors u, v, the determinant of M paired with the two-row-replaced cofactor-row pairing satisfies the quadratic Sylvester relation against the four one-row cofactor-row pairings of u and v.

theorem Hex.Matrix.det_setRow_setRow_mul_det {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : M.det * ((M.setRow a u).setRow b v).det = (M.setRow a u).det * (M.setRow b v).det - (M.setRow a v).det * (M.setRow b u).det

Two-row replacement determinant Plucker identity.