Products of complete homogeneous symmetric polynomials in the Schur basis

A product of complete homogeneous symmetric polynomials expands in the Schur polynomials with the Kostka numbers as coefficients: for a partition ν,

h_ν = h_{ν₁} ⋯ h_{ν_k} = ∑_μ K_{μν} s_μ,

where K_{μν} is the number of semistandard tableaux of shape μ and content ν. This is TauCeti.hsymmPart_eq_sum_kostkaNumber_smul_schurPoly, for Mathlib's MvPolynomial.hsymmPart in an arbitrary finite alphabet. The same holds for an arbitrary ordered sequence of degrees in place of the parts of ν, with the Kostka number of a shape and a content that need not be weakly decreasing (TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_diagramSchurPoly).

Together with the monomial expansion s_μ = ∑_ξ K_{μξ} m_ξ (TauCeti.schurPoly_eq_sum_kostkaNumber_smul_msymm), the expansion computes the coefficients of h_ν in terms of Kostka numbers alone: the coefficient of x^ξ in h_ν is ∑_μ K_{μν} K_{μξ} (TauCeti.coeff_hsymmPart, and TauCeti.coeff_hsymmPart_partWeight at partitions). On the side of the symmetric groups h_ν corresponds to the permutation module M^ν and s_μ to the Specht module S^μ (classically, through the Frobenius characteristic map), so this is the symmetric-function half of Young's rule M^ν ≅ ⊕_μ K_{μν} S^μ.

The argument

The expansion is the Pieri rule h_r · s_ν = ∑ s_μ (TauCeti.hsymm_mul_diagramSchurPoly), the sum running over the shapes μ obtained from ν by adding a horizontal strip of r cells, iterated along a sequence of degrees c₀, …, c_{k-1}. Each iteration adds one horizontal strip, so after k steps the coefficient of s_μ counts the chains ∅ = μ⁰ ⊆ μ¹ ⊆ ⋯ ⊆ μᵏ = μ of shapes in which μⁱ / μⁱ⁻¹ is a horizontal strip of c_{i-1} cells. Such a chain is a semistandard tableau of shape μ and content c: the cells of μⁱ / μⁱ⁻¹ are those carrying the letter i - 1. The induction step reads this bijection one letter at a time, as the weight-refined branching rule for tableaux TauCeti.BoundedSSYT.card_weight_eq_sum_interlacingShapes, re-indexed by partitions: erasing the largest letter of a tableau leaves a tableau on a shape interlacing the original one, whose size is fixed by how often the erased letter occurred.

Main results

• TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_diagramSchurPoly: the expansion of h_{c₀} ⋯ h_{c_{k-1}} in the Schur polynomials, for an arbitrary sequence of degrees, and TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_schurPoly, the same in a finite alphabet.
• TauCeti.hsymmPart_eq_sum_kostkaNumber_smul_schurPoly: h_ν = ∑_μ K_{μν} s_μ for a partition ν, in a finite alphabet.
• TauCeti.coeff_hsymmPart: the coefficient of h_ν at an arbitrary monomial x^d is ∑_μ K_{μν} K_{μd}, and TauCeti.coeff_hsymmPart_partWeight, the same at the monomial of a partition ξ.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 6.
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Section 7.12.
• W. Fulton, Young Tableaux, Section 2.2.

theorem TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_diagramSchurPoly {R : Type u_1} [CommSemiring R] {N k n : ℕ} (d : Fin k →₀ ℕ) (hd : Finsupp.degree d = n) : ∏ i : Fin k, MvPolynomial.hsymm (Fin N) R (d i) = ∑ μ : n.Partition, ↑(diagramKostkaNumber (diagramOf μ) ⇑(Finsupp.mapDomain Fin.val d)) • diagramSchurPoly N R (diagramOf μ)

A product of complete homogeneous symmetric polynomials in the Schur basis. For a sequence of degrees d₀, …, d_{k-1} summing to n, in the alphabet Fin N,

h_{d₀} ⋯ h_{d_{k-1}} = ∑_μ K_{μ d} s_μ,

the sum running over the partitions μ of n, where K_{μ d} is the number of semistandard tableaux of shape μ using the letter i exactly dᵢ times. The degrees need not be weakly decreasing. No bound relating N and k is needed: the shapes with more than N rows contribute nothing, their Schur polynomials vanishing in N variables.

theorem TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_schurPoly {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {k n : ℕ} (d : Fin k →₀ ℕ) (hd : Finsupp.degree d = n) : ∏ i : Fin k, MvPolynomial.hsymm σ R (d i) = ∑ μ : n.Partition, ↑(diagramKostkaNumber (diagramOf μ) ⇑(Finsupp.mapDomain Fin.val d)) • schurPoly σ R μ

A product of complete homogeneous symmetric polynomials in the Schur basis, in a finite alphabet σ: for a sequence of degrees d₀, …, d_{k-1} summing to n, h_{d₀} ⋯ h_{d_{k-1}} = ∑_μ K_{μ d} s_μ, the sum running over the partitions μ of n. This is TauCeti.prod_hsymm_eq_sum_diagramKostkaNumber_smul_diagramSchurPoly with the alphabet renamed.

theorem TauCeti.hsymmPart_eq_sum_kostkaNumber_smul_schurPoly {R : Type u_1} [CommSemiring R] (σ : Type u_2) [Fintype σ] [DecidableEq σ] {n : ℕ} (ν : n.Partition) : MvPolynomial.hsymmPart σ R ν = ∑ μ : n.Partition, ↑(kostkaNumber μ ν) • schurPoly σ R μ

h_ν = ∑_μ K_{μν} s_μ. In a finite alphabet, the product h_ν = h_{ν₁} ⋯ h_{ν_k} of the complete homogeneous symmetric polynomials over the parts of a partition ν of n expands in the Schur polynomials of the partitions of n, with the Kostka numbers K_{μν} as coefficients. This is the symmetric-function form of Young's rule for the permutation modules of the symmetric groups.

theorem TauCeti.coeff_hsymmPart {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (ν : n.Partition) (d : σ →₀ ℕ) : (MvPolynomial.hsymmPart σ R ν).coeff d = ∑ μ : n.Partition, ↑(kostkaNumber μ ν) * ↑(diagramKostkaNumber (diagramOf μ) ⇑(Finsupp.mapDomain (fun (x : σ) => ↑((Fintype.equivFin σ) x)) d))

The coefficients of h_ν are sums of products of Kostka numbers: the coefficient of h_ν at an arbitrary exponent d is ∑_μ K_{μν} K_{μd}, where K_{μd} is the Kostka number of the shape of μ and the content obtained from d by numbering the alphabet with Fintype.equivFin, as in TauCeti.coeff_schurPoly.

theorem TauCeti.coeff_hsymmPart_partWeight {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (ν ξ : n.Partition) (h : (diagramOf ξ).colLen 0 ≤ Fintype.card σ) : (MvPolynomial.hsymmPart σ R ν).coeff (partWeight σ ξ) = ∑ μ : n.Partition, ↑(kostkaNumber μ ν) * ↑(kostkaNumber μ ξ)

The coefficients of h_ν at partitions: the coefficient of the monomial recording the parts of ξ in h_ν is ∑_μ K_{μν} K_{μξ}. The row bound is what makes the monomial record all of ξ, as in TauCeti.coeff_schurPoly_partWeight.