Schur Polynomials

This file formalizes the basics of Schur polynomials, including:

• Alternants and the ρ vector
• Young diagrams for N-partitions
• Semistandard Young tableaux (SSYT)
• Schur polynomials as sums over SSYT
• Skew Young diagrams and skew Schur polynomials

The main result is that Schur polynomials are symmetric (Theorem thm.sf.schur-symm and thm.sf.skew-schur-symm in the source).

Main Definitions

• NPartition N: An N-partition is an N-tuple of natural numbers that is weakly decreasing
• rhoVector N: The N-tuple (N-1, N-2, ..., 0)
• alternant α: The alternant a_α = det(x_i^{α_j})
• NPartition.youngDiagram: The Young diagram Y(λ) of an N-partition λ
• SSYT: Semistandard Young tableaux of shape λ
• schurPoly: The Schur polynomial s_λ
• SkewYoungDiagram: Skew Young diagrams Y(λ/μ)
• skewSchurPoly: The skew Schur polynomial s_{λ/μ}

References

Based on the LaTeX source AlgebraicCombinatorics/tex/SymmetricFunctions/SchurBasics.tex

Tags

Schur polynomial, Young diagram, semistandard tableau, alternant, symmetric polynomial

N-Partitions

This file uses the canonical NPartition definition from AlgebraicCombinatorics/SymmetricFunctions/NPartition.lean.

The canonical definition uses antitone as the field name, but provides a monotone alias theorem for compatibility. The weakly decreasing condition means: if i ≤ j then parts j ≤ parts i.

The ρ vector

Definition \ref{def.sf.alternants}(a) in the source defines the ρ vector as the N-tuple (N-1, N-2, ..., 0). In Lean, we use 0-based indexing via Fin N, so:

• ρ(0) = N - 1
• ρ(1) = N - 2
• ...
• ρ(N-1) = 0

For example, when N = 3, we have ρ = (2, 1, 0).

@[reducible, inline]

abbrev rhoVector (N : ℕ) : Fin N → ℕ

The ρ vector is the N-tuple (N-1, N-2, ..., 0). Definition \ref{def.sf.alternants}(a) in the source.

Note: The textbook uses 1-based indexing with ρ_j = N - j for j ∈ [N]. In Lean with 0-based indexing, this becomes ρ(i) = N - 1 - i for i ∈ Fin N.

This is an abbreviation for AlgebraicCombinatorics.rho N from LittlewoodRichardson.lean.

Equations

• rhoVector N = AlgebraicCombinatorics.rho N

theorem rhoVector_val (N : ℕ) (i : Fin N) : rhoVector N i = N - 1 - ↑i

The i-th component of ρ equals N - 1 - i

theorem rhoVector_strictAnti (N : ℕ) : StrictAnti (rhoVector N)

The ρ vector is strictly decreasing

theorem rhoVector_antitone (N : ℕ) : Antitone (rhoVector N)

The ρ vector is weakly decreasing

theorem rhoVector_zero (N : ℕ) [NeZero N] : rhoVector N ⟨0, ⋯⟩ = N - 1

The first component ρ_0 = N - 1

theorem rhoVector_last (N : ℕ) [NeZero N] : rhoVector N ⟨N - 1, ⋯⟩ = 0

The last component ρ_{N-1} = 0

theorem rhoVector_sum (N : ℕ) : ∑ i : Fin N, rhoVector N i = N * (N - 1) / 2

The sum of the ρ vector equals N(N-1)/2, which is the triangular number T_{N-1}. This follows from ∑{i=0}^{N-1} (N-1-i) = ∑{k=0}^{N-1} k = N(N-1)/2.

def rhoPartition (N : ℕ) [NeZero N] : NPartition N

The ρ vector as an N-partition (when N > 0)

Equations

• rhoPartition N = { parts := rhoVector N, antitone := ⋯ }

Alternants

Definition \ref{def.sf.alternants}(b) in the source defines the alternant a_α for an N-tuple α = (α_1, α_2, ..., α_N) as the determinant:

a_α = det((x_i^{α_j})_{1≤i≤N, 1≤j≤N})

where entry (i, j) is x_i^{α_j}. This is a polynomial in R[x_1, ..., x_N].

In our implementation, we use: alternant N α = det(Matrix.of (fun i j => X j ^ α i))

This gives entry (i, j) = x_j^{α_i}, which is the transpose of the textbook matrix. Since det(A) = det(A^T), both definitions yield the same polynomial.

For example, when N = 3 and α = (5, 3, 0), the textbook matrix is: | x_1^5 x_1^3 x_1^0 | | x_2^5 x_2^3 x_2^0 | | x_3^5 x_3^3 x_3^0 |

and our matrix is the transpose of this.

@[reducible, inline]

noncomputable abbrev alternant {R : Type u_1} [CommRing R] (N : ℕ) (α : Fin N → ℕ) : MvPolynomial (Fin N) R

The alternant a_α for an N-tuple α. Definition \ref{def.sf.alternants}(b) in the source.

This is an abbreviation for AlgebraicCombinatorics.alternant from LittlewoodRichardson.lean, which defines it as ∑_{σ ∈ S_N} sign(σ) · x^(σ·α). This equals the determinant-based definition det(x_j^{α_i}) by AlgebraicCombinatorics.alternant_eq_det.

The explicit N parameter is kept for backward compatibility with existing code.

Equations

• alternant N α = AlgebraicCombinatorics.alternant α

def alternantTextbook {R : Type u_1} [CommRing R] (N : ℕ) (α : Fin N → ℕ) : MvPolynomial (Fin N) R

Alternative definition matching the textbook convention exactly: entry (i, j) = x_i^{α_j}. This equals alternant since det(A) = det(A^T).

Equations

• alternantTextbook N α = (Matrix.of fun (i j : Fin N) => MvPolynomial.X i ^ α j).det

theorem alternantTextbook_eq_alternant (N : ℕ) {R : Type u_1} [CommRing R] (α : Fin N → ℕ) : alternantTextbook N α = alternant N α

The two alternant definitions are equal. This uses AlgebraicCombinatorics.alternant_eq_det to bridge the sum-based alternant definition with the determinant-based alternantTextbook.

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)

The Vandermonde alternant a_ρ equals the Vandermonde product ∏_{i<j}(x_i - x_j). Equation \ref{eq.def.sf.alternants.arho=vdm} in the source.

This is the classical Vandermonde determinant identity. The matrix for a_ρ is: | x_1^{N-1} x_1^{N-2} ... x_1^0 | | x_2^{N-1} x_2^{N-2} ... x_2^0 | | ... ... ... ... | | x_N^{N-1} x_N^{N-2} ... x_N^0 |

Young Diagrams for N-partitions

The Young diagram infrastructure is now provided by NPartition.lean. See NPartition.youngDiagram, NPartition.mem_youngDiagram, etc.

Young Tableaux

structure YoungTableau {N : ℕ} [NeZero N] (lam : NPartition N) : Type

A Young tableau of shape lam is a filling of the Young diagram Y(lam) with elements of [N]. Definition \ref{def.sf.ytab} in the source.

• entry : Fin N × ℕ → Fin N

  The filling function

• support (c : Fin N × ℕ) : c ∉ lam.youngDiagram → self.entry c = 0

  The entry is only meaningful for cells in the diagram

theorem YoungTableau.ext {N : ℕ} [NeZero N] {lam : NPartition N} {T₁ T₂ : YoungTableau lam} (h : ∀ (c : Fin N × ℕ), T₁.entry c = T₂.entry c) : T₁ = T₂

Two Young tableaux are equal iff their entries agree.

theorem YoungTableau.ext_iff {N : ℕ} [NeZero N] {lam : NPartition N} {T₁ T₂ : YoungTableau lam} : T₁ = T₂ ↔ ∀ (c : Fin N × ℕ), T₁.entry c = T₂.entry c

instance YoungTableau.instCoeFunForallProdFinNat {N : ℕ} [NeZero N] {lam : NPartition N} : CoeFun (YoungTableau lam) fun (x : YoungTableau lam) => Fin N × ℕ → Fin N

Coercion to function, allowing T c notation.

Equations

• YoungTableau.instCoeFunForallProdFinNat = { coe := YoungTableau.entry }

def YoungTableau.entryAt {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) (i : Fin N) (j : ℕ) : Fin N

Entry at row i, column j.

Equations

• T.entryAt i j = T.entry (i, j)

def YoungTableau.size {N : ℕ} [NeZero N] {lam : NPartition N} (_T : YoungTableau lam) : ℕ

The number of cells in the tableau (equals the size of the Young diagram).

Equations

• _T.size = lam.youngDiagram.card

@[simp]

theorem YoungTableau.size_eq {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : T.size = lam.youngDiagram.card

The size of a Young tableau equals the cardinality of its Young diagram.

theorem YoungTableau.entry_of_not_mem {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) {c : Fin N × ℕ} (hc : c ∉ lam.youngDiagram) : T.entry c = 0

Entry outside the diagram is zero.

theorem YoungTableau.entry_of_ge {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) {i : Fin N} {j : ℕ} (hj : lam.parts i ≤ j) : T.entry (i, j) = 0

Entry at a cell (i, j) where j ≥ lam_i is zero.

theorem YoungTableau.entry_mem_iff {N : ℕ} [NeZero N] {lam : NPartition N} (_T : YoungTableau lam) {i : Fin N} {j : ℕ} : (i, j) ∈ lam.youngDiagram ↔ j < lam.parts i

Entry at a cell (i, j) is in the diagram iff j < lam_i.

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

The size of a tableau equals the sum of parts of the partition.

structure SSYT {N : ℕ} [NeZero N] (lam : NPartition N) extends YoungTableau lam : Type

A semistandard Young tableau (SSYT) is a tableau where:

• entries increase weakly along each row (left to right)
• entries increase strictly down each column (top to bottom)

Definition \ref{def.sf.ssyt} in the source.

Formally, a Young tableau T : Y(λ) → [N] is semistandard if and only if:

• T(i, j) ≤ T(i, j+1) for any (i, j) ∈ Y(λ) with (i, j+1) ∈ Y(λ)
• T(i, j) < T(i+1, j) for any (i, j) ∈ Y(λ) with (i+1, j) ∈ Y(λ)

The set of all semistandard Young tableaux of shape λ is denoted SSYT(λ).

Note: This is one of two SSYT definitions in this project:

• This definition (SchurBasics.SSYT): Uses entry : Fin N × ℕ → Fin N with a support condition that entries outside the Young diagram are 0. Extends YoungTableau. Requires [NeZero N]. Field names: row_weak, col_strict.
• Alternative definition (SymmetricFunctions.SSYT in PieriJacobiTrudi.lean): Uses dependent types entries : (i : Fin N) → (j : Fin (lam.parts i)) → Fin N. Standalone structure. No [NeZero N] requirement. Field names: rowWeak, colStrict.

The equivalence between these definitions is established in SSYTEquiv.lean via SSYTEquiv.ssytEquiv. Use SSYTEquiv.toSchurBasicsSSYT and SSYTEquiv.toSFSSYT to convert between representations.

When to use which:

• Use this definition when working with cell coordinates (i, j) directly, or when extending the YoungTableau structure is beneficial.
• Use SymmetricFunctions.SSYT when the dependent type ensures bounds checking at compile time, or when [NeZero N] is not available.

• entry : Fin N × ℕ → Fin N
• support (c : Fin N × ℕ) : c ∉ lam.youngDiagram → self.entry c = 0
• row_weak (i : Fin N) (j₁ j₂ : ℕ) : (i, j₂) ∈ lam.youngDiagram → j₁ < j₂ → self.entry (i, j₁) ≤ self.entry (i, j₂)

  Entries increase weakly along rows

• col_strict (i₁ i₂ : Fin N) (j : ℕ) : (i₂, j) ∈ lam.youngDiagram → i₁ < i₂ → self.entry (i₁, j) < self.entry (i₂, j)

  Entries increase strictly down columns

Basic Properties

theorem SSYT.ext {N : ℕ} [NeZero N] {lam : NPartition N} {T₁ T₂ : SSYT lam} (h : ∀ (c : Fin N × ℕ), T₁.entry c = T₂.entry c) : T₁ = T₂

Two SSYTs are equal iff their entries agree on all cells.

theorem SSYT.ext_iff {N : ℕ} [NeZero N] {lam : NPartition N} {T₁ T₂ : SSYT lam} : T₁ = T₂ ↔ ∀ (c : Fin N × ℕ), T₁.entry c = T₂.entry c

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₂)

Row-weak property extended to non-strict inequality.

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)

Column-weak property (derived from col_strict).

Entry Bounds

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))

In a semistandard tableau, entry values in a column are at least the row index. This is because entries strictly increase down columns, starting from some value ≥ 0.

theorem SSYT.entry_col_zero_ge_row {N : ℕ} [NeZero N] {lam : NPartition N} (T : SSYT lam) (i : Fin N) (h : (i, 0) ∈ lam.youngDiagram) : ↑i ≤ ↑(T.entry (i, 0))

Entries in the first column are at least the row index.

theorem SSYT.entry_lt_N {N : ℕ} [NeZero N] {lam : NPartition N} (T : SSYT lam) (c : Fin N × ℕ) : ↑(T.entry c) < N

Entry values are bounded by N - 1 (since entries are in Fin N).

The Highest Weight Tableau

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

The "highest weight" SSYT has entry i in every cell of row i. This is the semistandard tableau where each entry is the smallest possible value that an entry could have in that position (the row index).

For example, for the partition (4, 2, 1), the highest weight tableau is:

0 0 0 0
1 1
2

where each row i is filled with the value i.

Equations

• SSYT.highestWeight lam = { entry := fun (c : Fin N × ℕ) => if (c.1, c.2) ∈ lam.youngDiagram then c.1 else 0, support := ⋯, row_weak := ⋯, col_strict := ⋯ }

@[simp]

theorem SSYT.highestWeight_entry_of_mem {N : ℕ} [NeZero N] {lam : NPartition N} (c : Fin N × ℕ) (h : c ∈ lam.youngDiagram) : (highestWeight lam).entry c = c.1

@[simp]

theorem SSYT.highestWeight_entry_of_not_mem {N : ℕ} [NeZero N] {lam : NPartition N} (c : Fin N × ℕ) (h : c ∉ lam.youngDiagram) : (highestWeight lam).entry c = 0

instance SSYT.instInhabited {N : ℕ} [NeZero N] (lam : NPartition N) : Inhabited (SSYT lam)

The highest weight tableau exists for any partition.

Equations

• SSYT.instInhabited lam = { default := SSYT.highestWeight lam }

theorem SSYT.highestWeight_entry_eq_row {N : ℕ} [NeZero N] {lam : NPartition N} (i : Fin N) (j : ℕ) (h : (i, j) ∈ lam.youngDiagram) : (highestWeight lam).entry (i, j) = i

The highest weight tableau has the property that T(i,j) = i for all cells in the diagram.

theorem SSYT.highestWeight_entry_le {N : ℕ} [NeZero N] {lam : NPartition N} (T : SSYT lam) (c : Fin N × ℕ) (h : c ∈ lam.youngDiagram) : (highestWeight lam).entry c ≤ T.entry c

The highest weight tableau achieves the minimum possible entry at each cell.

Monomials from tableaux

def YoungTableau.monomial {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : MvPolynomial (Fin N) ℤ

The monomial x_T associated to a Young tableau T. Definition \ref{def.sf.ytab.xT} in the source. x_T = ∏{c ∈ Y(lam)} x{T(c)}

Equations

• T.monomial = ∏ c ∈ lam.youngDiagram, MvPolynomial.X (T.entry c)

API lemmas for YoungTableau.monomial (Definition def.sf.ytab.xT)

These lemmas provide the alternative characterization of x_T as a product of powers, matching the third form of the definition: x_T = ∏_{k=1}^N x_k^{(# of times k appears in T)}

def YoungTableau.occurrences {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) (k : Fin N) : ℕ

The number of times a value k appears in a Young tableau T. This is the count #{c ∈ Y(λ) | T(c) = k}.

Equations

• T.occurrences k = {c ∈ lam.youngDiagram | T.entry c = k}.card

theorem YoungTableau.monomial_eq_prod_pow {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : T.monomial = ∏ k : Fin N, MvPolynomial.X k ^ T.occurrences k

The monomial x_T equals the product ∏{k=1}^N x_k^{#{times k appears in T}}. This is the third form of the definition in def.sf.ytab.xT: x_T = ∏{k=1}^N x_k^{(# of times k appears in T)}

theorem YoungTableau.sum_occurrences_eq_card {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : ∑ k : Fin N, T.occurrences k = lam.youngDiagram.card

The occurrences of each value in a Young tableau sum to the diagram size. This is because each cell is counted exactly once.

theorem YoungTableau.monomial_totalDegree {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : T.monomial.totalDegree = lam.youngDiagram.card

The total degree of x_T equals the number of cells in the Young diagram. This is |Y(λ)| = λ₁ + λ₂ + ... + λ_N.

theorem YoungTableau.monomial_isMonomial {N : ℕ} [NeZero N] {lam : NPartition N} (T : YoungTableau lam) : ∃ (d : Fin N →₀ ℕ), T.monomial = (MvPolynomial.monomial d) 1

The monomial x_T is indeed a monomial in the MvPolynomial sense (a single term with coefficient 1).

Schur Polynomials

Finiteness of SSYT

To define the Schur polynomial as a sum over all semistandard Young tableaux, we need to show that the set of such tableaux is finite. The key insight is that:

1. The Young diagram Y(λ) is a finite set
2. Entries are bounded (they live in Fin N)
3. The SSYT conditions are decidable

We represent tableaux as functions from the diagram to Fin N, and filter for those satisfying the SSYT conditions.

def Filling {N : ℕ} [NeZero N] (lam : NPartition N) : Type

The type of all fillings of a Young diagram with entries in Fin N. This is finite since the diagram is finite and Fin N is finite.

Equations

• Filling lam = ({ c : Fin N × ℕ // c ∈ lam.youngDiagram } → Fin N)

noncomputable instance filling_fintype {N : ℕ} [NeZero N] (lam : NPartition N) : Fintype (Filling lam)

Fillings are finite.

Equations

• filling_fintype lam = Fintype.ofFinite (Filling lam)

def isSSYTFillingYoung {N : ℕ} [NeZero N] (lam : NPartition N) (f : Filling lam) : Prop

The set of fillings that correspond to valid semistandard tableaux. We check the conditions on pairs of cells in the diagram:

• Row-weak: if c1 and c2 are in the same row with c1 to the left, then f(c1) ≤ f(c2)
• Column-strict: if c1 and c2 are in the same column with c1 above, then f(c1) < f(c2)

Equations

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

instance isSSYTFillingYoung_decidable {N : ℕ} [NeZero N] (lam : NPartition N) (f : Filling lam) : Decidable (isSSYTFillingYoung lam f)

The SSYT condition is decidable since we're quantifying over finite types.

Equations

• isSSYTFillingYoung_decidable lam f = id inferInstance

def ssytFillingsYoung {N : ℕ} [NeZero N] (lam : NPartition N) : Finset (Filling lam)

The finite set of all valid SSYT fillings of a Young diagram.

Equations

• ssytFillingsYoung lam = Finset.filter (isSSYTFillingYoung lam) Finset.univ

def fillingMonomialYoung {N : ℕ} [NeZero N] {lam : NPartition N} (f : Filling lam) : MvPolynomial (Fin N) ℤ

The monomial associated to a filling of a Young diagram. x_f = ∏{c ∈ Y(λ)} x{f(c)}

Equations

• fillingMonomialYoung f = ∏ c : { c : Fin N × ℕ // c ∈ lam.youngDiagram }, MvPolynomial.X (f c)

def schurPoly {N : ℕ} [NeZero N] (lam : NPartition N) : MvPolynomial (Fin N) ℤ

The Schur polynomial s_λ is the sum of monomials x_T over all SSYT of shape λ. Definition \ref{def.sf.schur} in the source.

We define this as a sum over the finite set of valid SSYT fillings: s_λ = ∑_{T ∈ SSYT(λ)} x_T

The definition proceeds by:

1. Representing tableaux as functions from the Young diagram to Fin N
2. Filtering for those satisfying the SSYT conditions (row-weak, column-strict)
3. Summing the associated monomials

This is equivalent to skewSchurPoly lam 0 since skewYoungDiagram lam 0 = lam.youngDiagram.

Relationship to Other Definitions

This project has two Schur polynomial definitions with different design tradeoffs:

Definition	File	Input	Ring	Use case
schurPoly (this)	SchurBasics.lean	NPartition N	ℤ	Proofs using Young diagrams, symmetry
AlgebraicCombinatorics.schurPoly	LittlewoodRichardson.lean	Fin N → ℕ	generic R	Littlewood-Richardson rule, generic rings

When to use which:

• Use this definition when working with Young diagrams, SSYT fillings, or proving symmetry properties. It requires [NeZero N] and uses integer coefficients.
• Use AlgebraicCombinatorics.schurPoly when you need a generic coefficient ring or when working with the Littlewood-Richardson rule. It takes unbundled Fin N → ℕ.

Equivalence: The two definitions agree when the partition is valid. See:

• SSYTEquiv.schurPoly_eq_schur: relates this definition to SymmetricFunctions.schur
• schurPoly_eq_AC_schurPoly: relates this definition to AlgebraicCombinatorics.schurPoly

Equations

• schurPoly lam = ∑ f ∈ ssytFillingsYoung lam, fillingMonomialYoung f

Examples of Schur Polynomials

theorem schurPoly_row_eq_h (N : ℕ) [NeZero N] [DecidableEq (Fin N)] (n : ℕ) (lam : NPartition N) (hlam : lam.parts 0 = n ∧ ∀ (i : Fin N), i ≠ 0 → lam.parts i = 0) : schurPoly lam = MvPolynomial.hsymm (Fin N) ℤ n

The Schur polynomial s_{(n,0,...,0)} equals the complete homogeneous symmetric polynomial h_n. Example \ref{exa.sf.schur-h-e}(a) in the source.

The complete homogeneous symmetric polynomial h_n is the sum over all monomials of degree n: h_n = ∑{i₁ ≤ i₂ ≤ ... ≤ iₙ} x{i₁} x_{i₂} ⋯ x_{iₙ}. This equals the Schur polynomial for the single-row partition (n, 0, ..., 0).

def col_partition_equiv {N : ℕ} [NeZero N] (n : ℕ) (hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) : { c : Fin N × ℕ // c ∈ lam.youngDiagram } ≃ Fin n

Equivalence between cells in a column partition's Young diagram and Fin n. For a column partition (1,1,...,1,0,...,0) with n ones, the Young diagram consists of n cells in column 0, which can be identified with Fin n.

Equations

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

theorem col_partition_cell_snd_eq_zero {N : ℕ} [NeZero N] (n : ℕ) (_hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) (c : { c : Fin N × ℕ // c ∈ lam.youngDiagram }) : (↑c).2 = 0

In a column partition, all cells have j = 0 (they're all in column 0).

theorem col_partition_equiv_symm_snd {N : ℕ} [NeZero N] (n : ℕ) (hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) (k : Fin n) : (↑((col_partition_equiv n hn lam hlam).symm k)).2 = 0

theorem col_partition_equiv_symm_fst {N : ℕ} [NeZero N] (n : ℕ) (hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) (k : Fin n) : ↑(↑((col_partition_equiv n hn lam hlam).symm k)).1 = ↑k

theorem col_partition_ssyt_iff {N : ℕ} [NeZero N] (n : ℕ) (hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) (f : Filling lam) : isSSYTFillingYoung lam f ↔ StrictMono (f ∘ ⇑(col_partition_equiv n hn lam hlam).symm)

For a column partition, the SSYT condition is equivalent to strict monotonicity. Since all cells are in column 0, the row-weak condition is vacuously true, and the column-strict condition becomes strict monotonicity.

theorem schurPoly_col_eq_e (N : ℕ) [NeZero N] (n : ℕ) (hn : n ≤ N) (lam : NPartition N) (hlam : (∀ (i : Fin N), ↑i < n → lam.parts i = 1) ∧ ∀ (i : Fin N), ↑i ≥ n → lam.parts i = 0) : schurPoly lam = MvPolynomial.esymm (Fin N) ℤ n

The Schur polynomial s_{(1,1,...,1,0,...,0)} (with n ones) equals the elementary symmetric polynomial e_n. Example \ref{exa.sf.schur-h-e}(b) in the source.

The elementary symmetric polynomial e_n is the sum over all squarefree monomials of degree n: e_n = ∑{i₁ < i₂ < ... < iₙ} x{i₁} x_{i₂} ⋯ x_{iₙ}. This equals the Schur polynomial for the single-column partition (1, 1, ..., 1, 0, ..., 0) with n ones.

Helper lemmas for schurPoly_21_eq

theorem esymm_3_eq_sum_strictlyOrdered (N : ℕ) : MvPolynomial.esymm (Fin N) ℤ 3 = ∑ i : Fin N, ∑ j : Fin N, ∑ k : Fin N, if i < j ∧ j < k then MvPolynomial.X i * MvPolynomial.X j * MvPolynomial.X k else 0

The elementary symmetric polynomial e_3 equals the sum over strictly ordered triples. This is a key identity used in the proof of schurPoly_21_eq.

The bijection between powersetCard 3 and strictly ordered triples (i, j, k) with i < j < k is established by sorting the 3-element set. Each 3-element subset {a, b, c} corresponds uniquely to the ordered triple (min, mid, max).

theorem esymm_2_mul_esymm_1_expansion (N : ℕ) : MvPolynomial.esymm (Fin N) ℤ 2 * MvPolynomial.esymm (Fin N) ℤ 1 = (3 * MvPolynomial.esymm (Fin N) ℤ 3 + ∑ a : Fin N, ∑ b : Fin N, if a < b then MvPolynomial.X a * MvPolynomial.X a * MvPolynomial.X b else 0) + ∑ a : Fin N, ∑ b : Fin N, if a < b then MvPolynomial.X a * MvPolynomial.X b * MvPolynomial.X b else 0

The product e_2 * e_1 expands as 3*e_3 plus squared terms. This is a key identity used in the proof of schurPoly_21_eq.

The expansion proceeds by writing e_2 * e_1 = (∑_{a<b} X_a X_b) * (∑_c X_c) and partitioning the terms by the relationship of c to {a, b}:

• c < a: contributes e_3 (strictly ordered triple (c, a, b))
• c = a: contributes ∑_{a<b} X_a² X_b
• a < c < b: contributes e_3 (strictly ordered triple (a, c, b))
• c = b: contributes ∑_{a<b} X_a X_b²
• c > b: contributes e_3 (strictly ordered triple (a, b, c)) Total: 3*e_3 + ∑{a<b} X_a² X_b + ∑{a<b} X_a X_b²

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 ≤ ↑i → lam.parts i = 0) : schurPoly lam = MvPolynomial.esymm (Fin N) ℤ 2 * MvPolynomial.esymm (Fin N) ℤ 1 - MvPolynomial.esymm (Fin N) ℤ 3

The Schur polynomial s_{(2,1,0,...,0)} equals e_2 * e_1 - e_3. Example \ref{exa.sf.schur-h-e}(c) in the source.

This is computed by summing over all SSYT of shape (2,1), which have the form ⌜i j⌝ with i ≤ j and i < k. The sum splits into cases based on the relative ⌞k⌟ order of i, j, k.

Partition Containment

The partition containment infrastructure (LE, Preorder, PartialOrder, size, etc.) is now provided by NPartition.lean. See NPartition.instLE, NPartition.size, etc.

Skew Young Diagrams

Note: The canonical Finset version of skew Young diagrams is NPartition.skewYoungDiagram in NPartition.lean, which does not require [NeZero N]. The definition below is retained for backwards compatibility but prefer NPartition.skewYoungDiagram for new code.

See also AlgebraicCombinatorics.skewYoungDiagram in LittlewoodRichardson.lean for the Set version with 1-indexed columns (textbook convention).

def skewYoungDiagram {N : ℕ} [NeZero N] (lam mu : NPartition N) : Finset (Fin N × ℕ)

The skew Young diagram Y(λ/μ) is the set difference Y(λ) \ Y(μ). Definition \ref{def.sf.skew-diag} in the source.

Note: This is a duplicate of NPartition.skewYoungDiagram that requires [NeZero N]. Prefer NPartition.skewYoungDiagram for new code as it works for all N.

For N-partitions λ and μ with μ ⊆ λ, the skew Young diagram Y(λ/μ) is defined as:

Y(λ) \ Y(μ) = {(i,j) | i ∈ [N] and j ∈ [λ_i] \ [μ_i]}
            = {(i,j) | i ∈ [N] and j ∈ ℤ and μ_i < j ≤ λ_i}

(The second form uses 1-indexed j as in the textbook.)

In our 0-indexed formalization, this becomes:

Y(λ/μ) = {(i,j) | i ∈ Fin N and μ_i ≤ j < λ_i}

Example: Y((4,3,1)/(2,1,0)) consists of cells:

• Row 0: (0, 2), (0, 3) (since μ₀ = 2, λ₀ = 4)
• Row 1: (1, 1), (1, 2) (since μ₁ = 1, λ₁ = 3)
• Row 2: (2, 0) (since μ₂ = 0, λ₂ = 1)

Equations

• skewYoungDiagram lam mu = lam.youngDiagram \ mu.youngDiagram

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

Membership in a skew Young diagram: (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i. This is the 0-indexed version of the textbook condition μ_i < j ≤ λ_i.

theorem mem_skewYoungDiagram' {N : ℕ} [NeZero N] {lam mu : NPartition N} {i : Fin N} {j : ℕ} : (i, j) ∈ skewYoungDiagram lam mu ↔ j ∈ Finset.Ico (mu.parts i) (lam.parts i)

Alternative characterization: membership in terms of the interval [μ_i, λ_i).

@[simp]

theorem skewYoungDiagram_self {N : ℕ} [NeZero N] (lam : NPartition N) : skewYoungDiagram lam lam = ∅

The skew Young diagram is empty when μ = λ.

@[simp]

theorem skewYoungDiagram_zero {N : ℕ} [NeZero N] (lam : NPartition N) : skewYoungDiagram lam 0 = lam.youngDiagram

The skew Young diagram equals the full diagram when μ = 0.

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) : (c, d) ∈ skewYoungDiagram lam mu

Convexity of skew Young diagrams: if (a,b) and (e,f) are in Y(lam/mu), and a ≤ c ≤ e and b ≤ d ≤ f, then (c,d) ∈ Y(lam/mu). Lemma \ref{lem.sf.skew-diag.convexity} in the source.

Skew Young Tableaux

structure SkewYoungTableau {N : ℕ} [NeZero N] (lam mu : NPartition N) : Type

A skew Young tableau of shape λ/μ is a filling of Y(λ/μ) with elements of [N]. Definition \ref{def.sf.skew-tab} in the source.

Formally, a Young tableau of shape λ/μ is a map T : Y(λ/μ) → [N]. We represent this as a total function entry : Fin N × ℕ → Fin N with a support condition that entries outside the skew diagram are 0.

Young tableaux of shape λ/μ are often called "skew Young tableaux".

Note: If μ ⊈ λ (i.e., not μ ≤ λ), then there are no Young tableaux of shape λ/μ because the skew diagram would be empty or malformed.

• entry : Fin N × ℕ → Fin N

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

• support (c : Fin N × ℕ) : c ∉ skewYoungDiagram lam mu → self.entry c = 0

  The entry is only meaningful for cells in the skew diagram

theorem SkewYoungTableau.ext {N : ℕ} [NeZero N] {lam mu : NPartition N} {T₁ T₂ : SkewYoungTableau lam mu} (h : ∀ c ∈ skewYoungDiagram lam mu, T₁.entry c = T₂.entry c) : T₁ = T₂

Two skew Young tableaux are equal if their entries agree on the skew diagram

theorem SkewYoungTableau.ext_iff {N : ℕ} [NeZero N] {lam mu : NPartition N} {T₁ T₂ : SkewYoungTableau lam mu} : T₁ = T₂ ↔ ∀ c ∈ skewYoungDiagram lam mu, T₁.entry c = T₂.entry c

instance SkewYoungTableau.instCoeFunForallProdFinNat {N : ℕ} [NeZero N] {lam mu : NPartition N} : CoeFun (SkewYoungTableau lam mu) fun (x : SkewYoungTableau lam mu) => Fin N × ℕ → Fin N

Coercion to function

Equations

• SkewYoungTableau.instCoeFunForallProdFinNat = { coe := SkewYoungTableau.entry }

def SkewYoungTableau.empty {N : ℕ} [NeZero N] (lam : NPartition N) : SkewYoungTableau lam lam

The empty skew tableau when lam = mu

Equations

• SkewYoungTableau.empty lam = { entry := fun (x : Fin N × ℕ) => 0, support := ⋯ }

def SkewYoungTableau.size {N : ℕ} [NeZero N] {lam mu : NPartition N} (_T : SkewYoungTableau lam mu) : ℕ

The number of cells in a skew Young tableau

Equations

• _T.size = (skewYoungDiagram lam mu).card

@[simp]

theorem SkewYoungTableau.size_eq {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) : T.size = (skewYoungDiagram lam mu).card

The size of a skew Young tableau equals the cardinality of its skew Young diagram.

def SkewYoungTableau.entryAt {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) (i : Fin N) (j : ℕ) : Fin N

Entry at a specific row and column

Equations

• T.entryAt i j = T.entry (i, j)

def SkewYoungTableau.Nonempty {N : ℕ} [NeZero N] {lam mu : NPartition N} (_T : SkewYoungTableau lam mu) : Prop

A skew tableau is nonempty if the skew diagram is nonempty

Equations

• _T.Nonempty = (skewYoungDiagram lam mu).Nonempty

theorem SkewYoungTableau.entry_of_not_mem {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) {c : Fin N × ℕ} (hc : c ∉ skewYoungDiagram lam mu) : T.entry c = 0

Entry outside the skew diagram is 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

Entry at a cell (i, j) where j < mu_i is 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

Entry at a cell (i, j) where j ≥ lam_i is zero

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

A semistandard skew Young tableau is a skew tableau where:

• entries increase weakly along each row (left to right)
• entries increase strictly down each column (top to bottom) Definition \ref{def.sf.skew-ssyt} in the source.

Note: This is one of two SkewSSYT definitions in this project:

• This definition (SchurBasics.SkewSSYT): Uses entry : Fin N × ℕ → Fin N with a support condition. Extends SkewYoungTableau. Takes lam mu : NPartition N as separate arguments. Requires [NeZero N]. Field names: row_weak, col_strict.
• Alternative definition (SymmetricFunctions.SkewSSYT in PieriJacobiTrudi.lean): Uses dependent types. Takes s : SkewPartition N as a single bundled argument. No [NeZero N] requirement. Field names: rowWeak, colStrict.

See SSYTEquiv.lean for conversions between representations.

• entry : Fin N × ℕ → Fin N
• support (c : Fin N × ℕ) : c ∉ skewYoungDiagram lam mu → self.entry c = 0
• row_weak (i : Fin N) (j₁ j₂ : ℕ) : (i, j₁) ∈ skewYoungDiagram lam mu → (i, j₂) ∈ skewYoungDiagram lam mu → j₁ < j₂ → self.entry (i, j₁) ≤ self.entry (i, j₂)

  Entries increase weakly along rows

• col_strict (i₁ i₂ : Fin N) (j : ℕ) : (i₁, j) ∈ skewYoungDiagram lam mu → (i₂, j) ∈ skewYoungDiagram lam mu → i₁ < i₂ → self.entry (i₁, j) < self.entry (i₂, j)

  Entries increase strictly down columns

Properties of Semistandard Skew Tableaux

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₂)

In a semistandard skew tableau, entries increase weakly along rows (general version). Lemma \ref{lem.sf.skew-ssyt.increase}(a) in the source.

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)

In a semistandard skew tableau, entries increase weakly down columns. Lemma \ref{lem.sf.skew-ssyt.increase}(b) in the source.

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)

In a semistandard skew tableau, entries increase strictly down columns. Lemma \ref{lem.sf.skew-ssyt.increase}(c) in the source.

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₂)

In a semistandard skew tableau, if (i₁, j₁) ≤ (i₂, j₂) componentwise, then T(i₁, j₁) ≤ T(i₂, j₂). Lemma \ref{lem.sf.skew-ssyt.increase}(d) in the source.

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₂)

In a semistandard skew tableau, if i₁ < i₂ and j₁ ≤ j₂, then T(i₁, j₁) < T(i₂, j₂). Lemma \ref{lem.sf.skew-ssyt.increase}(e) in the source.

Monomials from Skew Tableaux

def SkewYoungTableau.monomial {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) : MvPolynomial (Fin N) ℤ

The monomial x_T associated to a skew Young tableau T. Definition \ref{def.sf.ytab.skew-xT} in the source. x_T = ∏{c ∈ Y(lam/mu)} x{T(c)}

Equations

• T.monomial = ∏ c ∈ skewYoungDiagram lam mu, MvPolynomial.X (T.entry c)

def SkewYoungTableau.countValue {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) (k : Fin N) : ℕ

The number of times a value k appears in a skew tableau T. This is the exponent of x_k in the monomial x_T.

Equations

• T.countValue k = {c ∈ skewYoungDiagram lam mu | T.entry c = k}.card

theorem SkewYoungTableau.monomial_eq_prod_pow {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) : T.monomial = ∏ k : Fin N, MvPolynomial.X k ^ T.countValue k

The monomial x_T equals ∏_{k=1}^N x_k^{(# of times k appears in T)}. This is the third equivalent form from Definition \ref{def.sf.ytab.skew-xT}.

theorem SkewYoungTableau.sum_countValue_eq_card {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) : ∑ k : Fin N, T.countValue k = (skewYoungDiagram lam mu).card

The sum of countValue over all k equals the cardinality of the skew diagram.

theorem SkewYoungTableau.monomial_empty {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) (h : skewYoungDiagram lam mu = ∅) : T.monomial = 1

The monomial of the empty skew diagram is 1.

@[simp]

theorem SkewYoungTableau.countValue_zero_of_not_mem {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewYoungTableau lam mu) (k : Fin N) (h : ∀ c ∈ skewYoungDiagram lam mu, T.entry c ≠ k) : T.countValue k = 0

countValue is zero for values that don't appear in the tableau.

def SkewYoungTableau.SkewSSYT.monomial' {N : ℕ} [NeZero N] {lam mu : NPartition N} (T : SkewSSYT lam mu) : MvPolynomial (Fin N) ℤ

For a semistandard skew tableau, the monomial is the same.

Equations

• SkewYoungTableau.SkewSSYT.monomial' T = T.monomial

Skew Schur Polynomials

Finiteness of SkewSSYT

To define the skew Schur polynomial as a sum over all semistandard skew tableaux, we need to show that the set of such tableaux is finite. The key insight is that:

1. The skew diagram Y(λ/μ) is a finite set
2. Entries are bounded (they live in Fin N)
3. The SSYT conditions are decidable

We represent tableaux as functions from the diagram to Fin N, and filter for those satisfying the SSYT conditions.

def SkewFilling {N : ℕ} [NeZero N] (lam mu : NPartition N) : Type

The type of all fillings of a skew diagram with entries in Fin N. This is finite since the diagram is finite and Fin N is finite.

Equations

• SkewFilling lam mu = ({ c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } → Fin N)

noncomputable instance skewFilling_fintype {N : ℕ} [NeZero N] (lam mu : NPartition N) : Fintype (SkewFilling lam mu)

Fillings are finite.

Equations

• skewFilling_fintype lam mu = Fintype.ofFinite (SkewFilling lam mu)

def isSSYTFilling {N : ℕ} [NeZero N] (lam mu : NPartition N) (f : SkewFilling lam mu) : Prop

The set of fillings that correspond to valid semistandard tableaux. We check the conditions on pairs of cells in the diagram:

• Row-weak: if c1 and c2 are in the same row with c1 to the left, then f(c1) ≤ f(c2)
• Column-strict: if c1 and c2 are in the same column with c1 above, then f(c1) < f(c2)

Equations

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

instance isSSYTFilling_decidable {N : ℕ} [NeZero N] (lam mu : NPartition N) (f : SkewFilling lam mu) : Decidable (isSSYTFilling lam mu f)

The SSYT condition is decidable since we're quantifying over finite types.

Equations

• isSSYTFilling_decidable lam mu f = id inferInstance

Bridge between SchurBasics and LittlewoodRichardson representations

The two files use different indexing conventions for skew diagrams:

• SchurBasics.lean: 0-indexed columns, mu.parts i ≤ j < lam.parts i
• LittlewoodRichardson.lean: 1-indexed columns, mu i < j ≤ lam i

The bijection between cells is: (i, j) ↔ (i, j+1)

We define equivalences to bridge these representations.

def skewCellEquiv {N : ℕ} [NeZero N] (lam mu : NPartition N) : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } ≃ { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam.parts mu.parts }

Cell bijection: SchurBasics cell (i, j) ↔ LittlewoodRichardson cell (i, j+1).

SchurBasics: (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i LittlewoodRichardson: (i, j) ∈ Y(λ/μ) iff μ_i < j ≤ λ_i

The map (i, j) ↦ (i, j+1) transforms the first to the second.

Equations

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

theorem skewYoungDiagram_equiv_LR {N : ℕ} [NeZero N] (lam mu : NPartition N) : Nonempty ({ c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } ≃ { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam.parts mu.parts })

The two skewYoungDiagram definitions are isomorphic via the column shift bijection.

This theorem makes explicit that skewCellEquiv provides an equivalence between:

• skewYoungDiagram lam mu (SchurBasics): Finset (Fin N × ℕ) with 0-indexed columns where (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i
• AlgebraicCombinatorics.skewYoungDiagram lam.parts mu.parts (LittlewoodRichardson): Set (Fin N × ℕ) with 1-indexed columns where (i, j) ∈ Y(λ/μ) iff μ_i < j ≤ λ_i

The bijection is: (i, j) in SchurBasics ↔ (i, j+1) in LittlewoodRichardson

Note: This provides the explicit equivalence theorem that was missing from the bridge infrastructure.

theorem skewYoungDiagram_card_eq_LR {N : ℕ} [NeZero N] (lam mu : NPartition N) : (skewYoungDiagram lam mu).card = Nat.card { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam.parts mu.parts }

The cardinalities of the two skew Young diagram representations are equal.

This follows directly from skewCellEquiv being an equivalence.

theorem mem_skewYoungDiagram_iff_mem_LR_shifted {N : ℕ} [NeZero N] (lam mu : NPartition N) (i : Fin N) (j : ℕ) : (i, j) ∈ skewYoungDiagram lam mu ↔ (i, j + 1) ∈ AlgebraicCombinatorics.skewYoungDiagram lam.parts mu.parts

Membership characterization: (i, j) is in the SchurBasics skew diagram iff (i, j+1) is in the LittlewoodRichardson skew diagram.

This is the fundamental relationship between the two indexing conventions.

def skewFillingEquiv {N : ℕ} [NeZero N] (lam mu : NPartition N) : SkewFilling lam mu ≃ AlgebraicCombinatorics.Tableau lam.parts mu.parts

Filling bijection: convert between SkewFilling and Tableau.

This bridges the two representations by composing with the cell bijection.

Equations

• skewFillingEquiv lam mu = (skewCellEquiv lam mu).arrowCongr (Equiv.refl (Fin N))

theorem skewFillingEquiv_isSSYT {N : ℕ} [NeZero N] (lam mu : NPartition N) (f : SkewFilling lam mu) : isSSYTFilling lam mu f ↔ AlgebraicCombinatorics.IsSemistandard ((skewFillingEquiv lam mu) f)

The filling bijection preserves the SSYT property.

def ssytFillings {N : ℕ} [NeZero N] (lam mu : NPartition N) : Finset (SkewFilling lam mu)

The finite set of all valid SSYT fillings.

Equations

• ssytFillings lam mu = Finset.filter (isSSYTFilling lam mu) Finset.univ

def fillingMonomial {N : ℕ} [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) : MvPolynomial (Fin N) ℤ

The monomial associated to a filling. x_f = ∏{c ∈ Y(λ/μ)} x{f(c)}

Equations

• fillingMonomial f = ∏ c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }, MvPolynomial.X (f c)

def fillingContent {N : ℕ} [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) : Fin N → ℕ

The content of a filling: the number of cells with each entry value. content(f)(i) = |{c ∈ Y(λ/μ) : f(c) = i}|

This is related to the monomial by: x_f = ∏_i x_i^{content(f)(i)}

The Bender-Knuth involution BK_k swaps the content of k and k+1: content(BK_k(f))(k) = content(f)(k+1) and content(BK_k(f))(k+1) = content(f)(k)

Equations

• fillingContent f i = {c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } | f c = i}.card

theorem fillingMonomial_eq_prod_pow {N : ℕ} [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) : fillingMonomial f = ∏ i : Fin N, MvPolynomial.X i ^ fillingContent f i

The fillingMonomial equals the product of X i raised to the content power.

theorem skewFillingEquiv_content {N : ℕ} [NeZero N] (lam mu : NPartition N) (f : SkewFilling lam mu) (i : Fin N) : fillingContent f i = AlgebraicCombinatorics.contentTableau ((skewFillingEquiv lam mu) f) i

Content bridge: the content of a filling equals the content of the corresponding tableau under the skewFillingEquiv bijection.

This is a key lemma for bridging the Bender-Knuth involution from LittlewoodRichardson.lean to SchurBasics.lean. It allows us to transport content-related properties across the bijection.

Both definitions count cells with entry i:

• fillingContent f i counts cells c with f(c) = i using Finset.card
• contentTableau T i counts cells c with T(c) = i using Nat.card

The bijection (skewCellEquiv) maps (row, col) ↦ (row, col+1), which doesn't change the entry.

Proof sketch: The key is to show that the bijection skewCellEquiv induces a bijection between {c | f c = i} and {c | (skewFillingEquiv f) c = i}. Since skewFillingEquiv is defined as Equiv.arrowCongr (skewCellEquiv) (Equiv.refl), we have (skewFillingEquiv f) c = f ((skewCellEquiv).symm c), so the sets are in bijection.

def skewSchurPoly {N : ℕ} [NeZero N] (lam mu : NPartition N) : MvPolynomial (Fin N) ℤ

The skew Schur polynomial s_{λ/μ} is the sum of monomials x_T over all semistandard skew tableaux of shape λ/μ. Definition \ref{def.sf.skew-schur} in the source.

We define this as a sum over the finite set of valid SSYT fillings: s_{λ/μ} = ∑_{T ∈ SSYT(λ/μ)} x_T

The definition proceeds by:

1. Representing tableaux as functions from the skew diagram to Fin N
2. Filtering for those satisfying the SSYT conditions (row-weak, column-strict)
3. Summing the associated monomials

Relationship to Other Definitions

This project has two skew Schur polynomial definitions with different design tradeoffs:

Definition	File	Input	Ring	Use case
skewSchurPoly (this)	SchurBasics.lean	NPartition N	ℤ	Proofs using skew diagrams, symmetry
AlgebraicCombinatorics.skewSchurPoly	LittlewoodRichardson.lean	Fin N → ℕ	generic R	Littlewood-Richardson rule, generic rings

When to use which:

• Use this definition when working with skew Young diagrams, SSYT fillings, or proving symmetry properties. It requires [NeZero N] and uses integer coefficients.
• Use AlgebraicCombinatorics.skewSchurPoly when you need a generic coefficient ring or when working with the Littlewood-Richardson rule. It takes unbundled Fin N → ℕ.

Equivalence: See SSYTEquiv.lean for the bridge between these definitions.

Equations

• skewSchurPoly lam mu = ∑ f ∈ ssytFillings lam mu, fillingMonomial f

theorem skewSchurPoly_zero {N : ℕ} [NeZero N] (lam : NPartition N) : skewSchurPoly lam 0 = schurPoly lam

When mu = 0, the skew Schur polynomial equals the regular Schur polynomial. Remark \ref{rmk.sf.skew-0} in the source.

def applyPermToFilling {N : ℕ} [NeZero N] {lam mu : NPartition N} (σ : Equiv.Perm (Fin N)) (f : SkewFilling lam mu) : SkewFilling lam mu

Applying a permutation σ to each entry of a filling.

Equations

• applyPermToFilling σ f c = σ (f c)

theorem rename_fillingMonomial_eq {N : ℕ} [NeZero N] {lam mu : NPartition N} (f : SkewFilling lam mu) (σ : Equiv.Perm (Fin N)) : (MvPolynomial.rename ⇑σ) (fillingMonomial f) = fillingMonomial (applyPermToFilling σ f)

Renaming variables in a filling monomial equals applying the permutation to entries.

Bender-Knuth Involutions

The Bender-Knuth involution is a key tool for proving that Schur polynomials are symmetric. For each k ∈ {0, 1, ..., N-2}, the Bender-Knuth involution BK_k is a bijection on the set of semistandard Young tableaux that swaps certain entries k and k+1 while preserving the semistandardness property.

Key Properties

1. Involution: BK_k ∘ BK_k = id
2. Preserves shape: BK_k(T) has the same shape as T
3. Monomial effect: x_{BK_k(T)} = (swap x_k x_{k+1}) · x_T

How BK_k Works

For each row i:

• Consider cells containing k or k+1
• Some cells are "forced" (must stay the same due to column constraints)
• The remaining "free" cells can be swapped
• BK_k swaps the free k's and (k+1)'s while maintaining semistandardness

A cell (i, j) with entry k is "forced" if there exists a cell (i', j) with i' > i in the same column with entry k+1 (column-strict constraint would be violated). Similarly for entry k+1 being forced by a k above it.

Note: The full implementation of the Bender-Knuth involution requires careful handling of decidability instances. The proofs below are complete and sorry-free.

def simpleTransposition {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) : Equiv.Perm (Fin N)

The simple transposition swapping k and k+1.

This is an alternative signature for AlgebraicCombinatorics.simpleTransposition. Instead of taking Fin (N - 1) (which encodes the constraint), this takes Fin N with an explicit proof hk : k.val + 1 < N.

See simpleTransposition_eq_canonical for the equivalence with the canonical definition.

Equations

• simpleTransposition k hk = Equiv.swap k ⟨↑k + 1, hk⟩

theorem simpleTransposition_eq_canonical {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) : simpleTransposition k hk = AlgebraicCombinatorics.simpleTransposition ⟨↑k, ⋯⟩

The alternative signature simpleTransposition equals the canonical definition.

Given k : Fin N with proof hk : k.val + 1 < N, we can form ⟨k.val, _⟩ : Fin (N - 1) and the resulting transpositions are equal.

def benderKnuthInvol {N : ℕ} [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : ↑k + 1 < N) (f : SkewFilling lam mu) : SkewFilling lam mu

The Bender-Knuth involution BK_k on skew fillings.

For a filling f and index k, BK_k swaps certain entries k and k+1 while preserving the semistandardness property. The construction works row by row:

• In each row, identify which k's and (k+1)'s are "free" (not forced by column constraints)
• Use parenthesis-matching: each free (k+1) "matches" with the nearest unmatched free k to its left
• Only UNMATCHED free entries get swapped

Implementation: This bridges to the full implementation in LittlewoodRichardson.lean via skewFillingEquiv. For SSYT fillings, it applies AlgebraicCombinatorics.benderKnuth; for non-SSYT fillings, it returns the input unchanged (the lemmas only apply to SSYT anyway).

Equations

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

theorem benderKnuthInvol_eq_of_ssyt {N : ℕ} [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : ↑k + 1 < N) (f : SkewFilling lam mu) (hf : isSSYTFilling lam mu f) : benderKnuthInvol lam mu k hk f = (skewFillingEquiv lam mu).symm (AlgebraicCombinatorics.benderKnuth k hk ((skewFillingEquiv lam mu) f) ⋯)

Helper lemma: benderKnuthInvol on SSYT fillings equals the bridged BK.

theorem benderKnuthInvol_mem {N : ℕ} [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : ↑k + 1 < N) (f : SkewFilling lam mu) : f ∈ ssytFillings lam mu → benderKnuthInvol lam mu k hk f ∈ ssytFillings lam mu

The Bender-Knuth involution preserves SSYT membership. This is a key property: BK_k maps semistandard tableaux to semistandard tableaux.

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

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

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 mu → have 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 ≠ k → i ≠ ⟨↑k + 1, hk⟩ → fillingContent f' i = fillingContent f i

The key property that the Bender-Knuth involution satisfies: BK_k swaps the content of k and k+1, leaving other entries unchanged.

This is the content-level statement that implies benderKnuthInvol_mono: If content(BK_k(f))(k) = content(f)(k+1) and content(BK_k(f))(k+1) = content(f)(k), then fillingMonomial(BK_k(f)) = rename(swap k (k+1))(fillingMonomial(f)).

The proof transfers benderKnuth_content_swap from LittlewoodRichardson.lean through the skewFillingEquiv bijection, using skewFillingEquiv_content to relate fillingContent and contentTableau.

theorem benderKnuthInvol_mono {N : ℕ} [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : ↑k + 1 < N) (f : SkewFilling lam mu) : f ∈ ssytFillings lam mu → fillingMonomial (benderKnuthInvol lam mu k hk f) = (MvPolynomial.rename ⇑(simpleTransposition k hk)) (fillingMonomial f)

The monomial effect of the Bender-Knuth involution: x_{BK_k(f)} = (swap x_k x_{k+1}) · x_f

This says that BK_k effectively swaps the roles of variables x_k and x_{k+1} in the monomial, which is the key property for proving symmetry.

The proof uses benderKnuthInvol_content_swap_spec: if the content swaps k and k+1, then the monomial (which is ∏ i, X i ^ content(f)(i)) is renamed by swap k (k+1).

theorem swap_invariant_of_adj_invariant {N : ℕ} (P : MvPolynomial (Fin N) ℤ) (h_adj : ∀ (k : Fin N) (hk : ↑k + 1 < N), (MvPolynomial.rename ⇑(simpleTransposition k hk)) P = P) (i j : Fin N) (hij : i ≠ j) : (MvPolynomial.rename ⇑(Equiv.swap i j)) P = P

Helper lemma: Any swap leaves a polynomial invariant if all adjacent swaps do. This reduces the symmetry proof to showing invariance under adjacent transpositions.

theorem skewSchurPoly_swap_invariant {N : ℕ} [NeZero N] (lam mu : NPartition N) (k : Fin N) (hk : ↑k + 1 < N) : (MvPolynomial.rename ⇑(simpleTransposition k hk)) (skewSchurPoly lam mu) = skewSchurPoly lam mu

The skew Schur polynomial is invariant under simple transpositions. This is the key lemma that uses Bender-Knuth involutions.

The proof strategy is:

1. Define the Bender-Knuth involution BK_k on ssytFillings
2. Show BK_k is a bijection that preserves the SSYT property
3. Show fillingMonomial (BK_k f) = rename (swap k (k+1)) (fillingMonomial f)
4. Use the bijection to reindex the sum

theorem skewSchurPoly_isSymmetric {N : ℕ} [NeZero N] (lam mu : NPartition N) (σ : Equiv.Perm (Fin N)) : (MvPolynomial.rename ⇑σ) (skewSchurPoly lam mu) = skewSchurPoly lam mu

Skew Schur polynomials are symmetric. Theorem \ref{thm.sf.skew-schur-symm} in the source.

Proof Strategy (Bender-Knuth involutions): The proof uses the Bender-Knuth involutions, which are combinatorial bijections on semistandard skew tableaux. For each k ∈ [N-1], the k-th Bender-Knuth involution BK_k swaps certain entries k and k+1 in a tableau T while preserving the semistandardness condition. The key properties are:

1. BK_k is an involution: BK_k(BK_k(T)) = T
2. BK_k preserves the shape of the tableau
3. x_{BK_k(T)} = s_k · x_T (where s_k swaps x_k and x_{k+1})

Since the simple transpositions s_1, ..., s_{N-1} generate S_N, and each BK_k establishes that s_k · s_{λ/μ} = s_{λ/μ}, we conclude that s_{λ/μ} is symmetric.

Schur Polynomials are Symmetric

theorem schurPoly_isSymmetric {N : ℕ} [NeZero N] (lam : NPartition N) (σ : Equiv.Perm (Fin N)) : (MvPolynomial.rename ⇑σ) (schurPoly lam) = schurPoly lam

Schur polynomials are symmetric. Theorem \ref{thm.sf.schur-symm}(a) in the source.

This follows from skewSchurPoly_isSymmetric using the fact that schurPoly lam = skewSchurPoly lam 0 (see skewSchurPoly_zero).

theorem alternant_eq_AC_alternant {N : ℕ} {R : Type u_2} [CommRing R] (α : Fin N → ℕ) : alternant N α = AlgebraicCombinatorics.alternant α

The determinant-based alternant (from SchurBasics) equals the sum-based alternant (from LittlewoodRichardson).

Since alternant is now an abbreviation for AlgebraicCombinatorics.alternant, this theorem is trivially true by reflexivity.

Both compute the same polynomial; the determinant expands to the signed sum over permutations. See also AlgebraicCombinatorics.alternant_eq_det for the determinant form.

theorem schurPoly_eq_AC_schurPoly {N : ℕ} [NeZero N] (lam : NPartition N) : schurPoly lam = AlgebraicCombinatorics.schurPoly lam.parts

The Schur polynomial defined in SchurBasics equals the one in LittlewoodRichardson.

Both definitions compute the same polynomial:

• SchurBasics: ∑ f ∈ ssytFillingsYoung lam, fillingMonomialYoung f
• LittlewoodRichardson: ∑ T : {T : Tableau lam.parts 0 // IsSemistandard T}, xPow (contentTableau T.val)

Both sum over semistandard Young tableaux of shape λ, but use different representations:

• SchurBasics uses 0-indexed columns: cell (i,j) with 0 ≤ j < λ_i
• LittlewoodRichardson uses 1-indexed columns: cell (i,j) with 0 < j ≤ λ_i

The bijection between these representations preserves the monomial, so the sums are equal.

Note: Currently proved only for ℤ coefficients.

See also:

• SSYTEquiv.schur_eq_schurPoly_int: equivalence with SymmetricFunctions.schur
• alternant_eq_AC_alternant: corresponding equivalence for alternants

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

The alternant identity: a_{lam+ρ} = a_ρ · s_lam. Theorem \ref{thm.sf.schur-symm}(b) in the source.

Proof Strategy (from the tex source, using Stembridge's Lemma):

1. Apply Stembridge's Lemma (lem.sf.stemb-lem) with μ = 0 and ν = 0: a_{0+ρ} · s_{λ/0} = ∑{T 0-Yamanouchi of shape λ/0} a{0 + cont(T) + ρ}

2. Simplify using 0 + ρ = ρ and s_{λ/0} = s_λ: a_ρ · s_λ = ∑{T 0-Yamanouchi of shape λ} a{cont(T) + ρ}

3. Show that the only 0-Yamanouchi semistandard tableau of shape λ is the "minimalistic" (highest weight) tableau T₀ where each row i contains only i's. This is SSYT.highestWeight in our formalization.

4. The content of T₀ equals λ: cont(T₀) = λ (since row i has λᵢ cells, all filled with value i, so the count of i's is λᵢ)

5. Therefore: a_ρ · s_λ = a_{λ + ρ}

Proof: We use schurPoly_eq_alternant_div from LittlewoodRichardson.lean and bridge the type systems.

Properties of Alternants

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

An alternant is zero if two entries of α are equal. Lemma \ref{lem.sf.alternant-0}(a) in the source.

This delegates to AlgebraicCombinatorics.alternant_eq_zero_of_repeated.

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 α

Swapping columns of an alternant multiplies it by -1. Lemma \ref{lem.sf.alternant-0}(b) in the source.

This delegates to AlgebraicCombinatorics.alternant_swap.