Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

6.3 Schur polynomials

6.3.1 Alternants

We work over a fixed positive integer \(N\) and the polynomial ring \(\mathcal{P} = \mathbb {Z}[x_1, x_2, \ldots , x_N]\). An \(N\)-partition is a weakly decreasing \(N\)-tuple \(\lambda = (\lambda _1, \lambda _2, \ldots , \lambda _N) \in \mathbb {N}^N\) with \(\lambda _1 \geq \lambda _2 \geq \cdots \geq \lambda _N\).

Definition 6.85
#

(a) We let \(\rho \) be the \(N\)-tuple \(\left( N-1,N-2,\ldots ,N-N\right) \in \mathbb {N}^{N}\).

(b) For any \(N\)-tuple \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{N}\right) \in \mathbb {N}^{N}\), we define

\[ a_{\alpha }:=\det \left( \underbrace{\left( x_{i}^{\alpha _{j}}\right) _{1\leq i\leq N,\ 1\leq j\leq N}}_{\in \mathcal{P}^{N\times N}}\right) \in \mathcal{P}. \]

This is called the \(\alpha \)-alternant (of \(x_{1},x_{2},\ldots ,x_{N}\)).

noncomputable abbrev alternant {R : Type u_1} [CommRing R] (N : ) (α : Fin N) :
Lemma 6.86

The \(\rho \) vector is strictly decreasing: if \(i {\lt} j\) (as indices in \(\{ 0, 1, \ldots , N{-}1\} \)), then \(\rho _i {\gt} \rho _j\).

Proof

Immediate from \(\rho _i = N - 1 - i\).

Lemma 6.87

The sum of the \(\rho \) vector equals the triangular number:

\[ \sum _{i=0}^{N-1} \rho _i = \frac{N(N-1)}{2}. \]
theorem rhoVector_sum (N : ) :
i : Fin N, rhoVector N i = N * (N - 1) / 2
Proof

Follows from \(\sum _{i=0}^{N-1}(N-1-i) = \sum _{k=0}^{N-1} k = N(N-1)/2\).

Definition 6.88
#

The \(\rho \) vector \((N{-}1, N{-}2, \ldots , 0)\) is itself an \(N\)-partition (since it is strictly decreasing, hence weakly decreasing).

Theorem 6.89

We have \(a_\rho = \prod _{1 \le i {\lt} j \le N}(x_i - x_j)\).

theorem alternant_rho_eq_vandermonde (N : ) [NeZero N] {R : Type u_1} [CommRing R] :
alternant N (rhoVector N) = i : Fin N, j : Fin N with j > i, (MvPolynomial.X i - MvPolynomial.X j)
Proof

This is the classical Vandermonde determinant identity. The matrix for \(a_\rho \) has entry \((i,j)\) equal to \(x_i^{N-j}\), and its determinant equals \(\prod _{i{\lt}j}(x_i - x_j)\) by the Vandermonde formula.

Lemma 6.90

Let \(\alpha \in \mathbb {N}^{N}\).

(a) If the \(N\)-tuple \(\alpha \) has two equal entries, then \(a_{\alpha }=0\).

(b) Let \(\beta \in \mathbb {N}^{N}\) be an \(N\)-tuple obtained from \(\alpha \) by swapping two entries. Then, \(a_{\beta }=-a_{\alpha }\).

theorem alternant_zero_of_eq (N : ) {R : Type u_2} [CommRing R] {α : Fin N} (i j : Fin N) (hij : i j) (heq : α i = α j) :
alternant N α = 0
theorem alternant_swap (N : ) {R : Type u_2} [CommRing R] {α : Fin N} (i j : Fin N) (hij : i j) :
alternant N (α (Equiv.swap i j)) = -alternant N α
Proof

(a) If \(\alpha _i = \alpha _j\), then two columns of the matrix \((x_k^{\alpha _\ell })\) are equal, so its determinant is \(0\).

(b) Swapping entries \(\alpha _i\) and \(\alpha _j\) amounts to permuting two columns of the matrix by a transposition, which multiplies the determinant by \(-1\).

6.3.2 Young diagrams and Schur polynomials

Definition 6.91
#

Let \(\lambda \) be an \(N\)-partition.

The Young diagram of \(\lambda \) is defined as the set

\[ \left\{ \left( i,j\right) \ \mid \ i\in \left[ N\right] \text{ and }j\in \left[ \lambda _{i}\right] \right\} \subseteq \left\{ 1,2,3,\ldots \right\} ^{2}. \]

We visually represent each element \(\left( i,j\right) \) of this Young diagram as a box in row \(i\) and column \(j\).

We denote the Young diagram of \(\lambda \) by \(Y\left( \lambda \right) \).

Lemma 6.92

A cell \((i,j)\) belongs to \(Y(\lambda )\) if and only if \(j {\lt} \lambda _i\).

theorem NPartition.mem_youngDiagram {N : } {μ : NPartition N} {c : Fin N × } :
c μ.youngDiagram c.2 < μ.parts c.1
Proof

Immediate from the definition.

Definition 6.93
#

Let \(\lambda \) be an \(N\)-partition.

A Young tableau of shape \(\lambda \) means a way of filling the boxes of \(Y\left( \lambda \right) \) with elements of \(\left[ N\right] \) (one element per box). Formally speaking, it is defined as a map \(T:Y\left( \lambda \right) \rightarrow \left[ N\right] \).

structure YoungTableau {N : } [NeZero N] (lam : NPartition N) :
Definition 6.94
#

Let \(\lambda \) be an \(N\)-partition.

A Young tableau \(T\) of shape \(\lambda \) is said to be semistandard if its entries

  • increase weakly along each row (from left to right);

  • increase strictly down each column (from top to bottom).

Formally speaking, this means that a Young tableau \(T:Y\left( \lambda \right) \rightarrow \left[ N\right] \) is semistandard if and only if

  • we have \(T\left( i,j\right) \leq T\left( i,j+1\right) \) for any \(\left( i,j\right) \in Y\left( \lambda \right) \) satisfying \(\left( i,j+1\right) \in Y\left( \lambda \right) \);

  • we have \(T\left( i,j\right) {\lt}T\left( i+1,j\right) \) for any \(\left( i,j\right) \in Y\left( \lambda \right) \) satisfying \(\left( i+1,j\right) \in Y\left( \lambda \right) \).

We let \(\operatorname *{SSYT}\left( \lambda \right) \) denote the set of all semistandard Young tableaux of shape \(\lambda \).

structure SSYT {N : } [NeZero N] (lam : NPartition N) extends YoungTableau lam :
Lemma 6.95

Let \(T\) be a semistandard Young tableau of shape \(\lambda \). If \((i, j_1)\) and \((i, j_2)\) are cells of \(Y(\lambda )\) with \(j_1 \le j_2\), then \(T(i,j_1) \le T(i,j_2)\).

theorem SSYT.row_weak_of_le {N : } [NeZero N] {lam : NPartition N} (T : SSYT lam) {i : Fin N} {j₁ j₂ : } (h : (i, j₂) lam.youngDiagram) (hle : j₁ j₂) :
T.entry (i, j₁) T.entry (i, j₂)
Proof

If \(j_1 = j_2\) the claim is trivial; otherwise \(j_1 {\lt} j_2\) and we apply the row-weak condition.

Lemma 6.96

Let \(T\) be a semistandard Young tableau of shape \(\lambda \). If \((i_1, j)\) and \((i_2, j)\) are cells of \(Y(\lambda )\) with \(i_1 \le i_2\), then \(T(i_1,j) \le T(i_2,j)\).

theorem SSYT.col_weak {N : } [NeZero N] {lam : NPartition N} (T : SSYT lam) {i₁ i₂ : Fin N} {j : } (h : (i₂, j) lam.youngDiagram) (hle : i₁ i₂) :
T.entry (i₁, j) T.entry (i₂, j)
Proof

If \(i_1 = i_2\) the claim is trivial; otherwise \(i_1 {\lt} i_2\) and \(T(i_1,j) {\lt} T(i_2,j)\) by column-strictness.

Lemma 6.97

In a semistandard tableau \(T\) of shape \(\lambda \), we have \(T(i,j) \ge i\) for every cell \((i,j) \in Y(\lambda )\).

theorem SSYT.entry_ge_row {N : } [NeZero N] {lam : NPartition N} (T : SSYT lam) (i : Fin N) {j : } (h : (i, j) lam.youngDiagram) :
i (T.entry (i, j))
Proof

By induction on \(i\). For \(i = 0\), this holds since entries are nonneg. For the inductive step, column-strictness gives \(T(i, j) {\gt} T(i{-}1, j) \ge i{-}1\), so \(T(i,j) \ge i\).

Lemma 6.98

For any \(N\)-partition \(\lambda \), the tableau that fills every cell \((i,j)\) with the value \(i\) is semistandard. This is called the highest weight tableau.

def SSYT.highestWeight {N : } [NeZero N] (lam : NPartition N) :
SSYT lam
Proof

Row-weakness holds because each row is constant. Column-strictness holds because entry values equal row indices, which are strictly increasing down columns.

Lemma 6.99

The highest weight tableau achieves the minimum possible entry at each cell: for any semistandard tableau \(T\) of shape \(\lambda \) and any cell \(c \in Y(\lambda )\), the entry of the highest weight tableau at \(c\) is \(\le T(c)\).

theorem SSYT.highestWeight_entry_le {N : } [NeZero N] {lam : NPartition N} (T : SSYT lam) (c : Fin N × ) (h : c lam.youngDiagram) :
Proof

The highest weight entry at \((i,j)\) is \(i\), and by Lemma 6.97, \(T(i,j) \ge i\).

Lemma 6.100

The size of a Young tableau (the number of cells in \(Y(\lambda )\)) equals \(\sum _{i=1}^{N} \lambda _i\).

theorem YoungTableau.size_eq_sum_parts {N : } [NeZero N] {lam : NPartition N} (T : YoungTableau lam) :
T.size = i : Fin N, lam.parts i
Proof

The Young diagram is the disjoint union of rows, and row \(i\) has \(\lambda _i\) cells.

Definition 6.101
#

Let \(\lambda \) be an \(N\)-partition. If \(T\) is any Young tableau of shape \(\lambda \), then we define the corresponding monomial

\[ x_{T}:=\prod _{c\text{ is a box of }Y\left( \lambda \right) }x_{T\left( c\right) }=\prod _{\left( i,j\right) \in Y\left( \lambda \right) }x_{T\left( i,j\right) }=\prod _{k=1}^{N}x_{k}^{\left( \text{\# of times }k\text{ appears in }T\right) }. \]
Lemma 6.102

For any Young tableau \(T\) of shape \(\lambda \),

\[ x_T = \prod _{k=1}^{N} x_k^{(\text{occurrences of } k \text{ in } T)}. \]
Proof

Reindex the product over cells by partitioning according to the entry value.

Definition 6.103
#

Let \(\lambda \) be an \(N\)-partition. We define the Schur polynomial \(s_{\lambda }\in \mathcal{P}\) by

\[ s_{\lambda }:=\sum _{T\in \operatorname *{SSYT}\left( \lambda \right) }x_{T}. \]

6.3.3 Examples of Schur polynomials

Theorem 6.104

The Schur polynomial \(s_{(n,0,\ldots ,0)}\) equals the complete homogeneous symmetric polynomial \(h_n\):

\[ s_{(n,0,\ldots ,0)} = h_n = \sum _{i_1 \le i_2 \le \cdots \le i_n} x_{i_1} x_{i_2} \cdots x_{i_n}. \]
theorem schurPoly_row_eq_h (N : ) [NeZero N] [DecidableEq (Fin N)] (n : ) (lam : NPartition N) (hlam : lam.parts 0 = n ∀ (i : Fin N), i 0lam.parts i = 0) :
Proof

For a single-row partition \((n,0,\ldots ,0)\), the Young diagram has \(n\) cells in row 0. An SSYT filling is a weakly increasing sequence of \(n\) elements from \([N]\), which corresponds bijectively to a multiset of size \(n\). The monomials correspond under this bijection, so the sums are equal.

Theorem 6.105

The Schur polynomial \(s_{(1^n, 0^{N-n})}\) (with \(n\) ones followed by zeros) equals the elementary symmetric polynomial \(e_n\):

\[ s_{(1,1,\ldots ,1,0,\ldots ,0)} = e_n = \sum _{i_1 {\lt} i_2 {\lt} \cdots {\lt} i_n} x_{i_1} x_{i_2} \cdots x_{i_n}. \]
theorem schurPoly_col_eq_e (N : ) [NeZero N] (n : ) (hn : n N) (lam : NPartition N) (hlam : (∀ (i : Fin N), i < nlam.parts i = 1) ∀ (i : Fin N), i nlam.parts i = 0) :
Proof

For a single-column partition \((1^n)\), the Young diagram has \(n\) cells in column 0. An SSYT filling assigns strictly increasing values (by column-strictness), which corresponds bijectively to an \(n\)-element subset of \([N]\). The monomials match under this bijection.

Theorem 6.106

For \(N \ge 2\), the Schur polynomial \(s_{(2,1,0,\ldots ,0)}\) equals \(e_2 \cdot e_1 - e_3\).

theorem schurPoly_21_eq (N : ) [NeZero N] [DecidableEq (Fin N)] (hN : 2 N) (lam : NPartition N) (hlam : lam.parts 0 = 2 lam.parts 1, = 1 ∀ (i : Fin N), 2 ilam.parts i = 0) :
Proof

The Young diagram of \((2,1)\) has three cells: \((0,0)\), \((0,1)\), \((1,0)\). An SSYT filling assigns values \((i, j, k)\) with \(i \le j\) and \(i {\lt} k\). Summing \(x_i x_j x_k\) over all such triples and comparing with the expansion \(e_2 \cdot e_1 = 3 e_3 + \sum _{a{\lt}b} x_a^2 x_b + \sum _{a{\lt}b} x_a x_b^2\) yields the result.

6.3.4 Symmetry of Schur polynomials

Theorem 6.107

Let \(\lambda \) be an \(N\)-partition. Then:

(a) The polynomial \(s_{\lambda }\) is symmetric.

(b) We have

\[ a_{\lambda +\rho }=a_{\rho }\cdot s_{\lambda }. \]

Here, the addition on \(\mathbb {N}^{N}\) is defined entrywise.

theorem schurPoly_isSymmetric {N : } [NeZero N] (lam : NPartition N) (σ : Equiv.Perm (Fin N)) :
theorem alternant_eq_rho_mul_schur {N : } [NeZero N] (lam : NPartition N) :
(alternant N fun (i : Fin N) => lam.parts i + rhoVector N i) = alternant N (rhoVector N) * schurPoly lam
Proof

(a) This follows from Theorem 6.127 applied to \(\mu = \mathbf{0}\), since \(s_{\lambda /\mathbf{0}} = s_\lambda \). The proof of Theorem 6.127 uses Bender–Knuth involutions.

(b) The proof uses Stembridge’s Lemma applied to \(\mu = 0\) and \(\nu = 0\). The only \(0\)-Yamanouchi semistandard tableau of shape \(\lambda \) is the highest weight tableau \(T_0\) (where each row \(i\) contains only \(i\)’s). The content of \(T_0\) equals \(\lambda \), so the result reduces to \(a_\rho \cdot s_\lambda = a_{\lambda + \rho }\).

6.3.5 Skew Young diagrams and skew Schur polynomials

Definition 6.108
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions.

We say that \(\mu \subseteq \lambda \) if and only if \(Y\left( \mu \right) \subseteq Y\left( \lambda \right) \). Equivalently, \(\mu \subseteq \lambda \) if and only if

\[ \text{each }i\in \left[ N\right] \text{ satisfies }\mu _{i}\leq \lambda _{i}. \]

Thus we have defined a partial order \(\subseteq \) on the set of all \(N\)-partitions.

instance NPartition.instLE {N : } :
Lemma 6.109

We have \(\mu \le \lambda \) if and only if \(Y(\mu ) \subseteq Y(\lambda )\).

Proof

\((\Rightarrow )\): If \(\mu _i \le \lambda _i\) for all \(i\) and \((i,j) \in Y(\mu )\) (i.e. \(j {\lt} \mu _i\)), then \(j {\lt} \lambda _i\), so \((i,j) \in Y(\lambda )\). \((\Leftarrow )\): If \(\mu _i {\gt} \lambda _i\) for some \(i\), then \((i, \lambda _i) \in Y(\mu ) \setminus Y(\lambda )\).

Definition 6.110
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions such that \(\mu \subseteq \lambda \). Then, we define the skew Young diagram \(Y\left( \lambda /\mu \right) \) to be the set difference

\begin{align*} Y\left( \lambda \right) \setminus Y\left( \mu \right) & =\left\{ \left( i,j\right) \ \mid \ i\in \left[ N\right] \text{ and }j\in \left[ \lambda _{i}\right] \setminus \left[ \mu _{i}\right] \right\} \\ & =\left\{ \left( i,j\right) \ \mid \ i\in \left[ N\right] \text{ and }j\in \mathbb {Z}\text{ and }\mu _{i}{\lt}j\leq \lambda _{i}\right\} . \end{align*}
Lemma 6.111

A cell \((i,j)\) belongs to \(Y(\lambda /\mu )\) if and only if \(\mu _i \le j {\lt} \lambda _i\) (in 0-indexed coordinates).

theorem mem_skewYoungDiagram {N : } [NeZero N] {lam mu : NPartition N} {c : Fin N × } :
c skewYoungDiagram lam mu mu.parts c.1 c.2 c.2 < lam.parts c.1
Proof

Follows from the definition \(Y(\lambda /\mu ) = Y(\lambda ) \setminus Y(\mu )\) and the membership characterization of Young diagrams.

Lemma 6.112

The skew Young diagram \(Y(\lambda /\mathbf{0})\) equals the full Young diagram \(Y(\lambda )\).

Proof

Since \(\mathbf{0}_i = 0\) for all \(i\), the condition \(\mu _i \le j\) is automatic, and the skew diagram reduces to the full diagram.

Lemma 6.113 Convexity of skew Young diagrams

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions such that \(\mu \subseteq \lambda \). Let \(\left( a,b\right) \) and \(\left( e,f\right) \) be two elements of \(Y\left( \lambda /\mu \right) \). Let \(\left( c,d\right) \in \mathbb {Z}^{2}\) satisfy \(a\leq c\leq e\) and \(b\leq d\leq f\). Then, \(\left( c,d\right) \in Y\left( \lambda /\mu \right) \).

theorem skewYoungDiagram_convex {N : } [NeZero N] {lam mu : NPartition N} {a e : Fin N} {b f : } (hab : (a, b) skewYoungDiagram lam mu) (hef : (e, f) skewYoungDiagram lam mu) {c : Fin N} {d : } (hac : a c) (hce : c e) (hbd : b d) (hdf : d f) :
Proof

We need \(\mu _c \le d\) and \(d {\lt} \lambda _c\). Since \(\mu \) is weakly decreasing and \(a \le c\), we have \(\mu _c \le \mu _a \le b \le d\). Since \(\lambda \) is weakly decreasing and \(c \le e\), we have \(d \le f {\lt} \lambda _e \le \lambda _c\).

Definition 6.114
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions such that \(\mu \subseteq \lambda \). A Young tableau of shape \(\lambda /\mu \) means a way of filling the boxes of \(Y\left( \lambda /\mu \right) \) with elements of \(\left[ N\right] \) (one element per box). Formally speaking, it is defined as a map \(T:Y\left( \lambda /\mu \right) \rightarrow \left[ N\right] \).

Young tableaux of shape \(\lambda /\mu \) are often called skew Young tableaux.

If we don’t have \(\mu \subseteq \lambda \), then we agree that there are no Young tableaux of shape \(\lambda /\mu \).

structure SkewYoungTableau {N : } [NeZero N] (lam mu : NPartition N) :
  • entry : Fin N × Fin N

    The filling function T : Y(λ/μ) → [N]

  • support (c : Fin N × ) : cskewYoungDiagram lam muself.entry c = 0

    The entry is only meaningful for cells in the skew diagram

Definition 6.115
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions.

A Young tableau \(T\) of shape \(\lambda /\mu \) is said to be semistandard if its entries

  • increase weakly along each row (from left to right);

  • increase strictly down each column (from top to bottom).

Formally speaking, this means that a Young tableau \(T:Y\left( \lambda /\mu \right) \rightarrow \left[ N\right] \) is semistandard if and only if

  • we have \(T\left( i,j\right) \leq T\left( i,j+1\right) \) for any \(\left( i,j\right) \in Y\left( \lambda /\mu \right) \) satisfying \(\left( i,j+1\right) \in Y\left( \lambda /\mu \right) \);

  • we have \(T\left( i,j\right) {\lt}T\left( i+1,j\right) \) for any \(\left( i,j\right) \in Y\left( \lambda /\mu \right) \) satisfying \(\left( i+1,j\right) \in Y\left( \lambda /\mu \right) \).

We let \(\operatorname *{SSYT}\left( \lambda /\mu \right) \) denote the set of all semistandard Young tableaux of shape \(\lambda /\mu \).

structure SkewSSYT {N : } [NeZero N] (lam mu : NPartition N) extends SkewYoungTableau lam mu :
Lemma 6.116

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. Let \(T\) be a semistandard Young tableau of shape \(\lambda /\mu \). Then:

(a) If \(\left( i,j_{1}\right) \) and \(\left( i,j_{2}\right) \) are two elements of \(Y\left( \lambda /\mu \right) \) satisfying \(j_{1}\leq j_{2}\), then \(T\left( i,j_{1}\right) \leq T\left( i,j_{2}\right) \).

(b) If \(\left( i_{1},j\right) \) and \(\left( i_{2},j\right) \) are two elements of \(Y\left( \lambda /\mu \right) \) satisfying \(i_{1}\leq i_{2}\), then \(T\left( i_{1},j\right) \leq T\left( i_{2},j\right) \).

(c) If \(\left( i_{1},j\right) \) and \(\left( i_{2},j\right) \) are two elements of \(Y\left( \lambda /\mu \right) \) satisfying \(i_{1}{\lt}i_{2}\), then \(T\left( i_{1},j\right) {\lt}T\left( i_{2},j\right) \).

(d) If \(\left( i_{1},j_{1}\right) \) and \(\left( i_{2},j_{2}\right) \) are two elements of \(Y\left( \lambda /\mu \right) \) satisfying \(i_{1}\leq i_{2}\) and \(j_{1}\leq j_{2}\), then \(T\left( i_{1},j_{1}\right) \leq T\left( i_{2},j_{2}\right) \).

(e) If \(\left( i_{1},j_{1}\right) \) and \(\left( i_{2},j_{2}\right) \) are two elements of \(Y\left( \lambda /\mu \right) \) satisfying \(i_{1}{\lt}i_{2}\) and \(j_{1}\leq j_{2}\), then \(T\left( i_{1},j_{1}\right) {\lt}T\left( i_{2},j_{2}\right) \).

theorem SkewSSYT.row_weak_of_le {N : } [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) {i : Fin N} {j₁ j₂ : } (h1 : (i, j₁) skewYoungDiagram lam mu) (h2 : (i, j₂) skewYoungDiagram lam mu) (hle : j₁ j₂) :
T.entry (i, j₁) T.entry (i, j₂)
theorem SkewSSYT.col_weak {N : } [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) {i₁ i₂ : Fin N} {j : } (h1 : (i₁, j) skewYoungDiagram lam mu) (h2 : (i₂, j) skewYoungDiagram lam mu) (hle : i₁ i₂) :
T.entry (i₁, j) T.entry (i₂, j)
theorem SkewSSYT.col_strict_of_lt {N : } [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) {i₁ i₂ : Fin N} {j : } (h1 : (i₁, j) skewYoungDiagram lam mu) (h2 : (i₂, j) skewYoungDiagram lam mu) (hlt : i₁ < i₂) :
T.entry (i₁, j) < T.entry (i₂, j)
theorem SkewSSYT.monotone {N : } [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) {i₁ i₂ : Fin N} {j₁ j₂ : } (h1 : (i₁, j₁) skewYoungDiagram lam mu) (h2 : (i₂, j₂) skewYoungDiagram lam mu) (hi : i₁ i₂) (hj : j₁ j₂) :
T.entry (i₁, j₁) T.entry (i₂, j₂)
theorem SkewSSYT.strict_monotone {N : } [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) {i₁ i₂ : Fin N} {j₁ j₂ : } (h1 : (i₁, j₁) skewYoungDiagram lam mu) (h2 : (i₂, j₂) skewYoungDiagram lam mu) (hi : i₁ < i₂) (hj : j₁ j₂) :
T.entry (i₁, j₁) < T.entry (i₂, j₂)
Proof

(a) If \(j_1 = j_2\) the claim is trivial; otherwise apply row-weakness.

(b) If \(i_1 = i_2\) the claim is trivial; otherwise \(T(i_1,j) {\lt} T(i_2,j)\) by column-strictness.

(c) This is just the column-strict condition.

(d) By convexity (Lemma 6.113), \((i_2, j_1) \in Y(\lambda /\mu )\). Then \(T(i_1, j_1) \le T(i_2, j_1) \le T(i_2, j_2)\) using parts (b) and (a).

(e) Similarly, \((i_2, j_1) \in Y(\lambda /\mu )\) by convexity. Then \(T(i_1, j_1) {\lt} T(i_2, j_1) \le T(i_2, j_2)\) using parts (c) and (a).

Definition 6.117
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. If \(T\) is any Young tableau of shape \(\lambda /\mu \), then we define the corresponding monomial

\[ x_{T}:=\prod _{c\text{ is a box of }Y\left( \lambda /\mu \right) }x_{T\left( c\right) }=\prod _{\left( i,j\right) \in Y\left( \lambda /\mu \right) }x_{T\left( i,j\right) }=\prod _{k=1}^{N}x_{k}^{\left( \text{\# of times }k\text{ appears in }T\right) }. \]
Lemma 6.118

For any skew Young tableau \(T\) of shape \(\lambda /\mu \),

\[ x_T = \prod _{k=1}^{N} x_k^{(\text{occurrences of } k \text{ in } T)}. \]
Proof

Reindex the product over cells by partitioning according to the entry value.

Lemma 6.119

The skew Young diagram \(Y(\lambda /\lambda )\) is empty for any \(N\)-partition \(\lambda \).

theorem skewYoungDiagram_self {N : } [NeZero N] (lam : NPartition N) :
Proof

By the membership characterization, \((i,j) \in Y(\lambda /\lambda )\) iff \(\lambda _i \le j {\lt} \lambda _i\), which is impossible.

Lemma 6.120

For a skew Young tableau \(T\) of shape \(\lambda /\mu \), if \(j {\lt} \mu _i\) then \(T(i,j) = 0\). That is, entries to the left of the inner partition are zero.

theorem SkewYoungTableau.entry_of_lt_mu {N : } [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) {i : Fin N} {j : } (hj : j < mu.parts i) :
T.entry (i, j) = 0
Proof

If \(j {\lt} \mu _i\), then \((i,j) \notin Y(\lambda /\mu )\), so the support condition gives \(T(i,j) = 0\).

Lemma 6.121

For a skew Young tableau \(T\) of shape \(\lambda /\mu \), if \(j \ge \lambda _i\) then \(T(i,j) = 0\). That is, entries to the right of the outer partition are zero.

theorem SkewYoungTableau.entry_of_ge_lam {N : } [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) {i : Fin N} {j : } (hj : lam.parts i j) :
T.entry (i, j) = 0
Proof

If \(j \ge \lambda _i\), then \((i,j) \notin Y(\lambda /\mu )\), so the support condition gives \(T(i,j) = 0\).

6.3.6 Filling infrastructure for Schur polynomials

The formal definition of Schur polynomials represents SSYT as functions from the diagram to \([N]\) (“fillings”), filters for those satisfying the semistandard conditions, and sums the associated monomials.

Definition 6.122
#

A filling of a skew Young diagram \(Y(\lambda /\mu )\) is a function \(f : Y(\lambda /\mu ) \to [N]\). A filling is semistandard if it satisfies the row-weak and column-strict conditions. The filling monomial is \(x_f = \prod _{c \in Y(\lambda /\mu )} x_{f(c)}\).

def SkewFilling {N : } [NeZero N] (lam mu : NPartition N) :
def isSSYTFilling {N : } [NeZero N] (lam mu : NPartition N) (f : SkewFilling lam mu) :
  • One or more equations did not get rendered due to their size.
def fillingMonomial {N : } [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) :
Definition 6.123
#

The content of a filling \(f\) of \(Y(\lambda /\mu )\) is the function \(\mathrm{cont}(f) : [N] \to \mathbb {N}\) defined by

\[ \mathrm{cont}(f)(i) = \# \{ c \in Y(\lambda /\mu ) : f(c) = i\} . \]
def fillingContent {N : } [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) :
Fin N
Lemma 6.124

For any filling \(f\) of \(Y(\lambda /\mu )\),

\[ x_f = \prod _{i=0}^{N-1} x_i^{\mathrm{cont}(f)(i)}. \]
theorem fillingMonomial_eq_prod_pow {N : } [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) :
Proof

Reindex the product over cells by partitioning according to the entry value (fiberwise product decomposition).

Definition 6.125
#

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. We define the skew Schur polynomial \(s_{\lambda /\mu }\in \mathcal{P}\) by

\[ s_{\lambda /\mu }:=\sum _{T\in \operatorname *{SSYT}\left( \lambda /\mu \right) }x_{T}. \]
def skewSchurPoly {N : } [NeZero N] (lam mu : NPartition N) :
Lemma 6.126

For any \(N\)-partition \(\lambda \), we have \(s_{\lambda /\mathbf{0}} = s_\lambda \).

theorem skewSchurPoly_zero {N : } [NeZero N] (lam : NPartition N) :
Proof

The semistandard tableaux of shape \(\lambda /\mathbf{0}\) are precisely the semistandard tableaux of shape \(\lambda \), since \(Y(\lambda /\mathbf{0}) = Y(\lambda )\) by Lemma 6.112.

Theorem 6.127

Let \(\lambda \) and \(\mu \) be any two \(N\)-partitions. Then, the polynomial \(s_{\lambda /\mu }\) is symmetric.

theorem skewSchurPoly_isSymmetric {N : } [NeZero N] (lam mu : NPartition N) (σ : Equiv.Perm (Fin N)) :
Proof

The proof uses the Bender–Knuth involutions. For each \(k \in \{ 0, 1, \ldots , N{-}2\} \), the \(k\)-th Bender–Knuth involution \(\mathrm{BK}_k\) is a bijection on \(\operatorname {SSYT}(\lambda /\mu )\) satisfying:

  1. \(\mathrm{BK}_k\) is an involution: \(\mathrm{BK}_k \circ \mathrm{BK}_k = \mathrm{id}\);

  2. \(\mathrm{BK}_k\) preserves the shape of the tableau;

  3. \(x_{\mathrm{BK}_k(T)} = s_k \cdot x_T\) (where \(s_k\) swaps \(x_k\) and \(x_{k+1}\)).

Since the simple transpositions \(s_0, s_1, \ldots , s_{N-2}\) generate \(S_N\), and each \(\mathrm{BK}_k\) establishes that \(s_k \cdot s_{\lambda /\mu } = s_{\lambda /\mu }\) (Lemma 6.137), we conclude that \(s_{\lambda /\mu }\) is symmetric.

The reduction from arbitrary permutations to adjacent transpositions uses Lemma 6.138 (strong induction on the distance \(|j - i|\)).

6.3.7 Bender–Knuth involutions (helper lemmas)

The following helper lemmas formalize the key properties of the Bender–Knuth involution, used in the proof of Theorem 6.127.

Definition 6.128
#

The cell bijection between two representations of skew Young diagrams. The first uses 0-indexed columns (\((i,j) \in Y(\lambda /\mu )\) iff \(\mu _i \le j {\lt} \lambda _i\)), and the second uses 1-indexed columns (\((i,j) \in Y(\lambda /\mu )\) iff \(\mu _i {\lt} j \le \lambda _i\)). The bijection is \((i, j) \mapsto (i, j+1)\).

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

The filling bijection converts fillings between the two skew diagram representations by composing with the cell bijection.

Lemma 6.130

The filling bijection preserves the semistandard property: a filling \(f\) is semistandard if and only if its image under the filling bijection is semistandard in the 1-indexed representation.

Proof

Both row-weak and column-strict conditions depend only on the relative ordering of indices, which is preserved by the column shift \(j \mapsto j+1\).

Lemma 6.131

The filling bijection preserves content: for any filling \(f\) and index \(i\), the content of \(f\) at \(i\) equals the content of the corresponding filling in the 1-indexed representation at \(i\).

Proof

The cell bijection induces a bijection between \(\{ c : f(c) = i\} \) and the corresponding set in the 1-indexed representation, since the entry values are unchanged.

Definition 6.132
#

The Bender–Knuth involution \(\mathrm{BK}_k\) on fillings of \(Y(\lambda /\mu )\). For a semistandard filling \(f\), \(\mathrm{BK}_k(f)\) swaps certain entries \(k\) and \(k{+}1\) while preserving semistandardness. For non-semistandard fillings, it returns the input unchanged.

def benderKnuthInvol {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) (f : SkewFilling lam mu) :
  • One or more equations did not get rendered due to their size.
Lemma 6.133

The Bender–Knuth involution \(\mathrm{BK}_k\) preserves SSYT membership: if \(f\) is a semistandard filling, then so is \(\mathrm{BK}_k(f)\).

theorem benderKnuthInvol_mem {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) (f : SkewFilling lam mu) :
f ssytFillings lam mubenderKnuthInvol lam mu k hk f ssytFillings lam mu
Proof

Transfers through the filling bijection: the image is semistandard by the Bender–Knuth semistandard preservation theorem, and the bijection preserves semistandardness.

Lemma 6.134

The Bender–Knuth map is an involution: applying it twice returns the original filling.

theorem benderKnuthInvol_invol {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) (f : SkewFilling lam mu) :
f ssytFillings lam mubenderKnuthInvol lam mu k hk (benderKnuthInvol lam mu k hk f) = f
Proof

Transfers through the filling bijection using the Bender–Knuth involutivity theorem.

Lemma 6.135

Let \(f\) be a semistandard filling and \(f' = \mathrm{BK}_k(f)\). Then the content of \(f'\) at index \(k\) equals the content of \(f\) at \(k{+}1\), the content of \(f'\) at \(k{+}1\) equals the content of \(f\) at \(k\), and the content at all other indices is unchanged.

theorem benderKnuthInvol_content_swap_spec {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) (f : SkewFilling lam mu) :
f ssytFillings lam muhave f' := benderKnuthInvol lam mu k hk f; fillingContent f' k = fillingContent f k + 1, hk fillingContent f' k + 1, hk = fillingContent f k ∀ (i : Fin N), i ki k + 1, hkfillingContent f' i = fillingContent f i
Proof

This is the key property of the Bender–Knuth involution. Proved via the Bender–Knuth content swap theorem, transferred through the filling bijection using Lemma 6.131.

Lemma 6.136

The monomial effect of the Bender–Knuth involution: \(x_{\mathrm{BK}_k(f)} = (\text{swap } x_k\, x_{k+1}) \cdot x_f\).

This says that \(\mathrm{BK}_k\) effectively swaps the roles of variables \(x_k\) and \(x_{k+1}\) in the monomial.

theorem benderKnuthInvol_mono {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) (f : SkewFilling lam mu) :
Proof

By Lemma 6.135, the content of \(\mathrm{BK}_k(f)\) is obtained from that of \(f\) by swapping entries \(k\) and \(k{+}1\). Since the monomial is \(\prod _i x_i^{\mathrm{cont}(f)(i)}\), this transposition of the content corresponds to renaming \(x_k \leftrightarrow x_{k+1}\).

Lemma 6.137

The skew Schur polynomial is invariant under simple transpositions:

\[ s_k \cdot s_{\lambda /\mu } = s_{\lambda /\mu } \]

for each \(k \in \{ 0, 1, \ldots , N{-}2\} \).

theorem skewSchurPoly_swap_invariant {N : } [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : k + 1 < N) :
Proof

Apply \(s_k\) to the sum \(s_{\lambda /\mu } = \sum _f x_f\). By Lemma 6.136, \(s_k \cdot x_f = x_{\mathrm{BK}_k(f)}\). Since \(\mathrm{BK}_k\) is an involution on the SSYT fillings (Lemmas 6.133 and 6.134), reindexing the sum by \(\mathrm{BK}_k\) shows \(\sum _f x_{\mathrm{BK}_k(f)} = \sum _f x_f\).

Lemma 6.138

If a polynomial \(P\) is invariant under every simple transposition \(s_k\) (swapping \(x_k\) and \(x_{k+1}\)), then \(P\) is invariant under every transposition (swapping any two variables \(x_i\) and \(x_j\)).

Proof

By strong induction on the distance \(|j - i|\). If \(|j - i| = 1\), the swap is already a simple transposition. Otherwise, decompose \(\mathrm{swap}(i, j) = \mathrm{swap}(k, j) \cdot \mathrm{swap}(i, k) \cdot \mathrm{swap}(k, j)\) where \(k = j - 1\), and apply the inductive hypothesis to the smaller swap.

Lemma 6.139

Renaming variables in a filling monomial equals applying the permutation to each entry:

\[ \mathrm{rename}(\sigma )(x_f) = x_{\sigma \circ f}. \]
Proof

Follows from \(\mathrm{rename}(\sigma )(X_i) = X_{\sigma (i)}\) applied to each factor of the product.

6.3.8 Equivalences between Schur polynomial definitions

The project maintains multiple representations of SSYT and Schur polynomials for different proof contexts. This subsection records the key equivalence results.

Theorem 6.140

The two definitions of Schur polynomials in this project (one using \(\mathbb {Z}\) coefficients and \(N\)-partitions, the other using generic coefficients and raw \(N\)-tuples) are equal.

Proof

Both definitions sum over semistandard Young tableaux of shape \(\lambda \). The cell bijection \((i,j) \mapsto (i,j+1)\) between the two indexing conventions preserves the SSYT conditions and the monomials.

Definition 6.141
#

An equivalence between the two SSYT representations in this project:

  • The first uses a total function \(T : [N] \times \mathbb {N} \to [N]\) with a support condition (entries outside the diagram are \(0\)).

  • The second uses a dependent function where the column index is bounded by the partition part: \(T(i, j)\) for \(j {\lt} \lambda _i\).

The equivalence converts between the total function and the bounded representations.

Theorem 6.142

The two Schur polynomial definitions agree over \(\mathbb {Z}\). More precisely, the Schur polynomial defined via fillings of the Young diagram equals the one defined via the bounded representation.

Proof

Both are sums over SSYT with the same monomials. The equivalence on tableaux preserves the monomial at each tableau, so the sums are equal.

Theorem 6.143

Corollary of Theorem 6.142: the filling-based Schur polynomial equals the bounded-representation Schur polynomial (with appropriate conversion of the partition).

Proof

Direct application of Theorem 6.142 with the partition conversion being an involution.