Pieri rules and hook positivity for Schur specialisations

Three layers on top of the additive splitting of Schur specialisations.

1. Linear independence: the Schur specialisations of the shapes of one size, as functions of the scalar sequence, are linearly independent; a graded refinement separates sizes through the homogeneity of the specialisation under t c ↦ z^c · t c.
2. Pieri rules: the Schur specialisation of a diagram at t + superPS 1 0 (one extra even variable) is the sum of the Schur specialisations of its horizontal-strip sub-diagrams, by a unipotent row operation on the Jacobi–Trudi matrix followed by a multilinear expansion of the rows; at t + superPS 0 1 (one extra odd variable) the analogous identity over vertical-strip sub-diagrams follows from a direct two-term expansion of the rows. Extracting coefficients through the graded linear independence yields the induction-multiplicity Pieri rules indMult lam μ (rowShape m) and indMult lam μ (colShape m).
3. Hook positivity: building a diagram avoiding the cell (p, q) by horizontal strips in the first p rows and vertical strips in the first q columns shows that its Schur specialisation at superPS p q is a positive natural number — the nonvanishing direction of Deligne 1.9 on the character side.

Linear independence of Schur specialisations at a fixed size

The hypothesis pairs the class function π ↦ ∑ μ, c μ · jtChar μ (recast π) to zero against every completed cycle product; the Frobenius determination of class functions forces the character combination to vanish, and orthonormality of the recast characters extracts each coefficient.

theorem RS.diagramSchur_lin_indep {n : ℕ} (c : Shape n → ℂ) (h : ∀ (t : ℕ → ℂ), ∑ μ : Shape n, c μ * diagramSchur (↑μ) t = 0) (μ : Shape n) : c μ = 0

Linear independence of Schur specialisations at a fixed size: a coefficient family on the shapes of size n whose weighted sum of Schur specialisations vanishes at every scalar sequence is identically zero.

Homogeneity and the graded refinement

theorem RS.cycleFun_smul_pow {n : ℕ} (z : ℂ) (t : ℕ → ℂ) (π : Equiv.Perm (Fin n)) : cycleFun (fun (c : ℕ) => z ^ c * t c) π = z ^ n * cycleFun t π

The completed cycle product scales by z^n under the substitution t c ↦ z^c · t c.

theorem RS.diagramSchur_smul_pow (mu : YoungDiagram) (t : ℕ → ℂ) (z : ℂ) : (diagramSchur mu fun (c : ℕ) => z ^ c * t c) = z ^ mu.card * diagramSchur mu t

Homogeneity of the Schur specialisation: substituting t c ↦ z^c · t c scales the value of a diagram by z to its number of cells.

theorem RS.diagramSchur_graded_lin_indep {n : ℕ} (c : (k : ℕ) → Shape k → ℂ) (h : ∀ (t : ℕ → ℂ), ∑ k ∈ Finset.range (n + 1), ∑ κ : Shape k, c k κ * diagramSchur (↑κ) t = 0) (k : ℕ) : k ≤ n → ∀ (κ : Shape k), c k κ = 0

Graded linear independence: a size-indexed coefficient family on the shapes of sizes ≤ n whose combined Schur pairing vanishes at every scalar sequence vanishes in every graded piece — homogeneity separates the sizes, and the fixed-size independence finishes.

Row-length utilities for Young diagrams

theorem RS.rowLen_pos_of_lt_length (mu : YoungDiagram) {i : ℕ} (h : i < mu.rowLens.length) : 0 < mu.rowLen i

Rows inside the row-length list are nonempty.

theorem RS.ext_of_rowLen_eq {mu nu : YoungDiagram} (h : ∀ (i : ℕ), mu.rowLen i = nu.rowLen i) : mu = nu

Diagrams with the same row lengths are equal.

theorem RS.colLen_le_of_le {mu lam : YoungDiagram} (h : mu ≤ lam) (j : ℕ) : mu.colLen j ≤ lam.colLen j

Containment of diagrams is monotone on column lengths.

theorem RS.le_of_rowLen_le {mu lam : YoungDiagram} (h : ∀ (i : ℕ), mu.rowLen i ≤ lam.rowLen i) : mu ≤ lam

Rowwise domination of row lengths gives containment.

theorem RS.card_eq_sum_range_rowLen (mu : YoungDiagram) (N : ℕ) (hN : mu.colLen 0 ≤ N) : mu.card = ∑ i ∈ Finset.range N, mu.rowLen i

The cell count as a row-length sum over any range covering the column length.

Diagrams from finite antitone row-length vectors

noncomputable def RS.stripDiagram {ℓ : ℕ} (r : Fin ℓ → ℕ) : YoungDiagram

The diagram of an antitone row-length vector on Fin ℓ: the Young diagram whose row i < ℓ has length r i (and ⊥ on non-antitone junk input).

Equations

• RS.stripDiagram r = if h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i then YoungDiagram.ofRowLens (List.ofFn r) ⋯ else ⊥

theorem RS.stripDiagram_mem {ℓ : ℕ} {r : Fin ℓ → ℕ} (h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i) (c : ℕ × ℕ) : c ∈ stripDiagram r ↔ ∃ (hc : c.1 < ℓ), c.2 < r ⟨c.1, hc⟩

Membership in the diagram of a row-length vector.

theorem RS.stripDiagram_rowLen_lt {ℓ : ℕ} {r : Fin ℓ → ℕ} (h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i) (i : Fin ℓ) : (stripDiagram r).rowLen ↑i = r i

Row lengths of the diagram of a vector, inside the range.

theorem RS.stripDiagram_rowLen_le {ℓ : ℕ} {r : Fin ℓ → ℕ} (h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i) {i : ℕ} (hi : ℓ ≤ i) : (stripDiagram r).rowLen i = 0

Row lengths of the diagram of a vector, beyond the range.

theorem RS.stripDiagram_colLen {ℓ : ℕ} {r : Fin ℓ → ℕ} (h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i) : (stripDiagram r).colLen 0 ≤ ℓ

The diagram of a vector on Fin ℓ has at most ℓ rows.

theorem RS.stripDiagram_of_rowLen {ℓ : ℕ} {mu : YoungDiagram} (hc : mu.colLen 0 ≤ ℓ) : (stripDiagram fun (i : Fin ℓ) => mu.rowLen ↑i) = mu

A diagram with at most ℓ rows is the diagram of its own row-length vector on Fin ℓ.

theorem RS.stripDiagram_card {ℓ : ℕ} {r : Fin ℓ → ℕ} (h : ∀ (i j : Fin ℓ), i ≤ j → r j ≤ r i) : (stripDiagram r).card = ∑ i : Fin ℓ, r i

The cell count of the diagram of a vector is the sum of the vector.

Horizontal and vertical strips

def RS.IsHStrip (lam mu : YoungDiagram) : Prop

Horizontal strip: mu is contained in lam and interlaces it — each row of lam reaches at most the previous row of mu, so the removed skew cells occupy distinct columns.

Equations

• RS.IsHStrip lam mu = (mu ≤ lam ∧ ∀ (i : ℕ), lam.rowLen (i + 1) ≤ mu.rowLen i)

def RS.IsVStrip (lam mu : YoungDiagram) : Prop

Vertical strip: mu is contained in lam and each row shrinks by at most one cell, so the removed skew cells occupy distinct rows.

Equations

• RS.IsVStrip lam mu = (mu ≤ lam ∧ ∀ (i : ℕ), lam.rowLen i ≤ mu.rowLen i + 1)

The one-row and one-column shapes

noncomputable def RS.rowShape (m : ℕ) : Shape m

The single-row shape of size m.

Equations

• RS.rowShape m = ⟨RS.stripDiagram fun (x : Fin 1) => m, ⋯⟩

noncomputable def RS.colShape (m : ℕ) : Shape m

The single-column shape of size m.

Equations

• RS.colShape m = ⟨RS.stripDiagram fun (x : Fin m) => 1, ⋯⟩

theorem RS.rowShape_rowLen_zero (m : ℕ) : (↑(rowShape m)).rowLen 0 = m

The first row of the one-row shape.

theorem RS.rowShape_rowLen_succ (m i : ℕ) : (↑(rowShape m)).rowLen (i + 1) = 0

The later rows of the one-row shape.

theorem RS.rowShape_colLen (m : ℕ) : (↑(rowShape m)).colLen 0 ≤ 1

The one-row shape has at most one row.

theorem RS.colShape_rowLen_lt (m : ℕ) {i : ℕ} (hi : i < m) : (↑(colShape m)).rowLen i = 1

The rows of the one-column shape, inside the column.

theorem RS.colShape_rowLen_le (m : ℕ) {i : ℕ} (hi : m ≤ i) : (↑(colShape m)).rowLen i = 0

The rows of the one-column shape, beyond the column.

theorem RS.colShape_rowLen_zero_le (m : ℕ) : (↑(colShape m)).rowLen 0 ≤ 1

The one-column shape has rows of length at most one.

theorem RS.shape_eq_rowShape {b : ℕ} (ν : Shape b) (h : (↑ν).colLen 0 ≤ 1) : ν = rowShape b

Uniqueness of the one-row shape: a shape of size b with at most one row is rowShape b.

theorem RS.shape_eq_colShape {b : ℕ} (ν : Shape b) (h : (↑ν).rowLen 0 ≤ 1) : ν = colShape b

Uniqueness of the one-column shape: a shape of size b with rows of length at most one is colShape b.

The graded reindexing of strip-vector sums

A sum over a set of antitone row-length vectors, of a function of the associated diagrams, is a graded sum over the shapes of each size satisfying the membership predicate of the vector set.

The Jacobi–Trudi determinant in row-length form

theorem RS.diagramSchur_eq_det_rowLen (mu : YoungDiagram) {k : ℕ} (hk : mu.colLen 0 ≤ k) (t : ℕ → ℂ) : diagramSchur mu t = (Matrix.of fun (i j : Fin k) => newtonHZ t (↑(mu.rowLen ↑i) + ↑↑j - ↑↑i)).det

The Schur specialisation of a diagram is its Jacobi–Trudi determinant over any square of rows covering the column length, with the row lengths as exponents — zero rows pad invisibly.

One extra even variable: the partial-sum sequence

At t + superPS 1 0 the complete homogeneous sequence is the partial-sum sequence of that of t; its integer-indexed first difference is newtonHZ t, and telescoping produces the interval-sum identity feeding the row operation.

The unipotent row operation

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

The unipotent row-operation matrix subtracting from each row its successor.

Equations

• RS.rowOp ℓ = Matrix.of fun (i k : Fin ℓ) => if k = i then 1 else if ↑k = ↑i + 1 then -1 else 0

theorem RS.rowOp_blockTriangular (ℓ : ℕ) : (rowOp ℓ).BlockTriangular id

The row operation is upper triangular.

theorem RS.det_rowOp (ℓ : ℕ) : (rowOp ℓ).det = 1

The row operation has determinant one.

The horizontal Pieri determinant identity

theorem RS.diagramSchur_add_one_row (lam : YoungDiagram) (t : ℕ → ℂ) : (diagramSchur lam fun (c : ℕ) => t c + superPS 1 0 c) = ∑ k ∈ Finset.range (lam.card + 1), ∑ μ : Shape k, (if IsHStrip lam ↑μ then 1 else 0) * diagramSchur (↑μ) t

One extra even variable — the horizontal Pieri identity: the Schur specialisation of lam at t + superPS 1 0 is the sum of the Schur specialisations at t of the horizontal-strip sub-diagrams of lam, presented as a graded sum over the shapes of each size with the strip indicator.

One extra odd variable: the two-term sequence

At t + superPS 0 1 the complete homogeneous sequence is the two-term convolution h_n + h_{n-1}: the generating series picks up one factor 1 + X.

The vertical Pieri determinant identity

theorem RS.diagramSchur_add_one_col (lam : YoungDiagram) (t : ℕ → ℂ) : (diagramSchur lam fun (c : ℕ) => t c + superPS 0 1 c) = ∑ k ∈ Finset.range (lam.card + 1), ∑ μ : Shape k, (if IsVStrip lam ↑μ then 1 else 0) * diagramSchur (↑μ) t

One extra odd variable — the vertical Pieri identity: the Schur specialisation of lam at t + superPS 0 1 is the sum of the Schur specialisations at t of the vertical-strip sub-diagrams of lam, presented as a graded sum over the shapes of each size with the strip indicator.

The multiplicity Pieri rules

Splitting t + superPS 1 0 through diagramSchur_add collapses the second tensor factor to the one-row shape; comparing with the determinant identity through the graded linear independence reads off the induction multiplicities.

Hook positivity

Building a diagram avoiding (p, q) by strips: the first p rows are grown one horizontal strip per new even variable, the columns of the remainder one vertical strip per new odd variable. Every term of the strip expansions is a natural number, and the specific strip term is positive by induction, so the total is positive.

theorem RS.diagramSchur_superPS_pos {p q : ℕ} (lam : YoungDiagram) (hcell : (p, q) ∉ lam) : ∃ (m : ℕ), 0 < m ∧ diagramSchur lam (superPS p q) = ↑m

Hook positivity (Deligne 1.9, nonvanishing direction, character side): the Schur specialisation at the super power sums of dimension (p, q) of any diagram avoiding the cell (p, q) is a positive natural number.