Determinants: Factor Hunting and Desnanot-Jacobi Identity #
This file formalizes results from the "Factor hunting" and "Desnanot-Jacobi and Dodgson condensation" sections of the determinants chapter.
Main definitions #
vandermondeMat: The Vandermonde matrix with entriesa i ^ (n - j)cauchyMat: The Cauchy matrix with entries1 / (x i + y j)
Main results #
Vandermonde determinant (Theorem thm.det.vander) #
vandermonde_det_a: det(aᵢⁿ⁻ʲ) = ∏_{i<j} (aᵢ - aⱼ)vandermonde_det_b: det(aⱼⁿ⁻ⁱ) = ∏_{i<j} (aᵢ - aⱼ)vandermonde_det_c: det(aᵢʲ⁻¹) = ∏_{j<i} (aᵢ - aⱼ)vandermonde_det_d: det(aⱼⁱ⁻¹) = ∏_{j<i} (aᵢ - aⱼ)
Proposition prop.det.(xi+yj)n-1 #
det_sum_pow: det((xᵢ + yⱼ)ⁿ⁻¹) = (∏ₖ C(n-1,k)) · (∏{i<j}(xᵢ-xⱼ)) · (∏{i<j}(yⱼ-yᵢ))
Laplace expansion (Theorem thm.det.laplace) #
det_laplace_row: det A = ∑q (-1)^(p+q) A{p,q} det(A_{~p,~q})det_laplace_col: det A = ∑p (-1)^(p+q) A{p,q} det(A_{~p,~q})
Proposition prop.det.laplace.0 #
det_laplace_row_zero: 0 = ∑q (-1)^(p+q) A{r,q} det(A_{~p,~q}) when p ≠ rdet_laplace_col_zero: 0 = ∑p (-1)^(p+q) A{p,r} det(A_{~p,~q}) when q ≠ r
Adjugate matrix (Definition def.det.adj, Theorem thm.det.adj.inverse) #
adjugate: The adjugate (classical adjoint) of a matrixadjugate_mul: A · adj(A) = det(A) · Imul_adjugate: adj(A) · A = det(A) · I
Desnanot-Jacobi identity (Theorem thm.det.des-jac-1, thm.det.des-jac-2) #
desnanot_jacobi: det(A) · det(A') = det(A_{~1,~1}) · det(A_{~n,~n}) - det(A_{~1,~n}) · det(A_{~n,~1})desnanot_jacobi_general: Generalization with arbitrary rows p,q and columns u,v
Cauchy determinant (Theorem thm.det.cauchy) #
cauchy_det: det(1/(xᵢ+yⱼ)) = ∏{i<j}((xᵢ-xⱼ)(yᵢ-yⱼ)) / ∏{i,j}(xᵢ+yⱼ)
Jacobi's complementary minor theorem (Theorem thm.det.jacobi-complement) #
jacobi_complementary_minor: det(sub_P^Q(adj A)) = (-1)^(sum P + sum Q) · (det A)^(|Q|-1) · det(sub_{~Q}^{~P} A)
References #
- Source: DesnanotJacobi.tex (Factor hunting and Desnanot-Jacobi sections)
Implementation notes #
Many of these results are already in Mathlib under Matrix.det_vandermonde, Matrix.adjugate,
Matrix.det_laplace_row, etc. This file provides the statements matching the textbook
presentation and connects them to Mathlib's API.
Fin.succAbove computation lemmas #
These simp lemmas allow efficient computation of Fin.succAbove for concrete Fin types.
They are used throughout this file for determinant expansions involving submatrices.
All lemmas are proved by rfl for maximum efficiency.
Fin 3 product lemmas #
These lemmas simplify products over pairs and singletons in Fin 3.
They are used in Cauchy determinant computations for the n = 3 case.
Product over {2} in Fin 3 equals f 2.
Ioi 0 in Fin 3 is {1, 2}.
Ioi 1 in Fin 3 is {2}.
Ioi 2 in Fin 3 is empty.
Vandermonde Determinant (Theorem thm.det.vander) #
The Vandermonde determinant is a classical result: the determinant of a matrix with entries aᵢʲ⁻¹ (or variants) equals a product of differences.
The proof uses "factor hunting": we show the determinant is divisible by each (aᵢ - aⱼ) for i < j, and then compare degrees to conclude equality up to a constant, which is determined by examining the leading coefficient.
The Vandermonde matrix with entries a i ^ (n - 1 - j) for 0-indexed i, j.
This corresponds to the matrix (aᵢⁿ⁻ʲ) in 1-indexed notation.
Label: thm.det.vander
Equations
Instances For
vandermondeMat a equals projVandermonde 1 a, which has entries (1)^j * (a i)^(n-1-j).
This allows us to use Mathlib's det_projVandermonde to compute the determinant.
Vandermonde determinant, part (a): det(aᵢⁿ⁻ʲ) = ∏_{i<j} (aᵢ - aⱼ) Label: thm.det.vander (a)
Note: Mathlib's Matrix.det_vandermonde uses a slightly different indexing convention.
This statement matches the textbook presentation.
Vandermonde determinant, part (b): det(aⱼⁿ⁻ⁱ) = ∏_{i<j} (aᵢ - aⱼ) This is the transpose of part (a). Label: thm.det.vander (b)
The standard Vandermonde matrix with entries a i ^ j.
This corresponds to the matrix (aᵢʲ⁻¹) in 1-indexed notation.
Equations
- AlgebraicCombinatorics.Determinants.vandermondeMat' a = Matrix.of fun (i j : Fin n) => a i ^ ↑j
Instances For
Vandermonde determinant, part (c): det(aᵢʲ⁻¹) = ∏_{j<i} (aᵢ - aⱼ) Label: thm.det.vander (c)
Vandermonde determinant, part (d): det(aⱼⁱ⁻¹) = ∏_{j<i} (aᵢ - aⱼ) This is the transpose of part (c). Label: thm.det.vander (d)
Mathlib's version of the Vandermonde determinant.
This relates our formulation to Mathlib's Matrix.det_vandermonde.
Lemma lem.det.vander.a.pol - Vandermonde determinant in polynomial ring #
This is a key lemma that establishes the Vandermonde identity for polynomial indeterminates. The general Vandermonde theorem (thm.det.vander) follows from this by substitution.
The proof relates our matrix convention to Mathlib's via column reversal, and uses the fact that swapping the order of subtraction in each factor introduces a sign that cancels with the sign from the column permutation.
Helper: card of Ioi for Fin n.
Sum of Ioi cardinalities equals n(n-1)/2.
The Vandermonde matrix in the polynomial ring ℤ[x₁,...,xₙ] with entries xᵢⁿ⁻ʲ. This is the matrix from Lemma lem.det.vander.a.pol. Entry (i,j) = xᵢ^{n-1-j} (using 0-indexed notation). Label: lem.det.vander.a.pol
Equations
- AlgebraicCombinatorics.Determinants.vandermondePolyMat m = Matrix.of fun (i j : Fin m) => MvPolynomial.X i ^ (m - 1 - ↑j)
Instances For
The product of differences ∏_{1≤i<j≤n} (xᵢ - xⱼ) in the polynomial ring. Label: lem.det.vander.a.pol
Equations
- AlgebraicCombinatorics.Determinants.vandermondePolyProd m = ∏ i : Fin m, ∏ j ∈ Finset.Ioi i, (MvPolynomial.X i - MvPolynomial.X j)
Instances For
Relation between vandermondePolyMat and Mathlib's vandermonde via column reversal.
Uses Mathlib's Fin.revPerm for the column reversal permutation.
The determinant of vandermondePolyMat in terms of Mathlib's vandermonde.
The sign of Mathlib's Fin.revPerm column reversal permutation.
Label: lem.det.vander.a.pol (helper)
The product transformation: swapping subtraction order introduces a sign. Label: lem.det.vander.a.pol (helper)
Lemma lem.det.vander.a.pol: The Vandermonde determinant in the polynomial ring.
In ℤ[x₁,...,xₙ], we have: det(xᵢⁿ⁻ʲ) = ∏_{1≤i<j≤n} (xᵢ - xⱼ)
This is the "universal" form of the Vandermonde determinant. The general theorem (Theorem thm.det.vander) follows by substituting specific ring elements for the indeterminates.
The proof uses Mathlib's Matrix.det_vandermonde combined with:
- Column reversal (relating our matrix to Mathlib's convention)
- Sign analysis (the two sign changes cancel)
Label: lem.det.vander.a.pol
Proposition prop.det.(xi+yj)n-1 #
The determinant of the matrix ((xᵢ + yⱼ)ⁿ⁻¹) can be expressed as a product of binomial coefficients and Vandermonde-like products.
The matrix with entries (xᵢ + yⱼ)ⁿ⁻¹. Label: prop.det.(xi+yj)n-1
Equations
Instances For
Proposition prop.det.(xi+yj)n-1: det((xᵢ + yⱼ)ⁿ⁻¹) = (∏ₖ C(n-1,k)) · (∏{i<j}(xᵢ-xⱼ)) · (∏{i<j}(yⱼ-yᵢ))
The proof can be done either by factor hunting (first proof in the source) or by factoring the matrix as P · Q where P and Q are related to Vandermonde matrices (second proof in the source). Label: prop.det.(xi+yj)n-1
Laplace Expansion (Theorem thm.det.laplace) #
Laplace expansion expresses a determinant as a sum over cofactors along any row or column.
Convention conv.mat.tilde: A_{~i,~j} denotes the submatrix obtained by removing row i and column j.
In Mathlib, this is Matrix.submatrix A (Fin.succAbove i) (Fin.succAbove j)
for an (n+1)×(n+1) matrix A, yielding an n×n matrix.
Equations
Instances For
Laplace expansion along row p (Theorem thm.det.laplace (a)): det A = ∑q (-1)^(p+q) A{p,q} det(A_{~p,~q})
In Mathlib, this is Matrix.det_succ_row.
Laplace expansion along column q (Theorem thm.det.laplace (b)): det A = ∑p (-1)^(p+q) A{p,q} det(A_{~p,~q})
In Mathlib, this is Matrix.det_laplace_column.
Proposition prop.det.laplace.0 #
When we use entries from a different row/column than the one we're expanding along, the sum is zero.
Proposition prop.det.laplace.0 (a): If p ≠ r, then ∑q (-1)^(p+q) A{r,q} det(A_{~p,~q}) = 0
The proof uses the adjugate: each term equals A r q * adjugate A q p, so the sum is (A * adjugate A) r p = (det A * I) r p = 0 when r ≠ p.
Adjugate Matrix (Definition def.det.adj) #
The adjugate (classical adjoint) of a matrix A is defined by (adj A){i,j} = (-1)^(i+j) det(A{~j,~i})
Note the index swap: the (i,j) entry involves removing row j and column i.
The adjugate matrix (Definition def.det.adj).
The adjugate (or classical adjoint) of an n×n matrix A is the n×n matrix whose (i,j) entry is (-1)^(i+j) times the determinant of the (n-1)×(n-1) submatrix obtained by deleting row j and column i from A. Note the index swap: the (i,j) entry involves removing row j and column i.
The key property is: A · adj(A) = adj(A) · A = det(A) · I
Note: Mathlib defines Matrix.adjugate which is the same concept, but using a different
but equivalent definition. We provide this definition for clarity and connection to the textbook.
Label: def.det.adj
Equations
- AlgebraicCombinatorics.Determinants.adjugateMat A = Matrix.of fun (i j : Fin (m + 1)) => (-1) ^ (↑i + ↑j) * (AlgebraicCombinatorics.Determinants.submatrixRemove A j i).det
Instances For
The adjugate as defined here equals Mathlib's definition.
Mathlib defines A.adjugate i j = (A.updateRow j (Pi.single i 1)).det.
Our definition is adjugateMat A i j = (-1)^(i+j) * det(A_{~j,~i}).
These are equal by Laplace expansion along row j of the updated matrix.
Label: def.det.adj
Theorem thm.det.adj.inverse #
The fundamental property of the adjugate matrix: multiplication by the adjugate yields the determinant times the identity matrix.
Theorem Statement: Let n ∈ ℕ. Let A ∈ K^{n×n} be an n×n matrix. Let I_n denote the n×n identity matrix. Then: A · (adj A) = (adj A) · A = (det A) · I_n
Proof Sketch (from the textbook): To show A · (adj A) = (det A) · I_n, we check that the (i,j)-th entry of A · (adj A) equals det A when i = j, and equals 0 otherwise.
Case i = j: This follows from Laplace expansion along row i (Theorem thm.det.laplace (a)). The (i,i) entry of A · (adj A) is ∑k A{i,k} · (adj A){k,i} = ∑k A{i,k} · (-1)^{i+k} · det(A{~i,~k}) which equals det A by Laplace expansion.
Case i ≠ j: This follows from Proposition prop.det.laplace.0 (a). The (i,j) entry of A · (adj A) is ∑k A{i,k} · (adj A){k,j} = ∑k A{i,k} · (-1)^{j+k} · det(A{~j,~k}) which equals 0 because we're using row i entries with row j cofactors.
Similarly, (adj A) · A = (det A) · I_n can be shown using column versions.
Theorem thm.det.adj.inverse (general form for Fin n): A · adj(A) = det(A) · I
This is the fundamental property of the adjugate matrix. For any n×n matrix A, multiplying A by its adjugate yields the determinant of A times the identity matrix.
This works for all n ≥ 0, including the trivial case n = 0 where both sides equal the 0×0 identity matrix.
Label: thm.det.adj.inverse
Theorem thm.det.adj.inverse (general form for Fin n): adj(A) · A = det(A) · I
The adjugate also satisfies the identity when multiplied on the left.
Together with mul_adjugate', this shows that the adjugate is a "pseudo-inverse"
of A scaled by det(A).
Label: thm.det.adj.inverse
Theorem thm.det.adj.inverse (for Fin (m+1) matrices): A · adj(A) = det(A) · I
This version is specialized to non-empty matrices (size at least 1×1). Label: thm.det.adj.inverse
Theorem thm.det.adj.inverse (for Fin (m+1) matrices): adj(A) · A = det(A) · I
This version is specialized to non-empty matrices (size at least 1×1). Label: thm.det.adj.inverse
Corollary of thm.det.adj.inverse: Entry-wise form for the diagonal.
The (i,i) entry of A · adj(A) equals det(A). This is a direct consequence of the main theorem.
Corollary of thm.det.adj.inverse: Entry-wise form for off-diagonal entries.
The (i,j) entry of A · adj(A) equals 0 when i ≠ j. This is a direct consequence of the main theorem.
Laplace Expansion Along Multiple Rows/Columns (Theorem thm.det.laplace-multi) #
This generalizes Laplace expansion to expanding along multiple rows or columns simultaneously.
For a subset P of row indices, the determinant can be expanded as a sum over all column subsets Q of the same size, involving products of complementary minors.
Helper: Given a finset of indices, produce an order-preserving embedding into Fin m. This is used to extract submatrices corresponding to index subsets.
Equations
- AlgebraicCombinatorics.Determinants.finsetToFin S hk = (S.orderIsoOfFin hk).toEmbedding.trans (Function.Embedding.subtype fun (x : Fin m) => x ∈ S)
Instances For
The submatrix of A with rows from P and columns from Q (when |P| = |Q|). This is the minor sub_P^Q(A) in the source notation.
Equations
Instances For
The determinant of a submatrix corresponding to row set P and column set Q. Returns 0 if |P| ≠ |Q|.
Equations
- AlgebraicCombinatorics.Determinants.submatrixDet A P Q = if h : P.card = Q.card then (AlgebraicCombinatorics.Determinants.submatrixOfFinsets' A P Q ⋯ ⋯).det else 0
Instances For
Determinants.submatrixDet equals PermFinset.submatrixDet.
Both are "total" definitions (return 0 when |P| ≠ |Q|). They differ only in
implementation: this one uses finsetToFin/submatrixOfFinsets', while
PermFinset.submatrixDet uses orderEmbOfFin directly. These are definitionally equal.
The set of column subsets Q with |Q| = |P|.
Equations
- AlgebraicCombinatorics.Determinants.sameCardSubsets m P = {Q ∈ Finset.univ.powerset | Q.card = P.card}
Instances For
Permutation image definitions #
This section uses the canonical definitions from PermFinset:
PermFinset.imageFinset σ P- The image of a finset P under a permutation σPermFinset.permsMapping P Q- The set of permutations that map P to Q
See Determinants/PermFinset.lean for the shared definitions and API.
Helper lemmas for sum_perms_eq_det_prod #
The following lemmas establish properties of permutations that map one finset to another, which are needed for the multi-row Laplace expansion proof.
Sorting permutation and its sign #
The key to the multi-row Laplace expansion is understanding how permutations that map one finset to another decompose. Given finsets P and Q of the same cardinality, a permutation σ with σ(P) = Q can be decomposed as:
σ = sortQ⁻¹ ∘ (sumCongr τ ρ) ∘ sortP
where:
- sortP : Fin m ≃ Fin |P| ⊕ Fin |Pᶜ| is the "sorting" equivalence for P
- sortQ : Fin m ≃ Fin |Q| ⊕ Fin |Qᶜ| is the "sorting" equivalence for Q
- τ : Perm (Fin |P|) is the restriction of σ to P
- ρ : Perm (Fin |Pᶜ|) is the restriction of σ to Pᶜ
The sign of σ then decomposes as: sign(σ) = sign(sortP) · sign(sortQ)⁻¹ · sign(τ) · sign(ρ) = sign(sortP) · sign(sortQ) · sign(τ) · sign(ρ) (since sign² = 1)
The key identity is: sign(sortP) · sign(sortQ) = (-1)^(∑ P + ∑ Q) when |P| = |Q|
The sign decomposition: for σ ∈ PermFinset.permsMapping P Q with corresponding (τ, ρ), sign(σ) = (-1)^(∑ P + ∑ Q) · sign(τ) · sign(ρ)
Proof: By permsMappingEquiv_sign_spec, sign(σ) = sign(sortP) · sign(sortQ) · sign(τ) · sign(ρ). By sign_sortingPermOfFinset_mul, sign(sortP) · sign(sortQ) = (-1)^(∑P + ∑Q).
Theorem thm.det.laplace-multi (a): For any subset P of [n], det A = ∑{Q : |Q|=|P|} (-1)^(sum P + sum Q) det(sub_P^Q A) det(sub{~P}^{~Q} A)
This is a more general form of Laplace expansion. When |P| = 1, this reduces to the standard single-row Laplace expansion. Label: thm.det.laplace-multi
Proof strategy (from Theorem 6.156 of detnotes):
- Express det A using the Leibniz formula: det A = ∑{σ ∈ Sₙ} sign(σ) ∏ᵢ A{i,σ(i)}
- Partition permutations σ based on how they map P to subsets Q of the same size
- For each Q with |Q| = |P|, the permutations σ with σ(P) = Q factor as:
- A bijection τ : P → Q (contributing to det(sub_P^Q A))
- A bijection ρ : Pᶜ → Qᶜ (contributing to det(sub_{Pᶜ}^{Qᶜ} A))
- The sign of σ decomposes as sign(σ) = (-1)^(sum P + sum Q) · sign(τ) · sign(ρ) where the (-1)^(sum P + sum Q) accounts for reordering indices.
- Summing over all τ and ρ gives the product of minors.
Theorem thm.det.laplace-multi (b): For any subset Q of [n], det A = ∑{P : |P|=|Q|} (-1)^(sum P + sum Q) det(sub_P^Q A) det(sub{~P}^{~Q} A) Label: thm.det.laplace-multi
Desnanot-Jacobi Identity (Theorem thm.det.des-jac-1) #
The Desnanot-Jacobi identity relates the determinant of a matrix to determinants of its submatrices. This is the foundation of Dodgson condensation.
For an n×n matrix A with n ≥ 2, let A' be the (n-2)×(n-2) matrix obtained by removing the first row, last row, first column, and last column. Then:
det(A) · det(A') = det(A_{~1,~1}) · det(A_{~n,~n}) - det(A_{~1,~n}) · det(A_{~n,~1})
The proof uses the relationship between the adjugate matrix and submatrix determinants. The key insight is that the 2×2 determinant of the corner submatrix of adj(A) equals det(A) · det(A') by Jacobi's complementary minor theorem.
Helper lemmas for Desnanot-Jacobi #
The 2×2 determinant of the corner entries of the adjugate simplifies to the product of diagonal minors minus the product of off-diagonal minors. This is a key step in proving the Desnanot-Jacobi identity.
Desnanot-Jacobi identity for 2×2 matrices (base case)
Desnanot-Jacobi identity for 3×3 matrices
Desnanot-Jacobi identity for 4×4 matrices. The proof expands all determinants and uses ring to verify the polynomial identity.
Helper lemma: explicit expansion of 4×4 determinant. Used for expanding submatrices in the 5×5 Desnanot-Jacobi proof. This follows the same pattern as det_fin_three but for 4×4 matrices.
Helper lemma: explicit expansion of 5×5 determinant. Used for the 5×5 Desnanot-Jacobi proof.
Helper lemma: cofactor expansion of 6×6 determinant along the first column.
Each 5×5 minor can be further expanded using det_fin_five'.
Used for the 6×6 Desnanot-Jacobi proof.
Note: This expands the determinant as a sum of 6 terms, where each term
is a matrix entry times a 5×5 minor determinant. The 5×5 minors can be
further expanded using det_fin_five' if needed.
Desnanot-Jacobi identity for 5×5 matrices. The proof follows the same pattern as the 4×4 case: expand all determinants and use ring to verify the polynomial identity.
This is a polynomial identity in 25 variables (the matrix entries). The inner submatrix is 3×3, the removed submatrices are 4×4, and the main matrix is 5×5.
Helper lemmas for Fin.succAbove computations in 6×6 matrices #
These lemmas are used to convert Fin.succAbove indices to concrete values
when expanding determinants. Each lemma states that Fin.succAbove i j equals
a specific concrete value for i : Fin 6 and j : Fin 5.
Helper lemma: expansion of the inner 4×4 determinant for a 6×6 matrix. The inner submatrix consists of entries A i j for i, j ∈ {1, 2, 3, 4}.
Helper lemma: expansion of (submatrixRemove A (Fin.last 5) (Fin.last 5)).det for 6×6 matrices. This is the 5×5 submatrix with rows/cols 0,1,2,3,4 (removing row 5 and col 5).
Block Matrix Helpers for Complementary Minor (2×2 Corner Case) #
These lemmas provide an alternative proof path for complementary_minor_2x2_corner using
block matrix techniques. The key idea is to permute the matrix A so that rows/columns
{0, last} come first, creating a block matrix where the Schur complement formula applies.
This breaks the circular dependency between complementary_minor_2x2_corner and
desnanot_jacobi for m ≥ 5 matrices. (The circular dependency has been resolved.)
Desnanot-Jacobi identity for 6×6 matrices. This lemma is placed after desnanot_jacobi_field to avoid circular dependencies. The proof uses the polynomial ring approach combined with field of fractions.
The key lemma for 2×2 matrices (base case n = 0): For a 2×2 matrix, adj₀₀ * adj₁₁ - adj₀₁ * adj₁₀ = det(A) * 1 = det(A).
This is the base case of Jacobi's complementary minor theorem. For 2×2 matrix [[a,b],[c,d]], adjugate = [[d,-b],[-c,a]], so:
- adj₀₀ * adj₁₁ = d * a
- adj₀₁ * adj₁₀ = (-b) * (-c) = bc
- LHS = da - bc = det(A)
- RHS = det(A) * det(0×0 matrix) = det(A) * 1 = det(A) ✓
The key lemma for 3×3 matrices (case n = 1): For a 3×3 matrix, the 2×2 determinant of the corner entries of the adjugate equals det(A) times the middle entry A₁₁.
This verifies Jacobi's complementary minor theorem for the specific case where P = Q = {0, 2} (first and last indices).
Desnanot-Jacobi identity (Theorem thm.det.des-jac-1): det(A) · det(A') = det(A_{~1,~1}) · det(A_{~n,~n}) - det(A_{~1,~n}) · det(A_{~n,~1})
Here A' is the inner submatrix (removing first/last rows and columns).
The proof uses Jacobi's complementary minor theorem: the 2×2 determinant of the corner submatrix of adj(A) at positions {0, last} × {0, last} equals det(A) · det(innerSubmatrix A).
Label: thm.det.des-jac-1
Alternative formulation of Desnanot-Jacobi using a 2×2 determinant: det(A) · det(A') = det [[det(A_{~1,~1}), det(A_{~1,~n})], [det(A_{~n,~1}), det(A_{~n,~n})]] Label: thm.det.des-jac-1
Generalized Desnanot-Jacobi (Theorem thm.det.des-jac-2) #
The generalized version allows choosing any two rows p < q and any two columns u < v, not just the first and last.
Alias for Fin.skipTwo - skip two indices p < q in Fin (m+2).
This definition is imported from AlgebraicCombinatorics.Fin.SkipTwo.
Equations
- AlgebraicCombinatorics.Determinants.skipTwo p q hpq = p.skipTwo q hpq
Instances For
Submatrix removing two rows (p, q with p < q) and two columns (u, v with u < v). This is the submatrix sub_{[n]{p,q}}^{[n]{u,v}} A in the source notation.
Equations
- AlgebraicCombinatorics.Determinants.submatrixRemove2 A p q u v hpq huv = A.submatrix (p.skipTwo q hpq) (u.skipTwo v huv)
Instances For
Properties of skipTwo #
These lemmas are aliases for the corresponding lemmas in AlgebraicCombinatorics.Fin.SkipTwo.
skipTwo is strictly monotone. Alias for Fin.skipTwo_strictMono.
skipTwo is injective. Alias for Fin.skipTwo_injective.
skipTwo equals the canonical orderEmbOfFin enumeration of {p,q}ᶜ. This is the key lemma that connects skipTwo with Mathlib's canonical enumeration, allowing us to use Mathlib's API for ordered enumerations of finsets.
skipTwo equals finsetToFin on the complement {p,q}ᶜ. This connects our explicit skipTwo function with the canonical enumeration used in submatrixDet and submatrixOfFinsets'.
The determinant of submatrixRemove2 equals submatrixDet on complements. This is the key connection between our explicit submatrix construction and the general submatrixDet definition using finsets. Combined with jacobi_complementary_minor, this allows proving desnanot_jacobi_direct for all matrix sizes.
Helper lemmas for skipTwo in Fin 4 #
These simp lemmas allow efficient computation of skipTwo values for all valid
(p, q) pairs in Fin 4. There are 6 such pairs: (0,1), (0,2), (0,3), (1,2), (1,3), (2,3).
Helper lemmas for Fin.succAbove in Fin 4 #
These simp lemmas allow efficient computation of Fin.succAbove for Fin 4.
Equations
- AlgebraicCombinatorics.Determinants.tacticDj4_tac = Lean.ParserDescr.node `AlgebraicCombinatorics.Determinants.tacticDj4_tac 1024 (Lean.ParserDescr.nonReservedSymbol "dj4_tac" false)
Instances For
For a matrix over a field with nonzero determinant, each entry of the inverse equals the corresponding adjugate entry divided by the determinant.
Note: A⁻¹ i j = adjugate(A) i j / det(A) (same indices, not swapped). This follows from A⁻¹ = det⁻¹ • adjugate.
Key lemma: For invertible A, the adjugate submatrix equals det(A) times the inverse submatrix. This follows from adj(A) = det(A) • A⁻¹ for invertible A.
For invertible A with |P| = |Q| = k, the determinant of the adjugate submatrix equals det(A)^k times the determinant of the inverse submatrix. This reduces Jacobi's complementary minor theorem to the complementary minor theorem for inverse matrices.
Complementary minor theorem for block matrices (special case).
For a block matrix M = [[A, B], [C, D]] with D invertible and the Schur complement (A - B * D⁻¹ * C) invertible, the determinant of the top-left block of M⁻¹ satisfies:
det(M) * det((M⁻¹)₁₁) = det(D)
This is the key lemma for Jacobi's complementary minor theorem. It follows from the Schur complement formula: det(M) = det(D) * det(A - B * D⁻¹ * C), combined with the fact that (M⁻¹)₁₁ = (A - B * D⁻¹ * C)⁻¹.
The general complementary minor theorem (for arbitrary index sets P, Q) follows by permuting rows and columns to bring P and Q to the first positions.
Helper lemmas for the Schur complement approach #
The key identity for block matrices relates the determinant of the adjugate's top-left block to the determinant of the original matrix and its bottom-right block:
det(adj(M).toBlocks₁₁) = det(M)^(k-1) * det(M.toBlocks₂₂)
where k is the size of the top-left block.
This follows from the Schur complement formula for block matrix inverses.
Key identity: For invertible block matrices with invertible bottom-right block, the determinant of the adjugate's top-left block equals det(M)^(k-1) * det(D).
This is the Schur complement version of Jacobi's complementary minor theorem for the special case of block matrices.
Helper: convert orderIsoOfFin to an embedding from Fin |P| to Fin m. This gives an order-preserving embedding that picks out the elements of P.
Equations
- AlgebraicCombinatorics.Determinants.finsetOrderEmb P = (P.orderIsoOfFin ⋯).toEmbedding.trans (Function.Embedding.subtype fun (x : Fin m) => x ∈ P)
Instances For
finsetOrderEmb is injective (follows from being an embedding).
Equivalence that sorts indices so that P elements come first (as Sum.inl)
and Pᶜ elements come second (as Sum.inr). This uses finSumEquivOfFinset.
Equations
Instances For
sortEquivPQ_cast sends Sum.inr to finsetOrderEmb of the complement (with appropriate casting). This is the key lemma for relating the bottom-right block of M to the complementary submatrix.
The top-left block of (A⁻¹.submatrix τ σ) equals sub_P^Q(A⁻¹).
Corollary: For invertible A with |P| = |Q| = k, the determinant of the adjugate submatrix can be computed from the complementary minor of A.
det(sub_P^Q(adj A)) = (-1)^(sum P + sum Q) * det(A)^(k-1) * det(sub_{Qᶜ}^{Pᶜ}(A))
This follows from:
- adj(A) = det(A) * A⁻¹ for invertible A
- det(sub_P^Q(adj A)) = det(A)^k * det(sub_P^Q(A⁻¹))
- complementary_minor_inverse: det(A) * det(sub_P^Q(A⁻¹)) = (-1)^(...) * det(sub_{Qᶜ}^{Pᶜ}(A))
Alternative Approach via Jacobi's Complementary Minor Theorem #
The desnanot_jacobi_direct lemma below can alternatively be proved using jacobi_complementary_minor
(which is already proved in this file). The key insight is:
jacobi_complementary_minorwith P = {u, v} and Q = {p, q} gives:submatrixDet A.adjugate {u,v} {p,q} = (-1)^(u+v+p+q) * A.det * submatrixDet A {p,q}ᶜ {u,v}ᶜThe LHS can be expressed as a 2×2 determinant of adjugate entries:
A.adjugate u p * A.adjugate v q - A.adjugate u q * A.adjugate v pBy
adjugate_2x2_eq, this equals:(-1)^(p+u+q+v) * (det(A_{~p,~u}) * det(A_{~q,~v}) - det(A_{~q,~u}) * det(A_{~p,~v}))Combining and canceling the sign factor:
det(A_{~p,~u}) * det(A_{~q,~v}) - det(A_{~p,~v}) * det(A_{~q,~u}) = A.det * submatrixDet A {p,q}ᶜ {u,v}ᶜThe RHS
submatrixDet A {p,q}ᶜ {u,v}ᶜequals(submatrixRemove2 A p q u v).det, giving the Desnanot-Jacobi identity.
This approach requires proving that orderEmbOfFin on the complement {p,q}ᶜ gives the same
indexing as skipTwo p q. The following helper lemmas support this approach.
Generalized Desnanot-Jacobi identity (Theorem thm.det.des-jac-2): For p < q and u < v, det(A) · det(sub_{[n]{p,q}}^{[n]{u,v}} A) = det(A_{~p,~u}) · det(A_{~q,~v}) - det(A_{~p,~v}) · det(A_{~q,~u})
The proof follows from Jacobi's complementary minor theorem for the 2×2 case. By comparing the 2×2 determinant of the adjugate submatrix (computed two ways), we obtain the desired identity. Label: thm.det.des-jac-2
Cauchy Determinant (Theorem thm.det.cauchy) #
The Cauchy determinant formula gives the determinant of the matrix (1/(xᵢ + yⱼ)).
Helper lemmas for Cauchy determinant #
The numerator of the Cauchy determinant formula: ∏_{i<j}((xᵢ - xⱼ)(yᵢ - yⱼ))
Equations
- AlgebraicCombinatorics.Determinants.cauchyNumerator x y = ∏ i : Fin m, ∏ j ∈ Finset.Ioi i, (x i - x j) * (y i - y j)
Instances For
The denominator of the Cauchy determinant formula: ∏_{i,j}(xᵢ + yⱼ)
Equations
- AlgebraicCombinatorics.Determinants.cauchyDenominator x y = ∏ i : Fin m, ∏ j : Fin m, (x i + y j)
Instances For
Multivariate Factor Theorem #
The multivariate factor theorem is a key tool for the factor hunting proof. It states that if a polynomial P evaluates to 0 when we substitute X_j for X_i, then (X_i - X_j) divides P.
This is proved by induction on the polynomial structure, showing that P - P|_{X_i = X_j} is divisible by (X_i - X_j).
Substitution that replaces X_i with X_j in a multivariate polynomial.
Equations
- AlgebraicCombinatorics.Determinants.substXiToXj i j = MvPolynomial.aeval fun (k : σ) => if k = i then MvPolynomial.X j else MvPolynomial.X k
Instances For
The multivariate factor theorem: (X_i - X_j) divides P - P|_{X_i = X_j}. This is the multivariate analogue of Polynomial.sub_dvd_eval_sub.
Corollary of the multivariate factor theorem: if P|_{X_i = X_j} = 0, then (X_i - X_j) | P.
When x_i = x_j for i ≠ j, the determinant of the polynomial Cauchy matrix is 0 because two rows become equal. This is a key lemma for the factor hunting proof.
When y_i = y_j for i ≠ j, the determinant of the polynomial Cauchy matrix is 0 because two columns become equal. This is a key lemma for the factor hunting proof.
Multivariate Factor Theorem #
The multivariate factor theorem states: if P ∈ MvPolynomial σ R (R a domain) and P evaluates to 0 when we substitute X_j for X_i, then (X_i - X_j) | P.
This is proved by viewing P as a univariate polynomial in X_i over the ring of polynomials in the other variables, and applying the standard factor theorem.
These lemmas provide the infrastructure needed for the factor hunting proof of the Cauchy determinant formula.
Key lemma: relates finSuccEquiv evaluation to variable substitution. When we evaluate the finSuccEquiv image at X 0, it corresponds to substituting X 1 for X 0 in the original polynomial.
Helper: finSuccEquiv sends rename Fin.succ to Polynomial.C
The multivariate factor theorem for Fin (m+2) with indices 0 and 1: If P(X_0, X_1, ...) vanishes when X_0 is replaced by X_1, then (X_0 - X_1) divides P.
The total degree of X_i - X_j is 1 for distinct i and j. This is a key lemma for proving irreducibility of linear factors.
The polynomial X_i - X_j is primitive (only units divide all coefficients).
This is needed for irreducible_of_totalDegree_eq_one.
The polynomial X_i - X_j is irreducible in MvPolynomial σ ℤ for distinct i and j. This is a key lemma for the factor hunting proof of the Cauchy determinant formula.
Divisibility lemmas for the polynomial Cauchy determinant #
These lemmas establish that the determinant of the polynomial Cauchy matrix is divisible by each factor (x_i - x_j) and (y_i - y_j) for i ≠ j. This is the key step in the factor hunting proof of the Cauchy determinant formula.
The polynomial Cauchy matrix over MvPolynomial (Fin n ⊕ Fin n) ℤ. Entry (i, j) is ∏{k ≠ j} (X{inl i} + X_{inr k}).
Equations
- AlgebraicCombinatorics.Determinants.polyCauchyMat' m = Matrix.of fun (i j : Fin m) => ∏ k : Fin m with k ≠ j, (MvPolynomial.X (Sum.inl i) + MvPolynomial.X (Sum.inr k))
Instances For
Substitution that sets x_i = x_j (replaces X_{inl i} with X_{inl j}).
Equations
- AlgebraicCombinatorics.Determinants.substX_inl m i j = MvPolynomial.aeval fun (k : Fin m ⊕ Fin m) => if k = Sum.inl i then MvPolynomial.X (Sum.inl j) else MvPolynomial.X k
Instances For
Substitution that sets y_i = y_j (replaces X_{inr i} with X_{inr j}).
Equations
- AlgebraicCombinatorics.Determinants.substY_inr m i j = MvPolynomial.aeval fun (k : Fin m ⊕ Fin m) => if k = Sum.inr i then MvPolynomial.X (Sum.inr j) else MvPolynomial.X k
Instances For
After substituting x_i = x_j, rows i and j of the polynomial Cauchy matrix become equal.
After substituting y_i = y_j, columns i and j of the polynomial Cauchy matrix become equal.
The determinant of the polynomial Cauchy matrix vanishes after substituting x_i = x_j.
The determinant of the polynomial Cauchy matrix vanishes after substituting y_i = y_j.
substX_inl is the same as substXiToXj for Sum.inl indices.
substY_inr is the same as substXiToXj for Sum.inr indices.
The determinant of the polynomial Cauchy matrix is divisible by (x_i - x_j) for i ≠ j.
The determinant of the polynomial Cauchy matrix is divisible by (y_i - y_j) for i ≠ j.
Coprimality of linear factors #
To complete the factor hunting proof of the Cauchy determinant, we need to show that the linear factors (X_i - X_j) and (X_k - X_l) are coprime when they correspond to different pairs. This section establishes the necessary lemmas.
Two linear factors X_i - X_j and X_k - X_l are equal iff (i,j) = (k,l).
X_i - X_j equals -(X_k - X_l) iff (i,j) = (l,k).
Units in MvPolynomial σ ℤ are exactly ±1.
X_i - X_j and X_k - X_l are associated iff (i,j) = (k,l) or (i,j) = (l,k).
Distinct linear factors X_i - X_j and X_k - X_l are not divisible by each other when they're not associated (i.e., when (i,j) ≠ (k,l) and (i,j) ≠ (l,k)).
Distinct linear factors (X_i - X_j) and (X_k - X_l) are relatively prime when not associated.
This is a key lemma for the factor hunting proof: we can use Finset.prod_dvd_of_isRelPrime
to show that the product of coprime factors divides the determinant.
An x-factor (X_{inl i} - X_{inl j}) and a y-factor (X_{inr k} - X_{inr l}) are always coprime because they involve variables from different sum sides. This is a key lemma for showing that the product of all factors divides the Cauchy determinant.
Helper lemmas for the factor hunting proof #
The following lemmas establish pairwise coprimality of factors and show that the product of all factors divides the determinant. This is the key step in the factor hunting proof of the Cauchy determinant formula.
Evaluation equality for the Cauchy determinant #
This section proves that at the evaluation point f(inl i) = i, f(inr j) = m + j, the determinant of the polynomial Cauchy matrix equals the product of squared differences.
This is the key lemma needed to complete the factor hunting proof for the Cauchy determinant.
Base cases for shifted Cauchy determinant #
These lemmas prove the determinant formula for shifted Cauchy matrices of small sizes. They are used in the inductive proof of the general Cauchy determinant formula.
Additional verified instances for polynomial interpolation #
For n=0, the identity is a polynomial identity in offset of degree 36. To prove by polynomial interpolation, we need 37 verified points. The following lemmas extend the verified instances.
Additional verified instances for n ≥ 5 #
These instances provide additional evidence for the algebraic identity and could be used in a polynomial interpolation proof. For n=5, the polynomial identity has degree ~256, so we would need ~257 verified points to use interpolation.
Polynomial approach for proving the identity #
The key insight is that genDenom n offset can be expressed as an explicit polynomial in offset. For small n, we can expand the product and use ring to prove the identity.
Helper lemmas for degree/homogeneity arguments #
These lemmas establish that when a polynomial divides another polynomial of the same homogeneous degree, the quotient must be a constant. This is key to completing the factor hunting proof for the Cauchy determinant.
Alternative form of Cauchy determinant without division: det(∏{k≠j}(xᵢ + yₖ)) = ∏{i<j}((xᵢ - xⱼ)(yᵢ - yⱼ))
This form is useful when working over polynomial rings.
The proof for n ≥ 4 uses the factor hunting technique:
- Both sides are homogeneous polynomials of degree n(n-1) in x_i and y_j
- The LHS vanishes when x_i = x_j (by
cauchy_poly_det_zero_of_x_eq) - The LHS vanishes when y_i = y_j (by
cauchy_poly_det_zero_of_y_eq) - Since the polynomial ring is a UFD, the LHS is divisible by each (x_i - x_j) and (y_i - y_j)
- The RHS is exactly this product, and degrees match, so LHS = c * RHS for some constant c
- Comparing leading coefficients shows c = 1
Label: thm.det.cauchy
Cauchy determinant follows from the polynomial version.
This lemma shows how cauchy_det can be derived from cauchy_det_poly.
The key insight is that:
cauchy_det_polyproves: det(∏{k≠j}(xᵢ + yₖ)) = ∏{i<j}((xᵢ - xⱼ)(yᵢ - yⱼ))- The LHS equals (∏ᵢ∏ⱼ(xᵢ + yⱼ)) · det(cauchyMat)
- Dividing both sides by ∏ᵢ∏ⱼ(xᵢ + yⱼ) gives the Cauchy determinant formula
Label: thm.det.cauchy
Cauchy determinant (Theorem thm.det.cauchy): det(1/(xᵢ + yⱼ)) = ∏{i<j}((xᵢ - xⱼ)(yᵢ - yⱼ)) / ∏{i,j}(xᵢ + yⱼ)
This is the main Cauchy determinant formula. The proof uses cauchy_det_of_poly,
which derives the formula from the polynomial version cauchy_det_poly.
Proof strategy (from the textbook):
- Work with the "cleared" polynomial version: det(∏{k≠j}(xᵢ + yₖ)) = ∏{i<j}((xᵢ - xⱼ)(yᵢ - yⱼ))
- Use factor hunting: both sides are polynomials, show divisibility + degree matching + evaluation
- Divide both sides by ∏_{i,j}(xᵢ + yⱼ) to recover the Cauchy formula
Note: The proof is complete for n = 0-7. For n ≥ 8, there is a sorry in cauchyMatEval_det
which is used to verify the evaluation equality in the factor hunting proof.
Label: thm.det.cauchy
Jacobi's Complementary Minor Theorem (Theorem thm.det.jacobi-complement) #
This is a far-reaching generalization of the Desnanot-Jacobi identity, relating minors of the adjugate to minors of the original matrix.
For subsets P, Q ⊆ [n] with |P| = |Q| ≥ 1: det(sub_P^Q(adj A)) = (-1)^(sum P + sum Q) · (det A)^(|Q|-1) · det(sub_{~Q}^{~P} A)
Jacobi's complementary minor theorem for adjugates (Theorem thm.det.jacobi-complement): det(sub_P^Q(adj A)) = (-1)^(sum P + sum Q) · (det A)^(|Q|-1) · det(sub_{~Q}^{~P} A)
Here P and Q are subsets of [n] with |P| = |Q| ≥ 1, and ~P, ~Q denote complements.
This theorem relates a minor of the adjugate matrix to a complementary minor of the original matrix, scaled by a power of the determinant. Label: thm.det.jacobi-complement
Proof strategy (following Prasolov's "Problems and Theorems in Linear Algebra"):
Polynomial matrix approach: Let A' = mvPolynomialX m m ℤ be the generic m×m matrix with polynomial entries. Since det(A') is a nonzero polynomial, we can work in a setting where A' is "generically invertible".
Key identity for invertible matrices: For invertible A, we have adj(A) = det(A) • A⁻¹. This means sub_P^Q(adj(A)) = det(A)^|P| • sub_P^Q(A⁻¹) (when taking a |P|×|Q| submatrix and |P| = |Q|).
Complementary minor theorem for inverse matrices: The classical result states that for invertible A with |P| = |Q|: det(sub_P^Q(A⁻¹)) = (-1)^(sum P + sum Q) • det(sub_{~Q}^{~P}(A)) / det(A)
Combining: For invertible A with |P| = |Q| = k: det(sub_P^Q(adj(A))) = det(A)^k • det(sub_P^Q(A⁻¹)) = det(A)^k • (-1)^(sum P + sum Q) • det(sub_{~Q}^{~P}(A)) / det(A) = (-1)^(sum P + sum Q) • det(A)^(k-1) • det(sub_{~Q}^{~P}(A))
Specialization: The result for the generic matrix A' implies the result for all matrices A via the evaluation homomorphism.
The key missing infrastructure in Mathlib is the complementary minor theorem for inverse matrices (step 3), which typically requires block matrix determinant formulas.
Desnanot-Jacobi is a special case of Jacobi's complementary minor theorem with P = {u, v} and Q = {p, q}.
This theorem provides a DIRECT proof using jacobi_complementary_minor, which is proved independently of desnanot_jacobi_direct.
The proof combines:
- jacobi_complementary_minor with P = {u, v}, Q = {p, q} (2×2 case)
- adjugate_2x2_eq to express adjugate products as submatrix determinants
- submatrixRemove2_det_eq_submatrixDet_compl to relate the complement to submatrixRemove2