Hook vanishing for Jacobi–Trudi determinants

If the complete homogeneous sequence attached to a scalar sequence t satisfies the alternating binomial recurrence of order p beyond degree q — the coefficient statement of (1 − X)^p · Σ h_n Xⁿ = polynomial of degree ≤ q — then the Schur specialisation diagramSchur λ t vanishes for every diagram λ containing the cell (p, q).

Route: a unipotent column operation turns each column ≥ p of the Jacobi–Trudi matrix into the recurrence sums; in the first p + 1 rows the recurrence applies and the transformed entries vanish, so those rows live in a p-dimensional coordinate subspace, are linearly dependent, and the determinant is zero.

noncomputable def RS.hookColOp (p ℓ : ℕ) : Matrix (Fin ℓ) (Fin ℓ) ℂ

The unipotent column-operation matrix: columns < p are left alone, and column j ≥ p becomes the alternating binomial combination of columns j, j − 1, …, j − p.

Equations

• RS.hookColOp p ℓ = Matrix.of fun (k j : Fin ℓ) => if ↑j < p then if k = j then 1 else 0 else if ↑k ≤ ↑j then (-1) ^ (↑j - ↑k) * ↑(p.choose (↑j - ↑k)) else 0

theorem RS.hookColOp_blockTriangular (p ℓ : ℕ) : (hookColOp p ℓ).BlockTriangular id

The column operation is upper triangular.

theorem RS.det_hookColOp (p ℓ : ℕ) : (hookColOp p ℓ).det = 1

The column operation has determinant one.

noncomputable def RS.jtMatrix (t : ℕ → ℂ) (rows : List ℕ) : Matrix (Fin rows.length) (Fin rows.length) ℂ

The Jacobi–Trudi matrix of a row-length list.

Equations

• RS.jtMatrix t rows = Matrix.of fun (i j : Fin rows.length) => RS.newtonHZ t (↑(rows.get i) + ↑↑j - ↑↑i)

theorem RS.schurDet_eq_det_jtMatrix (t : ℕ → ℂ) (rows : List ℕ) : schurDet t rows = (jtMatrix t rows).det

schurDet is the determinant of the Jacobi–Trudi matrix.

theorem RS.jtMatrix_mul_hookColOp (t : ℕ → ℂ) (rows : List ℕ) (p : ℕ) (i j : Fin rows.length) (hj : p ≤ ↑j) : (jtMatrix t rows * hookColOp p rows.length) i j = ∑ d ∈ Finset.range (p + 1), (-1) ^ d * ↑(p.choose d) * newtonHZ t (↑(rows.get i) + ↑↑j - ↑↑i - ↑d)

Columns ≥ p of the transformed Jacobi–Trudi matrix carry the alternating binomial recurrence sums.

theorem RS.jtMatrix_mul_hookColOp_eq_zero (t : ℕ → ℂ) {p q : ℕ} (hrec : ∀ (m : ℤ), ↑q < m → ∑ d ∈ Finset.range (p + 1), (-1) ^ d * ↑(p.choose d) * newtonHZ t (m - ↑d) = 0) (lam : YoungDiagram) (hcell : (p, q) ∈ lam) (i j : Fin lam.rowLens.length) (hi : ↑i ≤ p) (hj : p ≤ ↑j) : (jtMatrix t lam.rowLens * hookColOp p lam.rowLens.length) i j = 0

In the first p + 1 rows, the transformed entries in columns ≥ p vanish by the recurrence: the diagram contains the cell (p, q), so those rows are long enough to push the argument past degree q.

theorem RS.diagramSchur_eq_zero_of_hook (t : ℕ → ℂ) {p q : ℕ} (hrec : ∀ (m : ℤ), ↑q < m → ∑ d ∈ Finset.range (p + 1), (-1) ^ d * ↑(p.choose d) * newtonHZ t (m - ↑d) = 0) (lam : YoungDiagram) (hcell : (p, q) ∈ lam) : diagramSchur lam t = 0

Hook vanishing (the combinatorial engine behind Deligne 1.9): if the complete homogeneous sequence of t satisfies the alternating binomial recurrence of order p beyond degree q, the Schur specialisation vanishes on every diagram containing the cell (p, q).

theorem RS.superPS_rec_int (p q : ℕ) {m : ℤ} (hm : ↑q < m) : ∑ d ∈ Finset.range (p + 1), (-1) ^ d * ↑(p.choose d) * newtonHZ (superPS p q) (m - ↑d) = 0

The super-power-sum sequences satisfy the recurrence slot of diagramSchur_eq_zero_of_hook, in its integer-indexed form.

theorem RS.diagramSchur_superPS_eq_zero {p q : ℕ} (lam : YoungDiagram) (hcell : (p, q) ∈ lam) : diagramSchur lam (superPS p q) = 0

Deligne 1.9, vanishing direction, character side: the Schur specialisation at the super power sums of dimension (p, q) vanishes on every diagram containing the cell (p, q).

theorem RS.diagramSchur_superPS_row (ν : YoungDiagram) : diagramSchur ν (superPS 1 0) = if ν.colLen 0 ≤ 1 then 1 else 0

One h-variable: the Schur specialisation at superPS 1 0 is the indicator of single-row diagrams.

theorem RS.diagramSchur_superPS_col (ν : YoungDiagram) : diagramSchur ν (superPS 0 1) = if ν.rowLen 0 ≤ 1 then 1 else 0

One e-variable: the Schur specialisation at superPS 0 1 is the indicator of single-column diagrams.