Jacobi's complementary minor theorem

For a square matrix A over a commutative ring and two finite sets I and J of row and column indices with #I = #J = k, Jacobi's complementary minor theorem relates the minor of the adjugate on the complementary index sets to the complementary minor of A:

det A * det ((adj A)[Jᶜ, Iᶜ]) = (-1) ^ (∑ I + ∑ J) * (det A) ^ (n - k) * det (A[I, J]).

Here A[I, J] denotes the submatrix with rows I and columns J, both listed in increasing order, and the exponent ∑ I is the sum of the indices in I. The sign is the relative sign of the shuffles that list I and J before their complements.

The theorem is the key step in passing between the complete-homogeneous Toeplitz matrix and its inverse, and hence in the dual Jacobi--Trudi formula for Schur polynomials. For k = n - 1 it is the cofactor formula for an entry of the adjugate multiplied by det A; when det A is a unit, this recovers the usual cofactor formula.

Main results

• Matrix.det_mul_det_submatrix_adjugate: Jacobi's complementary minor theorem in adjugate form.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013, Section 0.8.4, for Jacobi's theorem on complementary minors.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 2, for the dual Jacobi--Trudi application.

theorem Matrix.det_mul_det_submatrix_adjugate {R : Type u_1} [CommRing R] {n k : ℕ} (A : Matrix (Fin n) (Fin n) R) {I J : Finset (Fin n)} (hI : I.card = k) (hJ : J.card = k) : A.det * (A.adjugate.submatrix ⇑(Jᶜ.orderEmbOfFin ⋯) ⇑(Iᶜ.orderEmbOfFin ⋯)).det = (-1) ^ (∑ i ∈ I, ↑i + ∑ j ∈ J, ↑j) * A.det ^ (n - k) * (A.submatrix ⇑(I.orderEmbOfFin hI) ⇑(J.orderEmbOfFin hJ)).det

Jacobi's complementary minor theorem. For #I = #J = k, the product of the determinant of A and the complementary minor of the adjugate, with rows Jᶜ and columns Iᶜ, is (-1) ^ (∑ I + ∑ J) times (det A) ^ (n - k) times the minor A[I, J].