The Cauchy–Binet formula

For a rectangular pair A : Matrix m n R, B : Matrix n m R over a commutative ring, the determinant of the (square) product A * B is the sum, over all Fintype.card m-element subsets S of n, of the products of the two maximal minors selected by S:

det (A * B) = ∑ S, det (A.submatrix e.symm (S.orderEmbOfFin _)) * det (B.submatrix (S.orderEmbOfFin _) e.symm)

where e : m ≃ Fin (Fintype.card m) is the canonical enumeration and S.orderEmbOfFin enumerates S in increasing order. If Fintype.card m > Fintype.card n the sum is empty and the determinant vanishes; if m ≃ n the formula reduces to det_mul.

Main results

• Matrix.det_mul_eq_sum_det_submatrix_mul_prod: the Leibniz-type expansion of det (A * B) over all index functions g : m → n, with the column-minor det (A.submatrix id g) weighted by ∏ i, B (g i) i.
• Matrix.det_mul_cauchyBinet: the Cauchy–Binet formula.

Implementation notes

The proof expands det (A * B) over all functions g : m → n (det_mul_eq_sum_det_submatrix_mul_prod), discards the non-injective g (a repeated column), and groups the injective ones by their image S: summing over the (Fintype.card m)! relabellings of the columns of one minor reassembles the determinant of the other (Matrix.fiberSum). A linear order on n is required only to name the sorted minors.

theorem Matrix.det_mul_eq_sum_det_submatrix_mul_prod {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] (A : Matrix m n R) (B : Matrix n m R) : (A * B).det = ∑ g : m → n, (A.submatrix id g).det * ∏ i : m, B (g i) i

Leibniz-type expansion of the determinant of a product: det (A * B) is the sum, over all index functions g : m → n, of the column-minor det (A.submatrix id g) weighted by ∏ i, B (g i) i. This is the Cauchy–Binet formula before grouping the functions g by their image.

theorem Matrix.det_mul_cauchyBinet {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [LinearOrder n] (A : Matrix m n R) (B : Matrix n m R) : (A * B).det = ∑ S : { s : Finset n // s.card = Fintype.card m }, (A.submatrix ⇑(Fintype.equivFin m).symm ⇑((↑S).orderEmbOfFin ⋯)).det * (B.submatrix ⇑((↑S).orderEmbOfFin ⋯) ⇑(Fintype.equivFin m).symm).det

The Cauchy–Binet formula. The determinant of A * B, for a rectangular pair A : Matrix m n R and B : Matrix n m R, is the sum over all Fintype.card m-element subsets S of n of the product of the two maximal minors with columns (resp. rows) selected by S in increasing order.