The Jacobi--Trudi identity

The Schur polynomial s_μ, defined in TauCeti.diagramSchurPoly as the generating function of the semistandard tableaux of shape μ, is a determinant of complete homogeneous symmetric polynomials:

s_μ = det (h_{μᵢ - i + j})_{0 ≤ i, j < r}

for every r at least the number of rows of μ, in any number of variables and over any commutative ring. The indices μᵢ - i + j are integers, and h_m is 0 for m < 0; this is TauCeti.hsymmInt. The statement is TauCeti.diagramSchurPoly_eq_det_hsymmInt for Young diagrams in the alphabet Fin N, and TauCeti.schurPoly_eq_det_hsymmInt for partitions in an arbitrary finite alphabet.

The proof

The route is Macdonald's (I.3.4), through Jacobi's bialternant formula TauCeti.diagramSchurPoly_mul_alternant, s_μ · a_δ = a_{μ+δ}, with δ_j = N - 1 - j.

• For a variable x_k, the generating functions ∑ₙ hₙ tⁿ = ∏ᵢ (1 - xᵢ t)⁻¹ (TauCeti.mk_hsymm_eq_prod_mk_pow) and E⁽ᵏ⁾(t) = ∏_{i ≠ k} (1 - xᵢ t) multiply to (1 - x_k t)⁻¹. Comparing coefficients of tᵐ gives x_kᵐ = ∑_{r < N} e⁽ᵏ⁾_r h_{m - r}, where e⁽ᵏ⁾_r is the coefficient of tʳ in E⁽ᵏ⁾, which vanishes for r ≥ N.
• For every exponent vector α, this factors the alternant matrix (x_k^{α_j}) as the product of the matrix (e⁽ᵏ⁾_{N-1-l})_{k,l} and the matrix (h_{α_j - (N - 1 - l)})_{l,j}. For α = δ the second factor is unitriangular, so the first has determinant a_δ, and for α = μ + δ the second factor is the transpose of the Jacobi--Trudi matrix. Hence a_{μ+δ} = a_δ · det (h_{μᵢ - i + j}).
• Over ℤ the polynomial ring is a domain and a_δ ≠ 0, so a_δ cancels against the bialternant formula. Both sides commute with changing the coefficients, which carries the identity to every commutative ring.

This proves the identity with an N × N matrix when μ has at most N rows. A row of μ of length 0 contributes a last row (0, …, 0, 1) to the matrix, so the determinant does not depend on the size r once r is at least the number of rows. Finally, for μ with more than N rows both sides vanish compatibly: setting a variable to 0 preserves Schur polynomials (TauCeti.aeval_snoc_zero_diagramSchurPoly) and complete homogeneous symmetric polynomials (TauCeti.aeval_snoc_zero_hsymmInt), so the identity descends from N + 1 variables to N.

Main results

• TauCeti.diagramSchurPoly_eq_det_hsymmInt: the Jacobi--Trudi identity for the Schur polynomial of a Young diagram.
• TauCeti.schurPoly_eq_det_hsymmInt: the Jacobi--Trudi identity for the Schur polynomial of a partition.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 3, formula (3.4) and its proof.
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Theorem 7.16.1.

Expanding a power of a variable in complete homogeneous symmetric polynomials

Factoring the alternant matrix

The Jacobi--Trudi identity

theorem TauCeti.diagramSchurPoly_eq_det_hsymmInt {R : Type u_1} [CommRing R] (N : ℕ) (μ : YoungDiagram) {r : ℕ} (hr : μ.colLen 0 ≤ r) : diagramSchurPoly N R μ = (Matrix.of fun (i j : Fin r) => hsymmInt (Fin N) R (↑(μ.rowLen ↑i) - ↑↑i + ↑↑j)).det

The Jacobi--Trudi identity. The Schur polynomial of a Young diagram μ in the alphabet Fin N is the determinant det (h_{μᵢ - i + j})_{0 ≤ i, j < r} of complete homogeneous symmetric polynomials, for every r at least the number of rows of μ. The index μᵢ - i + j is an integer, and h_m = 0 for m < 0 (TauCeti.hsymmInt).

There is no condition relating N to μ: when μ has more than N rows, both sides vanish.

theorem TauCeti.schurPoly_eq_det_hsymmInt {R : Type u_1} [CommRing R] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (μ : n.Partition) {r : ℕ} (hr : μ.parts.card ≤ r) : schurPoly σ R μ = (Matrix.of fun (i j : Fin r) => hsymmInt σ R (↑((diagramOf μ).rowLen ↑i) - ↑↑i + ↑↑j)).det

The Jacobi--Trudi identity for partitions. In a finite alphabet σ, the Schur polynomial of a partition μ is det (h_{μᵢ - i + j})_{0 ≤ i, j < r} for every r at least the number of parts of μ, where μᵢ is the i-th largest part (0 past the last part) and h_m = 0 for m < 0.