Schur polynomials

The Schur polynomial s_μ of a Young diagram μ in N variables is the generating function of the semistandard Young tableaux of shape μ whose entries are drawn from the N-letter alphabet: each such tableau contributes the monomial ∏ᵢ xᵢ ^ (number of cells filled with i). This file defines it, TauCeti.diagramSchurPoly, reads off the basic structure that the definition alone gives, and transports it to the partition-indexed Schur polynomial TauCeti.schurPoly in an arbitrary finite alphabet.

The tableaux summed over are the bounded ones, TauCeti.BoundedSSYT: Mathlib's SemistandardYoungTableau μ fills cells with arbitrary natural numbers, and it is the bound that makes the sum finite. The alphabet is 0, 1, …, N - 1 rather than the classical 1, …, N, matching SemistandardYoungTableau.content.

The load-bearing statement is TauCeti.coeff_diagramSchurPoly: the coefficient of a monomial x^d in s_μ is the image in the coefficient semiring of the Kostka number K_{μ d}, the number of semistandard tableaux of shape μ and content d. Every other result here is read off it together with the Kostka theory of TauCeti.Combinatorics.Young.Kostka:

• TauCeti.diagramSchurPoly_eq_zero_iff: s_μ vanishes exactly when μ is taller than the alphabet, since columns are strict and the entry in row i is at least i.
• TauCeti.coeff_diagramSchurPoly_rowLenWeight: the coefficient at the exponent recording the row lengths of μ is 1, the highest-weight tableau being the unique one of that content.
• TauCeti.coeff_diagramSchurPoly_diagramOf_eq_zero_of_not_dominates: for partitions, the exponent recording the parts of ν occurs in s_μ only if μ dominates ν. Together with the previous item this is the triangularity of the Schur polynomials against the dominance order, and TauCeti.coeff_diagramSchurPoly_eq_zero_of_sum_lt is the partial-sum form it comes from.
• TauCeti.isHomogeneous_diagramSchurPoly: s_μ is homogeneous of degree the number of cells of μ, every tableau of shape μ having that many entries.

An arbitrary finite alphabet σ is ordered by Fintype.equivFin σ, and TauCeti.schurPoly σ R μ is TauCeti.diagramSchurPoly renamed along that ordering. The result does not depend on the ordering, but that is the symmetry of s_μ, which is not proved here: it is the Bender-Knuth involution, and it lives downstream in TauCeti.RingTheory.MvPolynomial.Symmetric.Schur.Symmetric. None of the results below need it.

Main definitions

• TauCeti.BoundedSSYT.weight: the content of a bounded tableau, packaged as an exponent vector on the alphabet.
• TauCeti.diagramSchurPoly: the Schur polynomial of a Young diagram in the alphabet Fin N.
• TauCeti.rowLenWeight: the exponent vector recording the row lengths of a shape, the exponent of the monomial contributed by the highest-weight tableau.
• TauCeti.schurPoly: the Schur polynomial of a partition in a finite alphabet.
• TauCeti.partWeight: the exponent vector on a finite alphabet recording the parts of a partition.

Main results

• TauCeti.coeff_diagramSchurPoly: the coefficients of a Schur polynomial are the images of the Kostka numbers, TauCeti.coeff_schurPoly is its form in an arbitrary finite alphabet, and TauCeti.coeff_schurPoly_partWeight reads it at the exponent of a partition.
• TauCeti.eval_diagramSchurPoly: evaluating a Schur polynomial sums the monomials of its tableaux.
• TauCeti.eval_one_diagramSchurPoly_eq_card_boundedSSYT and TauCeti.eval_one_schurPoly_eq_card_boundedSSYT: evaluating at one counts the bounded tableaux.
• TauCeti.diagramSchurPoly_eq_zero_iff and TauCeti.schurPoly_eq_zero_iff: a Schur polynomial vanishes exactly for a shape taller than its alphabet.
• TauCeti.isHomogeneous_diagramSchurPoly and TauCeti.isHomogeneous_schurPoly: a Schur polynomial is homogeneous of degree the number of cells of its shape.

References

• W. Fulton, Young Tableaux, Section 2.2.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 5.
• Schur--Weyl roadmap, Layer 7.

noncomputable def TauCeti.BoundedSSYT.weight {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : Fin N →₀ ℕ

The weight of a bounded tableau: its content, read as an exponent vector indexed by the alphabet Fin N. This is the exponent of the monomial the tableau contributes to TauCeti.diagramSchurPoly.

Equations

• T.weight = Finsupp.comapDomain Fin.val (↑T).content ⋯

@[simp]

theorem TauCeti.BoundedSSYT.weight_apply {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) (i : Fin N) : T.weight i = (↑T).content ↑i

theorem TauCeti.BoundedSSYT.mapDomain_weight {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : Finsupp.mapDomain Fin.val T.weight = (↑T).content

Extending the weight of a bounded tableau by zero recovers its content: no letter outside the alphabet occurs.

theorem TauCeti.BoundedSSYT.sum_weight {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : ∑ i : Fin N, T.weight i = μ.card

The sum of the weight of a bounded tableau of shape μ is the number of cells of μ: every cell carries exactly one letter.

theorem TauCeti.BoundedSSYT.card_weight_eq {N : ℕ} {μ : YoungDiagram} (d : Fin N →₀ ℕ) : Nat.card { T : BoundedSSYT N μ // T.weight = d } = diagramKostkaNumber μ ⇑(Finsupp.mapDomain Fin.val d)

The number of bounded tableaux of a given weight is a Kostka number.

noncomputable def TauCeti.diagramSchurPoly (N : ℕ) (R : Type u_1) [CommSemiring R] (μ : YoungDiagram) : MvPolynomial (Fin N) R

The Schur polynomial s_μ of a Young diagram μ in the N variables x₀, …, x_{N-1}: the generating function of the semistandard Young tableaux of shape μ in the alphabet {0, …, N - 1}, each contributing the monomial ∏ᵢ xᵢ ^ (number of cells filled with i).

Equations

• TauCeti.diagramSchurPoly N R μ = ∑ T : TauCeti.BoundedSSYT N μ, (MvPolynomial.monomial T.weight) 1

theorem TauCeti.diagramSchurPoly_eq_sum (N : ℕ) (R : Type u_1) [CommSemiring R] (μ : YoungDiagram) : diagramSchurPoly N R μ = ∑ T : BoundedSSYT N μ, (MvPolynomial.monomial T.weight) 1

The defining sum of a Schur polynomial, one weight monomial per bounded tableau of the shape. TauCeti.diagramSchurPoly is public, but its body is not exposed — this file's public section carries no @[expose] — so no equation lemma for it reaches a downstream module; this restatement is what such a module rewrites with.

theorem TauCeti.coeff_diagramSchurPoly {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} (d : Fin N →₀ ℕ) : (diagramSchurPoly N R μ).coeff d = ↑(diagramKostkaNumber μ ⇑(Finsupp.mapDomain Fin.val d))

The coefficients of a Schur polynomial are the Kostka numbers: the coefficient of x^d in s_μ is the image in R of the number of semistandard tableaux of shape μ whose content is d.

theorem TauCeti.eval_diagramSchurPoly {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} (y : Fin N → R) : (MvPolynomial.eval y) (diagramSchurPoly N R μ) = ∑ T : BoundedSSYT N μ, ∏ i : Fin N, y i ^ T.weight i

A Schur polynomial is the generating function of its tableaux, in the literal sense: at any family of values it is the sum, over the bounded tableaux of its shape, of the product of the values raised to the multiplicities of the corresponding letters.

@[simp]

theorem TauCeti.eval_one_diagramSchurPoly_eq_card_boundedSSYT {R : Type u_1} [CommSemiring R] (N : ℕ) (μ : YoungDiagram) : (MvPolynomial.eval fun (x : Fin N) => 1) (diagramSchurPoly N R μ) = ↑(Nat.card (BoundedSSYT N μ))

A Schur polynomial evaluated at one counts bounded semistandard tableaux. Every monomial in the tableau generating function contributes one, so the value is the cardinality of TauCeti.BoundedSSYT N μ.

theorem TauCeti.map_diagramSchurPoly {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} {S : Type u_2} [CommSemiring S] (f : R →+* S) : (MvPolynomial.map f) (diagramSchurPoly N R μ) = diagramSchurPoly N S μ

Scalars pass through a Schur polynomial: every coefficient is the cast of a natural number, namely of a Kostka number, and casts of natural numbers are preserved by semiring homomorphisms.

theorem TauCeti.diagramSchurPoly_eq_zero_of_lt_colLen {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} (h : N < μ.colLen 0) : diagramSchurPoly N R μ = 0

A Schur polynomial of a shape taller than its alphabet vanishes, there being no tableau to sum over.

@[simp]

theorem TauCeti.diagramSchurPoly_bot {N : ℕ} {R : Type u_1} [CommSemiring R] : diagramSchurPoly N R ⊥ = 1

The Schur polynomial of the empty shape is 1, the empty tableau contributing the empty monomial.

noncomputable def TauCeti.rowLenWeight (N : ℕ) (μ : YoungDiagram) : Fin N →₀ ℕ

The exponent vector on the alphabet Fin N recording the row lengths of μ: the content of the highest-weight tableau of shape μ, and the exponent of the monomial it contributes to TauCeti.diagramSchurPoly.

Equations

• TauCeti.rowLenWeight N μ = Finsupp.equivFunOnFinite.symm fun (i : Fin N) => μ.rowLen ↑i

@[simp]

theorem TauCeti.rowLenWeight_apply (N : ℕ) (μ : YoungDiagram) (i : Fin N) : (rowLenWeight N μ) i = μ.rowLen ↑i

theorem TauCeti.mapDomain_rowLenWeight {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ N) : ⇑(Finsupp.mapDomain Fin.val (rowLenWeight N μ)) = μ.rowLen

Extending the row lengths of a shape no taller than the alphabet by zero recovers them.

theorem TauCeti.coeff_diagramSchurPoly_rowLenWeight {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} (h : μ.colLen 0 ≤ N) : (diagramSchurPoly N R μ).coeff (rowLenWeight N μ) = 1

The coefficient of a Schur polynomial at the row lengths of its shape is 1: the highest-weight tableau, whose i-th row consists of is, is the unique tableau of shape μ whose content is the row lengths of μ.

theorem TauCeti.diagramSchurPoly_ne_zero {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} [Nontrivial R] (h : μ.colLen 0 ≤ N) : diagramSchurPoly N R μ ≠ 0

A Schur polynomial of a shape no taller than its alphabet is nonzero.

theorem TauCeti.diagramSchurPoly_eq_zero_iff {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} [Nontrivial R] : diagramSchurPoly N R μ = 0 ↔ N < μ.colLen 0

A Schur polynomial vanishes exactly for a shape taller than its alphabet.

theorem TauCeti.coeff_diagramSchurPoly_eq_zero_of_sum_lt {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} {d : Fin N →₀ ℕ} {k : ℕ} (h : (List.take k μ.rowLens).sum < ∑ i ∈ Finset.range k, (Finsupp.mapDomain Fin.val d) i) : (diagramSchurPoly N R μ).coeff d = 0

Triangularity of the Schur polynomials: an exponent whose partial sums overshoot those of the row lengths of μ does not occur in s_μ. For partitions this is the vanishing of s_μ outside the dominance order, TauCeti.kostkaNumber_eq_zero_of_not_dominates.

theorem TauCeti.isHomogeneous_diagramSchurPoly {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} : (diagramSchurPoly N R μ).IsHomogeneous μ.card

A Schur polynomial is homogeneous of degree the number of cells of its shape: a tableau of shape μ has one entry per cell.

theorem TauCeti.totalDegree_diagramSchurPoly {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} [Nontrivial R] (h : μ.colLen 0 ≤ N) : (diagramSchurPoly N R μ).totalDegree = μ.card

The total degree of a nonzero Schur polynomial is the number of cells of its shape.

theorem TauCeti.coeff_diagramSchurPoly_diagramOf {N : ℕ} {R : Type u_1} [CommSemiring R] {n : ℕ} (μ ν : n.Partition) (h : (diagramOf ν).colLen 0 ≤ N) : (diagramSchurPoly N R (diagramOf μ)).coeff (rowLenWeight N (diagramOf ν)) = ↑(kostkaNumber μ ν)

The coefficients of a Schur polynomial are the Kostka numbers of partitions: the coefficient of s_μ at the exponent recording the parts of ν is the image in R of K_{μν}. The row bound is what makes the exponent record all of ν: an alphabet shorter than the number of parts of ν would truncate it.

theorem TauCeti.coeff_diagramSchurPoly_diagramOf_eq_zero_of_not_dominates {N : ℕ} {R : Type u_1} [CommSemiring R] {n : ℕ} (μ ν : n.Partition) (hd : ¬Dominates μ ν) : (diagramSchurPoly N R (diagramOf μ)).coeff (rowLenWeight N (diagramOf ν)) = 0

The Schur polynomials are triangular for the dominance order: the exponent recording the parts of ν occurs in s_μ only if μ dominates ν. No row bound is needed: an alphabet too short to record all of ν truncates the exponent to one of degree less than n, where s_μ vanishes by homogeneity.

noncomputable def TauCeti.schurPoly (σ : Type u_3) [Fintype σ] (R : Type u_4) [CommSemiring R] {n : ℕ} (μ : n.Partition) : MvPolynomial σ R

The Schur polynomial s_μ of a partition μ in the finite alphabet σ: the Schur polynomial TauCeti.diagramSchurPoly of the Young diagram of μ in the alphabet Fin (Fintype.card σ), renamed along the ordering Fintype.equivFin σ of σ. The ordering does not matter, s_μ being symmetric (TauCeti.schurPoly_isSymmetric, proved downstream).

Equations

• TauCeti.schurPoly σ R μ = (MvPolynomial.rename ⇑(Fintype.equivFin σ).symm) (TauCeti.diagramSchurPoly (Fintype.card σ) R (TauCeti.diagramOf μ))

theorem TauCeti.schurPoly_eq_rename {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) : schurPoly σ R μ = (MvPolynomial.rename ⇑(Fintype.equivFin σ).symm) (diagramSchurPoly (Fintype.card σ) R (diagramOf μ))

The Schur polynomial of a partition is the Schur polynomial of its Young diagram, renamed along the chosen ordering of the alphabet. As for TauCeti.diagramSchurPoly_eq_sum, the body of TauCeti.schurPoly is not exposed outside this module, so this restatement is what a downstream module rewrites with.

@[simp]

theorem TauCeti.eval_one_schurPoly_eq_card_boundedSSYT {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) : (MvPolynomial.eval fun (x : σ) => 1) (schurPoly σ R μ) = ↑(Nat.card (BoundedSSYT (Fintype.card σ) (diagramOf μ)))

A Schur polynomial evaluated at one counts bounded semistandard tableaux: the value of s_μ at the all-ones point of the alphabet σ is the number of semistandard tableaux of shape μ with entries below the number of letters of σ.

noncomputable def TauCeti.partWeight (σ : Type u_3) [Fintype σ] {n : ℕ} (ν : n.Partition) : σ →₀ ℕ

The exponent vector on the alphabet σ recording the parts of ν, read through the ordering Fintype.equivFin σ: the image of TauCeti.rowLenWeight of the Young diagram of ν.

Equations

• TauCeti.partWeight σ ν = Finsupp.mapDomain (⇑(Fintype.equivFin σ).symm) (TauCeti.rowLenWeight (Fintype.card σ) (TauCeti.diagramOf ν))

@[simp]

theorem TauCeti.partWeight_apply {σ : Type u_2} [Fintype σ] {n : ℕ} (ν : n.Partition) (x : σ) : (partWeight σ ν) x = (diagramOf ν).rowLen ↑((Fintype.equivFin σ) x)

theorem TauCeti.coeff_schurPoly_mapDomain {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) (d : Fin (Fintype.card σ) →₀ ℕ) : (schurPoly σ R μ).coeff (Finsupp.mapDomain (⇑(Fintype.equivFin σ).symm) d) = ↑(diagramKostkaNumber (diagramOf μ) ⇑(Finsupp.mapDomain Fin.val d))

The coefficients of a Schur polynomial in a finite alphabet are the Kostka numbers: at the exponent obtained from d by the ordering of the alphabet, the coefficient of s_μ is the image in R of the Kostka number of μ and the content that d extends to by zero.

theorem TauCeti.coeff_schurPoly {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) (d : σ →₀ ℕ) : (schurPoly σ R μ).coeff d = ↑(diagramKostkaNumber (diagramOf μ) ⇑(Finsupp.mapDomain (fun (x : σ) => ↑((Fintype.equivFin σ) x)) d))

The coefficients of a Schur polynomial in a finite alphabet are the Kostka numbers: the coefficient of s_μ at an arbitrary exponent d is the image in R of the Kostka number of μ and the content obtained from d by numbering the alphabet with Fintype.equivFin.

theorem TauCeti.coeff_schurPoly_partWeight {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ ν : n.Partition) (h : (diagramOf ν).colLen 0 ≤ Fintype.card σ) : (schurPoly σ R μ).coeff (partWeight σ ν) = ↑(kostkaNumber μ ν)

The coefficient of a Schur polynomial at a partition is a Kostka number: the coefficient of s_μ at the exponent recording the parts of ν is the image in R of K_{μν}. The row bound is what makes the exponent record all of ν: an alphabet with fewer letters than ν has parts would truncate the record.

theorem TauCeti.coeff_schurPoly_partWeight_eq_zero_of_not_dominates {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ ν : n.Partition) (hd : ¬Dominates μ ν) : (schurPoly σ R μ).coeff (partWeight σ ν) = 0

Schur polynomials are triangular for dominance: the exponent recording the parts of ν occurs in s_μ only if μ dominates ν. No row bound needed: an alphabet too short to record all of ν truncates the exponent to degree less than n, where s_μ vanishes by homogeneity.

theorem TauCeti.map_schurPoly {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) {S : Type u_3} [CommSemiring S] (f : R →+* S) : (MvPolynomial.map f) (schurPoly σ R μ) = schurPoly σ S μ

Scalars pass through a Schur polynomial: every coefficient is the cast of a natural number, namely of a Kostka number, and casts of natural numbers are preserved by semiring homomorphisms.

@[simp]

theorem TauCeti.schurPoly_partition_zero {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] (p : Nat.Partition 0) : schurPoly σ R p = 1

The Schur polynomial of the partition of 0 is 1, its Young diagram being empty and the empty tableau contributing the empty monomial.

theorem TauCeti.schurPoly_eq_zero_iff {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {n : ℕ} (μ : n.Partition) [Nontrivial R] : schurPoly σ R μ = 0 ↔ Fintype.card σ < (diagramOf μ).colLen 0

A Schur polynomial vanishes exactly for a partition with more parts than the alphabet has letters.

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

A Schur polynomial is homogeneous of degree the natural number its partition partitions: a tableau of that shape has one entry per cell.