The monomial and Schur bases of the symmetric homogeneous polynomials

Let σ be a finite alphabet and R a commutative ring. This file proves that the Schur polynomials s_μ of TauCeti/RingTheory/MvPolynomial/Symmetric/Schur/Basic.lean form an R-basis of the symmetric polynomials in σ that are homogeneous of degree n, indexed by the partitions of n with at most Fintype.card σ parts. Taken over ℤ, this is the finite-alphabet, fixed-degree form of "the Schur functions are a ℤ-basis of the symmetric functions"; the stable symmetric-function ring, in which the unqualified statement lives, is not built here.

The index set

Both TauCeti.msymm_eq_zero_of_card_lt and TauCeti.schurPoly_eq_zero_iff say that a partition with more parts than the alphabet has letters contributes nothing, so neither family is linearly independent when indexed by all partitions of n. The bases below are therefore indexed by the subtype {ν : n.Partition // ν.parts.card ≤ Fintype.card σ}, which is exactly the range in which TauCeti.partWeight records a partition faithfully.

The route

Everything runs through a single linear map, TauCeti.partWeightCoeff, reading a symmetric homogeneous polynomial at the sorted monomials TauCeti.partWeight σ ν. It is bijective: a symmetric polynomial has the same coefficient at a monomial and at its sorted rearrangement (TauCeti.coeff_eq_coeff_partWeight), so a symmetric homogeneous polynomial is determined by those coefficients; and the monomial symmetric polynomials, whose coefficients at sorted monomials are the Kronecker delta (TauCeti.coeff_msymm_partWeight), realize every prescription. Reading that bijection as a coordinate system is the monomial basis TauCeti.msymmBasis.

The Schur basis is the monomial basis transported along the Kostka matrix. In the monomial basis the coordinates of s_μ are the Kostka numbers K_{μν} (TauCeti.msymmBasis_repr_schurPoly), which vanish unless μ dominates ν (TauCeti.kostkaNumber_eq_zero_of_not_dominates) and equal 1 on the diagonal (TauCeti.kostkaNumber_self). Since dominance refines the lexicographic linear order on partitions (TauCeti.lex_le_of_dominates), the Kostka matrix is triangular with 1s on the diagonal for that linear order, so its determinant is 1 and it is a change of basis. This is where the ring hypothesis enters: over ℕ the transition matrix is not invertible.

Main definitions

The module being based, TauCeti.symmetricHomogeneousSubmodule σ R n, carries no Schur content and is defined in TauCeti/RingTheory/MvPolynomial/Symmetric/Homogeneous.lean.

• TauCeti.partWeightCoeff: the coordinates of a symmetric homogeneous polynomial at the sorted monomials.
• TauCeti.msymmBasis: the monomial basis.
• TauCeti.schurPolyBasis: the Schur basis.

Main results

• TauCeti.coeff_eq_coeff_partWeight: a symmetric polynomial has the same coefficient at a monomial of degree n and at the sorted monomial of the partition of its exponents.
• TauCeti.partWeightCoeff_bijective: a symmetric homogeneous polynomial is exactly a prescription of coefficients at the sorted monomials.
• TauCeti.coe_msymmBasis and TauCeti.msymmBasis_repr_apply: the monomial basis consists of the monomial symmetric polynomials, and coordinates in it are coefficients at sorted monomials.
• TauCeti.msymmBasis_repr_schurPoly: the Kostka numbers are the change-of-basis matrix, the coordinates of s_μ in the monomial basis.
• TauCeti.schurPolyBasis and TauCeti.coe_schurPolyBasis: the Schur polynomials of the partitions of n with at most Fintype.card σ parts are a basis of the symmetric homogeneous polynomials of degree n.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Sections 2 and 6: the monomial symmetric functions are a basis, the Kostka matrix is unitriangular for the dominance order, and hence the Schur functions are a basis.
• R. P. Stanley, Enumerative Combinatorics, Volume 2, §7.10.
• Schur--Weyl roadmap, Layer 7, "The Schur functions are a ℤ-basis of the symmetric functions; msymm-to-schurPoly change of basis is the Kostka matrix Kλμ".

The symmetric homogeneous polynomials

theorem TauCeti.schurPoly_mem_symmetricHomogeneousSubmodule {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] (μ : n.Partition) : schurPoly σ R μ ∈ symmetricHomogeneousSubmodule σ R n

A Schur polynomial is symmetric and homogeneous of degree the natural number its partition partitions.

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

A monomial symmetric polynomial is symmetric and homogeneous of degree the natural number its partition partitions.

Coordinates at the sorted monomials

theorem TauCeti.coeff_eq_coeff_partWeight {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] [DecidableEq σ] {p : MvPolynomial σ R} (hp : p.IsSymmetric) {d : σ →₀ ℕ} (hd : Finsupp.degree d = n) : p.coeff d = p.coeff (partWeight σ (weightPartition d hd))

A symmetric polynomial does not see the order of the exponents of a monomial: its coefficient at a monomial of total degree n is its coefficient at the sorted monomial of the partition of those exponents. This is what makes the coordinates below complete.

noncomputable def TauCeti.partWeightCoeff (σ : Type u_1) (R : Type u_2) [CommSemiring R] (n : ℕ) [Fintype σ] : ↥(symmetricHomogeneousSubmodule σ R n) →ₗ[R] { ν : n.Partition // ν.parts.card ≤ Fintype.card σ } →₀ R

The coordinates of a symmetric homogeneous polynomial: its coefficients at the sorted monomials TauCeti.partWeight σ ν, one for each partition ν of n short enough for the alphabet to record. TauCeti.partWeightCoeff_bijective says these coordinates determine the polynomial and may be prescribed arbitrarily, and TauCeti.msymmBasis is the resulting basis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.partWeightCoeff_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] (p : ↥(symmetricHomogeneousSubmodule σ R n)) (ν : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ((partWeightCoeff σ R n) p) ν = (↑p).coeff (partWeight σ ↑ν)

The coordinates of TauCeti.partWeightCoeff are the coefficients at the sorted monomials. The body of TauCeti.partWeightCoeff is not exposed, so this is what a consumer rewrites with.

theorem TauCeti.partWeightCoeff_injective {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] : Function.Injective ⇑(partWeightCoeff σ R n)

A symmetric homogeneous polynomial is determined by its coefficients at the sorted monomials: away from them symmetry moves each coefficient to a sorted one, and away from degree n homogeneity kills it.

theorem TauCeti.partWeightCoeff_surjective {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] : Function.Surjective ⇑(partWeightCoeff σ R n)

The coefficients at the sorted monomials may be prescribed arbitrarily: the combination of the monomial symmetric polynomials with the prescribed coefficients realizes them, each m_ν being the indicator of its own sorted monomial.

theorem TauCeti.partWeightCoeff_bijective {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] : Function.Bijective ⇑(partWeightCoeff σ R n)

A symmetric homogeneous polynomial is exactly a prescription of coefficients at the sorted monomials.

The monomial basis

noncomputable def TauCeti.msymmBasis (σ : Type u_1) (R : Type u_2) [CommSemiring R] (n : ℕ) [Fintype σ] : Module.Basis { ν : n.Partition // ν.parts.card ≤ Fintype.card σ } R ↥(symmetricHomogeneousSubmodule σ R n)

The monomial basis: the coordinates of TauCeti.partWeightCoeff read as a basis of the symmetric polynomials of degree n, indexed by the partitions of n with at most Fintype.card σ parts. Its basis vectors are the monomial symmetric polynomials m_ν (TauCeti.coe_msymmBasis), which is what the name records.

Equations

• TauCeti.msymmBasis σ R n = { repr := LinearEquiv.ofBijective (TauCeti.partWeightCoeff σ R n) ⋯ }

@[simp]

theorem TauCeti.msymmBasis_repr_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] (p : ↥(symmetricHomogeneousSubmodule σ R n)) (ν : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ((msymmBasis σ R n).repr p) ν = (↑p).coeff (partWeight σ ↑ν)

The coordinates in the monomial basis are the coefficients at the sorted monomials: this is the normal form of a monomial-basis coordinate, and the elimination rule matching TauCeti.coe_msymmBasis.

@[simp]

theorem TauCeti.coe_msymmBasis {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] [DecidableEq σ] (ν : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ↑((msymmBasis σ R n) ν) = MvPolynomial.msymm σ R ↑ν

The vectors of the monomial basis are the monomial symmetric polynomials: TauCeti.msymmBasis is defined through its coordinates, and this reads its basis vectors back as the polynomials m_ν the name records.

theorem TauCeti.msymmBasis_repr_schurPoly {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} [Fintype σ] (μ : n.Partition) (ν : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ((msymmBasis σ R n).repr ⟨schurPoly σ R μ, ⋯⟩) ν = ↑(kostkaNumber μ ↑ν)

The Kostka numbers are the coordinates of a Schur polynomial in the monomial basis, which is the monomial expansion TauCeti.schurPoly_eq_sum_kostkaNumber_smul_msymm read as a change of basis. It is not a simp lemma: TauCeti.msymmBasis_repr_apply already puts a coordinate of the monomial basis into its normal form as a coefficient.

The Schur basis

noncomputable def TauCeti.schurPolyBasis (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (n : ℕ) : Module.Basis { ν : n.Partition // ν.parts.card ≤ Fintype.card σ } R ↥(symmetricHomogeneousSubmodule σ R n)

The Schur basis: the Schur polynomials s_μ, for the partitions μ of n with at most Fintype.card σ parts, are a basis of the symmetric polynomials in σ of degree n. Taken over ℤ, this is the finite-alphabet, fixed-degree form of "the Schur functions are a ℤ-basis of the symmetric functions". The basis vectors are read off by TauCeti.coe_schurPolyBasis.

A commutative ring is needed: the transition matrix from the monomial basis is the Kostka matrix, which is unitriangular and so invertible over any commutative ring, but its inverse has negative entries, and over a semiring such as ℕ the Schur polynomials do not span.

Equations

• TauCeti.schurPolyBasis σ R n = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.coe_schurPolyBasis {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (μ : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ↑((schurPolyBasis σ R n) μ) = schurPoly σ R ↑μ

The vectors of the Schur basis are the Schur polynomials: TauCeti.schurPolyBasis is produced from the invertibility of the Kostka matrix rather than from a formula, and this reads its basis vectors back as the polynomials s_μ. It is what makes the basis usable: a statement about TauCeti.schurPolyBasis becomes a statement about TauCeti.schurPoly.