The monomial expansion of a Schur polynomial

The Schur polynomial s_μ is a sum of one monomial per semistandard tableau, so its coefficient at an exponent vector d is the Kostka number counting the tableaux of shape μ and content d (TauCeti.coeff_schurPoly). That content is a function on the alphabet, while the Kostka numbers TauCeti.kostkaNumber are indexed by a partition: the two differ by sorting the exponents into decreasing order. This file closes that gap and reads off the expansion of a Schur polynomial in the monomial symmetric polynomials MvPolynomial.msymm,

s_μ = ∑_{ν ⊢ n} K_{μν} m_ν,

with the Kostka numbers as its coefficients.

The bridge is the symmetry of s_μ. Sorting the exponents of a monomial is a permutation of the alphabet, and a permutation of the alphabet does not change the coefficients of a symmetric polynomial, so the coefficient of s_μ at an arbitrary exponent vector of total degree n is its coefficient at the sorted one, which TauCeti.coeff_schurPoly_partWeight already computes as a Kostka number. Concretely, TauCeti.weightPartition records the multiset of nonzero exponents of a monomial, TauCeti.exists_perm_mapDomain_eq_partWeight produces the permutation that sorts them, and TauCeti.coeff_schurPoly_eq_kostkaNumber is the resulting coefficient formula.

The sum runs over all partitions of n, with no bound relating the number of parts of ν to the size of the alphabet: a partition with more parts than the alphabet has letters contributes nothing because its monomial symmetric polynomial vanishes there (TauCeti.msymm_eq_zero_of_card_lt), exactly as the Schur polynomial itself vanishes for such a shape (TauCeti.schurPoly_eq_zero_iff).

Main definitions

• TauCeti.weightSym: the multiset of letters of a monomial of total degree n, as an element of Sym σ n.
• TauCeti.weightPartition: the partition of n recording the multiset of nonzero exponents of a monomial of total degree n.

Main results

• TauCeti.exists_perm_mapDomain_eq_partWeight: a monomial of total degree n is a permutation of the alphabet away from the sorted monomial TauCeti.partWeight of its TauCeti.weightPartition.
• TauCeti.coeff_msymm: a monomial symmetric polynomial has coefficient 1 at the monomials of its shape and 0 at every other monomial, and TauCeti.msymm_eq_zero_of_card_lt: it vanishes in an alphabet with fewer letters than its partition has parts.
• TauCeti.coeff_schurPoly_eq_kostkaNumber: the coefficient of s_μ at any monomial of degree n is a Kostka number, that of μ and the partition of the monomial's exponents.
• TauCeti.schurPoly_eq_sum_kostkaNumber_smul_msymm: the monomial expansion s_μ = ∑_ν K_{μν} m_ν, writing a Schur polynomial as the combination of the monomial symmetric polynomials whose coefficients are the Kostka numbers. This is the expansion only: neither family is linearly independent as indexed here, both containing zero terms whenever the partition has more parts than the alphabet has letters. Restricted to the partitions the alphabet does record they are bases, and the Kostka numbers a genuine change-of-basis matrix, which is TauCeti/RingTheory/MvPolynomial/Symmetric/Schur/Basis.lean.
• TauCeti.degree_partWeight, TauCeti.weightPartition_partWeight and TauCeti.coeff_msymm_partWeight: the sorted monomial of a partition the alphabet records has degree n and shape that partition, so m_ν is the indicator of its own sorted monomial. This is what makes the monomial symmetric polynomials independent.
• TauCeti.isHomogeneous_msymm: a monomial symmetric polynomial is homogeneous.

Implementation notes

One general fact is used and kept private here rather than stated for its own sake: that two families on a finite type taking the same multiset of values differ by a permutation of the index type. It is the shape of the sorting argument in this file and has no other consumer yet.

References

• W. Fulton, Young Tableaux, Section 2.2, where s_λ = ∑_μ K_{λμ} m_μ is read off the tableau definition.
• R. P. Stanley, Enumerative Combinatorics, Volume 2, §7.10.
• Schur--Weyl roadmap, Layer 7, "the msymm-to-schurPoly change of basis is the Kostka matrix Kλμ".

Rearranging a family along a permutation

The partition of the exponents of a monomial

theorem TauCeti.card_toMultiset_eq_degree {σ : Type u_1} (d : σ →₀ ℕ) : (Finsupp.toMultiset d).card = Finsupp.degree d

The number of letters of the monomial with exponent vector d is its total degree. This is not a simp lemma: Finsupp.card_toMultiset already rewrites the left-hand side to d.sum fun _ => id, so tagging it would leave it out of simp-normal form.

noncomputable def TauCeti.weightSym {σ : Type u_1} {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : Sym σ n

The multiset of letters of a monomial of total degree n, read as an element of Sym σ n: the letter x occurs as often as the exponent of x prescribes.

Equations

• TauCeti.weightSym d h = ⟨Finsupp.toMultiset d, ⋯⟩

@[simp]

theorem TauCeti.coe_weightSym {σ : Type u_1} {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : ↑(weightSym d h) = Finsupp.toMultiset d

noncomputable def TauCeti.weightPartition {σ : Type u_1} [DecidableEq σ] {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : n.Partition

The partition of the exponents of a monomial of total degree n: its parts are the nonzero exponents, so it is the shape of the monomial once its exponents are sorted decreasingly.

Equations

• TauCeti.weightPartition d h = Nat.Partition.ofSym (TauCeti.weightSym d h)

@[simp]

theorem TauCeti.weightPartition_parts {σ : Type u_1} [DecidableEq σ] {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : (weightPartition d h).parts = Multiset.map (⇑d) d.support.val

The parts of the partition of the exponents of a monomial are the exponents of the letters that actually occur in it.

theorem TauCeti.card_parts_weightPartition_le {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : (weightPartition d h).parts.card ≤ Fintype.card σ

A monomial has one nonzero exponent per letter occurring in it, so the partition of its exponents has no more parts than the alphabet has letters.

Sorting the exponents of a monomial

theorem TauCeti.exists_perm_mapDomain_eq_partWeight {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (d : σ →₀ ℕ) (h : Finsupp.degree d = n) : ∃ (e : Equiv.Perm σ), Finsupp.mapDomain (⇑e) d = partWeight σ (weightPartition d h)

A monomial of total degree n is a rearrangement of the sorted monomial of its shape: some permutation of the alphabet carries it to the exponent vector TauCeti.partWeight recording the parts of its TauCeti.weightPartition.

The coefficients of a monomial symmetric polynomial

@[simp]

theorem TauCeti.coeff_msymm_eq_zero_of_degree_ne {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (ν : n.Partition) {d : σ →₀ ℕ} (h : Finsupp.degree d ≠ n) : (MvPolynomial.msymm σ R ν).coeff d = 0

A monomial symmetric polynomial is homogeneous: it has no monomial whose total degree is not that of its partition.

@[simp]

theorem TauCeti.coeff_msymm {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (ν : n.Partition) {d : σ →₀ ℕ} (h : Finsupp.degree d = n) : (MvPolynomial.msymm σ R ν).coeff d = if weightPartition d h = ν then 1 else 0

The coefficients of a monomial symmetric polynomial are 0 and 1: m_ν is the sum of the monomials of total degree n whose nonzero exponents are the parts of ν, each occurring once.

@[simp]

theorem TauCeti.msymm_eq_zero_of_card_lt {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (ν : n.Partition) (h : Fintype.card σ < ν.parts.card) : MvPolynomial.msymm σ R ν = 0

A monomial symmetric polynomial vanishes when its partition has more parts than the alphabet has letters: no monomial in that alphabet uses that many distinct letters.

theorem TauCeti.isHomogeneous_msymm {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (ν : n.Partition) : (MvPolynomial.msymm σ R ν).IsHomogeneous n

A monomial symmetric polynomial is homogeneous of degree the natural number its partition partitions: every monomial occurring in it has the parts of the partition as its exponents.

The sorted monomial of a partition

theorem TauCeti.degree_partWeight {σ : Type u_1} [Fintype σ] {n : ℕ} (ν : n.Partition) (hν : ν.parts.card ≤ Fintype.card σ) : Finsupp.degree (partWeight σ ν) = n

The sorted monomial of a partition of n has total degree n, its exponents being the parts of the partition padded with zeros. The hypothesis is what keeps every part inside the alphabet: a longer partition would be truncated.

theorem TauCeti.weightPartition_partWeight {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (ν : n.Partition) (hν : ν.parts.card ≤ Fintype.card σ) (h : Finsupp.degree (partWeight σ ν) = n) : weightPartition (partWeight σ ν) h = ν

Sorting the exponents of an already sorted monomial changes nothing: the partition of the exponents of TauCeti.partWeight σ ν is ν itself. Together with TauCeti.coeff_msymm this says that the monomial symmetric polynomials take the value 1 at their own sorted monomial and 0 at every other one.

@[simp]

theorem TauCeti.coeff_msymm_partWeight {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (ν ξ : n.Partition) (hξ : ξ.parts.card ≤ Fintype.card σ) : (MvPolynomial.msymm σ R ν).coeff (partWeight σ ξ) = if ξ = ν then 1 else 0

A monomial symmetric polynomial is the indicator of its own sorted monomial: m_ν has coefficient 1 at the sorted monomial of ν and 0 at the sorted monomial of any other partition. This is the statement that the monomial symmetric polynomials are dual to the sorted monomials, and the reason they are linearly independent.

The monomial expansion

@[simp]

theorem TauCeti.coeff_schurPoly_eq_kostkaNumber {σ : Type u_1} [Fintype σ] [DecidableEq σ] {n : ℕ} (R : Type u_2) [CommSemiring R] (μ : n.Partition) {d : σ →₀ ℕ} (h : Finsupp.degree d = n) : (schurPoly σ R μ).coeff d = ↑(kostkaNumber μ (weightPartition d h))

The coefficient of a Schur polynomial at any monomial of degree n is a Kostka number: that of the shape μ and the partition of the monomial's exponents. The exponents need not be sorted, since sorting them is a permutation of the alphabet, which a symmetric polynomial does not see.

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

The monomial expansion of a Schur polynomial: s_μ = ∑_ν K_{μν} m_ν, expanding s_μ in the monomial symmetric polynomials with the Kostka numbers as its coefficients. The sum runs over every partition of n: those with more parts than the alphabet has letters contribute nothing, their monomial symmetric polynomial vanishing there. (Being an expansion, this does not by itself say that the Kostka numbers are a change-of-basis matrix: no basis result is proved here.)