Jacobi's complementary-minor identity #
Let A and B be mutually inverse square matrices, A * B = 1. Jacobi's theorem says that a
minor of A is, up to sign and the factor det A, the complementary minor of B: the one on
the rows and the columns that the minor of A leaves out, with the roles of rows and columns
exchanged.
The index bookkeeping is carried here by a splitting of the index type as a sum m ⊕ p together
with two permutations σ and τ: the minor of A sits on the rows τ (p) and the columns
σ (p), and its complementary minor of B on the rows σ (m) and the columns τ (m). The sign
of the identity is then exactly the product of the signs of the two permutations, with no further
combinatorial factor, and no pair of index subsets has to be ordered. Choosing the permutations to
enumerate a subset and its complement in increasing order recovers the classical statement for
index sets.
Why this file #
Tau Ceti already has the h--e duality TauCeti.hsymmToeplitz_mul_esymmToeplitz, saying that
the Toeplitz matrices of the complete homogeneous and the signed elementary symmetric polynomials
are inverse to one another. Jacobi's identity is what turns that duality into the dual (transpose)
Jacobi--Trudi formula, by matching a minor of one Toeplitz matrix with the complementary minor of
the other; TauCeti.det_submatrix_hsymmToeplitz in
TauCeti/RingTheory/MvPolynomial/Symmetric/Complete/ToeplitzMinor.lean is that match.
The identity is independent of TauCeti.Matrix.det_sumElim_eq_det_mul in
TauCeti/LinearAlgebra/Matrix/Determinant/SumElim.lean, which compares the determinant of a fixed
family of rows followed by a varying one with a determinant of pairings; that statement is about
the Plücker coordinates of a subspace and of its orthogonal complement, and has no inverse pair of
matrices in it.
Main results #
Matrix.det_submatrix_inr_eq_sign_mul_det_mul_det_submatrix_inl: Jacobi's complementary-minor identity, for an index type presented as a sum.Matrix.det_submatrix_comp_inr_eq_sign_mul_det_mul_det_submatrix_comp_inl: the same identity for an arbitrary index type, split by a chosen equivalence with a sum.Matrix.det_submatrix_comp_inr_eq_sign_mul_det_submatrix_comp_inl_of_det_eq_one: the form the identity takes for a pair of inverse matrices of determinant one.Matrix.det_submatrix_comp_inr_eq_sign_mul_det_mul_det_submatrix_comp_inl_nonsing_inv: the form it takes for a matrix and its nonsingular inverse.
References #
- C. G. J. Jacobi, De formatione et proprietatibus determinantium, Journal fuer die reine und angewandte Mathematik 22 (1841), 285-318.
- I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I,
Section 2, Example 3, and Section 3, formula (3.5), where the identity is applied to the
Toeplitz matrices of
hande.
Jacobi's complementary-minor identity. For mutually inverse matrices A and B indexed
by m ⊕ p, and permutations σ, τ of that index type, the minor of A on the rows τ (p) and
the columns σ (p) is det A times the complementary minor of B, the one on the rows σ (m)
and the columns τ (m), signed by σ and τ.
For p empty both sides read det A * det B = 1, and for m empty they read det A = det A;
the content is in between.
Jacobi's complementary-minor identity for an arbitrary index type n, split into two
groups of indices by an equivalence e : m ⊕ p ≃ n.
Jacobi's complementary-minor identity for a pair of inverse matrices of determinant one: a
minor of A and the complementary minor of B agree up to the signs of the two permutations.
Jacobi's complementary-minor identity written with the nonsingular inverse: for a matrix with invertible determinant, a minor of the matrix is read off the complementary minor of its inverse.