Schur polynomials are symmetric

A Schur polynomial is the generating function of the semistandard tableaux of its shape, one monomial per tableau, the exponent of xᵢ being how often the letter i occurs. Nothing in that description is symmetric in the letters: the tableaux are ordered objects, and the alphabet {0, …, N - 1} enters TauCeti.diagramSchurPoly through the row-weak and column-strict conditions. Symmetry is a theorem, and this file proves it.

The mechanism is the Bender-Knuth involution of TauCeti.Combinatorics.Young.BenderKnuth: for each letter v it is a bijection of the tableaux of a fixed shape which exchanges how often v and v + 1 occur and fixes every other multiplicity (SemistandardYoungTableau.content_benderKnuth). Reindexing the defining sum along it therefore exchanges the variables x_v and x_{v+1}, which is TauCeti.rename_swap_diagramSchurPoly. Adjacent transpositions generate the symmetric group (Equiv.Perm.mclosure_swap_castSucc_succ), so this one exchange gives the whole symmetry, TauCeti.isSymmetric_diagramSchurPoly.

The involution moves only the letters v and v + 1, so it preserves the alphabet only when both of them belong to it; that is why the exchanged variables are given as a pair a, b : Fin N with (b : ℕ) = a + 1 rather than as an arbitrary pair of letters. Exchanging two letters that are not adjacent is not a Bender-Knuth move, and is obtained here only through the group generated by the adjacent ones.

Symmetry is what makes TauCeti.schurPoly independent of the ordering of its alphabet, so it also retro-justifies the definition of TauCeti.schurPoly on an arbitrary finite alphabet by an arbitrary choice of ordering, and it places the Schur polynomials in MvPolynomial.symmetricSubalgebra, where the elementary and complete homogeneous symmetric polynomials they generalize already live.

Main results

• TauCeti.rename_swap_diagramSchurPoly: a Schur polynomial is unchanged by exchanging two adjacent variables.
• TauCeti.isSymmetric_diagramSchurPoly and TauCeti.schurPoly_isSymmetric: Schur polynomials are symmetric.
• TauCeti.schurPoly_mem_symmetricSubalgebra: the same, read in MvPolynomial.symmetricSubalgebra.

References

• R. P. Stanley, Enumerative Combinatorics, Volume 2, §7.10, Theorem 7.10.2: the skew Schur function is symmetric, proved by the same reduction to interchanging xᵢ and x_{i+1}. The involution is that of E. A. Bender and D. E. Knuth, Enumeration of plane partitions, J. Combinatorial Theory 13 (1972), 40--54.
• W. Fulton, Young Tableaux, Section 2.2.
• Schur--Weyl roadmap, Layer 7.

def TauCeti.BoundedSSYT.benderKnuth {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) {a b : Fin N} (hab : ↑b = ↑a + 1) : BoundedSSYT N μ

The Bender-Knuth involution on bounded tableaux, exchanging two adjacent letters a and b of the alphabet. Adjacency is what keeps the alphabet: the involution writes no letter other than the ones already present and the two it exchanges.

Equations

• T.benderKnuth hab = ⟨(↑T).benderKnuth ↑a, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.benderKnuth_benderKnuth {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) {a b : Fin N} (hab : ↑b = ↑a + 1) : (T.benderKnuth hab).benderKnuth hab = T

theorem TauCeti.BoundedSSYT.benderKnuth_involutive (N : ℕ) (μ : YoungDiagram) {a b : Fin N} (hab : ↑b = ↑a + 1) : Function.Involutive fun (T : BoundedSSYT N μ) => T.benderKnuth hab

theorem TauCeti.BoundedSSYT.weight_benderKnuth {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) {a b : Fin N} (hab : ↑b = ↑a + 1) (i : Fin N) : (T.benderKnuth hab).weight i = T.weight ((Equiv.swap a b) i)

The Bender-Knuth involution exchanges two adjacent letters, read on the weight of a bounded tableau.

theorem TauCeti.BoundedSSYT.mapDomain_weight_swap {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) {a b : Fin N} (hab : ↑b = ↑a + 1) : Finsupp.mapDomain (⇑(Equiv.swap a b)) T.weight = (T.benderKnuth hab).weight

The weight of the Bender-Knuth image of a tableau, as the transported weight.

theorem TauCeti.rename_swap_diagramSchurPoly {N : ℕ} (R : Type u_2) [CommSemiring R] (μ : YoungDiagram) {a b : Fin N} (hab : ↑b = ↑a + 1) : (MvPolynomial.rename ⇑(Equiv.swap a b)) (diagramSchurPoly N R μ) = diagramSchurPoly N R μ

A Schur polynomial is unchanged by exchanging two adjacent variables: the Bender-Knuth involution at the corresponding letter reindexes the sum of monomials defining it.

theorem TauCeti.isSymmetric_diagramSchurPoly (N : ℕ) (R : Type u_2) [CommSemiring R] (μ : YoungDiagram) : (diagramSchurPoly N R μ).IsSymmetric

Schur polynomials are symmetric. Adjacent transpositions generate the symmetric group, so the single exchange TauCeti.rename_swap_diagramSchurPoly supplied by the Bender-Knuth involution gives the whole symmetry.

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

Schur polynomials are symmetric, on an arbitrary finite alphabet. This is what makes TauCeti.schurPoly independent of the ordering of the alphabet chosen to define it.

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

Schur polynomials are symmetric, read as membership in MvPolynomial.symmetricSubalgebra, where the elementary and complete homogeneous symmetric polynomials they generalize already live.