The Pieri rule for Schur polynomials

Multiplying a Schur polynomial by a complete homogeneous symmetric polynomial adds horizontal strips: for every r,

h_r · s_ν = ∑_μ s_μ,

the sum running over the diagrams μ with ν.card + r cells whose row lengths interlace those of ν, μ₀ ≥ ν₀ ≥ μ₁ ≥ ν₁ ≥ ⋯, equivalently over the μ ⊇ ν whose skew shape μ / ν has at most one cell in each column. Every term carries the coefficient 1. This is TauCeti.hsymm_mul_diagramSchurPoly for Young diagrams in the alphabet Fin N, and TauCeti.hsymm_mul_schurPoly for partitions in an arbitrary finite alphabet.

Iterating the rule from s_∅ = 1 along the parts of a partition ν expands the product h_{ν₁} ⋯ h_{ν_k} in Schur polynomials with the Kostka numbers as coefficients, which is the symmetric-function half of Young's rule for the permutation modules of the symmetric groups.

The cancellation

The computation happens on alternants. TauCeti.hsymm_mul_alternant expands h_r · a_α as the sum of a_{α + γ} over the exponent vectors γ of total degree r. Taking α to be the beta-numbers β_j = ν_j + (N - 1 - j) of ν, the shifted vectors β + γ are no longer decreasing, so each must be sorted back (Function.Injective.exists_strictAnti_comp, uniquely by StrictAnti.perm_eq) at the cost of the sign of the sorting permutation; a strictly decreasing result is again a vector of beta-numbers (YoungDiagram.exists_eq_betaNumber_of_strictAnti), and a repeated exponent kills the alternant. Grouping the shifts by the shape they sort to leaves, for each shape μ, the signed count of the permutations τ with β_j ≤ β(μ)_{τ j} for all j. That count is 1 exactly when the comparisons cut out the initial segments, which is interlacing, and 0 otherwise (TauCeti.sum_sign_filter_forall_le_of_antitone). Both the sorting and the cancellation are genuinely needed: a shift of total degree r is an arbitrary exponent vector, so the shifted beta-numbers are in general neither distinct nor decreasing.

Main statements

• TauCeti.hsymm_mul_alternant_betaNumber: the Pieri rule for alternants of beta-numbers.
• TauCeti.hsymm_mul_diagramSchurPoly: the Pieri rule for the Schur polynomial of a Young diagram.
• TauCeti.hsymm_mul_schurPoly: the Pieri rule for the Schur polynomial of a partition in a finite alphabet.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 5 (Pieri's formula).
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Section 7.15 (Pieri's rule).

theorem TauCeti.hsymm_mul_alternant_betaNumber {R : Type u_1} [CommRing R] {N : ℕ} (ν : YoungDiagram) (hν : ν.colLen 0 ≤ N) (r : ℕ) : (MvPolynomial.hsymm (Fin N) R r * alternant (Fin N) R fun (j : Fin N) => ν.betaNumber N ↑j) = ∑ μ : (ν.card + r).Partition with (diagramOf μ).InterlacedBy ν ∧ (diagramOf μ).colLen 0 ≤ N, alternant (Fin N) R fun (j : Fin N) => (diagramOf μ).betaNumber N ↑j

The Pieri rule for alternants of beta-numbers. Let ν be a Young diagram with at most N rows and β its beta-numbers relative to N, so that a_β = s_ν · a_δ. Multiplying a_β by the complete homogeneous symmetric polynomial h_r gives the sum, with no signs, of the alternants of the beta-numbers of the diagrams μ with at most N rows obtained from ν by adding a horizontal strip of r cells.

theorem TauCeti.hsymm_mul_diagramSchurPoly {R : Type u_1} [CommSemiring R] {N : ℕ} (ν : YoungDiagram) (r : ℕ) : MvPolynomial.hsymm (Fin N) R r * diagramSchurPoly N R ν = ∑ μ : (ν.card + r).Partition with (diagramOf μ).InterlacedBy ν, diagramSchurPoly N R (diagramOf μ)

The Pieri rule for Schur polynomials. Multiplying the Schur polynomial of a Young diagram ν in the alphabet Fin N by the complete homogeneous symmetric polynomial h_r gives the sum of the Schur polynomials of the diagrams μ obtained from ν by adding a horizontal strip of r cells, each with coefficient 1: h_r · s_ν = ∑_μ s_μ. No bound on the number of rows is needed: the Schur polynomials of the diagrams with more than N rows vanish on both sides. Nor is r required to be positive: at r = 0 the only strip is empty and the sum is the single term s_ν.

theorem TauCeti.hsymm_mul_schurPoly {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (ν : n.Partition) (r : ℕ) : MvPolynomial.hsymm σ R r * schurPoly σ R ν = ∑ μ : (n + r).Partition with (diagramOf μ).InterlacedBy (diagramOf ν), schurPoly σ R μ

The Pieri rule for Schur polynomials of partitions. In a finite alphabet σ, for a partition ν of n, h_r · s_ν = ∑_μ s_μ, the sum running over the partitions μ of n + r whose Young diagram contains that of ν with a horizontal strip as complement.