3.5. Cauchy-Binet and Plücker identities🔗

The determinant of a Gram matrix expands as a sum over column tuples (the Cauchy-Binet formula), and the three-term Plücker / Desnanot-Jacobi identity relates the determinants of a matrix and its bordered minors. 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 : Nat} (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 : Nat} (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_plucker_three_term_consecutive_top.{u} {R : Type u}
  [Lean.Grind.CommRing R] {k : Nat} (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 : Nat} (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_foldl_diag.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat} (M : Hex.Matrix R n n)
  (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) :
  M.det = List.foldl (fun acc i => acc * M[i][i]) 1 (List.finRange n)
Hex.Matrix.det_upperTriangular_eq_foldl_diag.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n)
  (hzero :
    ∀ (i j : Fin n),
      ↑j < ↑i → M[i][j] = 0) :
  M.det =
    List.foldl
      (fun acc i => acc * M[i][i]) 1
      (List.finRange n)

The determinant of an upper-triangular square matrix as a List.foldl product over the diagonal indices in Fin.finRange.