Prepending full columns to a shape

Lengthening every one of the first N rows of a Young diagram by the same amount c — equivalently, prepending c columns of full height N — multiplies its Schur polynomial in N variables by (x₀ ⋯ x_{N-1})^c:

s_ν(x) = (∏ᵢ xᵢ)^c · s_μ(x) whenever ν_j = μ_j + c for every j < N.

The reason is visible on the tableau side — the prepended columns of a semistandard tableau in the alphabet {0, …, N - 1} are forced to be 0, 1, …, N - 1 from top to bottom, contributing the monomial (x₀ ⋯ x_{N-1})^c and leaving a tableau of the shorter shape — but the proof here is the one-line bialternant computation: adding c to every row length adds c to every beta-number (YoungDiagram.betaNumber), and raising every exponent of an alternant by c multiplies it by (∏ᵢ xᵢ)^c (TauCeti.alternant_add_const). Cancelling the Vandermonde alternant, which is nonzero because the staircase exponents are distinct, gives the identity.

Both row bounds are needed, the hypothesis on the row lengths saying nothing about the rows past the first N of either shape. A shape taller than N has vanishing Schur polynomial in N variables (TauCeti.diagramSchurPoly_eq_zero_of_lt_colLen), so dropping either bound lets one side of the identity vanish while the other does not: without the bound on ν the left-hand side can vanish and the right-hand side not, and without the bound on μ the right-hand side can vanish and the left-hand side not.

This is the polynomial shadow of the determinant twist of a GL N-representation: a full column block contributes a factor of the determinant character, and TauCeti.char_rationalWeylRep_weightOfShape_diagonal reads the identity below that way.

Main results

• TauCeti.diagramSchurPoly_eq_prod_X_pow_mul_of_rowLen_eq_add: prepending c full columns multiplies the Schur polynomial by (∏ᵢ xᵢ)^c.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 3, Example 1, where the same shift of the bialternant numerator is read off.

theorem TauCeti.diagramSchurPoly_eq_prod_X_pow_mul_of_rowLen_eq_add {N c : ℕ} {μ ν : YoungDiagram} (R : Type u_1) [CommSemiring R] (hμ : μ.colLen 0 ≤ N) (hν : ν.colLen 0 ≤ N) (h : ∀ j < N, ν.rowLen j = μ.rowLen j + c) : diagramSchurPoly N R ν = (∏ i : Fin N, MvPolynomial.X i) ^ c * diagramSchurPoly N R μ

Prepending c columns of full height N multiplies a Schur polynomial by (∏ᵢ xᵢ)^c. If ν and μ both have at most N rows and ν_j = μ_j + c for every j < N, then s_ν = (x₀ ⋯ x_{N-1})^c · s_μ in N variables.