Determinants: Cauchy-Binet and Related Formulas

This file formalizes the Cauchy-Binet formula and related determinant identities, following Section "Cauchy--Binet ... Factoring the matrix" of the source (CauchyBinet.tex).

Main definitions

• Matrix.submatrix - The submatrix obtained by restricting to specific rows and columns. This corresponds to sub_U^V A in the source (Definition def.det.sub).
• colsSubmatrix, rowsSubmatrix - Submatrices selecting specific columns/rows.

Main results

• cauchyBinet - The general Cauchy-Binet formula for det(AB) where A is n×m and B is m×n (Theorem thm.det.CB)
• cauchyBinet_square - Special case for square matrices: det(AB) = det(A)·det(B)
• det_mul_eq_zero_of_rank_deficient - When m < n, det(AB) = 0
• det_add_sum - Formula for det(A+B) as a double sum over subsets (Theorem thm.det.det(A+B))
• det_diagonal_submatrix_eq, det_diagonal_submatrix_off_diag - Minors of diagonal matrices (Lemma lem.det.minors-diag)
• det_add_diagonal - Simplified formula when adding a diagonal matrix (Theorem thm.det.det(A+D))
• det_const_add_diagonal - Determinant of x + D where D is diagonal (Proposition prop.det.x+ai)
• det_charPoly_coeff - Coefficients of the characteristic polynomial (Proposition prop.det.charpol-explicit)
• det_pascal_matrix - The Pascal matrix has determinant 1 (Proposition prop.det.pascal-LU)

References

• Source: CauchyBinet.tex

Implementation notes

Mathlib already provides Matrix.det_mul in Mathlib.LinearAlgebra.Matrix.Determinant. We provide additional results and connect Mathlib's API to the textbook presentation.

The submatrix operation Matrix.submatrix uses functions for row/column selection, which is more general than the textbook's subset-based notation.

Submatrices (Definition def.det.sub)

For an n×m matrix A, subsets U ⊆ [n] and V ⊆ [m], we define sub_U^V A to be the |U|×|V| submatrix obtained by keeping only the rows indexed by U and columns indexed by V (in increasing order).

In Mathlib, this is Matrix.submatrix A f g where f and g are the order-preserving embeddings of U and V into [n] and [m].

noncomputable def AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset {R : Type u_1} {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) : Matrix (Fin U.card) (Fin V.card) R

The submatrix of A obtained by restricting to rows in U and columns in V. This corresponds to sub_U^V A in the source (Definition def.det.sub). Label: def.det.sub

Mathematical Description

Let A be an n×m matrix. Let U ⊆ [n] and V ⊆ [m] be subsets. Writing U = {u₁, u₂, ..., uₚ} with u₁ < u₂ < ... < uₚ and V = {v₁, v₂, ..., vₚ} with v₁ < v₂ < ... < vₚ, we define sub_U^V A := (A_{uᵢ,vⱼ})_{1≤i≤p, 1≤j≤q}.

This is the |U|×|V| matrix obtained from A by keeping only the rows indexed by U and columns indexed by V, in increasing order.

Terminology

• Submatrix: The matrix sub_U^V A
• Minor: When |U| = |V|, the determinant det(sub_U^V A) is called a minor of A
• Principal minor: When U = V, the minor det(sub_U^U A) is called a principal minor

Implementation

In Mathlib, Matrix.submatrix takes functions for row and column selection. For finite sets, we use the canonical order-preserving embedding orderEmbOfFin.

Equations

• AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset A U V = A.submatrix ⇑(U.orderEmbOfFin ⋯) ⇑(V.orderEmbOfFin ⋯)

def AlgebraicCombinatorics.CauchyBinet.«termSub[_,_]_» : Lean.ParserDescr

Notation for submatrices: sub[U,V] A denotes sub_U^V A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_apply {n m : ℕ} {R : Type u_2} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) (i : Fin U.card) (j : Fin V.card) : submatrixOfFinset A U V i j = A ((U.orderEmbOfFin ⋯) i) ((V.orderEmbOfFin ⋯) j)

The (i, j) entry of sub_U^V A is A_{uᵢ, vⱼ} where uᵢ is the i-th smallest element of U and vⱼ is the j-th smallest element of V.

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_empty_rows {n m : ℕ} {R : Type u_2} (A : Matrix (Fin n) (Fin m) R) (V : Finset (Fin m)) : submatrixOfFinset A ∅ V = ![]

The submatrix of the empty row set is a 0×|V| matrix.

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_empty_cols {n m : ℕ} {R : Type u_2} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) : submatrixOfFinset A U ∅ = fun (x : Fin U.card) (j : Fin ∅.card) => j.elim0

The submatrix of the empty column set is a |U|×0 matrix.

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_add {R : Type u_1} [CommRing R] {n m : ℕ} (A B : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) : submatrixOfFinset (A + B) U V = submatrixOfFinset A U V + submatrixOfFinset B U V

The submatrix respects matrix addition.

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_smul {R : Type u_1} [CommRing R] {n m : ℕ} (c : R) (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) : submatrixOfFinset (c • A) U V = c • submatrixOfFinset A U V

The submatrix respects scalar multiplication.

theorem AlgebraicCombinatorics.CauchyBinet.submatrixOfFinset_transpose {n m : ℕ} {R : Type u_2} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) : (submatrixOfFinset A U V).transpose = submatrixOfFinset A.transpose V U

The transpose of a submatrix equals the submatrix of the transpose with swapped indices.

noncomputable def AlgebraicCombinatorics.CauchyBinet.minor {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) : R

A minor of a matrix A is the determinant of a square submatrix. This is det(sub_U^V A) where |U| = |V|.

If |U| ≠ |V|, we define the minor to be 0 (since the submatrix is not square).

Equations

• AlgebraicCombinatorics.CauchyBinet.minor A U V = if h : U.card = V.card then (A.submatrix ⇑(U.orderEmbOfFin ⋯) ⇑(V.orderEmbOfFin ⋯)).det else 0

theorem AlgebraicCombinatorics.CauchyBinet.minor_eq_det {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) (h : U.card = V.card) : minor A U V = (A.submatrix ⇑(U.orderEmbOfFin ⋯) ⇑(V.orderEmbOfFin ⋯)).det

When |U| = |V|, the minor equals the determinant of the submatrix.

theorem AlgebraicCombinatorics.CauchyBinet.minor_eq_zero_of_card_ne {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (U : Finset (Fin n)) (V : Finset (Fin m)) (h : U.card ≠ V.card) : minor A U V = 0

When |U| ≠ |V|, the minor is 0.

theorem AlgebraicCombinatorics.CauchyBinet.minor_eq_permFinset_submatrixDet {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) : minor A P Q = PermFinset.submatrixDet A P Q

For square matrices, CauchyBinet.minor equals PermFinset.submatrixDet.

Both are "total" definitions (return 0 when |U| ≠ |V|). They are definitionally equal for square matrices.

noncomputable def AlgebraicCombinatorics.CauchyBinet.principalMinor {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P : Finset (Fin n)) : R

A principal minor of a square matrix is a minor where U = V. These are the determinants of principal submatrices (same rows and columns).

Equations

• AlgebraicCombinatorics.CauchyBinet.principalMinor A P = (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det

theorem AlgebraicCombinatorics.CauchyBinet.principalMinor_eq_minor {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P : Finset (Fin n)) : principalMinor A P = minor A P P

Principal minor equals the general minor when U = V.

theorem AlgebraicCombinatorics.CauchyBinet.minor_empty {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) : minor A ∅ ∅ = 1

The minor of the empty set is 1 (determinant of 0×0 matrix).

Cauchy-Binet Formula (Theorem thm.det.CB)

For an n×m matrix A and an m×n matrix B: det(AB) = ∑_{g : strictly increasing n-tuple from [m]} det(cols_g A) · det(rows_g B)

This generalizes det(AB) = det(A)·det(B) for square matrices.

Special cases:

• If m < n, the sum is empty, so det(AB) = 0
• If m = n, there's only one term: det(A)·det(B)

theorem AlgebraicCombinatorics.CauchyBinet.cauchyBinet_square {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (A B : Matrix n n R) : (A * B).det = A.det * B.det

The Cauchy-Binet formula for square matrices: det(AB) = det(A)·det(B). (Theorem thm.det.CB, special case m = n) Label: thm.det.CB

The general Cauchy-Binet formula for non-square matrices involves a sum over order-preserving embeddings. This special case is what Mathlib provides directly as Matrix.det_mul.

noncomputable def AlgebraicCombinatorics.CauchyBinet.colsSubmatrix {R : Type u_1} {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (S : Finset (Fin m)) (hcard : S.card = n) : Matrix (Fin n) (Fin n) R

Submatrix obtained by selecting specific columns of A. cols_g A in the source notation selects columns indexed by g.

Equations

• AlgebraicCombinatorics.CauchyBinet.colsSubmatrix A S hcard = A.submatrix id ⇑(S.orderEmbOfFin hcard)

noncomputable def AlgebraicCombinatorics.CauchyBinet.rowsSubmatrix {R : Type u_1} {n m : ℕ} (B : Matrix (Fin m) (Fin n) R) (S : Finset (Fin m)) (hcard : S.card = n) : Matrix (Fin n) (Fin n) R

Submatrix obtained by selecting specific rows of B. rows_g B in the source notation selects rows indexed by g.

Equations

• AlgebraicCombinatorics.CauchyBinet.rowsSubmatrix B S hcard = B.submatrix (⇑(S.orderEmbOfFin hcard)) id

theorem AlgebraicCombinatorics.CauchyBinet.det_mul_aux_nonsquare {R : Type u_1} [CommRing R] {n m : ℕ} {A : Matrix (Fin n) (Fin m) R} {B : Matrix (Fin m) (Fin n) R} {f : Fin n → Fin m} (hf : ¬Function.Injective f) : ∑ σ : Equiv.Perm (Fin n), ↑↑(Equiv.Perm.sign σ) * ∏ i : Fin n, A (σ i) (f i) * B (f i) i = 0

Helper lemma: when f is not injective, the alternating sum over permutations is 0.

theorem AlgebraicCombinatorics.CauchyBinet.sum_over_subset_eq_det_mul {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (B : Matrix (Fin m) (Fin n) R) (S : Finset (Fin m)) (hcard : S.card = n) : ∑ τ : Equiv.Perm (Fin n), ∑ σ : Equiv.Perm (Fin n), ↑↑(Equiv.Perm.sign σ) * ∏ i : Fin n, A (σ i) ((S.orderEmbOfFin hcard) (τ i)) * B ((S.orderEmbOfFin hcard) (τ i)) i = (colsSubmatrix A S hcard).det * (rowsSubmatrix B S hcard).det

Key identity: for a fixed subset S, the sum over permutations gives det(cols_S A) * det(rows_S B).

theorem AlgebraicCombinatorics.CauchyBinet.cauchyBinet {R : Type u_1} [CommRing R] {n m : ℕ} (A : Matrix (Fin n) (Fin m) R) (B : Matrix (Fin m) (Fin n) R) : (A * B).det = ∑ S ∈ Finset.powersetCard n Finset.univ, if h : S.card = n then (colsSubmatrix A S h).det * (rowsSubmatrix B S h).det else 0

The general Cauchy-Binet formula (Theorem thm.det.CB). For an n×m matrix A and an m×n matrix B: det(AB) = ∑_{S ⊆ [m], |S|=n} det(cols_S A) · det(rows_S B)

The sum ranges over all n-element subsets S of [m], where cols_S A is the n×n matrix formed by selecting columns of A indexed by S (in increasing order), and rows_S B is the n×n matrix formed by selecting rows of B indexed by S.

Special cases:

• If m < n, the sum is empty (no n-element subsets), so det(AB) = 0
• If m = n, there's only one term S = [m], giving det(A)·det(B)

theorem AlgebraicCombinatorics.CauchyBinet.det_mul_eq_zero_of_rank_deficient {R : Type u_1} [CommRing R] {n m : ℕ} [NeZero n] (A : Matrix (Fin n) (Fin m) R) (B : Matrix (Fin m) (Fin n) R) (h : m < n) : (A * B).det = 0

When m < n for an n×m matrix times an m×n matrix, det(AB) = 0. (Remark after Theorem thm.det.CB)

This follows from the general Cauchy-Binet formula: when m < n, there are no n-element subsets of [m], so the sum is empty.

When K is a field, this can also be seen from rank considerations: the product AB has rank at most m < n.

Determinant of A + B (Theorem thm.det.det(A+B))

For n×n matrices A and B: det(A+B) = ∑{P ⊆ [n]} ∑{Q ⊆ [n], |P|=|Q|} (-1)^(sum P + sum Q) · det(sub_P^Q A) · det(sub_P̃^Q̃ B)

where P̃ denotes the complement [n] \ P.

This is a "binomial theorem" for determinants, containing det(A) (P=Q=[n]) and det(B) (P=Q=∅) as special terms.

def AlgebraicCombinatorics.CauchyBinet.finsetSumFin {n : ℕ} (P : Finset (Fin n)) : ℕ

Sum of elements in a finset of Fin n, viewed as natural numbers. Used in the sign factor of the det(A+B) formula.

Note: This is named finsetSumFin to distinguish from AlgebraicCombinatorics.QBinomialRec.finsetSumNat, which computes the sum of elements in a Finset ℕ directly. Both compute "the sum of elements" but for different element types.

Equations

• AlgebraicCombinatorics.CauchyBinet.finsetSumFin P = ∑ i ∈ P, ↑i

@[simp]

theorem AlgebraicCombinatorics.CauchyBinet.finsetSumFin_empty {n : ℕ} : finsetSumFin ∅ = 0

The sum over the empty set is 0.

noncomputable def AlgebraicCombinatorics.CauchyBinet.submatrixDet {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (h : P.card = Q.card) : R

Helper: Given P, Q with same cardinality, compute the determinant of the submatrix of A restricted to rows P and columns Q.

Equations

• AlgebraicCombinatorics.CauchyBinet.submatrixDet A P Q h = (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(Q.orderEmbOfFin ⋯)).det

theorem AlgebraicCombinatorics.CauchyBinet.submatrixDet_eq_permFinset {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (h : P.card = Q.card) : submatrixDet A P Q h = PermFinset.submatrixDet A P Q

CauchyBinet.submatrixDet equals PermFinset.submatrixDet when cardinalities match.

This lemma bridges the proof-requiring version in CauchyBinet with the total version in PermFinset. Use this when migrating code between the two styles.

Proof infrastructure for det(A+B) formula

The proof proceeds in several steps:

1. Expand det(A+B) using the Leibniz formula
2. Use the product rule ∏(a+b) = ∑P (∏{i∈P} a_i)(∏_{i∈Pᶜ} b_i)
3. Swap the order of summation
4. Partition the sum over σ based on σ(P) = Q
5. Factor out the sign and show it equals (-1)^(sum P + sum Q)
6. Recognize the remaining sums as determinants of submatrices

Permutation image definitions

These are local definitions that duplicate the bodies of the canonical definitions in PermFinset namespace (Determinants/PermFinset.lean). The definitions are definitionally equal to their PermFinset counterparts (witnessed by imageFinset_eq_permFinset and permsMapping_eq_permFinset), but are kept as separate defs rather than wrappers because many proofs in this file rely on specific unfolding behavior with simp [imageFinset].

For new code: Use PermFinset.imageFinset and PermFinset.permsMapping directly.

def AlgebraicCombinatorics.CauchyBinet.imageFinset {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) : Finset (Fin n)

The image of a finset under a permutation.

This is definitionally equal to PermFinset.imageFinset (see imageFinset_eq_permFinset). New code should prefer PermFinset.imageFinset.

Equations

• AlgebraicCombinatorics.CauchyBinet.imageFinset σ P = Finset.map { toFun := ⇑σ, inj' := ⋯ } P

theorem AlgebraicCombinatorics.CauchyBinet.imageFinset_card {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) : (imageFinset σ P).card = P.card

The image has the same cardinality as the original set. See also PermFinset.imageFinset_card.

theorem AlgebraicCombinatorics.CauchyBinet.imageFinset_compl {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) : imageFinset σ Pᶜ = (imageFinset σ P)ᶜ

The image of a complement equals the complement of the image. See also PermFinset.imageFinset_compl.

def AlgebraicCombinatorics.CauchyBinet.permsMapping {n : ℕ} (P Q : Finset (Fin n)) : Finset (Equiv.Perm (Fin n))

The set of permutations that map P to Q.

This is definitionally equal to PermFinset.permsMapping (see permsMapping_eq_permFinset). New code should prefer PermFinset.permsMapping.

Equations

• AlgebraicCombinatorics.CauchyBinet.permsMapping P Q = {σ : Equiv.Perm (Fin n) | AlgebraicCombinatorics.CauchyBinet.imageFinset σ P = Q}

theorem AlgebraicCombinatorics.CauchyBinet.permsMapping_empty_of_card_ne {n : ℕ} (P Q : Finset (Fin n)) (h : P.card ≠ Q.card) : permsMapping P Q = ∅

If |P| ≠ |Q|, no permutation maps P to Q. See also PermFinset.permsMapping_empty_of_card_ne.

theorem AlgebraicCombinatorics.CauchyBinet.imageFinset_eq_permFinset {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) : imageFinset σ P = PermFinset.imageFinset σ P

imageFinset is definitionally equal to PermFinset.imageFinset.

theorem AlgebraicCombinatorics.CauchyBinet.permsMapping_eq_permFinset {n : ℕ} (P Q : Finset (Fin n)) : permsMapping P Q = PermFinset.permsMapping P Q

permsMapping is definitionally equal to PermFinset.permsMapping.

theorem AlgebraicCombinatorics.CauchyBinet.det_add_expand_step1 {R : Type u_1} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : (A + B).det = ∑ σ : Equiv.Perm (Fin n), Equiv.Perm.sign σ • ∑ P : Finset (Fin n), (∏ i ∈ P, A (σ i) i) * ∏ i ∈ Pᶜ, B (σ i) i

First step: expand det(A+B) using the Leibniz formula and product rule.

This expands det(A+B) = ∑σ sign(σ) ∏i (A + B){σ(i),i} into ∑σ sign(σ) ∑P (∏{i∈P} A{σ(i),i}) · (∏{i∈Pᶜ} B_{σ(i),i}) using the product rule for (a + b).

theorem AlgebraicCombinatorics.CauchyBinet.det_add_expand_step2 {R : Type u_1} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : (A + B).det = ∑ P : Finset (Fin n), ∑ σ : Equiv.Perm (Fin n), Equiv.Perm.sign σ • ((∏ i ∈ P, A (σ i) i) * ∏ i ∈ Pᶜ, B (σ i) i)

Second step: swap the order of summation over σ and P.

theorem AlgebraicCombinatorics.CauchyBinet.det_add_expand_step3 {R : Type u_1} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : (A + B).det = ∑ P : Finset (Fin n), ∑ Q : Finset (Fin n), ∑ σ ∈ permsMapping P Q, Equiv.Perm.sign σ • ((∏ i ∈ P, A (σ i) i) * ∏ i ∈ Pᶜ, B (σ i) i)

Third step: partition the sum over σ based on σ(P) = Q.

theorem AlgebraicCombinatorics.CauchyBinet.det_add_fin_two {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : (A + B).det = A.det + B.det + A 0 0 * B 1 1 + A 1 1 * B 0 0 - A 0 1 * B 1 0 - A 1 0 * B 0 1

The n=2 case of det(A+B) formula, expanded explicitly. This serves as a sanity check for the general formula.

Helper lemmas for the key factorization

The proof of sum_perms_mapping_eq_det_product requires:

1. A bijection between {σ : σ(P) = Q} and Perm(Fin |P|) × Perm(Fin |Pᶜ|)
2. A sign identity: sign(σ) = (-1)^(sum P + sum Q) · sign(α) · sign(β)
3. Product factorization into determinants

We build these up step by step.

theorem AlgebraicCombinatorics.CauchyBinet.sigma_orderEmb_mem_of_imageFinset {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin P.card) : σ ((P.orderEmbOfFin ⋯) i) ∈ Q

For σ with σ(P) = Q, the image of any element of P under σ lies in Q.

theorem AlgebraicCombinatorics.CauchyBinet.sigma_orderEmb_compl_mem_of_imageFinset {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin Pᶜ.card) : σ ((Pᶜ.orderEmbOfFin ⋯) i) ∈ Qᶜ

For σ with σ(P) = Q, the image of any element of Pᶜ under σ lies in Qᶜ.

noncomputable def AlgebraicCombinatorics.CauchyBinet.extractAlpha {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : Equiv.Perm (Fin P.card)

Extract α from σ: For σ with σ(P) = Q, extract the permutation α ∈ Perm(Fin |P|) that describes how σ permutes the elements of P.

Specifically, if p₁ < p₂ < ... < pₖ are the elements of P and q₁ < q₂ < ... < qₖ are the elements of Q, then α is defined by σ(pᵢ) = q_{α(i)}.

Equations

• AlgebraicCombinatorics.CauchyBinet.extractAlpha P Q hcard σ hσ = Equiv.ofBijective (fun (i : Fin P.card) => (Q.orderIsoOfFin ⋯).symm ⟨σ ((P.orderEmbOfFin ⋯) i), ⋯⟩) ⋯

noncomputable def AlgebraicCombinatorics.CauchyBinet.extractBeta {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : Equiv.Perm (Fin Pᶜ.card)

Extract β from σ: For σ with σ(P) = Q, extract the permutation β ∈ Perm(Fin |Pᶜ|) that describes how σ permutes the elements of Pᶜ.

Equations

• AlgebraicCombinatorics.CauchyBinet.extractBeta P Q hcard σ hσ = Equiv.ofBijective (fun (i : Fin Pᶜ.card) => (Qᶜ.orderIsoOfFin ⋯).symm ⟨σ ((Pᶜ.orderEmbOfFin ⋯) i), ⋯⟩) ⋯

Helper lemmas for empty set case in sign_decomposition

noncomputable def AlgebraicCombinatorics.CauchyBinet.constructSigma {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (α : Equiv.Perm (Fin P.card)) (β : Equiv.Perm (Fin Pᶜ.card)) : Equiv.Perm (Fin n)

Given α ∈ Perm(Fin |P|) and β ∈ Perm(Fin |Pᶜ|), construct σ ∈ Perm(Fin n) with σ(P) = Q. This is the inverse of the (extractAlpha, extractBeta) bijection.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.CauchyBinet.constructSigma_imageFinset {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (α : Equiv.Perm (Fin P.card)) (β : Equiv.Perm (Fin Pᶜ.card)) : imageFinset (constructSigma P Q hcard α β) P = Q

The constructed permutation maps P to Q.

theorem AlgebraicCombinatorics.CauchyBinet.constructSigma_mem_permsMapping {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (α : Equiv.Perm (Fin P.card)) (β : Equiv.Perm (Fin Pᶜ.card)) : constructSigma P Q hcard α β ∈ permsMapping P Q

The constructed permutation is in permsMapping P Q.

Base case lemmas for sign decomposition using subtypePerm

When P = Q = {0, 1, ..., k-1} (the first k elements), the sign identity simplifies because inversions split cleanly into three categories:

1. Inversions within P (counted by α)
2. Inversions within Pᶜ (counted by β)
3. Inversions between P and Pᶜ (which are zero because σ preserves both sets)

We formalize this using Mathlib's sign_subtypeCongr lemma and Equiv.Perm.subtypePerm.

def AlgebraicCombinatorics.CauchyBinet.ltPred (n k : ℕ) : Fin n → Prop

Predicate for "i.val < k" used to partition Fin n.

Equations

• AlgebraicCombinatorics.CauchyBinet.ltPred n k i = (↑i < k)

instance AlgebraicCombinatorics.CauchyBinet.instDecidablePredLtPred (n k : ℕ) : DecidablePred (ltPred n k)

Equations

• AlgebraicCombinatorics.CauchyBinet.instDecidablePredLtPred n k i = (↑i).decLt k

def AlgebraicCombinatorics.CauchyBinet.preservesPrefix {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) : Prop

A permutation "preserves [k]" if it maps elements with index < k to elements with index < k.

Equations

• AlgebraicCombinatorics.CauchyBinet.preservesPrefix σ k = ∀ (i : Fin n), ↑i < k ↔ ↑(σ i) < k

noncomputable def AlgebraicCombinatorics.CauchyBinet.restrictToLt {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hσ : preservesPrefix σ k) : Equiv.Perm { i : Fin n // ltPred n k i }

Restriction of a permutation to {i | i.val < k} using Mathlib's subtypePerm.

Equations

• AlgebraicCombinatorics.CauchyBinet.restrictToLt σ k hσ = σ.subtypePerm ⋯

noncomputable def AlgebraicCombinatorics.CauchyBinet.restrictToGe {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hσ : preservesPrefix σ k) : Equiv.Perm { i : Fin n // ¬ltPred n k i }

Restriction of a permutation to {i | i.val ≥ k} using Mathlib's subtypePerm.

Equations

• AlgebraicCombinatorics.CauchyBinet.restrictToGe σ k hσ = σ.subtypePerm ⋯

theorem AlgebraicCombinatorics.CauchyBinet.eq_subtypeCongr_of_preservesPrefix {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hσ : preservesPrefix σ k) : σ = (restrictToLt σ k hσ).subtypeCongr (restrictToGe σ k hσ)

A permutation that preserves [k] equals the subtypeCongr of its restrictions.

theorem AlgebraicCombinatorics.CauchyBinet.sign_split_preservesPrefix {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hσ : preservesPrefix σ k) : Equiv.Perm.sign σ = Equiv.Perm.sign (restrictToLt σ k hσ) * Equiv.Perm.sign (restrictToGe σ k hσ)

Base case: When σ preserves [k], sign(σ) = sign(α) * sign(β) where α, β are restrictions. This follows from Mathlib's sign_subtypeCongr.

def AlgebraicCombinatorics.CauchyBinet.prefixFinset (n k : ℕ) (_hk : k ≤ n) : Finset (Fin n)

The finset {0, 1, ..., k-1} ⊆ Fin n.

Equations

• AlgebraicCombinatorics.CauchyBinet.prefixFinset n k _hk = {i : Fin n | ↑i < k}

theorem AlgebraicCombinatorics.CauchyBinet.mem_prefixFinset_iff {n k : ℕ} (hk : k ≤ n) (i : Fin n) : i ∈ prefixFinset n k hk ↔ ↑i < k

theorem AlgebraicCombinatorics.CauchyBinet.prefixFinset_card (n k : ℕ) (hk : k ≤ n) : (prefixFinset n k hk).card = k

theorem AlgebraicCombinatorics.CauchyBinet.finsetSumFin_prefixFinset (n k : ℕ) (hk : k ≤ n) : finsetSumFin (prefixFinset n k hk) = k * (k - 1) / 2

Sum of 0 + 1 + ... + (k-1) = k(k-1)/2

theorem AlgebraicCombinatorics.CauchyBinet.prefixFinset_orderEmbOfFin_eq {n k : ℕ} (hk : k ≤ n) (j : Fin k) : ((prefixFinset n k hk).orderEmbOfFin ⋯) j = ⟨↑j, ⋯⟩

The j-th element of prefixFinset (in sorted order) is just j. This is because prefixFinset = {0, 1, ..., k-1} is already sorted.

theorem AlgebraicCombinatorics.CauchyBinet.prefixFinset_orderIsoOfFin_symm {n k : ℕ} (hk : k ≤ n) (x : ↥(prefixFinset n k hk)) : ((prefixFinset n k hk).orderIsoOfFin ⋯).symm x = ⟨↑↑x, ⋯⟩

The inverse of orderIsoOfFin for prefixFinset extracts the value. Since prefixFinset = {0, 1, ..., k-1}, the index of element x is just x.val.

theorem AlgebraicCombinatorics.CauchyBinet.prefixFinset_compl_orderEmbOfFin_eq {n k : ℕ} (hk : k ≤ n) (j : Fin (n - k)) : let P := prefixFinset n k hk; have hcard := ⋯; (Pᶜ.orderEmbOfFin hcard) j = ⟨k + ↑j, ⋯⟩

The j-th element of prefixFinset^c (in sorted order) is k + j. Since prefixFinset^c = {k, k+1, ..., n-1}, the elements in sorted order are k, k+1, etc.

theorem AlgebraicCombinatorics.CauchyBinet.prefixFinset_compl_orderIsoOfFin_symm {n k : ℕ} (hk : k ≤ n) (x : ↥(prefixFinset n k hk)ᶜ) : let P := prefixFinset n k hk; have hcard := ⋯; ↑((Pᶜ.orderIsoOfFin hcard).symm x) = ↑↑x - k

The inverse of orderIsoOfFin for prefixFinset^c extracts the value minus k. Since prefixFinset^c = {k, k+1, ..., n-1}, the index of element x is x.val - k.

theorem AlgebraicCombinatorics.CauchyBinet.preservesPrefix_of_imageFinset_prefix {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) : preservesPrefix σ k

When P = Q = prefixFinset n k hk, and σ(P) = Q, then σ preserves the prefix.

theorem AlgebraicCombinatorics.CauchyBinet.finsetSumFin_swap_of_left_shift {n : ℕ} (P : Finset (Fin n)) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : finsetSumFin (imageFinset (Equiv.swap i ⟨↑i + 1, hi⟩) P) = finsetSumFin P - 1

A "left shift" replaces P with s_i(P) where i ∉ P and i+1 ∈ P. This decrements finsetSumFin P by 1.

theorem AlgebraicCombinatorics.CauchyBinet.sign_mul_swap {n : ℕ} (σ : Equiv.Perm (Fin n)) (i j : Fin n) (hij : i ≠ j) : Equiv.Perm.sign (σ * Equiv.swap i j) = -Equiv.Perm.sign σ

Key lemma: When σ(P) = Q and we multiply σ by a transposition, the sign flips.

theorem AlgebraicCombinatorics.CauchyBinet.sign_swap_mul {n : ℕ} (σ : Equiv.Perm (Fin n)) (i j : Fin n) (hij : i ≠ j) : Equiv.Perm.sign (Equiv.swap i j * σ) = -Equiv.Perm.sign σ

The sign of s_i · σ also flips

theorem AlgebraicCombinatorics.CauchyBinet.leftShift_preserves_combined_sign {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : have P' := imageFinset (Equiv.swap i ⟨↑i + 1, hi⟩) P; have σ' := σ * Equiv.swap i ⟨↑i + 1, hi⟩; have Q' := imageFinset σ' P'; (-1) ^ (finsetSumFin P' + finsetSumFin Q') * ↑(Equiv.Perm.sign σ') = (-1) ^ (finsetSumFin P + finsetSumFin Q) * ↑(Equiv.Perm.sign σ)

Left shift preserves the combined sign factor.

When we replace σ by σ * swap i (i+1) and P by (swap i (i+1))(P), the product (-1)^(finsetSumFin P + finsetSumFin Q) * sign(σ) is preserved, provided i ∉ P and i+1 ∈ P (so finsetSumFin decreases by 1).

This is the key invariant for the shift reduction in the proof of sign_decomposition.

theorem AlgebraicCombinatorics.CauchyBinet.leftCoShift_preserves_combined_sign {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (_hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notQ : i ∉ Q) (hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) : have Q' := imageFinset (Equiv.swap i ⟨↑i + 1, hi⟩) Q; have σ' := Equiv.swap i ⟨↑i + 1, hi⟩ * σ; (-1) ^ (finsetSumFin P + finsetSumFin Q') * ↑(Equiv.Perm.sign σ') = (-1) ^ (finsetSumFin P + finsetSumFin Q) * ↑(Equiv.Perm.sign σ)

Left co-shift preserves the combined sign factor.

When we replace σ by (swap i (i+1)) * σ and Q by (swap i (i+1))(Q), the product (-1)^(finsetSumFin P + finsetSumFin Q) * sign(σ) is preserved, provided i ∉ Q and i+1 ∈ Q (so finsetSumFin Q decreases by 1).

This is the key invariant for the co-shift reduction in the proof of sign_decomposition.

theorem AlgebraicCombinatorics.CauchyBinet.even_mul_pred (k : ℕ) : Even (k * (k - 1))

k * (k - 1) is always even (consecutive integers).

theorem AlgebraicCombinatorics.CauchyBinet.two_dvd_mul_pred (k : ℕ) : 2 ∣ k * (k - 1)

2 divides k * (k - 1).

theorem AlgebraicCombinatorics.CauchyBinet.orderEmbOfFin_idxOf_eq {α : Type u_2} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : List.idxOf ((s.orderEmbOfFin h) i) (s.sort fun (x1 x2 : α) => x1 ≤ x2) = ↑i

Helper lemma: the index of orderEmbOfFin i in the sorted list is i.val.

theorem AlgebraicCombinatorics.CauchyBinet.swap_preserves_position {n k : ℕ} (Q : Finset (Fin n)) (hQ_card : Q.card = k) (i : Fin n) (hi : ↑i + 1 < n) (hi_notQ : i ∉ Q) (_hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) (j : Fin k) : have s := Equiv.swap i ⟨↑i + 1, hi⟩; let Q' := Finset.map { toFun := ⇑s, inj' := ⋯ } Q; have hQ'_card := ⋯; s ((Q.orderEmbOfFin hQ_card) j) = (Q'.orderEmbOfFin hQ'_card) j

Key lemma for co-shifts: when we swap i and i+1 in Q (where i ∉ Q, i+1 ∈ Q), the swap preserves the sorted order within Q.

More precisely: s(Q.orderEmbOfFin j) = Q'.orderEmbOfFin j where Q' = s(Q). This is because s swaps i and i+1, and i replaces i+1 at the same position in the sorted order.

theorem AlgebraicCombinatorics.CauchyBinet.position_preserved_under_swap {n k : ℕ} (Q : Finset (Fin n)) (hQ_card : Q.card = k) (s : Equiv.Perm (Fin n)) (Q' : Finset (Fin n)) (hQ'_card : Q'.card = k) (h_swap : ∀ (j : Fin k), s ((Q.orderEmbOfFin hQ_card) j) = (Q'.orderEmbOfFin hQ'_card) j) (x : Fin n) (hx : x ∈ Q) (hsx : s x ∈ Q') : (Q'.orderIsoOfFin hQ'_card).symm ⟨s x, hsx⟩ = (Q.orderIsoOfFin hQ_card).symm ⟨x, hx⟩

Positions are preserved under a permutation that preserves sorted order. If s(Q.orderEmbOfFin j) = Q'.orderEmbOfFin j for all j, then the position of s(x) in Q' equals the position of x in Q for all x ∈ Q.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_val_eq_of_coshift {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (s : Equiv.Perm (Fin n)) (Q' : Finset (Fin n)) (hQ'_card : Q'.card = Q.card) (hcard' : P.card = Q'.card) (σ' : Equiv.Perm (Fin n)) (hσ' : imageFinset σ' P = Q') (h_σ'_eq : ∀ (j : Fin P.card), σ' ((P.orderEmbOfFin ⋯) j) = s (σ ((P.orderEmbOfFin ⋯) j))) (h_swap : ∀ (j : Fin Q.card), s ((Q.orderEmbOfFin ⋯) j) = (Q'.orderEmbOfFin hQ'_card) j) (j : Fin P.card) : ↑((extractAlpha P Q' hcard' σ' hσ') j) = ↑((extractAlpha P Q hcard σ hσ) j)

Key lemma: extractAlpha values are equal under co-shift. If σ' = s * σ and Q' = s(Q), then extractAlpha P Q' σ' j = extractAlpha P Q σ j (as values).

theorem AlgebraicCombinatorics.CauchyBinet.neg_one_pow_double_sum_prefix (n k : ℕ) (hk : k ≤ n) : (-1) ^ (finsetSumFin (prefixFinset n k hk) + finsetSumFin (prefixFinset n k hk)) = 1

When P = Q = prefixFinset n k hk, the sign factor (-1)^(sum P + sum Q) = 1. This is because sum P = sum Q = k(k-1)/2, so the exponent is k(k-1), which is even.

theorem AlgebraicCombinatorics.CauchyBinet.orderEmbOfFin_val_ge {n k : ℕ} (P : Finset (Fin n)) (hcard : P.card = k) (j : Fin k) : ↑j ≤ ↑((P.orderEmbOfFin hcard) j)

The j-th element of a k-element subset (in sorted order) has value ≥ j. This is because if we list the elements as p₀ < p₁ < ... < p_{k-1}, then pᵢ ≥ i for all i (since there are at least i elements below pᵢ).

theorem AlgebraicCombinatorics.CauchyBinet.exists_left_shift_witness {n k : ℕ} (hk : k ≤ n) (P : Finset (Fin n)) (hcard : P.card = k) (hne : P ≠ prefixFinset n k hk) : ∃ (i : Fin n) (hi : ↑i + 1 < n), i ∉ P ∧ ⟨↑i + 1, hi⟩ ∈ P

Key lemma for the left shift induction: if P ≠ prefixFinset, there exists i ∉ P with i+1 ∈ P. This allows us to apply a transposition to reduce finsetSumFin P while preserving the cardinality.

theorem AlgebraicCombinatorics.CauchyBinet.finsetSumFin_ge_prefixFinset {n k : ℕ} (hk : k ≤ n) (P : Finset (Fin n)) (hcard : P.card = k) : finsetSumFin P ≥ finsetSumFin (prefixFinset n k hk)

The minimum sum for a k-element subset of Fin n is achieved by prefixFinset. This is because prefixFinset = {0, 1, ..., k-1} has sum 0+1+...+(k-1) = k(k-1)/2, and any other k-element subset must have at least one element ≥ k, giving a larger sum.

theorem AlgebraicCombinatorics.CauchyBinet.exists_shift_opportunity {n k : ℕ} (hk : k ≤ n) (hk_pos : 0 < k) (_hn : k < n) (P : Finset (Fin n)) (hcard : P.card = k) (hne : P ≠ prefixFinset n k hk) : ∃ (i : Fin n) (hi : ↑i + 1 < n), i ∉ P ∧ ⟨↑i + 1, hi⟩ ∈ P

If P has card k and P ≠ prefixFinset, then there's a shift opportunity: some i with i ∉ P and i+1 ∈ P. This is because P has a "gap" that can be shifted.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_prefixFinset_val {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) (j : Fin (prefixFinset n k hk).card) : ↑((extractAlpha (prefixFinset n k hk) (prefixFinset n k hk) ⋯ σ hσ) j) = ↑(σ (((prefixFinset n k hk).orderEmbOfFin ⋯) j))

When P = Q = prefixFinset, extractAlpha(j).val = (σ(orderEmbOfFin j)).val. This shows that extractAlpha just extracts the value of σ on the prefix.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_prefixFinset_val {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) (j : Fin (prefixFinset n k hk)ᶜ.card) : ↑((extractBeta (prefixFinset n k hk) (prefixFinset n k hk) ⋯ σ hσ) j) = ↑(σ (((prefixFinset n k hk)ᶜ.orderEmbOfFin ⋯) j)) - k

For prefixFinset^c, extractBeta j gives the position of σ(Pᶜ.orderEmbOfFin j) in Pᶜ. Since Pᶜ = {k, ..., n-1}, this equals (σ(k+j)).val - k.

noncomputable def AlgebraicCombinatorics.CauchyBinet.finEquivSubtypeLt (n k : ℕ) (hk : k ≤ n) : Fin k ≃ { i : Fin n // ltPred n k i }

Equivalence between Fin k and the subtype {i : Fin n // i.val < k}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicCombinatorics.CauchyBinet.finEquivSubtypeGe (n k : ℕ) (hk : k ≤ n) : Fin (n - k) ≃ { i : Fin n // ¬ltPred n k i }

Equivalence between Fin (n-k) and the subtype {i : Fin n // ¬(i.val < k)}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicCombinatorics.CauchyBinet.restrictToLtAsFink {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : preservesPrefix σ k) : Equiv.Perm (Fin k)

Convert restrictToLt to a permutation on Fin k using finEquivSubtypeLt.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicCombinatorics.CauchyBinet.restrictToGeAsFinNK {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : preservesPrefix σ k) : Equiv.Perm (Fin (n - k))

Convert restrictToGe to a permutation on Fin (n-k) using finEquivSubtypeGe.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.CauchyBinet.sign_restrictToLt_eq_sign_restrictToLtAsFink {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : preservesPrefix σ k) : Equiv.Perm.sign (restrictToLt σ k hσ) = Equiv.Perm.sign (restrictToLtAsFink hk σ hσ)

Sign of restrictToLt equals sign of restrictToLtAsFink by sign_permCongr.

theorem AlgebraicCombinatorics.CauchyBinet.sign_restrictToGe_eq_sign_restrictToGeAsFinNK {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : preservesPrefix σ k) : Equiv.Perm.sign (restrictToGe σ k hσ) = Equiv.Perm.sign (restrictToGeAsFinNK hk σ hσ)

Sign of restrictToGe equals sign of restrictToGeAsFinNK by sign_permCongr.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_cast_apply_val {n : ℕ} (P : Finset (Fin n)) (k : ℕ) (hcard : P.card = k) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = P) (j : Fin k) : ↑((hcard ▸ extractAlpha P P ⋯ σ hσ) j) = ↑((extractAlpha P P ⋯ σ hσ) ⟨↑j, ⋯⟩)

Auxiliary lemma: casting extractAlpha and applying to j gives the same value as applying extractAlpha to the corresponding element.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_cast_apply_val {n : ℕ} (P : Finset (Fin n)) (m : ℕ) (hcard : Pᶜ.card = m) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = P) (j : Fin m) : ↑((hcard ▸ extractBeta P P ⋯ σ hσ) j) = ↑((extractBeta P P ⋯ σ hσ) ⟨↑j, ⋯⟩)

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_eq_restrictToLtAsFink_at_prefix {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) (hpres : preservesPrefix σ k) : let P := prefixFinset n k hk; have hcard_eq := ⋯; hcard_eq ▸ extractAlpha P P ⋯ σ hσ = restrictToLtAsFink hk σ hpres

At the base case (P = Q = prefixFinset), extractAlpha equals restrictToLtAsFink. This is because both permutations act the same way: for j : Fin k,

• extractAlpha j = position of σ(j) in prefixFinset = (σ ⟨j, _⟩).val
• restrictToLtAsFink j = (σ ⟨j, _⟩).val

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_eq_restrictToGeAsFinNK_at_prefix {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) (hpres : preservesPrefix σ k) : let P := prefixFinset n k hk; have hcard_compl := ⋯; hcard_compl ▸ extractBeta P P ⋯ σ hσ = restrictToGeAsFinNK hk σ hpres

At the base case (P = Q = prefixFinset), extractBeta equals restrictToGeAsFinNK. Similar to extractAlpha_eq_restrictToLtAsFink_at_prefix but for the complement.

theorem AlgebraicCombinatorics.CauchyBinet.sign_eq_of_cast_eq {m n : ℕ} (h : m = n) (α : Equiv.Perm (Fin m)) (β : Equiv.Perm (Fin n)) (heq : h ▸ α = β) : Equiv.Perm.sign α = Equiv.Perm.sign β

Helper lemma: sign is preserved under casting between Fin types.

theorem AlgebraicCombinatorics.CauchyBinet.sign_decomposition_prefix {n k : ℕ} (hk : k ≤ n) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ (prefixFinset n k hk) = prefixFinset n k hk) : let P := prefixFinset n k hk; ↑(Equiv.Perm.sign σ) = (-1) ^ (finsetSumFin P + finsetSumFin P) * ↑(Equiv.Perm.sign (extractAlpha P P ⋯ σ hσ)) * ↑(Equiv.Perm.sign (extractBeta P P ⋯ σ hσ))

Base case of sign_decomposition: when P = Q = prefixFinset n k hk.

theorem AlgebraicCombinatorics.CauchyBinet.imageFinset_leftShift_eq {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (_hi_notP : i ∉ P) (_hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : have s := Equiv.swap i ⟨↑i + 1, hi⟩; have P' := imageFinset s P; have σ' := σ * s; imageFinset σ' P' = Q

Key lemma: After a left shift, Q' = Q (the image is preserved).

When we apply swap(i, i+1) to P (where i ∉ P, i+1 ∈ P) and compose σ with swap, the image σ'(P') equals the original image Q.

This is because:

• For p ∈ P with p ≠ i+1: swap(p) = p, so σ'(swap(p)) = σ(swap(swap(p))) = σ(p)
• For p = i+1: swap(i+1) = i, so σ'(i) = σ(swap(i)) = σ(i+1)

Thus the multiset of images is unchanged.

theorem AlgebraicCombinatorics.CauchyBinet.perm_cast_apply_val {m n : ℕ} (h : m = n) (α : Equiv.Perm (Fin m)) (j : Fin n) : ↑((h ▸ α) j) = ↑(α ⟨↑j, ⋯⟩)

Helper lemma for casting permutations: the value of a cast permutation applied to j equals the original permutation applied to the corresponding element.

theorem AlgebraicCombinatorics.CauchyBinet.swap_orderEmbOfFin_eq {n : ℕ} (P : Finset (Fin n)) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (_hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : have s := Equiv.swap i ⟨↑i + 1, hi⟩; let P' := Finset.map { toFun := ⇑s, inj' := ⋯ } P; ∀ (j : Fin P.card), (P'.orderEmbOfFin ⋯) j = s ((P.orderEmbOfFin ⋯) j)

Key lemma: when P' = s(P) for a swap s = swap(i, i+1) with i ∉ P and i+1 ∈ P, the sorted order of P' is s applied to the sorted order of P.

This is because s swaps adjacent elements i < i+1, and since i ∉ P but i+1 ∈ P, replacing i+1 with i preserves the relative order of all elements.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_leftShift_eq {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let P' := imageFinset s P; let σ' := σ * s; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign (extractAlpha P' Q hcard' σ' hσ')) = ↑(Equiv.Perm.sign (extractAlpha P Q hcard σ hσ))

Key insight: extractAlpha is preserved under left shifts.

When we apply a left shift:

• P' = swap(P) where i ∉ P and i+1 ∈ P (so P' has i instead of i+1)
• σ' = σ * swap
• Q' = Q (unchanged, by imageFinset_leftShift_eq)

The extractAlpha permutation describes the bijection from sorted P to sorted Q via σ. After the shift, the same bijection exists from sorted P' to sorted Q via σ'.

The key observation is that for each position j in the sorted order:

• If P_j ≠ i+1: P'_j' = P_j for some j', and σ'(P'_j') = σ(P_j)
• If P_j = i+1: P'_j' = i, and σ'(i) = σ(swap(i)) = σ(i+1) = σ(P_j)

Since the images are the same, extractAlpha' = extractAlpha.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_leftShift_eq {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let P' := imageFinset s P; let σ' := σ * s; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign (extractBeta P' Q hcard' σ' hσ')) = ↑(Equiv.Perm.sign (extractBeta P Q hcard σ hσ))

Key insight: extractBeta is also preserved under left shifts.

Similar reasoning to extractAlpha: the complement P'ᶜ has the same structure as Pᶜ (with i and i+1 swapped), and the bijection from sorted P'ᶜ to sorted Qᶜ via σ' is the same as from sorted Pᶜ to sorted Qᶜ via σ.

theorem AlgebraicCombinatorics.CauchyBinet.sign_decomposition_leftShift_invariant {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notP : i ∉ P) (hiplus_P : ⟨↑i + 1, hi⟩ ∈ P) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let P' := imageFinset s P; let σ' := σ * s; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign σ') = (-1) ^ (finsetSumFin P' + finsetSumFin Q) * ↑(Equiv.Perm.sign (extractAlpha P' Q hcard' σ' hσ')) * ↑(Equiv.Perm.sign (extractBeta P' Q hcard' σ' hσ')) → ↑(Equiv.Perm.sign σ) = (-1) ^ (finsetSumFin P + finsetSumFin Q) * ↑(Equiv.Perm.sign (extractAlpha P Q hcard σ hσ)) * ↑(Equiv.Perm.sign (extractBeta P Q hcard σ hσ))

The sign decomposition formula is preserved under left shifts.

This combines:

1. leftShift_preserves_combined_sign: (-1)^(sum P + sum Q) * sign(σ) is preserved
2. extractAlpha_leftShift_eq: sign(extractAlpha) is preserved
3. extractBeta_leftShift_eq: sign(extractBeta) is preserved

Together, these show that if the formula holds for (P', Q, σ'), it holds for (P, Q, σ).

theorem AlgebraicCombinatorics.CauchyBinet.imageFinset_leftCoShift_eq {n : ℕ} (P Q : Finset (Fin n)) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (_hi_notQ : i ∉ Q) (_hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) : have s := Equiv.swap i ⟨↑i + 1, hi⟩; have Q' := imageFinset s Q; have σ' := s * σ; imageFinset σ' P = Q'

Left co-shift: when σ' = s * σ and Q' = s(Q), we have σ'(P) = Q'.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_leftCoShift_eq {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notQ : i ∉ Q) (hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let Q' := imageFinset s Q; let σ' := s * σ; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign (extractAlpha P Q' hcard' σ' hσ')) = ↑(Equiv.Perm.sign (extractAlpha P Q hcard σ hσ))

Key insight: extractAlpha is preserved under left co-shifts.

When we apply a left co-shift:

• P stays the same
• Q' = swap(Q) where i ∉ Q and i+1 ∈ Q (so Q' has i instead of i+1)
• σ' = swap * σ

The key observation is that swap_preserves_position shows: s(Q.orderEmbOfFin j) = Q'.orderEmbOfFin j

Since σ'(P.orderEmbOfFin j) = s(σ(P.orderEmbOfFin j)), and the position of s(x) in Q' equals the position of x in Q (for x ∈ Q), we have extractAlpha P Q' σ' = extractAlpha P Q σ.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_leftCoShift_eq {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notQ : i ∉ Q) (hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let Q' := imageFinset s Q; let σ' := s * σ; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign (extractBeta P Q' hcard' σ' hσ')) = ↑(Equiv.Perm.sign (extractBeta P Q hcard σ hσ))

Key insight: extractBeta is also preserved under left co-shifts.

Similar reasoning to extractAlpha: the complement Q'ᶜ has the same structure as Qᶜ (with i and i+1 swapped), and the bijection from sorted Pᶜ to sorted Q'ᶜ via σ' is the same as from sorted Pᶜ to sorted Qᶜ via σ.

theorem AlgebraicCombinatorics.CauchyBinet.sign_decomposition_leftCoShift_invariant {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (i : Fin n) (hi : ↑i + 1 < n) (hi_notQ : i ∉ Q) (hiplus_Q : ⟨↑i + 1, hi⟩ ∈ Q) : let s := Equiv.swap i ⟨↑i + 1, hi⟩; let Q' := imageFinset s Q; let σ' := s * σ; have hcard' := ⋯; have hσ' := ⋯; ↑(Equiv.Perm.sign σ') = (-1) ^ (finsetSumFin P + finsetSumFin Q') * ↑(Equiv.Perm.sign (extractAlpha P Q' hcard' σ' hσ')) * ↑(Equiv.Perm.sign (extractBeta P Q' hcard' σ' hσ')) → ↑(Equiv.Perm.sign σ) = (-1) ^ (finsetSumFin P + finsetSumFin Q) * ↑(Equiv.Perm.sign (extractAlpha P Q hcard σ hσ)) * ↑(Equiv.Perm.sign (extractBeta P Q hcard σ hσ))

The sign decomposition formula is preserved under left co-shifts.

This combines:

1. leftCoShift_preserves_combined_sign: (-1)^(sum P + sum Q) * sign(σ) is preserved
2. extractAlpha_leftCoShift_eq: sign(extractAlpha) is preserved
3. extractBeta_leftCoShift_eq: sign(extractBeta) is preserved

Together, these show that if the formula holds for (P, Q', σ'), it holds for (P, Q, σ).

theorem AlgebraicCombinatorics.CauchyBinet.sign_decomposition {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : ↑(Equiv.Perm.sign σ) = (-1) ^ (finsetSumFin P + finsetSumFin Q) * ↑(Equiv.Perm.sign (extractAlpha P Q hcard σ hσ)) * ↑(Equiv.Perm.sign (extractBeta P Q hcard σ hσ))

The sign decomposition theorem: for any σ with σ(P) = Q, sign(σ) = (-1)^(sum P + sum Q) * sign(extractAlpha) * sign(extractBeta).

This is proved by strong induction on finsetSumFin P + finsetSumFin Q.

• Base case: P = Q = prefixFinset (handled by sign_decomposition_prefix)
• Inductive case: Either P or Q can be shifted towards prefixFinset
  • If P ≠ prefixFinset: apply left shift (sign_decomposition_leftShift_invariant)
  • If P = prefixFinset but Q ≠ prefixFinset: apply co-shift (sign_decomposition_leftCoShift_invariant)

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_spec {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (j : Fin P.card) : σ ((P.orderEmbOfFin ⋯) j) = (Q.orderEmbOfFin ⋯) ((extractAlpha P Q hcard σ hσ) j)

The key property of extractAlpha: σ(pⱼ) = q_{α(j)} where pⱼ and qⱼ are the j-th elements of P and Q in sorted order.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_spec {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) (j : Fin Pᶜ.card) : σ ((Pᶜ.orderEmbOfFin ⋯) j) = (Qᶜ.orderEmbOfFin ⋯) ((extractBeta P Q hcard σ hσ) j)

The key property of extractBeta: σ(pᶜⱼ) = qᶜ_{β(j)} where pᶜⱼ and qᶜⱼ are the j-th elements of Pᶜ and Qᶜ in sorted order.

theorem AlgebraicCombinatorics.CauchyBinet.extractAlpha_constructSigma {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (α : Equiv.Perm (Fin P.card)) (β : Equiv.Perm (Fin Pᶜ.card)) (hσ : imageFinset (constructSigma P Q hcard α β) P = Q) : extractAlpha P Q hcard (constructSigma P Q hcard α β) hσ = α

Round-trip lemma: extractAlpha of constructSigma equals the original α.

theorem AlgebraicCombinatorics.CauchyBinet.extractBeta_constructSigma {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (α : Equiv.Perm (Fin P.card)) (β : Equiv.Perm (Fin Pᶜ.card)) (hσ : imageFinset (constructSigma P Q hcard α β) P = Q) : extractBeta P Q hcard (constructSigma P Q hcard α β) hσ = β

Round-trip lemma: extractBeta of constructSigma equals the original β.

theorem AlgebraicCombinatorics.CauchyBinet.constructSigma_extract {n : ℕ} (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : constructSigma P Q hcard (extractAlpha P Q hcard σ hσ) (extractBeta P Q hcard σ hσ) = σ

Round-trip lemma: constructSigma of (extractAlpha, extractBeta) equals the original σ. This is the other direction of the bijection, showing that extract ∘ construct = id.

theorem AlgebraicCombinatorics.CauchyBinet.prod_P_eq_submatrix_det {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : ∏ i ∈ P, A (σ i) i = ∏ j : Fin P.card, A ((Q.orderEmbOfFin ⋯) ((extractAlpha P Q hcard σ hσ) j)) ((P.orderEmbOfFin ⋯) j)

The product over P factors through the submatrix determinant. ∑{σ : σ(P)=Q} sign(σ) · ∏{i∈P} A_{σ(i),i} relates to det(sub_Q^P A).

theorem AlgebraicCombinatorics.CauchyBinet.prod_Pc_eq_submatrix_det {R : Type u_1} [CommRing R] {n : ℕ} (B : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (σ : Equiv.Perm (Fin n)) (hσ : imageFinset σ P = Q) : ∏ i ∈ Pᶜ, B (σ i) i = ∏ j : Fin Pᶜ.card, B ((Qᶜ.orderEmbOfFin ⋯) ((extractBeta P Q hcard σ hσ) j)) ((Pᶜ.orderEmbOfFin ⋯) j)

The product over Pᶜ factors through the submatrix determinant.

theorem AlgebraicCombinatorics.CauchyBinet.sum_perms_mapping_eq_det_product {R : Type u_1} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (hcard : P.card = Q.card) : ∑ σ ∈ permsMapping P Q, Equiv.Perm.sign σ • ((∏ i ∈ P, A (σ i) i) * ∏ i ∈ Pᶜ, B (σ i) i) = (-1) ^ (finsetSumFin P + finsetSumFin Q) * submatrixDet A Q P ⋯ * submatrixDet B Qᶜ Pᶜ ⋯

The key factorization lemma: For fixed P and Q with |P| = |Q|, the sum over permutations σ with σ(P) = Q factors into a product of determinants.

This is equation (pf.thm.det.det(A+B).sumPQ) from the tex source.

The proof involves:

1. A bijection σ ↦ (α_σ, β_σ) from {σ : σ(P) = Q} to S_{|P|} × S_{|Pᶜ|} where α_σ describes σ's action on P and β_σ describes σ's action on Pᶜ
2. The sign identity: (-1)^σ = (-1)^(sum P + sum Q) · (-1)^α · (-1)^β
3. Factoring the products and recognizing them as determinants

See the tex source (CauchyBinet.tex, proof of Theorem thm.det.det(A+B)) for details.

The sign identity proof (step 2) uses the following key insight from the tex source:

• Define "left shifts" that replace σ by σ·s_i and P by s_i(P)
• Each left shift decrements sum(P) by 1 and flips both (-1)^(sum P + sum Q) and (-1)^σ
• After sum(P) - (1+2+...+k) left shifts, P becomes [k]
• Similarly for Q via "left co-shifts"
• When P = Q = [k], the sign identity reduces to ℓ(σ) = ℓ(α) + ℓ(β) (inversion counting)

theorem AlgebraicCombinatorics.CauchyBinet.det_add_sum {R : Type u_1} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : (A + B).det = ∑ P : Finset (Fin n), ∑ Q : Finset (Fin n), if h : Q.card = P.card then (-1) ^ (finsetSumFin P + finsetSumFin Q) * submatrixDet A Q P h * submatrixDet B Qᶜ Pᶜ ⋯ else 0

The formula for det(A+B) as a double sum over subsets. (Theorem thm.det.det(A+B)) Label: thm.det.det(A+B)

This expands det(A+B) into terms involving submatrices of A and B. The formula contains det(A) and det(B) as special cases (when P=Q=[n] or P=Q=∅).

Note: The statement uses submatrixDet helper to handle the cardinality constraints.

The proof uses the following key steps (see det_add_expand_step1/2/3):

1. Expand using Leibniz formula: det(A+B) = ∑_σ sign(σ) ∏i (A+B){σ(i),i}
2. Apply product rule: ∏(a+b) = ∑P (∏{i∈P} a_i)(∏_{i∈Pᶜ} b_i)
3. Swap summation order and partition by Q = σ(P)
4. Apply sum_perms_mapping_eq_det_product for each (P, Q) pair

Minors of Diagonal Matrices (Lemma lem.det.minors-diag)

For a diagonal matrix D with entries d₁, d₂, ..., dₙ:

(a) det(sub_P^P D) = ∏_{i ∈ P} dᵢ (principal minors are products of diagonal entries) (b) If P ≠ Q with |P| = |Q|, then det(sub_P^Q D) = 0 (off-diagonal submatrices have zero det)

theorem AlgebraicCombinatorics.CauchyBinet.det_diagonal_submatrix_eq {R : Type u_1} [CommRing R] {n : ℕ} (d : Fin n → R) (P : Finset (Fin n)) : ((Matrix.diagonal d).submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det = ∏ i ∈ P, d i

Part (a): Principal minors of a diagonal matrix are products of diagonal entries. (Lemma lem.det.minors-diag (a)) Label: lem.det.minors-diag.a

theorem AlgebraicCombinatorics.CauchyBinet.det_diagonal_submatrix_off_diag {R : Type u_1} [CommRing R] {n : ℕ} (d : Fin n → R) (P Q : Finset (Fin n)) (hcard : P.card = Q.card) (hne : P ≠ Q) : ((Matrix.diagonal d).submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(Q.orderEmbOfFin ⋯)).det = 0

Part (b): Off-diagonal submatrices of a diagonal matrix have zero determinant. (Lemma lem.det.minors-diag (b)) Label: lem.det.minors-diag.b

Determinant of A + D (Theorem thm.det.det(A+D))

When B = D is diagonal with entries d₁, ..., dₙ, the formula for det(A+B) simplifies: det(A+D) = ∑{P ⊆ [n]} det(sub_P^P A) · ∏{i ∈ [n]\P} dᵢ

The cross terms vanish because det(sub_P̃^Q̃ D) = 0 when P ≠ Q.

theorem AlgebraicCombinatorics.CauchyBinet.det_add_diagonal {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (d : Fin n → R) : (A + Matrix.diagonal d).det = ∑ P : Finset (Fin n), (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det * ∏ i ∈ Pᶜ, d i

Simplified formula for det(A+D) when D is diagonal. (Theorem thm.det.det(A+D)) Label: thm.det.det(A+D)

This follows from det_add_sum by observing that off-diagonal submatrices of D have zero determinant.

Determinant of x + D (Proposition prop.det.x+ai)

For the matrix F with entries F_{i,j} = x + d_i [i=j], i.e., F = (x x ... x) (x x+d₂ ... x) (⋮ ⋮ ⋱ ⋮) (x x ... x+dₙ)

we have: det F = d₁d₂...dₙ + x ∑_{i=1}^n d₁d₂...d̂ᵢ...dₙ

where d̂ᵢ means "omit dᵢ".

This is useful in graph theory (e.g., Laplacian matrices).

def AlgebraicCombinatorics.CauchyBinet.constPlusDiagMatrix {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (d : Fin n → R) : Matrix (Fin n) (Fin n) R

The matrix with x on all entries except diagonal which has x + dᵢ. (Used in Proposition prop.det.x+ai)

Equations

• AlgebraicCombinatorics.CauchyBinet.constPlusDiagMatrix x d i j = x + if i = j then d i else 0

def AlgebraicCombinatorics.CauchyBinet.fixedPoints' {n : ℕ} (σ : Equiv.Perm (Fin n)) : Finset (Fin n)

The set of fixed points of a permutation.

Equations

• AlgebraicCombinatorics.CauchyBinet.fixedPoints' σ = {i : Fin n | σ i = i}

theorem AlgebraicCombinatorics.CauchyBinet.fixedPoints'_one {n : ℕ} : fixedPoints' 1 = Finset.univ

The identity permutation has all points fixed.

theorem AlgebraicCombinatorics.CauchyBinet.prod_constPlusDiagMatrix_perm {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (d : Fin n → R) (σ : Equiv.Perm (Fin n)) : ∏ i : Fin n, constPlusDiagMatrix x d (σ i) i = x ^ (n - (fixedPoints' σ).card) * ∏ i ∈ fixedPoints' σ, (x + d i)

Key lemma: the product for a permutation σ in the determinant expansion. For constPlusDiagMatrix, entry (σ(i), i) equals x + d_i if σ(i) = i, else x. So the product splits into x^{non-fixed} · ∏_{fixed} (x + d_i).

theorem AlgebraicCombinatorics.CauchyBinet.card_nonfixed_ne_one {n : ℕ} (σ : Equiv.Perm (Fin n)) : (Finset.univ \ fixedPoints' σ).card ≠ 1

A permutation cannot have exactly 1 non-fixed point. If σ(i) ≠ i, then σ(σ(i)) = i ≠ σ(i), so σ(i) is also non-fixed.

def AlgebraicCombinatorics.CauchyBinet.constMatrix {R : Type u_1} {n : ℕ} (x : R) : Matrix (Fin n) (Fin n) R

The constant x matrix (all entries equal to x).

Equations

• AlgebraicCombinatorics.CauchyBinet.constMatrix x x✝¹ x✝ = x

theorem AlgebraicCombinatorics.CauchyBinet.constPlusDiagMatrix_eq_add {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (d : Fin n → R) : constPlusDiagMatrix x d = constMatrix x + Matrix.diagonal d

constPlusDiagMatrix = constMatrix + diagonal d

theorem AlgebraicCombinatorics.CauchyBinet.det_submatrix_constMatrix_eq_zero {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (P : Finset (Fin n)) (hP : 2 ≤ P.card) : ((constMatrix x).submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det = 0

For a submatrix of a constant matrix, if the submatrix has size ≥ 2, its determinant is 0. This is because all rows are identical.

theorem AlgebraicCombinatorics.CauchyBinet.det_submatrix_constMatrix_singleton {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (P : Finset (Fin n)) (hP : P.card = 1) : ((constMatrix x).submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det = x

For a 1×1 constant matrix, the determinant is x.

theorem AlgebraicCombinatorics.CauchyBinet.det_submatrix_constMatrix_empty {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (P : Finset (Fin n)) (hP : P.card = 0) : ((constMatrix x).submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det = 1

For a 0×0 matrix, the determinant is 1.

theorem AlgebraicCombinatorics.CauchyBinet.det_const_add_diagonal {R : Type u_1} [CommRing R] {n : ℕ} (x : R) (d : Fin n → R) : (constPlusDiagMatrix x d).det = ∏ i : Fin n, d i + x * ∑ i : Fin n, ∏ j ∈ Finset.univ.erase i, d j

Determinant of the matrix with constant x plus diagonal d. (Proposition prop.det.x+ai) Label: prop.det.x+ai

det F = d₁d₂...dₙ + x ∑_{i=1}^n d₁...d̂ᵢ...dₙ

Proof: Write F = A + D where A is the constant x matrix and D = diagonal(d). By det_add_diagonal: det(A+D) = ∑P det(sub_P^P A) · ∏{i∈Pᶜ} d_i

For |P| ≥ 2: det(sub_P^P A) = 0 (constant matrix with identical rows) For |P| = 1, P = {i}: det(sub_P^P A) = x (1×1 matrix) For |P| = 0, P = ∅: det(sub_P^P A) = 1 (0×0 matrix)

So only the P = ∅ term and the P = {i} terms survive: det F = 1 · ∏_i d_i + ∑i x · ∏{j≠i} d_j = ∏_i d_i + x · ∑i ∏{j≠i} d_j

Characteristic Polynomial Coefficients (Proposition prop.det.charpol-explicit)

The characteristic polynomial of A is det(xI - A) (or det(A + xI) up to sign). Its coefficients are sums of principal minors:

det(A + xI) = ∑{k=0}^n (∑{P ⊆ [n], |P|=n-k} det(sub_P^P A)) · x^k

The coefficient of x^{n-k} is the sum of all k×k principal minors of A.

theorem AlgebraicCombinatorics.CauchyBinet.det_charPoly_coeff {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (x : R) : (A + x • 1).det = ∑ P : Finset (Fin n), (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det * x ^ (n - P.card)

The coefficient of x^k in det(A + xI) is a sum of principal minors (first form). (Proposition prop.det.charpol-explicit) Label: prop.det.charpol-explicit

This gives an explicit formula for the coefficients of the characteristic polynomial: det(A + xI) = ∑_{P ⊆ [n]} det(sub_P^P A) · x^{n-|P|}

See also det_charPoly_coeff' for the equivalent form grouped by powers of x.

theorem AlgebraicCombinatorics.CauchyBinet.det_charPoly_coeff' {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (x : R) : (A + x • 1).det = ∑ k ∈ Finset.range (n + 1), (∑ P : Finset (Fin n) with P.card = n - k, (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(P.orderEmbOfFin ⋯)).det) * x ^ k

The coefficient of x^k in det(A + xI) is the sum of principal minors of size (n-k). (Proposition prop.det.charpol-explicit, second form) Label: prop.det.charpol-explicit

This regroups the sum by powers of x: det(A + xI) = ∑{k=0}^n (∑{P ⊆ [n], |P|=n-k} det(sub_P^P A)) · x^k

This form makes explicit that the coefficient of x^k is the sum of all (n-k) × (n-k) principal minors of A. In particular:

• The coefficient of x^n is 1 (the only principal minor of size 0 is det(∅) = 1)
• The coefficient of x^{n-1} is Tr(A) (the sum of 1×1 principal minors)
• The constant term is det(A) (the only principal minor of size n)

Pascal Matrix Determinant (Proposition prop.det.pascal-LU)

The Pascal matrix P_n has entries P_{i,j} = C(i+j-2, i-1), i.e., P = (C(0,0) C(1,0) ... C(n-1,0)) (C(1,1) C(2,1) ... C(n,1)) (⋮ ⋮ ⋱ ⋮) (C(n-1,n-1) C(n,n-1) ... C(2n-2,n-1))

For n=4, this is: (1 1 1 1) (1 2 3 4) (1 3 6 10) (1 4 10 20)

The determinant is 1, which can be proven via LU decomposition.

def AlgebraicCombinatorics.CauchyBinet.pascalMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The Pascal matrix with entries C(i+j, i). (Proposition prop.det.pascal-LU)

Note: We use 0-indexing, so entry (i,j) is C(i+j, i).

Equations

• AlgebraicCombinatorics.CauchyBinet.pascalMatrix n i j = (↑i + ↑j).choose ↑i

@[simp]

theorem AlgebraicCombinatorics.CauchyBinet.pascalMatrix_apply (n : ℕ) (i j : Fin n) : pascalMatrix n i j = (↑i + ↑j).choose ↑i

def AlgebraicCombinatorics.CauchyBinet.pascalLowerTriangular (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The lower triangular factor L in the LU decomposition of the Pascal matrix. L_{i,k} = C(i, k)

Equations

• AlgebraicCombinatorics.CauchyBinet.pascalLowerTriangular n i k = (↑i).choose ↑k

@[simp]

theorem AlgebraicCombinatorics.CauchyBinet.pascalLowerTriangular_apply (n : ℕ) (i k : Fin n) : pascalLowerTriangular n i k = (↑i).choose ↑k

def AlgebraicCombinatorics.CauchyBinet.pascalUpperTriangular (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The upper triangular factor U in the LU decomposition of the Pascal matrix. U_{k,j} = C(j, k)

Equations

• AlgebraicCombinatorics.CauchyBinet.pascalUpperTriangular n k j = (↑j).choose ↑k

@[simp]

theorem AlgebraicCombinatorics.CauchyBinet.pascalUpperTriangular_apply (n : ℕ) (k j : Fin n) : pascalUpperTriangular n k j = (↑j).choose ↑k

theorem AlgebraicCombinatorics.CauchyBinet.pascal_eq_LU (n : ℕ) : ((pascalMatrix n).map fun (x : ℕ) => ↑x) = ((pascalLowerTriangular n).map fun (x : ℕ) => ↑x) * (pascalUpperTriangular n).map fun (x : ℕ) => ↑x

The Pascal matrix factors as L * U where L and U are lower and upper triangular. This is the LU decomposition of the Pascal matrix.

The proof uses Vandermonde's identity: C(i+j, i) = ∑_k C(i,k) * C(j,k).

theorem AlgebraicCombinatorics.CauchyBinet.pascalLowerTriangular_diag (n : ℕ) (i : Fin n) : pascalLowerTriangular n i i = 1

The lower triangular factor L has all diagonal entries equal to 1.

theorem AlgebraicCombinatorics.CauchyBinet.pascalUpperTriangular_diag (n : ℕ) (i : Fin n) : pascalUpperTriangular n i i = 1

The upper triangular factor U has all diagonal entries equal to 1.

theorem AlgebraicCombinatorics.CauchyBinet.pascalLowerTriangular_is_lower (n : ℕ) (i k : Fin n) (h : i < k) : pascalLowerTriangular n i k = 0

The lower triangular factor L is indeed lower triangular.

theorem AlgebraicCombinatorics.CauchyBinet.pascalUpperTriangular_is_upper (n : ℕ) (k j : Fin n) (h : k > j) : pascalUpperTriangular n k j = 0

The upper triangular factor U is indeed upper triangular.

theorem AlgebraicCombinatorics.CauchyBinet.det_pascalLowerTriangular (n : ℕ) : ((pascalLowerTriangular n).map fun (x : ℕ) => ↑x).det = 1

The determinant of the lower triangular factor is 1.

The proof uses that L is lower triangular with 1s on the diagonal, so its determinant is the product of diagonal entries, which is 1.

theorem AlgebraicCombinatorics.CauchyBinet.det_pascalUpperTriangular (n : ℕ) : ((pascalUpperTriangular n).map fun (x : ℕ) => ↑x).det = 1

The determinant of the upper triangular factor is 1.

The proof uses that U is upper triangular with 1s on the diagonal, so its determinant is the product of diagonal entries, which is 1.

theorem AlgebraicCombinatorics.CauchyBinet.det_pascal_matrix (n : ℕ) : ((pascalMatrix n).map fun (x : ℕ) => ↑x).det = 1

The Pascal matrix has determinant 1. (Proposition prop.det.pascal-LU) Label: prop.det.pascal-LU

This follows from the LU decomposition: det(P) = det(L) · det(U) = 1 · 1 = 1.

The proof strategy:

1. Factor P = L * U where L is lower triangular and U is upper triangular
2. Both L and U have 1s on the diagonal (since C(n,n) = 1)
3. Determinant of a triangular matrix is the product of diagonal entries
4. Therefore det(P) = det(L) * det(U) = 1 * 1 = 1

Additional Lemmas

Some auxiliary results used in the main theorems.

theorem AlgebraicCombinatorics.CauchyBinet.finset_compl_card {n : ℕ} (P : Finset (Fin n)) : Pᶜ.card = n - P.card

The complement of a finset has the expected cardinality.

theorem AlgebraicCombinatorics.CauchyBinet.finsetSumFin_add_compl {n : ℕ} (P : Finset (Fin n)) : finsetSumFin P + finsetSumFin Pᶜ = finsetSumFin Finset.univ

The sum of elements in a finset and its complement equals the sum of all elements.