Jacobi's bialternant formula

For a Young diagram μ with at most N rows, write λ_j = μ.rowLen j for its row lengths and δ_j = N - 1 - j for the staircase exponents on the alphabet Fin N. Jacobi's bialternant formula says that the Schur polynomial s_μ, defined combinatorially as the generating function of the semistandard tableaux of shape μ, is the quotient of two alternants, s_μ = a_{λ+δ} / a_δ. The quotient is not itself an operation on MvPolynomial, so the formula is stated here in the division-free form

s_μ · a_δ = a_{λ+δ},

TauCeti.diagramSchurPoly_mul_alternant. It is the symmetric-polynomial form of the Weyl character formula for GL_N, with a_δ the Weyl denominator and a_{λ+δ} the Weyl numerator; identifying s_μ with the character of the irreducible representation of highest weight λ is a separate statement, not made here.

Both sides branch in the same way

The tableau side has a branching rule in the last variable, TauCeti.diagramSchurPoly_eq_sum_interlacingShapes: s_μ(x₀, …, x_n) = ∑_{ν ≺ μ} x_n ^ (|μ| - |ν|) · s_ν(x₀, …, x_{n-1}), the sum running over the shapes ν with at most n rows interlacing μ. The alternant side satisfies the same rule up to the Vandermonde factor ∏_{i < n} (x_i - x_n): this is TauCeti.alternant_eq_prod_mul_sum_interlacingShapes,

a_{λ+δ}(x₀, …, x_n) = ∏_{i < n} (x_i - x_n) · ∑_{ν ≺ μ} x_n ^ (|μ| - |ν|) · a_{ν+δ'}(x'),

with x' = (x₀, …, x_{n-1}) and δ' the staircase on those n letters. For the empty shape it is the recursion a_δ = ∏_{i < n} (x_i - x_n) · a_{δ'} of the Vandermonde determinant, and the bialternant formula follows from the two branching rules by induction on the number of variables.

Main statements

• TauCeti.alternant_eq_prod_mul_sum_interlacingShapes: the branching rule for the alternants a_{λ+δ}.
• TauCeti.diagramSchurPoly_mul_alternant: Jacobi's bialternant formula for Young diagrams.
• TauCeti.schurPoly_mul_alternant: the formula for partitions in any finite alphabet.

Implementation notes

The branching rule for alternants is a determinant computation. Writing y = x_n and e_j = λ_j + n - j for the exponents, subtracting y ^ (e_j - e_{j+1}) times column j + 1 from column j for every j < n at once (right multiplication by a unitriangular matrix) empties the last row except for its final entry y ^ λ_n. In the remaining n × n block the entry in row i and column j is x_i - y times the geometric sum ∑_{λ_{j+1} ≤ m ≤ λ_j} x_i ^ (m + n - 1 - j) · y ^ (λ_j - m). Pulling the factor x_i - y out of each row and expanding the determinant multilinearly in its columns (MultilinearMap.map_sum_finset) gives a sum over families m_j ∈ [λ_{j+1}, λ_j]. These are the row lengths of shapes interlacing μ (YoungDiagram.sum_interlacingShapes_eq_sum_piFinset).

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 3 (the Schur functions as quotients of alternants) and Section 5 (their tableau expansion).
• W. Fulton, Young Tableaux, Chapter 6.

theorem TauCeti.alternant_eq_prod_mul_sum_interlacingShapes {R : Type u_1} [CommRing R] (n : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n + 1) : (alternant (Fin (n + 1)) R fun (j : Fin (n + 1)) => μ.betaNumber (n + 1) ↑j) = (∏ i : Fin n, (MvPolynomial.X i.castSucc - MvPolynomial.X (Fin.last n))) * ∑ ν ∈ YoungDiagram.interlacingShapes n μ, MvPolynomial.X (Fin.last n) ^ (μ.card - ν.card) * (MvPolynomial.rename Fin.castSucc) (alternant (Fin n) R fun (j : Fin n) => ν.betaNumber n ↑j)

The branching rule for alternants. For a shape μ with at most n + 1 rows, the alternant a_{λ+δ} of its row lengths λ shifted by the staircase δ_j = n - j on n + 1 letters is the Vandermonde factor ∏_{i < n} (x_i - x_n) times the sum, over the shapes ν with at most n rows interlacing μ, of x_n ^ (|μ| - |ν|) times the alternant a_{ν+δ'} in the first n letters, δ'_j = n - 1 - j.

This is the alternant counterpart of the branching rule TauCeti.diagramSchurPoly_eq_sum_interlacingShapes for Schur polynomials.

theorem TauCeti.diagramSchurPoly_mul_alternant {R : Type u_1} [CommRing R] (N : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ N) : (diagramSchurPoly N R μ * alternant (Fin N) R fun (j : Fin N) => N - 1 - ↑j) = alternant (Fin N) R fun (j : Fin N) => μ.betaNumber N ↑j

Jacobi's bialternant formula. For a Young diagram μ with at most N rows, the Schur polynomial s_μ in the alphabet Fin N times the Vandermonde alternant a_δ, δ_j = N - 1 - j, is the alternant a_{λ+δ} of the row lengths λ_j = μ.rowLen j shifted by the staircase: s_μ · a_δ = a_{λ+δ}. This is the division-free form of s_μ = a_{λ+δ} / a_δ.

The row bound is necessary: for a taller shape s_μ vanishes, while the right-hand side, which only sees the first N rows, need not.

theorem TauCeti.schurPoly_mul_alternant {R : Type u_1} [CommRing R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) (hμ : (diagramOf μ).colLen 0 ≤ Fintype.card σ) : schurPoly σ R μ * (MvPolynomial.rename ⇑(Fintype.equivFin σ).symm) (alternant (Fin (Fintype.card σ)) R fun (j : Fin (Fintype.card σ)) => Fintype.card σ - 1 - ↑j) = (MvPolynomial.rename ⇑(Fintype.equivFin σ).symm) (alternant (Fin (Fintype.card σ)) R fun (j : Fin (Fintype.card σ)) => (diagramOf μ).betaNumber (Fintype.card σ) ↑j)

Jacobi's bialternant formula for partitions. In a finite alphabet σ, ordered by Fintype.equivFin σ, the Schur polynomial of μ times the renamed staircase alternant equals the renamed alternant of the beta-numbers of its Young diagram.