22.5. Cauchy-Binet and Plücker identities🔗

The determinant of a Gram matrix expands as a sum over column tuples: the Cauchy-Binet formula.

Two quadratic identities among minors follow, and their names are worth keeping apart. The two-row replacement identity relates the determinant of a square matrix, times the determinant with two rows replaced, to the four determinants with one row replaced; it is the 2 × 2 case of Jacobi's identity for minors of the adjugate, and substituting standard basis vectors recovers Desnanot-Jacobi. The three-term Grassmann-Plücker relation instead relates the maximal minors of a tall matrix B to those of B with a column appended, proved here in the specialisation where the two larger of the three distinguished rows are the last two rows. Sylvester's determinant identity, the general statement about an m × m matrix of bordered minors, is not proved in this project.

The triangular-determinant law gives the determinant of an upper- or lower-triangular matrix as the product of its diagonal entries.

theorem

Hex.Matrix.det_gramMatrix_eq_sum_columnTuples.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n m : ℕ} (A : Hex.Matrix R n m) :
  A.gramMatrix.det =
    List.foldl
      (fun acc cols =>
        acc +
          A.columnTupleCoeff cols *
            (A.columnTupleMatrix
                (Hex.Matrix.columnTupleVectorFn cols)).det)
      0 (Hex.Matrix.columnTupleVectors n m)
Hex.Matrix.det_gramMatrix_eq_sum_columnTuples.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n m : ℕ} (A : Hex.Matrix R n m) :
  A.gramMatrix.det =
    List.foldl
      (fun acc cols =>
        acc +
          A.columnTupleCoeff cols *
            (A.columnTupleMatrix
                (Hex.Matrix.columnTupleVectorFn
                  cols)).det)
      0
      (Hex.Matrix.columnTupleVectors n m)

The determinant of a row Gram matrix expands as the ordered-column tuple sum induced by the generic column-sum determinant expansion.

theorem

Hex.Matrix.det_setRow_setRow_mul_det.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.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
Hex.Matrix.det_setRow_setRow_mul_det.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.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 identity: replacing distinct rows a and b of M by u and v relates det M times the doubly-replaced determinant to the four singly-replaced determinants.

Substituting standard basis vectors for u and v turns each singly-replaced determinant into a signed one-row/one-column minor, recovering Desnanot-Jacobi for an arbitrary row pair and column pair.

theorem

Hex.Matrix.det_plucker_three_term_consecutive_top.{u} {R : Type u}
  [Lean.Grind.CommRing R] {k : ℕ} (B : Hex.Matrix R (k + 2) k)
  (v : Vector R (k + 2)) (alpha : Fin (k + 2)) (halpha : ↑alpha < k) :
  let pk := ⟨k, ⋯⟩;
  let plast := Fin.last (k + 1);
  B.mDet v alpha * B.nDet pk plast ⋯ -
        B.mDet v pk * B.nDet alpha plast ⋯ +
      B.mDet v plast * B.nDet alpha pk ⋯ =
    0
Hex.Matrix.det_plucker_three_term_consecutive_top.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {k : ℕ} (B : Hex.Matrix R (k + 2) k)
  (v : Vector R (k + 2))
  (alpha : Fin (k + 2))
  (halpha : ↑alpha < k) :
  let pk := ⟨k, ⋯⟩;
  let plast := Fin.last (k + 1);
  B.mDet v alpha * B.nDet pk plast ⋯ -
        B.mDet v pk *
          B.nDet alpha plast ⋯ +
      B.mDet v plast * B.nDet alpha pk ⋯ =
    0

Consecutive-top vector-column Plücker identity.

This is the Mathlib-free specialization used by the Gram/Bareiss trajectory: the three distinguished rows are alpha, k, and k+1 inside Fin (k + 2), so the top row is the last possible row and there is no q > p3 basis-vector case.

theorem

Hex.Matrix.det_upperTriangular_eq_finFoldl_diag.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.Matrix R n n)
  (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) :
  M.det = Fin.foldl n (fun acc i => acc * M[i][i]) 1
Hex.Matrix.det_upperTriangular_eq_finFoldl_diag.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ} (M : Hex.Matrix R n n)
  (hzero :
    ∀ (i j : Fin n),
      ↑j < ↑i → M[i][j] = 0) :
  M.det =
    Fin.foldl n
      (fun acc i => acc * M[i][i]) 1

The determinant of an upper-triangular square matrix (entries below the diagonal are zero) over a commutative ring is the product of its diagonal entries, expressed via a Fin.foldl over the diagonal indices.