The Littlewood-Richardson Rule

This file formalizes the Littlewood-Richardson rule for Schur polynomials, following the presentation in the Algebraic Combinatorics textbook.

The Littlewood-Richardson rule is one of the most famous results in the theory of symmetric polynomials. It provides a combinatorial formula for expanding the product of Schur polynomials as a sum of Schur polynomials: $$s_\nu \cdot s_{\lambda/\mu} = \sum_{T} s_{\nu + \operatorname{cont}(T)}$$ where the sum is over all ν-Yamanouchi semistandard tableaux T of shape λ/μ.

Main definitions

• NPartition: An N-partition is a weakly decreasing N-tuple of natural numbers
• contentTableau: The content of a tableau (counting occurrences of each entry)
• colGeq: Restriction of a tableau to columns ≥ j
• IsYamanouchi: A semistandard tableau is ν-Yamanouchi if certain conditions hold
• alternant: The alternant polynomial a_α
• schurPoly: The Schur polynomial s_λ (via the Jacobi-Trudi formula)
• skewSchurPoly: The skew Schur polynomial s_{λ/μ}

Main results

• littlewoodRichardson: Zelevinsky's generalized Littlewood-Richardson rule (thm.sf.lr-zy)
• stembridgeLemma: Stembridge's lemma (lem.sf.stemb-lem)
• schurPoly_eq_alternant_div: Theorem relating Schur polynomials to alternants (thm.sf.schur-symm (b))

Indexing Convention

This file uses 1-indexed columns for skew Young diagrams, matching the textbook convention:

• A cell (i, j) is in Y(λ/μ) iff μ_i < j ≤ λ_i
• Column indices start at 1 (the first column is j = 1)

This differs from SchurBasics.lean which uses 0-indexed columns (Mathlib convention):

• A cell (i, j) is in Y(λ/μ) iff μ_i ≤ j < λ_i
• Column indices start at 0 (the first column is j = 0)

The bijection (i, j) ↔ (i, j+1) converts between the conventions. See SchurBasics.skewCellEquiv and SchurBasics.mem_skewYoungDiagram_iff_mem_LR_shifted for explicit equivalences.

References

• [Stembridge, A concise proof of the Littlewood-Richardson rule][Stembr02]
• [Grinberg-Reiner, Hopf algebras in Combinatorics][GriRei]

Tags

Littlewood-Richardson rule, Schur polynomial, Yamanouchi tableau, symmetric polynomial

N-partitions and N-tuples

An N-partition is a weakly decreasing N-tuple of natural numbers. We use Fin N → ℕ to represent N-tuples.

The IsNPartition predicate is defined in NPartition.lean and re-exported here for backwards compatibility.

@[reducible, inline]

abbrev AlgebraicCombinatorics.IsNPartition {N : ℕ} (lam : Fin N → ℕ) : Prop

An N-partition is a weakly decreasing N-tuple of natural numbers. (Used throughout the source)

This is an alias for the canonical definition in NPartition.lean.

Equations

• AlgebraicCombinatorics.IsNPartition lam = IsNPartition lam

@[reducible, inline]

abbrev AlgebraicCombinatorics.zeroTuple {N : ℕ} : Fin N → ℕ

The zero N-tuple (0, 0, ..., 0). (def.sf.tuple-addition (a)) Note: This is definitionally equal to (0 : Fin N → ℕ) via Mathlib's Pi.instZero.

Equations

• AlgebraicCombinatorics.zeroTuple = 0

@[reducible, inline]

abbrev AlgebraicCombinatorics.addTuple {N : ℕ} (α β : Fin N → ℕ) : Fin N → ℕ

Addition of N-tuples, defined entrywise. (def.sf.tuple-addition (b)) Note: This is definitionally equal to (· + ·) on Fin N → ℕ via Mathlib's Pi.instAdd.

Equations

• AlgebraicCombinatorics.addTuple α β = α + β

def AlgebraicCombinatorics.subTuple {N : ℕ} (α β : Fin N → ℕ) : Fin N → ℤ

Subtraction of N-tuples, defined entrywise. Note: result is in ℤ. (def.sf.tuple-addition (b))

Equations

• AlgebraicCombinatorics.subTuple α β i = ↑(α i) - ↑(β i)

theorem AlgebraicCombinatorics.addTuple_apply {N : ℕ} (α β : Fin N → ℕ) (i : Fin N) : (α + β) i = α i + β i

API for def.sf.tuple-addition

The following lemmas establish the basic properties of N-tuple arithmetic as stated in Definition def.sf.tuple-addition:

• (a) The zero N-tuple 0 = (0, 0, ..., 0)
• (b) Addition α + β and subtraction α - β are entrywise operations

Key properties (from the source text):

• "The addition operation + is associative and commutative"
• "The N-tuple 0 is its neutral element"
• "The subtraction operation − undoes +"

Part (a): The zero N-tuple

@[simp]

theorem AlgebraicCombinatorics.zeroTuple_apply {N : ℕ} (i : Fin N) : zeroTuple i = 0

The zero tuple has all entries equal to 0. (def.sf.tuple-addition (a))

theorem AlgebraicCombinatorics.isNPartition_zeroTuple {N : ℕ} : IsNPartition zeroTuple

The zero tuple is an N-partition (trivially weakly decreasing). This is an alias for isNPartition_zero from NPartition.lean.

Part (b): Entrywise operations

@[simp]

theorem AlgebraicCombinatorics.subTuple_apply' {N : ℕ} (α β : Fin N → ℕ) (i : Fin N) : subTuple α β i = ↑(α i) - ↑(β i)

Subtraction is computed entrywise. (def.sf.tuple-addition (b))

Algebraic properties of addition

theorem AlgebraicCombinatorics.addTuple_assoc {N : ℕ} (α β γ : Fin N → ℕ) : α + β + γ = α + (β + γ)

Addition of N-tuples is associative.

theorem AlgebraicCombinatorics.addTuple_comm {N : ℕ} (α β : Fin N → ℕ) : α + β = β + α

Addition of N-tuples is commutative.

@[simp]

theorem AlgebraicCombinatorics.addTuple_zeroTuple {N : ℕ} (α : Fin N → ℕ) : α + zeroTuple = α

The zero tuple is the right identity for addition.

@[simp]

theorem AlgebraicCombinatorics.zeroTuple_addTuple {N : ℕ} (α : Fin N → ℕ) : zeroTuple + α = α

The zero tuple is the left identity for addition.

Subtraction undoes addition

theorem AlgebraicCombinatorics.subTuple_add_left {N : ℕ} (α β : Fin N → ℕ) : subTuple (α + β) β = fun (i : Fin N) => ↑(α i)

Subtraction recovers the first argument from the sum. This formalizes "The subtraction operation − undoes +".

theorem AlgebraicCombinatorics.subTuple_add_right {N : ℕ} (α β : Fin N → ℕ) : subTuple (α + β) α = fun (i : Fin N) => ↑(β i)

Subtraction recovers the second argument from the sum.

@[simp]

theorem AlgebraicCombinatorics.subTuple_self {N : ℕ} (α : Fin N → ℕ) : subTuple α α = fun (x : Fin N) => 0

Subtracting a tuple from itself gives zero.

@[simp]

theorem AlgebraicCombinatorics.subTuple_zeroTuple {N : ℕ} (α : Fin N → ℕ) : subTuple α zeroTuple = fun (i : Fin N) => ↑(α i)

Subtracting zero gives the original tuple (as integers).

@[simp]

theorem AlgebraicCombinatorics.zeroTuple_subTuple {N : ℕ} (α : Fin N → ℕ) : subTuple zeroTuple α = fun (i : Fin N) => -↑(α i)

Subtracting from zero gives negation.

Interaction with N-partitions

theorem AlgebraicCombinatorics.isNPartition_add {N : ℕ} (α β : Fin N → ℕ) (hα : IsNPartition α) (hβ : IsNPartition β) : IsNPartition (α + β)

The sum of two N-partitions is an N-partition. This is an alias for IsNPartition.add from NPartition.lean.

def AlgebraicCombinatorics.rho (N : ℕ) : Fin N → ℕ

The staircase partition ρ = (N-1, N-2, ..., 1, 0).

Equations

• AlgebraicCombinatorics.rho N i = N - 1 - ↑i

theorem AlgebraicCombinatorics.rho_apply {N : ℕ} (i : Fin N) : rho N i = N - 1 - ↑i

theorem AlgebraicCombinatorics.isNPartition_rho {N : ℕ} : IsNPartition (rho N)

ρ is an N-partition when N > 0.

theorem AlgebraicCombinatorics.rho_strictAnti {N : ℕ} : StrictAnti (rho N)

The ρ vector is strictly decreasing

theorem AlgebraicCombinatorics.rho_antitone {N : ℕ} : Antitone (rho N)

The ρ vector is weakly decreasing

theorem AlgebraicCombinatorics.rho_zero {N : ℕ} (hN : 0 < N) : rho N ⟨0, hN⟩ = N - 1

The first component ρ_0 = N - 1 (when N > 0)

theorem AlgebraicCombinatorics.rho_last {N : ℕ} (hN : 0 < N) : rho N ⟨N - 1, ⋯⟩ = 0

The last component ρ_{N-1} = 0 (when N > 0)

theorem AlgebraicCombinatorics.rho_sum {N : ℕ} : ∑ i : Fin N, rho 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.

Tableaux and their content

We work with semistandard Young tableaux. The content of a tableau counts how many times each value appears.

Indexing Convention

This file uses 1-indexed columns for skew Young diagrams:

• A cell (i, j) is in Y(λ/μ) iff μ_i < j ≤ λ_i
• Column indices start at 1 (the first column is j = 1)
• This matches the textbook convention

SchurBasics.lean uses 0-indexed columns:

• A cell (i, j) is in Y(λ/μ) iff μ_i ≤ j < λ_i
• Column indices start at 0 (the first column is j = 0)
• This follows Mathlib/programming convention

Conversion: The bijection (i, j) ↔ (i, j+1) transforms between conventions. See SchurBasics.skewCellEquiv and SchurBasics.mem_skewYoungDiagram_iff_mem_LR_shifted for the explicit equivalences and conversion lemmas.

def AlgebraicCombinatorics.skewYoungDiagram {N : ℕ} (lam mu : Fin N → ℕ) : Set (Fin N × ℕ)

The skew Young diagram Y(lam/mu) as a set of cells. A cell (i,j) is in Y(lam/mu) if mu_i < j ≤ lam_i.

This is the Set version with 1-indexed columns (textbook convention). The first column is j = 1, not j = 0.

For the canonical Finset version with 0-indexed columns, see:

• NPartition.skewYoungDiagram in NPartition.lean (canonical, no [NeZero N] required)
• skewYoungDiagram in SchurBasics.lean (duplicate, requires [NeZero N])

Comparison:

• Here: (i, j) ∈ Y(λ/μ) iff μ_i < j ≤ λ_i (1-indexed)
• NPartition/SchurBasics: (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i (0-indexed)

The bijection between them is: (i, j) here ↔ (i, j-1) in NPartition/SchurBasics. See SchurBasics.mem_skewYoungDiagram_iff_mem_LR_shifted for the conversion lemma.

Equations

• AlgebraicCombinatorics.skewYoungDiagram lam mu = {c : Fin N × ℕ | mu c.1 < c.2 ∧ c.2 ≤ lam c.1}

instance AlgebraicCombinatorics.skewYoungDiagram_decidable {N : ℕ} (lam mu : Fin N → ℕ) (c : Fin N × ℕ) : Decidable (c ∈ skewYoungDiagram lam mu)

Decidability of membership in the skew Young diagram.

Equations

• AlgebraicCombinatorics.skewYoungDiagram_decidable lam mu c = inferInstanceAs (Decidable (mu c.1 < c.2 ∧ c.2 ≤ lam c.1))

def AlgebraicCombinatorics.Tableau {N : ℕ} (lam mu : Fin N → ℕ) : Type

A tableau of shape lam/mu is a function from cells to [N].

Equations

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

def AlgebraicCombinatorics.IsSemistandard {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : Prop

A tableau is semistandard if entries weakly increase along rows and strictly increase down columns.

Equations

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

noncomputable instance AlgebraicCombinatorics.skewYoungDiagram_fintype {N : ℕ} (lam mu : Fin N → ℕ) : Fintype { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }

The set of cells in the skew Young diagram as a Fintype.

Equations

• AlgebraicCombinatorics.skewYoungDiagram_fintype lam mu = ⋯.fintype

noncomputable def AlgebraicCombinatorics.contentTableau {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : Fin N → ℕ

Definition (def.sf.content): The content of a tableau T is the N-tuple counting occurrences of each value.

For a tableau T of shape λ/μ, we define the content of T to be the N-tuple (a₁, a₂, ..., a_N), where aᵢ = (# of i's in T) = (# of boxes c of T such that T(c) = i).

We denote this N-tuple by cont(T).

Example: If N=5, then cont([[1,1,2],[4]]) = (2,1,0,1,0).

Key property (eq.def.sf.content.xT=): x_T = x^(cont(T)) for any tableau T. (Both sides equal ∏ᵢ xᵢ^(# of i's in T).)

Equations

• AlgebraicCombinatorics.contentTableau T i = Nat.card { c : { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam mu } // T c = i }

def AlgebraicCombinatorics.termCont : Lean.ParserDescr

Equations

• AlgebraicCombinatorics.termCont = Lean.ParserDescr.node `AlgebraicCombinatorics.termCont 1024 (Lean.ParserDescr.symbol "cont")

Content API lemmas (def.sf.content)

theorem AlgebraicCombinatorics.contentTableau_eq_card {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i : Fin N) : contentTableau T i = {c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } | T c = i}.card

Alternative characterization: content counts cells using Finset.card.

theorem AlgebraicCombinatorics.contentTableau_sum {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : ∑ i : Fin N, contentTableau T i = Fintype.card { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }

The sum of content entries equals the number of cells in the tableau. (∑ᵢ cont(T)ᵢ = |Y(λ/μ)|)

This follows from the fact that content partitions the cells by their entries.

theorem AlgebraicCombinatorics.contentTableau_nonneg {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i : Fin N) : 0 ≤ contentTableau T i

Content is nonnegative (trivially true for ℕ, but stated for documentation).

theorem AlgebraicCombinatorics.contentTableau_eq_of_iff {N : ℕ} {lam mu : Fin N → ℕ} (T T' : Tableau lam mu) (i : Fin N) (h : ∀ (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }), T' c = i ↔ T c = i) : contentTableau T' i = contentTableau T i

If two tableaux have the same cells with value i (i.e., T' c = i ↔ T c = i for all c), then they have the same content at i. This is useful for proving that transformations that don't affect certain values preserve the content at those values.

@[reducible, inline]

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

x^α = ∏ᵢ xᵢ^(αᵢ) for an N-tuple α.

This is an alias for AlgebraicCombinatorics.SymmetricFunctions.monomialExp from MonomialSymmetric.lean. The two definitions are identical: both equal ∏ i, X i ^ α i.

See also: xPow_eq_monomialExp for the equivalence lemma.

Equations

• AlgebraicCombinatorics.xPow α = AlgebraicCombinatorics.SymmetricFunctions.monomialExp α

theorem AlgebraicCombinatorics.xPow_eq_monomialExp {R : Type u_1} [CommRing R] {N : ℕ} (α : Fin N → ℕ) : xPow α = SymmetricFunctions.monomialExp α

xPow equals monomialExp (definitional equality).

This lemma witnesses that the two definitions are the same:

• xPow α = ∏ i, X i ^ α i (from LittlewoodRichardson.lean)
• monomialExp α = ∏ i, X i ^ α i (from MonomialSymmetric.lean)

theorem AlgebraicCombinatorics.xPow_mul {R : Type u_1} [CommRing R] {N : ℕ} (α β : Fin N → ℕ) : xPow α * xPow β = xPow (α + β)

x^α · x^β = x^(α+β). (eq.def.sf.tuple-addition.xab)

This is equivalent to monomialExp_add from MonomialSymmetric.lean.

Column restriction of tableaux (def.sf.col-tab)

Definition (def.sf.col-tab): Let λ and μ be two N-partitions. Let T be a tableau of shape λ/μ. Let j be a positive integer. Then, col_{≥j}(T) means the restriction of T to columns j, j+1, j+2, ... (that is, the result of removing the first j-1 columns from T).

Formally speaking, this means the restriction of the map T to the set {(u,v) ∈ Y(λ/μ) | v ≥ j}.

Note: col_{≥1}(T) = T for any tableau T.

def AlgebraicCombinatorics.colGeq {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j } → Fin N

The restriction of a tableau to columns ≥ j. (def.sf.col-tab)

For a tableau T of shape λ/μ, colGeq T j is the restriction of T to the cells in columns j, j+1, j+2, ... This is the formal definition of col_{≥j}(T).

The domain is {(u,v) ∈ Y(λ/μ) | v ≥ j}, and the function returns T(u,v) for each such cell.

Equations

• AlgebraicCombinatorics.colGeq T j ⟨c, hc⟩ = T ⟨c, ⋯⟩

@[simp]

theorem AlgebraicCombinatorics.colGeq_apply {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j }) : colGeq T j c = T ⟨↑c, ⋯⟩

col_{≥j}(T) at cell c equals T at cell c. (def.sf.col-tab)

This is the defining property: the restriction to columns ≥ j simply returns the same value as T at each cell.

theorem AlgebraicCombinatorics.colGeq_col_ge {N : ℕ} {lam mu : Fin N → ℕ} (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j }) : (↑c).2 ≥ j

For any cell in the domain of col_{≥j}(T), its column index is at least j.

theorem AlgebraicCombinatorics.colGeq_one {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 }) : colGeq T 1 c = T ⟨↑c, ⋯⟩

col_{≥1}(T) = T for any tableau T.

This is a key property from the source text: "Note that col_{≥1}(T) = T for any tableau T."

theorem AlgebraicCombinatorics.skewYoungDiagram_col_pos {N : ℕ} {lam mu : Fin N → ℕ} (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : (↑c).2 ≥ 1

Every cell in a skew Young diagram has column ≥ 1.

This is because cells (i,j) in Y(λ/μ) satisfy μ_i < j, and μ_i ≥ 0, so j ≥ 1. This is why col_{≥1}(T) has the same domain as T.

def AlgebraicCombinatorics.embedColGeqOne {N : ℕ} {lam mu : Fin N → ℕ} : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } → { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 }

The embedding from the domain of T to the domain of col_{≥1}(T).

Since every cell in Y(λ/μ) has column ≥ 1, this is a natural inclusion.

Equations

• AlgebraicCombinatorics.embedColGeqOne c = ⟨↑c, ⋯⟩

def AlgebraicCombinatorics.embedFromColGeqOne {N : ℕ} {lam mu : Fin N → ℕ} : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 } → { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }

The projection from the domain of col_{≥1}(T) to the domain of T.

Equations

• AlgebraicCombinatorics.embedFromColGeqOne c = ⟨↑c, ⋯⟩

theorem AlgebraicCombinatorics.embedColGeqOne_embedFromColGeqOne {N : ℕ} {lam mu : Fin N → ℕ} (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 }) : embedColGeqOne (embedFromColGeqOne c) = c

embedColGeqOne is a left inverse of embedFromColGeqOne.

theorem AlgebraicCombinatorics.embedFromColGeqOne_embedColGeqOne {N : ℕ} {lam mu : Fin N → ℕ} (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : embedFromColGeqOne (embedColGeqOne c) = c

embedFromColGeqOne is a left inverse of embedColGeqOne.

def AlgebraicCombinatorics.equivColGeqOne {N : ℕ} {lam mu : Fin N → ℕ} : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } ≃ { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 }

The domain of col_{≥1}(T) is equivalent to the domain of T.

This formalizes the note "col_{≥1}(T) = T for any tableau T" from the source: the two functions have equivalent domains and agree on corresponding elements.

Equations

• AlgebraicCombinatorics.equivColGeqOne = { toFun := AlgebraicCombinatorics.embedColGeqOne, invFun := AlgebraicCombinatorics.embedFromColGeqOne, left_inv := ⋯, right_inv := ⋯ }

theorem AlgebraicCombinatorics.colGeq_one_eq_tableau {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : colGeq T 1 ∘ embedColGeqOne = T

col_{≥1}(T) = T (as functions, up to domain equivalence).

This is the formal statement of "Note that col_{≥1}(T) = T for any tableau T" from the source text.

def AlgebraicCombinatorics.embedColGeq {N : ℕ} {lam mu : Fin N → ℕ} {j k : ℕ} (hjk : j ≤ k) : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ k } → { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j }

The embedding from the domain of col_{≥k}(T) to the domain of col_{≥j}(T) when j ≤ k.

Equations

• AlgebraicCombinatorics.embedColGeq hjk c = ⟨↑c, ⋯⟩

theorem AlgebraicCombinatorics.colGeq_compose {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) {j k : ℕ} (hjk : j ≤ k) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ k }) : colGeq T j (embedColGeq hjk c) = colGeq T k c

Composing column restrictions: col_{≥k}(T) factors through col_{≥j}(T) when j ≤ k.

theorem AlgebraicCombinatorics.colGeq_empty_of_large {N : ℕ} {lam mu : Fin N → ℕ} (j : ℕ) (hj : ∀ (i : Fin N), lam i < j) : IsEmpty { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j }

The domain of col_{≥j}(T) is empty when j exceeds all column indices in the diagram.

This corresponds to the example in the source text where col_{≥5}(T) = (empty tableau) when the tableau has no columns ≥ 5.

theorem AlgebraicCombinatorics.colGeq_domain_subset {N : ℕ} {lam mu : Fin N → ℕ} {j k : ℕ} (hjk : j ≤ k) : {c : Fin N × ℕ | c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ k} ⊆ {c : Fin N × ℕ | c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ j}

Monotonicity: if j ≤ k, then the domain of col_{≥k}(T) is a subset of the domain of col_{≥j}(T).

theorem AlgebraicCombinatorics.colGeq_zero_domain {N : ℕ} {lam mu : Fin N → ℕ} : {c : Fin N × ℕ | c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 0} = {c : Fin N × ℕ | c ∈ skewYoungDiagram lam mu}

The domain of col_{≥0}(T) equals the entire domain of T (since all columns are ≥ 0).

noncomputable def AlgebraicCombinatorics.contentColGeq {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) : Fin N → ℕ

The content of a restricted tableau col_{≥j}(T). Counts occurrences of each value in columns j and beyond.

Equations

• AlgebraicCombinatorics.contentColGeq T j i = Nat.card { c : { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam mu ∧ c.2 ≥ j } // T ⟨↑c, ⋯⟩ = i }

Yamanouchi tableaux

A semistandard tableau T is ν-Yamanouchi if ν + cont(col_{≥j}(T)) is an N-partition for every positive integer j.

def AlgebraicCombinatorics.IsYamanouchi {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) : Prop

A semistandard tableau T of shape λ/μ is ν-Yamanouchi if for each positive integer j, the N-tuple ν + cont(col_{≥j}(T)) is an N-partition (i.e., weakly decreasing).

Definition (def.sf.yamanouchi): Let λ, μ, ν be three N-partitions. A semistandard tableau T of shape λ/μ is said to be ν-Yamanouchi if for each positive integer j, the N-tuple ν + cont(col_{≥j}T) ∈ ℕ^N is an N-partition (i.e., weakly decreasing).

Key properties:

• The condition ensures that as we process the tableau column by column from right to left, starting with tally ν, the running tally always remains weakly decreasing.
• For j = 1, we get that ν + cont(T) is an N-partition (see IsYamanouchi.isNPartition_add_content).
• A 0-Yamanouchi tableau (also called a "ballot tableau") has content that is itself an N-partition.

Voting interpretation (rmk.sf.yamanouchi.votes): Think of each entry i in T as a vote for candidate i. Starting with tally ν and counting votes column by column from right to left, the tally must remain weakly decreasing at every step. Since columns have distinct entries (strictly increasing), no candidate gains more than one vote at a time.

Equations

• AlgebraicCombinatorics.IsYamanouchi nu T = (AlgebraicCombinatorics.IsSemistandard T ∧ ∀ j > 0, AlgebraicCombinatorics.IsNPartition (nu + AlgebraicCombinatorics.contentColGeq T j))

API lemmas for IsYamanouchi

theorem AlgebraicCombinatorics.IsYamanouchi.isSemistandard {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} (h : IsYamanouchi nu T) : IsSemistandard T

A ν-Yamanouchi tableau is semistandard.

theorem AlgebraicCombinatorics.IsYamanouchi.isNPartition_add_contentColGeq {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} (h : IsYamanouchi nu T) {j : ℕ} (hj : j > 0) : IsNPartition (nu + contentColGeq T j)

For a ν-Yamanouchi tableau T and any j > 0, ν + cont(col_{≥j}(T)) is an N-partition.

theorem AlgebraicCombinatorics.isYamanouchi_iff {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} : IsYamanouchi nu T ↔ IsSemistandard T ∧ ∀ j > 0, IsNPartition (nu + contentColGeq T j)

Constructing a Yamanouchi tableau from its components.

theorem AlgebraicCombinatorics.skewYoungDiagram_col_ge_one {N : ℕ} {lam mu : Fin N → ℕ} (c : Fin N × ℕ) (hc : c ∈ skewYoungDiagram lam mu) : c.2 ≥ 1

A cell in the skew diagram has column index ≥ 1 (since column indices start from 1 in the standard convention where column j contains cells with c.2 = j).

noncomputable def AlgebraicCombinatorics.skewDiagramColGeqOneEquiv {N : ℕ} (lam mu : Fin N → ℕ) : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 } ≃ { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }

The type of cells in the skew diagram with column ≥ 1 is equivalent to the full diagram.

Equations

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

noncomputable def AlgebraicCombinatorics.contentColGeqOneEquiv {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i : Fin N) : { c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu ∧ c.2 ≥ 1 } // T ⟨↑c, ⋯⟩ = i } ≃ { c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu } // T c = i }

Equivalence between cells with entry i in col_{≥1} and all cells with entry i.

Equations

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

theorem AlgebraicCombinatorics.contentColGeq_one_eq_contentTableau {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : contentColGeq T 1 = contentTableau T

col_{≥1}(T) = T, i.e., the content of col_{≥1}(T) equals the content of T. This is because all cells in the skew diagram have column index ≥ 1.

theorem AlgebraicCombinatorics.contentColGeq_mono {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) (i : Fin N) : contentColGeq T (j + 1) i ≤ contentColGeq T j i

contentColGeq is monotonic: cells in columns >= j+1 are a subset of cells in columns >= j.

theorem AlgebraicCombinatorics.contentColGeq_succ_le {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (_hT : IsSemistandard T) (j : ℕ) (i : Fin N) : contentColGeq T j i ≤ contentColGeq T (j + 1) i + 1

For semistandard tableaux, contentColGeq T j i ≤ contentColGeq T (j+1) i + 1. This is because adding column j can add at most 1 cell with entry i (since columns are strictly increasing in semistandard tableaux).

theorem AlgebraicCombinatorics.contentTableau_ge_contentColGeq {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) (i : Fin N) : contentTableau T i ≥ contentColGeq T j i

contentTableau is at least contentColGeq for any j. This is because contentColGeq counts cells in columns >= j, which is a subset of all cells.

theorem AlgebraicCombinatorics.IsYamanouchi.isNPartition_add_content {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} (h : IsYamanouchi nu T) : IsNPartition (nu + contentTableau T)

Key property: For a ν-Yamanouchi tableau T, ν + cont(T) is an N-partition. This is the j=1 case of the Yamanouchi condition, and is essential for the Littlewood-Richardson rule since it ensures the output partitions are valid.

theorem AlgebraicCombinatorics.isNPartition_zero {N : ℕ} : IsNPartition 0

The zero N-tuple is an N-partition. This is an alias for isNPartition_zero from NPartition.lean.

theorem AlgebraicCombinatorics.IsNPartition.add {N : ℕ} {α β : Fin N → ℕ} (hα : IsNPartition α) (hβ : IsNPartition β) : IsNPartition (α + β)

Adding two N-partitions gives an N-partition. This is an alias for IsNPartition.add from NPartition.lean.

theorem AlgebraicCombinatorics.IsYamanouchi.isNPartition_content_of_zero {N : ℕ} {lam mu : Fin N → ℕ} {T : Tableau lam mu} (h : IsYamanouchi zeroTuple T) : IsNPartition (contentTableau T)

A 0-Yamanouchi tableau (ballot tableau) has content that is itself an N-partition.

Voting metaphor for Yamanouchi condition

The Yamanouchi condition can be understood through a voting metaphor (rmk.sf.yamanouchi.votes):

• Each entry i in T is a vote for candidate i
• We count votes column by column, from right to left
• Starting with tally ν, after processing each column, the tally must remain weakly decreasing
• Key observation: no candidate gains more than one vote at a time (since columns have distinct entries)

Alternants and Schur polynomials

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

The alternant a_α = ∑{σ ∈ S_N} sign(σ) · x^(σ·α). Here σ·α means (α{σ(1)}, α_{σ(2)}, ..., α_{σ(N)}).

Equivalence with SchurBasics.alternant: This sum-based definition equals the determinant-based definition in alternant (from SchurBasics.lean). See alternant_eq_det for the proof that this equals det(alternantMatrix α).

Equations

• AlgebraicCombinatorics.alternant α = ∑ σ : Equiv.Perm (Fin N), Equiv.Perm.sign σ • AlgebraicCombinatorics.xPow (α ∘ ⇑σ)

noncomputable def AlgebraicCombinatorics.vandermonde {R : Type u_1} [CommRing R] {N : ℕ} : MvPolynomial (Fin N) R

The Vandermonde determinant: a_ρ = ∏_{i<j} (xᵢ - xⱼ). (eq.def.sf.alternants.arho=vdm)

Equations

• AlgebraicCombinatorics.vandermonde = ∏ i : Fin N, ∏ j : Fin N, if i < j then MvPolynomial.X i - MvPolynomial.X j else 1

Helper lemmas for alternant_rho_eq_vandermonde

noncomputable def AlgebraicCombinatorics.alternantMatrix {R : Type u_1} [CommRing R] {N : ℕ} (α : Fin N → ℕ) : Matrix (Fin N) (Fin N) (MvPolynomial (Fin N) R)

Matrix whose determinant equals the alternant. Entry (i, j) is x_j^{α_i}.

Equations

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

theorem AlgebraicCombinatorics.alternant_eq_det {R : Type u_1} [CommRing R] {N : ℕ} (α : Fin N → ℕ) : alternant α = (alternantMatrix α).det

The sum-based alternant definition equals the determinant of the alternant matrix.

This establishes the equivalence: ∑ σ : Perm (Fin N), sign(σ) • x^(α ∘ σ) = det(x_j^{α_i})

The determinant-based definition is used in SchurBasics.lean (see alternant there), while this file uses the sum-based definition. This theorem proves they are equal.

theorem AlgebraicCombinatorics.alternant_rho_eq_vandermonde {R : Type u_1} [CommRing R] {N : ℕ} : alternant (rho N) = vandermonde

a_ρ equals the Vandermonde determinant.

theorem AlgebraicCombinatorics.alternant_eq_zero_of_repeated {R : Type u_1} [CommRing R] {N : ℕ} {α : Fin N → ℕ} (h : ∃ (i : Fin N) (j : Fin N), i ≠ j ∧ α i = α j) : alternant α = 0

If α has two equal entries, then a_α = 0. (lem.sf.alternant-0 (a))

theorem AlgebraicCombinatorics.alternant_swap {R : Type u_1} [CommRing R] {N : ℕ} {α : Fin N → ℕ} {i j : Fin N} (hij : i ≠ j) : alternant (α ∘ ⇑(Equiv.swap i j)) = -alternant α

Swapping two entries of α negates the alternant. (lem.sf.alternant-0 (b))

Regular elements and cancellation

This section formalizes Definition def.cring.reg from the source material.

Definition (def.cring.reg)

Let L be a commutative ring. Let a ∈ L. The element a of L is said to be regular if and only if every x ∈ L satisfying ax = 0 satisfies x = 0.

Regular elements are also called "non-zero-divisors" or "cancellable" elements.

Connection to Mathlib

In Mathlib, the relevant concepts are:

• IsLeftRegular a: left multiplication by a is injective (i.e., a * x = a * y → x = y)
• IsRightRegular a: right multiplication by a is injective
• IsRegular a: both left and right regular

The textbook definition (ax = 0 → x = 0) is equivalent to IsLeftRegular in any ring. In a commutative ring, IsLeftRegular and IsRightRegular are equivalent, so IsRegular is equivalent to either one.

The key equivalence is isLeftRegular_iff_right_eq_zero_of_mul from Mathlib: IsLeftRegular r ↔ ∀ x, r * x = 0 → x = 0

def AlgebraicCombinatorics.IsRegularElement {L : Type u_2} [CommRing L] (a : L) : Prop

Definition (def.cring.reg): An element a of a commutative ring L is regular if and only if every x ∈ L satisfying a * x = 0 satisfies x = 0.

This is the textbook definition. We show it's equivalent to Mathlib's IsLeftRegular. In commutative rings, this is also equivalent to IsRegular and IsRightRegular.

Equations

• AlgebraicCombinatorics.IsRegularElement a = ∀ (x : L), a * x = 0 → x = 0

theorem AlgebraicCombinatorics.isRegularElement_iff_isLeftRegular {L : Type u_2} [CommRing L] {a : L} : IsRegularElement a ↔ IsLeftRegular a

The textbook definition of regular is equivalent to Mathlib's IsLeftRegular.

theorem AlgebraicCombinatorics.isRegularElement_iff_isRightRegular {L : Type u_2} [CommRing L] {a : L} : IsRegularElement a ↔ IsRightRegular a

In a commutative ring, IsRegularElement is equivalent to IsRightRegular.

theorem AlgebraicCombinatorics.isRegularElement_iff_isRegular {L : Type u_2} [CommRing L] {a : L} : IsRegularElement a ↔ IsRegular a

In a commutative ring, IsRegularElement is equivalent to Mathlib's IsRegular.

theorem AlgebraicCombinatorics.isRegularElement_iff_mem_nonZeroDivisorsLeft {L : Type u_2} [CommRing L] {a : L} : IsRegularElement a ↔ a ∈ nonZeroDivisorsLeft L

IsRegularElement is equivalent to membership in nonZeroDivisorsLeft.

theorem AlgebraicCombinatorics.isRegularElement_iff_mem_nonZeroDivisors {L : Type u_2} [CommRing L] {a : L} : IsRegularElement a ↔ a ∈ nonZeroDivisors L

In a commutative ring, IsRegularElement is equivalent to membership in nonZeroDivisors.

theorem AlgebraicCombinatorics.IsRegularElement.ne_zero {L : Type u_2} [CommRing L] [Nontrivial L] {a : L} (ha : IsRegularElement a) : a ≠ 0

Regular elements are non-zero in a nontrivial ring.

theorem AlgebraicCombinatorics.not_isRegularElement_zero {L : Type u_2} [CommRing L] [Nontrivial L] : ¬IsRegularElement 0

Zero is not regular in a nontrivial ring.

theorem AlgebraicCombinatorics.IsUnit.isRegularElement' {L : Type u_2} [CommRing L] {a : L} (ha : IsUnit a) : IsRegularElement a

Units are regular.

theorem AlgebraicCombinatorics.isRegularElement_one {L : Type u_2} [CommRing L] : IsRegularElement 1

One is regular.

theorem AlgebraicCombinatorics.IsRegularElement.mul {L : Type u_2} [CommRing L] {a b : L} (ha : IsRegularElement a) (hb : IsRegularElement b) : IsRegularElement (a * b)

The product of regular elements is regular.

theorem AlgebraicCombinatorics.IsRegularElement.cancel {L : Type u_2} [CommRing L] {a u v : L} (ha : IsRegularElement a) (h : a * u = a * v) : u = v

Lemma (lem.cring.reg.cancel): Regular elements can be cancelled. Let L be a commutative ring. Let a, u, v ∈ L be such that a is regular. Assume that au = av. Then u = v.

theorem AlgebraicCombinatorics.IsRegularElement.cancel_of_mul_eq_zero {L : Type u_2} [CommRing L] {a x : L} (ha : IsRegularElement a) (h : a * x = 0) : x = 0

Variant of the cancellation lemma using subtraction.

theorem AlgebraicCombinatorics.isRegular_cancel {L : Type u_2} [CommRing L] {a u v : L} (ha : IsRegular a) (h : a * u = a * v) : u = v

Regular elements can be cancelled (using Mathlib's IsRegular). (lem.cring.reg.cancel) This is a direct consequence of IsLeftRegular (injectivity of left multiplication).

theorem AlgebraicCombinatorics.X_sub_X_ne_zero {R : Type u_1} [CommRing R] {N : ℕ} [IsDomain R] (i j : Fin N) (hij : i ≠ j) : MvPolynomial.X i - MvPolynomial.X j ≠ 0

X i - X j is non-zero when i ≠ j (in a polynomial ring over an integral domain).

theorem AlgebraicCombinatorics.vandermonde_ne_zero {R : Type u_1} [CommRing R] {N : ℕ} [IsDomain R] : vandermonde ≠ 0

The Vandermonde polynomial is non-zero (in a polynomial ring over an integral domain).

theorem AlgebraicCombinatorics.alternant_rho_isRegular {R : Type u_1} [CommRing R] {N : ℕ} [IsDomain R] : IsRegular (alternant (rho N))

The alternant a_ρ is a regular element of the polynomial ring. (lem.sf.arho-reg)

Note: This requires R to be an integral domain. In a non-integral domain, the polynomial ring has zero divisors and regularity may fail.

Schur polynomials

noncomputable def AlgebraicCombinatorics.monomialTableau {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : MvPolynomial (Fin N) R

The monomial x_T = ∏_i x_i^(# of i's in T) for a tableau T. By definition, this equals x^(cont(T)).

Equations

• AlgebraicCombinatorics.monomialTableau T = AlgebraicCombinatorics.xPow (AlgebraicCombinatorics.contentTableau T)

theorem AlgebraicCombinatorics.monomialTableau_eq_xPow_content {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : monomialTableau T = xPow (contentTableau T)

Equation (eq.def.sf.content.xT=): The monomial x_T equals x^(cont(T)).

This is the key property of the content: both sides equal ∏ᵢ xᵢ^(# of i's in T).

This is definitional since monomialTableau is defined as xPow (contentTableau T).

Finiteness of tableaux

The set of semistandard tableaux of any fixed shape is finite, since entries are bounded by N and the shape is finite. Similarly, the set of Yamanouchi tableaux is finite.

noncomputable instance AlgebraicCombinatorics.isSemistandard_decidable {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) : Decidable (IsSemistandard T)

IsSemistandard is decidable since it's a conjunction of foralls over finite types.

Equations

• AlgebraicCombinatorics.isSemistandard_decidable T = id inferInstance

noncomputable instance AlgebraicCombinatorics.tableau_fintype {N : ℕ} (lam mu : Fin N → ℕ) : Fintype (Tableau lam mu)

The type of all tableaux of a given shape is finite. This follows from the fact that entries are in Fin N and the shape is finite.

Equations

• AlgebraicCombinatorics.tableau_fintype lam mu = id inferInstance

noncomputable instance AlgebraicCombinatorics.semistandardTableau_fintype {N : ℕ} (lam mu : Fin N → ℕ) : Fintype { T : Tableau lam mu // IsSemistandard T }

The type of semistandard tableaux of a given shape is finite. This follows from the fact that entries are bounded by N and the shape is finite.

Equations

• AlgebraicCombinatorics.semistandardTableau_fintype lam mu = Fintype.subtype (Finset.filter AlgebraicCombinatorics.IsSemistandard Finset.univ) ⋯

noncomputable def AlgebraicCombinatorics.skewSchurPoly {R : Type u_1} [CommRing R] {N : ℕ} (lam mu : Fin N → ℕ) : MvPolynomial (Fin N) R

The skew Schur polynomial s_{lam/mu}. Defined as a sum over semistandard tableaux of shape lam/mu: s_{lam/mu} = ∑_{T semistandard of shape lam/mu} x^(cont(T))

Note: This is a finite sum since there are finitely many semistandard tableaux of any given shape (entries are bounded by N).

Relationship to Other Definitions

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

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

When to use which:

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

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

Equations

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

noncomputable def AlgebraicCombinatorics.schurPoly {R : Type u_1} [CommRing R] {N : ℕ} (lam : Fin N → ℕ) : MvPolynomial (Fin N) R

The Schur polynomial s_lam for an N-partition lam. Defined as s_{lam/0}, i.e., the skew Schur polynomial with empty inner shape.

Relationship to Other Definitions

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

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

When to use which:

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

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

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

Equations

• AlgebraicCombinatorics.schurPoly lam = AlgebraicCombinatorics.skewSchurPoly lam 0

theorem AlgebraicCombinatorics.skewSchurPoly_zero {R : Type u_1} [CommRing R] {N : ℕ} (lam : Fin N → ℕ) : skewSchurPoly lam 0 = schurPoly lam

s_{lam/0} = s_lam for any partition lam (definitional).

noncomputable instance AlgebraicCombinatorics.yamanouchiTableau_fintype {N : ℕ} (lam mu nu : Fin N → ℕ) : Fintype { T : Tableau lam mu // IsYamanouchi nu T }

The type of Yamanouchi tableaux of a given shape is finite. This follows from the finiteness of tableaux (Yamanouchi tableaux are a subset).

Equations

• AlgebraicCombinatorics.yamanouchiTableau_fintype lam mu nu = ⋯.fintype

Bender-Knuth Involutions

The Bender-Knuth involutions are key tools for proving properties of Schur polynomials. For each k ∈ [N-1], the k-th Bender-Knuth involution BK_k is a bijection on semistandard tableaux that swaps certain k's and (k+1)'s while preserving the SSYT property.

Definition

For a semistandard tableau T and k ∈ [N-1], the Bender-Knuth involution BK_k works as follows:

1. For each row i, consider the cells containing k or k+1
2. Partition these cells into "free" and "forced" based on column constraints:
   • A cell with value k is "forced" if the cell above it has value k
   • A cell with value k+1 is "forced" if the cell below it has value k+1
   • All other k's and (k+1)'s are "free"
3. In each row, swap the free k's with the free (k+1)'s

Key Properties

1. Involution: BK_k ∘ BK_k = id
2. Preserves SSYT: If T is semistandard, so is BK_k(T)
3. Content change: cont(BK_k(T)) differs from cont(T) by swapping entries k and k+1
4. Monomial change: x_{BK_k(T)} = s_k · x_T where s_k swaps x_k and x_{k+1}

References

• [Stanley, EC2, Section 7.10]
• [Fulton, Young Tableaux, Section 4.3]
• [Bender-Knuth, "Enumeration of plane partitions", 1972]

Helper function for swapping adjacent values

def AlgebraicCombinatorics.swapAdjacentFin {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v : Fin N) : Fin N

Swap adjacent values k and k+1 in a Fin N.

Equations

• AlgebraicCombinatorics.swapAdjacentFin k hk v = if v = k then ⟨↑k + 1, hk⟩ else if v = ⟨↑k + 1, hk⟩ then k else v

@[simp]

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

@[simp]

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

theorem AlgebraicCombinatorics.swapAdjacentFin_other {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v : Fin N) (hv1 : v ≠ k) (hv2 : v ≠ ⟨↑k + 1, hk⟩) : swapAdjacentFin k hk v = v

@[simp]

theorem AlgebraicCombinatorics.swapAdjacentFin_involutive {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v : Fin N) : swapAdjacentFin k hk (swapAdjacentFin k hk v) = v

theorem AlgebraicCombinatorics.swapAdjacentFin_ne_k_iff {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v : Fin N) : swapAdjacentFin k hk v ≠ k ↔ v ≠ ⟨↑k + 1, hk⟩

The swap preserves the "not equal to k" property for values other than k+1.

theorem AlgebraicCombinatorics.swapAdjacentFin_ne_kSucc_iff {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v : Fin N) : swapAdjacentFin k hk v ≠ ⟨↑k + 1, hk⟩ ↔ v ≠ k

The swap preserves the "not equal to k+1" property for values other than k.

theorem AlgebraicCombinatorics.swapAdjacentFin_lt_iff_of_ne {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) (v w : Fin N) (hv1 : v ≠ k) (hv2 : v ≠ ⟨↑k + 1, hk⟩) (hw1 : w ≠ k) (hw2 : w ≠ ⟨↑k + 1, hk⟩) : swapAdjacentFin k hk v < swapAdjacentFin k hk w ↔ v < w

The swap is order-preserving on values not equal to k or k+1.

theorem AlgebraicCombinatorics.swapAdjacentFin_k_lt_kSucc {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) : swapAdjacentFin k hk ⟨↑k + 1, hk⟩ < swapAdjacentFin k hk k

Swapping k and k+1 reverses their order.

noncomputable def AlgebraicCombinatorics.rowCount {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) : ℕ

In row i of tableau T, count the number of cells with value k. This is used to define the Bender-Knuth involution.

Equations

• AlgebraicCombinatorics.rowCount T i k = Nat.card { c : { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam mu } // (↑c).1 = i ∧ T c = k }

def AlgebraicCombinatorics.isForcedK {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A cell containing k is "k-forced" if there's a k+1 directly BELOW it in the same column. This means the k and the k+1 below it form a "pair" that won't be swapped by BK_k.

Note: The original (incorrect) definition said "k above k", but in a semistandard tableau, entries strictly increase down columns, so you can't have the same value in vertically adjacent cells. The correct definition is: k is paired with k+1 below it.

Equations

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

def AlgebraicCombinatorics.isForcedKSucc {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A cell containing k+1 is "(k+1)-forced" if there's a k directly ABOVE it in the same column. This means the k above and this k+1 form a "pair" that won't be swapped by BK_k.

Note: The original (incorrect) definition said "k+1 below k+1", but in a semistandard tableau, entries strictly increase down columns. The correct definition is: k+1 is paired with k above it.

Equations

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

def AlgebraicCombinatorics.isFreeCell {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A cell containing k or k+1 is "free" if it is not forced. Free cells can be swapped by the Bender-Knuth involution.

Equations

• AlgebraicCombinatorics.isFreeCell T k hk c = (T c = k ∧ ¬AlgebraicCombinatorics.isForcedK T k hk c ∨ T c = ⟨↑k + 1, hk⟩ ∧ ¬AlgebraicCombinatorics.isForcedKSucc T k hk c)

noncomputable def AlgebraicCombinatorics.freeKCount {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) : ℕ

Count of free k's in row i.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKSuccCount {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) : ℕ

Count of free (k+1)'s in row i.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKCountBefore {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) : ℕ

Count of free k's in row i with column strictly less than j. Used for the parenthesis-matching algorithm in Bender-Knuth.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKCountUpTo {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) : ℕ

Count of free k's in row i with column at most j. Used for the parenthesis-matching algorithm in Bender-Knuth.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKSuccCountUpTo {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) : ℕ

Count of free (k+1)'s in row i with column at most j. Used for the parenthesis-matching algorithm in Bender-Knuth.

Equations

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

def AlgebraicCombinatorics.isUnmatchedFreeK {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A free k at position c is "unmatched" in the parenthesis-matching sense.

The Bender-Knuth involution uses a parenthesis-matching algorithm:

• Read free entries left-to-right in each row
• Each free (k+1) matches with the nearest unmatched free k to its left
• Unmatched entries get swapped

A free k is unmatched iff at its position, the cumulative count of free k's exceeds the TOTAL count of free (k+1)'s in the row. In other words, there aren't enough (k+1)'s in the entire row to match all the k's up to this position.

This definition correctly implements the standard parenthesis-matching algorithm:

• Unmatched k's are exactly those at positions where there's an "excess" of k's
• These are the rightmost free k's that don't have a (k+1) to match with

Note: We compare freeKCountUpTo(c) with freeKSuccCount (total), not freeKSuccCountUpTo(c), because a k can match with any (k+1) to its right, not just (k+1)'s up to its position.

Equations

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

def AlgebraicCombinatorics.isUnmatchedFreeKSucc {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A free (k+1) at position c is "unmatched" in the parenthesis-matching sense.

In the BK involution on a semistandard row with a free k's followed by b free (k+1)'s:

• If b > a: the LEFTMOST (b-a) free (k+1)'s are unmatched → become k
• If a ≥ b: all free (k+1)'s are matched (paired with the rightmost b free k's)

A free (k+1) at position c is unmatched iff it's among the leftmost (b-a) free (k+1)'s, i.e., the cumulative count of free (k+1)'s up to c is at most (b-a).

Equivalently: freeKSuccCountUpTo(c) + freeKCount ≤ freeKSuccCount

This marks the LEFTMOST excess (k+1)'s as unmatched, which is correct for the BK involution. The matched pairs are: leftmost min(a,b) k's paired with rightmost min(a,b) (k+1)'s.

Note: The previous (incorrect) definition used freeKSuccCountUpTo > freeKCountUpTo, which marked RIGHTMOST (k+1)'s as unmatched — the wrong polarity.

Equations

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

def AlgebraicCombinatorics.isMatchedFreeK {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A matched free k is a free k that is not unmatched. In the parenthesis-matching algorithm, these are the k's that get paired with (k+1)'s.

Equations

• AlgebraicCombinatorics.isMatchedFreeK T k hk c = (T c = k ∧ ¬AlgebraicCombinatorics.isForcedK T k hk c ∧ ¬AlgebraicCombinatorics.isUnmatchedFreeK T k hk c)

def AlgebraicCombinatorics.isMatchedFreeKSucc {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A matched free (k+1) is a free (k+1) that is not unmatched. In the parenthesis-matching algorithm, these are the (k+1)'s that get paired with k's.

Equations

• AlgebraicCombinatorics.isMatchedFreeKSucc T k hk c = (T c = ⟨↑k + 1, hk⟩ ∧ ¬AlgebraicCombinatorics.isForcedKSucc T k hk c ∧ ¬AlgebraicCombinatorics.isUnmatchedFreeKSucc T k hk c)

noncomputable def AlgebraicCombinatorics.benderKnuth {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (_hT : IsSemistandard T) : Tableau lam mu

The Bender-Knuth involution BK_k on semistandard tableaux.

This involution swaps UNMATCHED free k's with UNMATCHED free (k+1)'s in each row, using a parenthesis-matching algorithm that preserves semistandardness.

Algorithm (for each row independently):

1. Identify all "free" entries (k's not paired with k+1 below, (k+1)'s not paired with k above)
2. Read free entries left-to-right, matching each (k+1) with nearest unmatched k to its left
3. Swap only the UNMATCHED entries: unmatched k → k+1, unmatched (k+1) → k

Why this preserves row-weak ordering:

• Matched pairs don't change
• Unmatched k's (which become k+1) are always to the RIGHT of all matched (k+1)'s
• Unmatched (k+1)'s (which become k) are always to the LEFT of all matched k's

Key theorem: This is an involution that preserves semistandardness and swaps the counts of k and k+1 in the content.

Note: The naive cell-by-cell swap (swapping ALL free entries) is INCORRECT because adjacent free k and free (k+1) would become (k+1, k), violating row-weak ordering. The parenthesis-matching ensures only non-adjacent free entries get swapped.

Equations

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

theorem AlgebraicCombinatorics.forced_k_preserved' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hforced : isForcedK T k hk c) : have T' := benderKnuth k hk T hT; isForcedK T' k hk c

Forced k cells remain forced after Bender-Knuth.

theorem AlgebraicCombinatorics.forced_kSucc_preserved' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hforced : isForcedKSucc T k hk c) : have T' := benderKnuth k hk T hT; isForcedKSucc T' k hk c

Forced (k+1) cells remain forced after Bender-Knuth.

Key lemmas for benderKnuth_involutive

The proof of involutivity requires showing that the matching structure is preserved under BK. The key insights are:

1. Matching symmetry: If a free k at position c is matched with a free (k+1) at position c', then after BK, both stay as their original values (k and k+1).

2. Unmatched symmetry: An unmatched free k becomes an unmatched free (k+1) in T', and an unmatched free (k+1) becomes an unmatched free k in T'.

3. Row-weak preservation: In each row, the ordering of entries is preserved because:

   • Unmatched (k+1)'s (→ k) are to the LEFT of matched entries
   • Unmatched k's (→ k+1) are to the RIGHT of matched entries

4. Column-strict preservation: Forced pairs stay together, and free cells in the same column have the same matching status (since they're in the same row).

Partner functions for forced cells

Forced k cells and forced (k+1) cells come in pairs: each forced k has exactly one forced (k+1) directly below it, and vice versa. These helper functions extract the partner cell, which is useful for proving the content swap property.

Free k cells and column ordering

The following section documents the structure needed to prove matchedFreeK_card_eq_matchedFreeKSucc_card.

Key insight: Free k cells in a given row can be ordered by column. If we denote the columns of free k cells in row i as c₁ < c₂ < ... < cₘ, then:

• freeKCountUpTo(cⱼ) = j for each j (by definition of freeKCountUpTo)
• A free k cell at column cⱼ is matched iff freeKCountUpTo(cⱼ) ≤ freeKSuccCount, i.e., j ≤ n
• There are min(m, n) such cells

The formal proof requires:

1. Showing that free k columns in row i form a finset S
2. Using S.orderEmbOfFin to establish the bijection with Fin m
3. Showing that freeKCountUpTo at the j-th column equals j+1 (via count_le_nth_smallest)
4. Applying matched_position_count to count matched cells

The helper lemmas count_le_nth_smallest and matched_position_count provide the counting infrastructure. The remaining work is to formalize the bijection between free k cells and their position in the column ordering.

Free (k+1) cells and column ordering

Similar to the free k cell infrastructure, we define helpers for free (k+1) cells. The key difference is that for free (k+1) cells, the matched condition involves freeKCountBefore rather than freeKSuccCount.

Per-row count swap lemmas for Bender-Knuth

These lemmas establish that applying Bender-Knuth swaps the counts of free k's and free (k+1)'s in each row. This is the key fact needed to prove that matched cells stay matched after BK.

theorem AlgebraicCombinatorics.matched_k_stays_matched' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hval : T c = k) (hfree : ¬isForcedK T k hk c) (hmatched : ¬isUnmatchedFreeK T k hk c) : have T' := benderKnuth k hk T hT; T' c = k ∧ ¬isForcedK T' k hk c ∧ ¬isUnmatchedFreeK T' k hk c

A matched free k stays as k after BK, and remains matched in T'. This is the key lemma for proving that BK(BK(T)) = T for matched cells.

Definition reminder: A free k at position c is unmatched iff freeKCountUpTo(c.col) > freeKSuccCount (total in row). This compares the cumulative count of k's up to c with the TOTAL count of (k+1)'s in the row.

In a semistandard row with a free k's followed by b free (k+1)'s:

• The j-th free k has freeKCountUpTo = j
• It's unmatched iff j > b, i.e., the rightmost (a - b) free k's are unmatched
• The leftmost min(a, b) free k's are matched

So matched free k's DO exist when b > 0 (there are free (k+1)'s in the row).

Proof strategy:

1. freeKCountUpTo T' c.col = freeKCountUpTo T c.col (by matched_k_propagates_left, all free k's at columns ≤ c.col are matched, so they stay as k in T')
2. freeKCountUpTo T c.col ≤ freeKCount T (cumulative ≤ total)
3. freeKSuccCount T' = freeKCount T (count swap under BK)
4. Combining: freeKCountUpTo T' c.col ≤ freeKCount T = freeKSuccCount T'

theorem AlgebraicCombinatorics.matched_kSucc_stays_matched' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hval : T c = ⟨↑k + 1, hk⟩) (hfree : ¬isForcedKSucc T k hk c) (hmatched : ¬isUnmatchedFreeKSucc T k hk c) : have T' := benderKnuth k hk T hT; T' c = ⟨↑k + 1, hk⟩ ∧ ¬isForcedKSucc T' k hk c ∧ ¬isUnmatchedFreeKSucc T' k hk c

theorem AlgebraicCombinatorics.unmatched_k_becomes_unmatched_kSucc' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hunmatched : isUnmatchedFreeK T k hk c) : have T' := benderKnuth k hk T hT; T' c = ⟨↑k + 1, hk⟩ ∧ ¬isForcedKSucc T' k hk c ∧ isUnmatchedFreeKSucc T' k hk c

theorem AlgebraicCombinatorics.unmatched_kSucc_becomes_unmatched_k' {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hunmatched : isUnmatchedFreeKSucc T k hk c) : have T' := benderKnuth k hk T hT; T' c = k ∧ ¬isForcedK T' k hk c ∧ isUnmatchedFreeK T' k hk c

theorem AlgebraicCombinatorics.benderKnuth_row_weak {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c₁ c₂ : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (h_row : (↑c₁).1 = (↑c₂).1) (h_col : (↑c₁).2 < (↑c₂).2) : benderKnuth k hk T hT c₁ ≤ benderKnuth k hk T hT c₂

Row-weak preservation for Bender-Knuth: T' c₁ ≤ T' c₂ when c₁.col < c₂.col in the same row.

The key insight is:

• Unmatched free k's are the RIGHTMOST free k's (when a > b)
• Unmatched free (k+1)'s are the LEFTMOST free (k+1)'s (when b > a)

After BK:

• Rightmost k's become k+1 (moving to the right of remaining k's)
• Leftmost (k+1)'s become k (moving to the left of remaining (k+1)'s)

This preserves row-weak ordering because the new k's are to the LEFT of remaining (k+1)'s.

Proof strategy: Case analysis on what T c₁ and T c₂ are, using:

1. not_unmatched_k_and_unmatched_kSucc: Can't have unmatched k left of unmatched k+1
2. matched_k_propagates_left: If c₂ is matched k, then c₁ (to the left) is also matched
3. matched_kSucc_propagates_right: If c₁ is matched k+1, then c₂ (to the right) is also matched

theorem AlgebraicCombinatorics.benderKnuth_column_strict {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) (c₁ c₂ : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (h_col : (↑c₁).2 = (↑c₂).2) (h_row : (↑c₁).1 < (↑c₂).1) : benderKnuth k hk T hT c₁ < benderKnuth k hk T hT c₂

Column-strict preservation for Bender-Knuth involution.

This lemma proves that BK preserves column-strict ordering when lam and mu are N-partitions. The key insight is that if T c₁ = k and T c₂ = k+1 in the same column with c₁.row < c₂.row, then by the partition property (columns are contiguous), c₁ and c₂ must be adjacent. Adjacent cells with k above and k+1 below form a forced pair, which is unchanged by BK.

This lemma resolves the column-strict sorry in benderKnuth_involutive when partition hypotheses are available.

theorem AlgebraicCombinatorics.benderKnuth_involutive {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) : have T' := benderKnuth k hk T hT; ∃ (hT' : IsSemistandard T'), benderKnuth k hk T' hT' = T

theorem AlgebraicCombinatorics.benderKnuth_semistandard {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) : IsSemistandard (benderKnuth k hk T hT)

The Bender-Knuth involution preserves semistandardness.

theorem AlgebraicCombinatorics.benderKnuth_involutive_partition {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) : have T' := benderKnuth k hk T hT; ∃ (hT' : IsSemistandard T'), benderKnuth k hk T' hT' = T

The Bender-Knuth involution is an involution for N-partitions.

This is a version of benderKnuth_involutive that uses the partition hypotheses to prove column-strict preservation via benderKnuth_column_strict.

Content swap proof structure

The key insight for benderKnuth_content_swap is:

Decomposition of cells by type:

• {c | T c = k} = {forced k} ⊔ {free k}
• {c | T c = k+1} = {forced (k+1)} ⊔ {free (k+1)}

Forced pairs bijection: Forced k and forced (k+1) cells are in bijection: each forced k cell has a unique (k+1) directly below it, and vice versa. So |forced k| = |forced (k+1)|.

Free cell transformation by BK: In each row with m free k's and n free (k+1)'s:

• min(m,n) pairs are "matched" (paired by parenthesis matching)
• max(0, m-n) free k's are "unmatched" → become (k+1)
• max(0, n-m) free (k+1)'s are "unmatched" → become k
• After BK: new free k count = n, new free (k+1) count = m

Content swap:

cont(T')_k = |forced k| + |new free k|
          = |forced k| + Σ_rows (free (k+1) count in row)
          = |forced (k+1)| + |free (k+1)|
          = cont(T)_{k+1}

Similarly for cont(T')_{k+1} = cont(T)_k.

theorem AlgebraicCombinatorics.benderKnuth_content_swap {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) : have T' := benderKnuth k hk T hT; contentTableau T' k = contentTableau T ⟨↑k + 1, hk⟩ ∧ contentTableau T' ⟨↑k + 1, hk⟩ = contentTableau T k ∧ ∀ (i : Fin N), i ≠ k → ↑i ≠ ↑k + 1 → contentTableau T' i = contentTableau T i

The content of BK_k(T) differs from cont(T) by swapping entries k and k+1. Specifically: cont(BK_k(T))k = cont(T){k+1} and cont(BK_k(T))_{k+1} = cont(T)_k, while cont(BK_k(T))_i = cont(T)_i for i ≠ k, k+1.

This is the key property that makes Bender-Knuth involutions useful for proving symmetry of Schur polynomials.

theorem AlgebraicCombinatorics.benderKnuth_monomial {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (T : Tableau lam mu) (hT : IsSemistandard T) : monomialTableau (benderKnuth k hk T hT) = (MvPolynomial.rename ⇑(Equiv.swap k ⟨↑k + 1, hk⟩)) (monomialTableau T)

The monomial x_{BK_k(T)} equals s_k · x_T, where s_k swaps x_k and x_{k+1}. This follows from benderKnuth_content_swap.

Stembridge's Involution for Non-Yamanouchi Tableaux

For Stembridge's lemma, we need a sign-reversing involution on non-Yamanouchi tableaux. Given a tableau T that is not ν-Yamanouchi:

1. Find the largest "violator" column j (where ν + cont(col_{≥j}(T)) fails to be a partition)
2. Find the smallest "misstep" index k (where the partition condition fails)
3. Apply Bender-Knuth BK_k to columns 1, ..., j-1

This involution has the property that the paired tableaux contribute opposite signs to the alternant sum, causing them to cancel.

theorem AlgebraicCombinatorics.contentColGeq_eq_zero_of_large {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (j : ℕ) (hj : ∀ (i : Fin N), lam i < j) : contentColGeq T j = 0

When j is beyond all columns in the diagram, contentColGeq T j = 0.

noncomputable def AlgebraicCombinatorics.isPartitionAtColumn {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) (j : ℕ) : Prop

Check if ν + cont(col_{≥j}(T)) is an N-partition.

Equations

• AlgebraicCombinatorics.isPartitionAtColumn nu T j = AlgebraicCombinatorics.IsNPartition (nu + AlgebraicCombinatorics.contentColGeq T j)

noncomputable instance AlgebraicCombinatorics.isPartitionAtColumn_decidable {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) (j : ℕ) : Decidable (isPartitionAtColumn nu T j)

Decidability of isPartitionAtColumn.

Equations

• AlgebraicCombinatorics.isPartitionAtColumn_decidable nu T j = id (id inferInstance)

noncomputable def AlgebraicCombinatorics.violatorColumns {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) : Finset ℕ

The set of columns where ν + cont(col_{≥j}(T)) fails to be a partition.

Note: We use maxCol + 2 in the range to ensure that j = maxCol + 1 is included. This is important because for j > maxCol, contentColGeq T j = 0, so we're checking if nu itself is an N-partition. Without this, the lemma violatorColumns_nonempty_of_not_yamanouchi would fail when nu is not an N-partition but nu + contentColGeq T j is an N-partition for all j ≤ maxCol.

Equations

• AlgebraicCombinatorics.violatorColumns nu T = {j ∈ Finset.range (Finset.univ.sup lam + 2) | j > 0 ∧ ¬AlgebraicCombinatorics.isPartitionAtColumn nu T j}

noncomputable def AlgebraicCombinatorics.findViolatorColumn {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) : Option ℕ

Find the largest column j where ν + cont(col_{≥j}(T)) fails to be an N-partition. Returns none if T is ν-Yamanouchi (i.e., no such column exists).

Equations

• AlgebraicCombinatorics.findViolatorColumn nu T = if h : (AlgebraicCombinatorics.violatorColumns nu T).Nonempty then some ((AlgebraicCombinatorics.violatorColumns nu T).max' h) else none

def AlgebraicCombinatorics.isMisstep {N : ℕ} (α : Fin N → ℕ) (k : Fin N) : Prop

Check if index k is a misstep: α_k < α_{k+1}.

Equations

• AlgebraicCombinatorics.isMisstep α k = ∃ (h : ↑k + 1 < N), α k < α ⟨↑k + 1, h⟩

instance AlgebraicCombinatorics.isMisstep_decidable {N : ℕ} (α : Fin N → ℕ) (k : Fin N) : Decidable (isMisstep α k)

Decidability of isMisstep.

Equations

• AlgebraicCombinatorics.isMisstep_decidable α k = id inferInstance

noncomputable def AlgebraicCombinatorics.misstepSet {N : ℕ} (α : Fin N → ℕ) : Finset (Fin N)

The set of misstep indices for a tuple α.

Equations

• AlgebraicCombinatorics.misstepSet α = {k : Fin N | AlgebraicCombinatorics.isMisstep α k}

noncomputable def AlgebraicCombinatorics.findFirstMisstep {N : ℕ} (α : Fin N → ℕ) : Option (Fin N)

Find the smallest index k where α_k < α_{k+1}. Returns none if α is a partition.

Equations

• AlgebraicCombinatorics.findFirstMisstep α = if h : (AlgebraicCombinatorics.misstepSet α).Nonempty then some ((AlgebraicCombinatorics.misstepSet α).min' h) else none

noncomputable def AlgebraicCombinatorics.findMisstepIndex {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) (j : ℕ) : Option (Fin N)

Find the smallest index k where ν + cont(col_{≥j}(T)) fails the partition condition. That is, find k such that (ν + cont(col_{≥j}(T)))k < (ν + cont(col{≥j}(T)))_{k+1}.

Equations

• AlgebraicCombinatorics.findMisstepIndex nu T j = AlgebraicCombinatorics.findFirstMisstep (nu + AlgebraicCombinatorics.contentColGeq T j)

Prefix-restricted count functions for benderKnuthPrefixMatching

The following definitions compute matching for the Bender-Knuth involution restricted to a column prefix (columns < j). This infrastructure is used by benderKnuthPrefixMatching to correctly preserve row-weak ordering.

Key insight: When applying BK_k to columns < j only, the matching should be computed using only the free entries in columns < j, not the entire row. This ensures that unmatched entries are at the k/(k+1) boundary within the prefix.

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.freeKCountPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) : ℕ

Count of free k's in row i restricted to columns < j. This is an alias for freeKCountBefore for use in the prefix-matching context.

Equations

• AlgebraicCombinatorics.freeKCountPrefix T i k hk j = AlgebraicCombinatorics.freeKCountBefore T i k hk j

noncomputable def AlgebraicCombinatorics.freeKSuccCountPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) : ℕ

Count of free (k+1)'s in row i restricted to columns < j.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKCountUpToPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j col : ℕ) : ℕ

Count of free k's in row i with column ≤ col, restricted to columns < j. Used for the parenthesis-matching algorithm in benderKnuthPrefixMatching.

Equations

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

noncomputable def AlgebraicCombinatorics.freeKSuccCountUpToPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (i k : Fin N) (hk : ↑k + 1 < N) (j col : ℕ) : ℕ

Count of free (k+1)'s in row i with column ≤ col, restricted to columns < j. Used for the parenthesis-matching algorithm in benderKnuthPrefixMatching.

Equations

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

def AlgebraicCombinatorics.isUnmatchedFreeKPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A free k at position c is "unmatched" within the column prefix (columns < j).

This is the prefix-restricted version of isUnmatchedFreeK. The matching is computed using only free entries in columns < j, not the entire row.

A free k is unmatched in the prefix iff at its position, the cumulative count of free k's (in the prefix) exceeds the TOTAL count of free (k+1)'s (in the prefix).

Usage: Used by benderKnuthPrefixMatching to correctly preserve row-weak ordering.

Equations

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

def AlgebraicCombinatorics.isUnmatchedFreeKSuccPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A free (k+1) at position c is "unmatched" within the column prefix (columns < j).

This is the prefix-restricted version of isUnmatchedFreeKSucc. The matching is computed using only free entries in columns < j, not the entire row.

A free (k+1) is unmatched in the prefix iff it's among the leftmost excess (k+1)'s, i.e., the cumulative count of free (k+1)'s up to c plus the total free k count is at most the total free (k+1) count (all counts restricted to the prefix).

Usage: Used by benderKnuthPrefixMatching to correctly preserve row-weak ordering.

Equations

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

def AlgebraicCombinatorics.isMatchedFreeKPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A matched free k in the prefix (columns < j) is a free k that is not unmatched. In the parenthesis-matching algorithm restricted to the prefix, these are the k's that get paired with (k+1)'s.

Equations

• AlgebraicCombinatorics.isMatchedFreeKPrefix T k hk j c = ((↑c).2 < j ∧ T c = k ∧ ¬AlgebraicCombinatorics.isForcedK T k hk c ∧ ¬AlgebraicCombinatorics.isUnmatchedFreeKPrefix T k hk j c)

def AlgebraicCombinatorics.isMatchedFreeKSuccPrefix {N : ℕ} {lam mu : Fin N → ℕ} (T : Tableau lam mu) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) : Prop

A matched free (k+1) in the prefix (columns < j) is a free (k+1) that is not unmatched. In the parenthesis-matching algorithm restricted to the prefix, these are the (k+1)'s that get paired with k's.

Equations

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

Cardinality lemmas for prefix-restricted matching

These lemmas establish cardinalities of matched/unmatched cells in the prefix, analogous to matchedFreeK_row_card and unmatchedFreeK_row_card for the full-row version.

Key results:

• matchedFreeKPrefix_row_card: #{matched free k's in row i, prefix} = min(m, n)
• unmatchedFreeKPrefix_row_card: #{unmatched free k's in row i, prefix} = m - min(m, n)
• matchedFreeKSuccPrefix_row_card: #{matched free (k+1)'s in row i, prefix} = min(m, n)
• unmatchedFreeKSuccPrefix_row_card: #{unmatched free (k+1)'s in row i, prefix} = n - min(m, n)

where m = freeKCountPrefix T i k hk j and n = freeKSuccCountPrefix T i k hk j.

These are the prefix-restricted versions of the lemmas at lines 3244-3550.

Helper lemmas for prefix-restricted matching

These lemmas establish key properties of isUnmatchedFreeKPrefix and isUnmatchedFreeKSuccPrefix that are used by benderKnuthPrefixMatching_row_weak_stembridge and related proofs.

Key insight: In the prefix-restricted matching:

• Unmatched free k's are the RIGHTMOST excess free k's (after matching with free (k+1)'s)
• Unmatched free (k+1)'s are the LEFTMOST excess free (k+1)'s

This means if c₁ is unmatched free k and c₂ is unmatched free (k+1) in the same row, then c₁.col > c₂.col (c₁ is to the right of c₂). This is crucial for row-weak preservation.

Cross-boundary case analysis for benderKnuthPrefixMatching

The following lemma addresses the "cross-boundary" case in benderKnuthPrefixMatching_row_weak_stembridge: when c₁ is in the prefix (col < j) and c₂ is in the suffix (col ≥ j).

Problem: If c₁ is unmatched free k in the prefix and T c₂ = k in the suffix, then after transformation: T' c₁ = k+1 > k = T' c₂, violating row-weak.

Key insight: In the Stembridge involution, j is chosen as the largest violator column. This means ν + cont(col_{≥j}(T)) is NOT a partition, but ν + cont(col_{≥j+1}(T)) IS a partition. The misstep index k is chosen such that (ν + cont(col_{≥j}(T)))k < (ν + cont(col{≥j}(T)))_{k+1}.

This structure constrains what values can appear in which columns, potentially ruling out the problematic cross-boundary case.

theorem AlgebraicCombinatorics.column_j_no_k_at_max_violator {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (k : Fin N) (_hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) (hbeta : IsNPartition (nu + contentColGeq T (j + 1))) (hk_misstep : isMisstep (nu + contentColGeq T j) k) : contentColGeq T j k = contentColGeq T (j + 1) k

Column j has no k entries at max violator.

When j is the MAX violator column and k is the misstep index for α = ν + cont(col_{≥j}(T)), column j contains no cells with entry k. This is expressed as: contentColGeq T j k = contentColGeq T (j + 1) k

Context: In the Stembridge involution:

• j is a violator column (α = ν + cont(col_{≥j}(T)) is not a partition)
• j is the LARGEST violator (β = ν + cont(col_{≥j+1}(T)) IS a partition)
• k is the smallest misstep index (α k < α (k+1))

Proof idea:

• From misstep: α k < α (k+1), i.e., ν k + cont(col_{≥j}) k < ν (k+1) + cont(col_{≥j}) (k+1)
• From β partition: β (k+1) ≤ β k, i.e., ν (k+1) + cont(col_{≥j+1}) (k+1) ≤ ν k + cont(col_{≥j+1}) k
• From semistandard: cont(col_{≥j}) i ≤ cont(col_{≥j+1}) i + 1 (at most 1 entry per column)
• From monotonicity: cont(col_{≥j+1}) i ≤ cont(col_{≥j}) i
• Combining these constraints forces cont(col_{≥j}) k = cont(col_{≥j+1}) k

noncomputable def AlgebraicCombinatorics.benderKnuthPrefixMatching {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (_hT : IsSemistandard T) : Tableau lam mu

Apply the Bender-Knuth involution BK_k to columns < j of a tableau (matching-based version).

This definition uses isUnmatchedFreeKPrefix and isUnmatchedFreeKSuccPrefix (which compute matching restricted to columns < j) instead of simple free conditions. This is the correct definition that preserves row-weak ordering.

The matching-based conditions ensure that only unmatched free entries are swapped, preserving the row-weak property. See benderKnuthPrefixMatching_row_weak_stembridge below.

Equations

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

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_eq_on_suffix {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam mu }) (hc : (↑c).2 ≥ j) : benderKnuthPrefixMatching k hk j T hT c = T c

benderKnuthPrefixMatching agrees with the original tableau on columns ≥ j.

Count swap lemmas for benderKnuthPrefixMatching

After applying benderKnuthPrefixMatching, the counts of free k's and free (k+1)'s swap. These are the prefix-restricted versions of freeKCount_benderKnuth and freeKSuccCount_benderKnuth.

Key results (now proved):

• freeKCountPrefix_benderKnuthPrefixMatching: freeKCountPrefix T' = freeKSuccCountPrefix T
• freeKSuccCountPrefix_benderKnuthPrefixMatching: freeKSuccCountPrefix T' = freeKCountPrefix T

These lemmas, combined with the cardinality lemmas in the previous section, are used in benderKnuthPrefixMatching_involutive_stembridge.

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_semistandard_stembridge {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (hj_pos : j > 0) (T : Tableau lam mu) (hT : IsSemistandard T) (hbeta : IsNPartition (nu + contentColGeq T (j + 1))) (hk_misstep : isMisstep (nu + contentColGeq T j) k) : IsSemistandard (benderKnuthPrefixMatching k hk j T hT)

benderKnuthPrefixMatching preserves semistandardness in the Stembridge involution context.

This combines benderKnuthPrefixMatching_row_weak_stembridge and benderKnuthPrefixMatching_column_strict to show that the resulting tableau is semistandard.

The Stembridge context hypotheses (nu, hj_pos, hbeta, hk_misstep) are needed for the row-weak part to handle the cross-boundary case.

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_contentColGeq {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) : contentColGeq (benderKnuthPrefixMatching k hk j T hT) j = contentColGeq T j

benderKnuthPrefixMatching preserves contentColGeq for columns >= j. Since benderKnuthPrefixMatching only modifies cells in columns < j, the content in columns >= j is unchanged.

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_contentColGeq_ge {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) (j' : ℕ) (hj' : j' ≥ j) : contentColGeq (benderKnuthPrefixMatching k hk j T hT) j' = contentColGeq T j'

benderKnuthPrefixMatching preserves contentColGeq for all j' >= j. This generalizes benderKnuthPrefixMatching_contentColGeq to any column >= j.

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_contentTableau_other {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) (i : Fin N) (hi_ne_k : i ≠ k) (hi_ne_ksucc : ↑i ≠ ↑k + 1) : contentTableau (benderKnuthPrefixMatching k hk j T hT) i = contentTableau T i

benderKnuthPrefixMatching preserves contentTableau for indices i ≠ k, k+1. This is because the transformation only swaps k ↔ k+1 entries.

Helper lemmas for the involution proof

The following helper lemmas establish the counting arguments needed to prove benderKnuthPrefixMatching_involutive_stembridge. The key insight is that the counts swap under the transformation:

• freeKCountPrefix T' = freeKSuccCountPrefix T
• freeKSuccCountPrefix T' = freeKCountPrefix T

These lemmas are analogous to unmatched_k_becomes_unmatched_kSucc' for the full-row version, but restricted to the prefix (columns < j).

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_involutive_stembridge {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (hj_pos : j > 0) (T : Tableau lam mu) (hT : IsSemistandard T) (hbeta : IsNPartition (nu + contentColGeq T (j + 1))) (hk_misstep : isMisstep (nu + contentColGeq T j) k) : have T' := benderKnuthPrefixMatching k hk j T hT; ∃ (hT' : IsSemistandard T') (_ : IsNPartition (nu + contentColGeq T' (j + 1))) (_ : isMisstep (nu + contentColGeq T' j) k), benderKnuthPrefixMatching k hk j T' hT' = T

benderKnuthPrefixMatching is an involution in the Stembridge context.

This theorem proves that applying benderKnuthPrefixMatching twice returns the original tableau, when the Stembridge context hypotheses are satisfied.

Proof strategy: The key insight is that the matching-based conditions are symmetric:

• If c is unmatched free k in T, then T' c = k+1, and c becomes unmatched free (k+1) in T'
• If c is unmatched free (k+1) in T, then T' c = k, and c becomes unmatched free k in T'
• Forced cells and cells outside the prefix are unchanged

The matching counts are preserved because:

• freeKCountPrefix T' = freeKSuccCountPrefix T (unmatched k's become k+1's)
• freeKSuccCountPrefix T' = freeKCountPrefix T (unmatched k+1's become k's)
• The matching structure is exactly reversed

Note: This requires the Stembridge context hypotheses to ensure the result is semistandard, which is needed for the second application of benderKnuthPrefixMatching.

Helper lemmas for Stembridge's involution

The following lemmas establish the key properties needed for defining and proving properties of Stembridge's involution.

theorem AlgebraicCombinatorics.not_isNPartition_iff_exists_misstep {N : ℕ} (α : Fin N → ℕ) : ¬IsNPartition α ↔ ∃ (k : Fin N), isMisstep α k

If α is not an N-partition, then there exists a misstep index.

theorem AlgebraicCombinatorics.not_isYamanouchi_iff {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} : ¬IsYamanouchi nu T ↔ ¬IsSemistandard T ∨ ∃ j > 0, ¬IsNPartition (nu + contentColGeq T j)

A semistandard tableau T is not ν-Yamanouchi iff it's not semistandard or there exists j > 0 such that ν + cont(col_{≥j}(T)) is not an N-partition.

theorem AlgebraicCombinatorics.violatorColumns_nonempty_of_not_yamanouchi {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : (violatorColumns nu T).Nonempty

For a semistandard tableau T that is not ν-Yamanouchi, the violator columns set is nonempty.

theorem AlgebraicCombinatorics.misstepSet_nonempty_of_not_partition {N : ℕ} {α : Fin N → ℕ} (h : ¬IsNPartition α) : (misstepSet α).Nonempty

The misstep set is nonempty when the tuple is not a partition.

theorem AlgebraicCombinatorics.violatorColumn_pos {N : ℕ} {lam mu nu : Fin N → ℕ} {T : Tableau lam mu} {j : ℕ} (hj : j ∈ violatorColumns nu T) : j > 0

Any column in violatorColumns is positive (j > 0).

theorem AlgebraicCombinatorics.max_violator_succ_isNPartition {N : ℕ} {lam mu nu : Fin N → ℕ} (hnu : IsNPartition nu) {T : Tableau lam mu} (_hT : IsSemistandard T) (hviolator : (violatorColumns nu T).Nonempty) : have j := (violatorColumns nu T).max' hviolator; IsNPartition (nu + contentColGeq T (j + 1))

When j is the max violator column, j+1 gives an N-partition (or is out of range). This is the key hypothesis needed for benderKnuthPrefixMatching_involutive_stembridge.

Note: This lemma requires hnu : IsNPartition nu to handle the edge case where j = maxCol + 1 and contentColGeq T (j+1) = 0. In that case, we need to show IsNPartition nu, which is given by hypothesis.

noncomputable def AlgebraicCombinatorics.stembridgeInvolution {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : Tableau lam mu

Stembridge's involution on non-Yamanouchi tableaux. For T not ν-Yamanouchi:

1. Let j = findViolatorColumn ν T (largest column where ν + cont(col_{≥j}(T)) is not a partition)
2. Let k = findMisstepIndex ν T j (smallest index where the partition condition fails)
3. Apply BK_k to columns 1, ..., j-1 of T using benderKnuthPrefixMatching

This involution pairs non-Yamanouchi tableaux such that their alternant contributions cancel.

Key insight: The violator column j and misstep index k are the same for T and T' because benderKnuthPrefixMatching leaves columns ≥ j unchanged. This ensures the involution is well-defined and pairs tableaux correctly.

Implementation note: We use the helper functions findViolatorColumn and findMisstepIndex to extract j and k, then apply benderKnuthPrefixMatching. The proofs that these functions return valid values (Some j, Some k) follow from the non-Yamanouchi assumption.

Implementation: Uses violatorColumns_nonempty_of_not_yamanouchi to find j, misstepSet_nonempty_of_not_partition to find k, then applies benderKnuthPrefixMatching k j T.

Equations

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

Matching-based Stembridge involution

The stembridgeInvolutionMatching definition is an alternative to stembridgeInvolution that explicitly requires partition hypotheses. Both use benderKnuthPrefixMatching internally.

Port status: Complete. (The port to matching-based BK was completed and old code removed.)

• stembridgeInvolutionMatching: Definition using matching-based BK ✓
• Involutivity: Uses benderKnuthPrefixMatching_involutive_stembridge which is sorry-free

Key difference from stembridgeInvolution:

• Requires hlam : IsNPartition lam, hmu : IsNPartition mu, and hnu : IsNPartition nu parameters
• Uses matching-based conditions to determine which cells to swap

noncomputable def AlgebraicCombinatorics.stembridgeInvolutionMatching {N : ℕ} {lam mu : Fin N → ℕ} (_hlam : IsNPartition lam) (_hmu : IsNPartition mu) (nu : Fin N → ℕ) (_hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : Tableau lam mu

Stembridge's involution using matching-based Bender-Knuth (version with explicit partition hypotheses).

This version of the Stembridge involution explicitly requires partition hypotheses for lam, mu, and nu. The matching-based approach correctly preserves row-weak ordering by only swapping unmatched free entries.

Parameters:

• hlam, hmu: Partition hypotheses needed for the matching-based BK to preserve semistandardness
• hnu: Partition hypothesis for ν (needed to prove β is a partition when j is max violator)
• nu: The ν parameter for the Yamanouchi condition
• T: Input semistandard tableau
• hnotYam: Proof that T is not ν-Yamanouchi

Implementation: Same as stembridgeInvolution, but uses benderKnuthPrefixMatching in the final step.

Equations

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

theorem AlgebraicCombinatorics.stembridgeInvolutionMatching_semistandard {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : IsSemistandard (stembridgeInvolutionMatching hlam hmu nu hnu T hT hnotYam)

stembridgeInvolutionMatching preserves semistandardness.

theorem AlgebraicCombinatorics.stembridgeInvolutionMatching_involutive {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : have T' := stembridgeInvolutionMatching hlam hmu nu hnu T hT hnotYam; ∃ (hT' : IsSemistandard T') (hnotYam' : ¬IsYamanouchi nu T'), stembridgeInvolutionMatching hlam hmu nu hnu T' hT' hnotYam' = T

stembridgeInvolutionMatching is an involution on non-Yamanouchi tableaux.

This theorem uses benderKnuthPrefixMatching_involutive_stembridge which is sorry-free.

theorem AlgebraicCombinatorics.stembridgeInvolutionMatching_contentColGeq {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : have hviolator := ⋯; have j := (violatorColumns nu T).max' hviolator; contentColGeq (stembridgeInvolutionMatching hlam hmu nu hnu T hT hnotYam) j = contentColGeq T j

stembridgeInvolutionMatching preserves the content in columns ≥ j.

theorem AlgebraicCombinatorics.stembridgeInvolution_involutive {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : have T' := stembridgeInvolution nu T hT hnotYam; ∃ (hT' : IsSemistandard T') (hnotYam' : ¬IsYamanouchi nu T'), stembridgeInvolution nu T' hT' hnotYam' = T

Stembridge's involution is an involution on non-Yamanouchi tableaux.

Proof outline:

Let T' = stembridgeInvolution ν T. The involution is defined as:

1. Let j = findViolatorColumn ν T (largest column where ν + cont(col_{≥j}(T)) is not a partition)
2. Let k = findMisstepIndex ν T j (smallest index where the partition condition fails)
3. Apply BK_k to columns 1, ..., j-1 of T

To prove T' is semistandard:

• BK_k preserves semistandardness (benderKnuthPrefixMatching_semistandard_stembridge)
• The column restriction and recombination preserve semistandardness

To prove T' is not Yamanouchi:

• The violator column j and misstep index k are the same for T and T'
• This is because BK_k only affects columns < j, not columns ≥ j

To prove stembridgeInvolution T' = T:

• BK_k is an involution (benderKnuthPrefixMatching_involutive_stembridge)
• Applying BK_k twice to columns 1, ..., j-1 returns the original

theorem AlgebraicCombinatorics.stembridgeInvolution_semistandard {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : IsSemistandard (stembridgeInvolution nu T hT hnotYam)

Stembridge's involution preserves semistandardness.

theorem AlgebraicCombinatorics.stembridgeInvolution_not_yamanouchi {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : ¬IsYamanouchi nu (stembridgeInvolution nu T hT hnotYam)

Stembridge's involution maps non-Yamanouchi to non-Yamanouchi.

theorem AlgebraicCombinatorics.benderKnuthPrefixMatching_content_swap {N : ℕ} {lam mu : Fin N → ℕ} (k : Fin N) (hk : ↑k + 1 < N) (j : ℕ) (T : Tableau lam mu) (hT : IsSemistandard T) : contentTableau (benderKnuthPrefixMatching k hk j T hT) k + contentColGeq T j ⟨↑k + 1, hk⟩ = contentTableau T ⟨↑k + 1, hk⟩ + contentColGeq T j k

The prefix content swap lemma: the count of k's in the prefix of T' equals the count of k+1's in the prefix of T, where T' = benderKnuthPrefixMatching.

This is the key lemma for proving the content transposition property.

Proof strategy:

• prefix k in T' = (forced k in prefix of T) + (free k in prefix of T')
• prefix k' in T = (forced k' in prefix of T) + (free k' in prefix of T)
• By forced bijection: #{forced k in prefix} = #{forced k' in prefix}
• By count swap: #{free k in prefix of T'} = #{free k' in prefix of T}
• Therefore: prefix k in T' = prefix k' in T

theorem AlgebraicCombinatorics.stembridgeInvolution_content_transposition {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : ∃ (k : Fin N) (k' : Fin N), k ≠ k' ∧ nu + contentTableau (stembridgeInvolution nu T hT hnotYam) + rho N = (nu + contentTableau T + rho N) ∘ ⇑(Equiv.swap k k')

The Stembridge involution changes the content in such a way that ν + cont(T') + ρ differs from ν + cont(T) + ρ by a transposition.

Specifically, if T' = stembridgeInvolution ν T, then there exist indices k ≠ k' such that ν + cont(T') + ρ = (ν + cont(T) + ρ) ∘ swap(k, k').

This is the key property that enables the sign-reversing argument: the Stembridge involution applies BK_k to a prefix of T, which swaps the counts of k and k+1 in that prefix. Combined with the specific choice of the misstep index k, this results in the full expression being related by a transposition.

theorem AlgebraicCombinatorics.stembridgeInvolution_sign_reversing {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) : alternant (nu + contentTableau (stembridgeInvolution nu T hT hnotYam) + rho N) = -alternant (nu + contentTableau T + rho N)

The key sign-reversing property: the alternant contributions of T and its image under Stembridge's involution are negatives of each other.

This is because cont(T') differs from cont(T) by swapping entries k and k+1, and by alternant_swap, this negates the alternant.

theorem AlgebraicCombinatorics.stembridgeInvolution_fixed_point_implies_alternant_zero {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) (heq : stembridgeInvolution nu T hT hnotYam = T) : alternant (nu + contentTableau T + rho N) = 0

If the Stembridge involution has a fixed point, then the alternant is zero.

This is the key lemma that allows us to use Finset.sum_involution: we only need the involution to be fixed-point free when the alternant is non-zero.

Proof: If T' = T, then by stembridgeInvolution_content_transposition:

• f = f ∘ swap k k' where f = nu + contentTableau T + rho N and k ≠ k'
• This means f(k) = f(k'), so f has repeated entries
• By alternant_eq_zero_of_repeated, the alternant is zero.

theorem AlgebraicCombinatorics.stembridgeInvolution_no_fixed_points_of_alternant_ne_zero {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (nu : Fin N → ℕ) (hnu : IsNPartition nu) (T : Tableau lam mu) (hT : IsSemistandard T) (hnotYam : ¬IsYamanouchi nu T) (hne : alternant (nu + contentTableau T + rho N) ≠ 0) : stembridgeInvolution nu T hT hnotYam ≠ T

Stembridge's involution has no fixed points on non-Yamanouchi tableaux when the alternant is non-zero.

Proof strategy: The contrapositive of stembridgeInvolution_fixed_point_implies_alternant_zero. If T' = T, then the alternant is zero, so if the alternant is non-zero, then T' ≠ T.

Note: The unconditional version (without the alternant hypothesis) would require a detailed analysis of the Bender-Knuth structure, showing that the prefix content cannot be exactly balanced for non-Yamanouchi tableaux. For the application in alternant_sum_non_yamanouchi_eq_zero, the conditional version suffices.

noncomputable instance AlgebraicCombinatorics.nonYamanouchiTableau_fintype {N : ℕ} (lam mu nu : Fin N → ℕ) : Fintype { T : Tableau lam mu // IsSemistandard T ∧ ¬IsYamanouchi nu T }

The type of non-Yamanouchi semistandard tableaux is finite.

Equations

• AlgebraicCombinatorics.nonYamanouchiTableau_fintype lam mu nu = ⋯.fintype

theorem AlgebraicCombinatorics.skewSchurPoly_isSymmetric {R : Type u_1} [CommRing R] {N : ℕ} (lam mu : Fin N → ℕ) (hlam : IsNPartition lam) (hmu : IsNPartition mu) : (skewSchurPoly lam mu).IsSymmetric

The skew Schur polynomial is symmetric when lam and mu are N-partitions.

This follows from Bender-Knuth involutions: for each adjacent transposition (k, k+1), the Bender-Knuth involution BK_k gives a bijection on semistandard tableaux that swaps the content entries k and k+1. Since adjacent transpositions generate the symmetric group, this proves skewSchurPoly is invariant under all permutations.

The partition hypotheses are required for benderKnuth_involutive_partition.

theorem AlgebraicCombinatorics.alternant_mul_skewSchurPoly_eq_sum {R : Type u_1} [CommRing R] {N : ℕ} {lam mu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (α : Fin N → ℕ) : alternant α * skewSchurPoly lam mu = ∑ T : { T : Tableau lam mu // IsSemistandard T }, alternant (α + contentTableau ↑T)

The key expansion identity: alternant α * skewSchurPoly = ∑_T alternant (α + cont(T)).

This identity is the core of Stembridge's proof. It follows from:

1. The symmetry of skewSchurPoly (invariant under variable permutations)
2. The fact that alternant α = ∑_σ sign(σ) · x^(α ∘ σ)
3. For symmetric p: alternant α * p = ∑_σ sign(σ) · rename σ⁻¹ (x^α * p)

The proof uses Bender-Knuth involutions to establish the symmetry of skewSchurPoly.

theorem AlgebraicCombinatorics.alternant_sum_split {R : Type u_1} [CommRing R] {N : ℕ} {lam mu nu : Fin N → ℕ} : ∑ T : { T : Tableau lam mu // IsSemistandard T }, alternant (nu + contentTableau ↑T + rho N) = ∑ T : { T : Tableau lam mu // IsYamanouchi nu T }, alternant (nu + contentTableau ↑T + rho N) + ∑ T : { T : Tableau lam mu // IsSemistandard T ∧ ¬IsYamanouchi nu T }, alternant (nu + contentTableau ↑T + rho N)

The alternant sum over all semistandard tableaux equals the sum over Yamanouchi tableaux plus the sum over non-Yamanouchi tableaux.

theorem AlgebraicCombinatorics.alternant_sum_non_yamanouchi_eq_zero {R : Type u_1} [CommRing R] {N : ℕ} {lam mu nu : Fin N → ℕ} (hlam : IsNPartition lam) (hmu : IsNPartition mu) (hnu : IsNPartition nu) : ∑ T : { T : Tableau lam mu // IsSemistandard T ∧ ¬IsYamanouchi nu T }, alternant (nu + contentTableau ↑T + rho N) = 0

The sum over non-Yamanouchi tableaux is zero (they cancel in pairs via the involution).

Main theorems

theorem AlgebraicCombinatorics.stembridgeLemma {R : Type u_1} [CommRing R] {N : ℕ} (lam mu nu : Fin N → ℕ) (hlam : IsNPartition lam) (hmu : IsNPartition mu) (hnu : IsNPartition nu) : alternant (nu + rho N) * skewSchurPoly lam mu = ∑ T : { T : Tableau lam mu // IsYamanouchi nu T }, alternant (nu + contentTableau ↑T + rho N)

Stembridge's Lemma (lem.sf.stemb-lem): The key technical lemma for proving the Littlewood-Richardson rule.

For N-partitions lam, mu, nu: a_{nu+ρ} · s_{lam/mu} = ∑{T nu-Yamanouchi of shape lam/mu} a{nu + cont(T) + ρ}

The sum on the RHS is over all nu-Yamanouchi semistandard tableaux T of shape lam/mu. Note: The sum is finite since there are finitely many semistandard tableaux of any shape.

Proof Strategy (from Stembridge 1997)

The proof uses a sign-reversing involution on non-Yamanouchi tableaux:

Step 1: Express the LHS using the alternant definition and symmetry of skewSchurPoly:

a_{ν+ρ} · s_{λ/μ} = ∑_{σ ∈ S_N} (-1)^σ · σ(x^{ν+ρ}) · s_{λ/μ}
                  = ∑_{σ ∈ S_N} (-1)^σ · σ(x^{ν+ρ} · s_{λ/μ})  (since s_{λ/μ} is symmetric)

Step 2: Expand s_{λ/μ} as a sum over semistandard tableaux:

= ∑_{T ∈ SSYT(λ/μ)} ∑_{σ ∈ S_N} (-1)^σ · x^{σ(ν+cont(T)+ρ)}
= ∑_{T ∈ SSYT(λ/μ)} a_{ν+cont(T)+ρ}

Step 3: Define a sign-reversing involution on non-Yamanouchi tableaux: For T not ν-Yamanouchi:

• Let j be the largest "violator" column (where ν + cont(col≥j T) fails to be a partition)
• Let k be the smallest "misstep" index (where the partition condition fails)
• Apply the Bender-Knuth involution β_k to columns 1, ..., j-1 of T
• This gives T* with cont(T*) obtained from cont(T) by swapping entries k and k+1

Step 4: Show the involution is sign-reversing: Since cont(T*) differs from cont(T) by swapping entries k and k+1:

a_{ν+cont(T*)+ρ} = -a_{ν+cont(T)+ρ}  (by alternant_swap)

Step 5: Conclude that non-Yamanouchi tableaux cancel in pairs.

Dependencies

This proof requires:

1. skewSchurPoly to be properly defined as ∑_{T ∈ SSYT} x^{cont(T)}
2. alternant_swap: swapping two entries negates the alternant
3. alternant_eq_zero_of_repeated: equal entries give zero alternant
4. Bender-Knuth involutions β_k on tableaux
5. Properties of the involution (sign-reversing, fixed-point free on non-Yamanouchi)

Reference: [Stembridge, A concise proof of the Littlewood-Richardson rule, 2002]

theorem AlgebraicCombinatorics.tableau_entry_ge_row {N : ℕ} {lam : Fin N → ℕ} (hlam : IsNPartition lam) (T : Tableau lam zeroTuple) (hT : IsSemistandard T) (c : { c : Fin N × ℕ // c ∈ skewYoungDiagram lam zeroTuple }) : (↑c).1 ≤ T c

Lemma (lem.sf.tab-greater-i): In a semistandard tableau of shape lam, the entry at position (i,j) is at least i.

This follows from the strict increase down columns: for any cell (i, j) in the diagram, all cells (0, j), (1, j), ..., (i-1, j) are also in the diagram (since lam is weakly decreasing), and the entries strictly increase down the column, giving T(i, j) ≥ i.

def AlgebraicCombinatorics.minimalisticTableau {N : ℕ} (lam : Fin N → ℕ) : Tableau lam zeroTuple

The minimalistic tableau T₀ of shape lam has entry i in row i. (Defined in the proof of thm.sf.schur-symm (b))

Equations

• AlgebraicCombinatorics.minimalisticTableau lam c = (↑c).1

theorem AlgebraicCombinatorics.minimalisticTableau_semistandard {N : ℕ} (lam : Fin N → ℕ) : IsSemistandard (minimalisticTableau lam)

The minimalistic tableau is semistandard.

theorem AlgebraicCombinatorics.minimalisticTableau_yamanouchi {N : ℕ} (lam : Fin N → ℕ) (hlam : IsNPartition lam) : IsYamanouchi zeroTuple (minimalisticTableau lam)

The minimalistic tableau is 0-Yamanouchi. (Observation 1 in proof)

The key insight is that for the minimalistic tableau, contentColGeq T j at row i counts cells (i, k) where j ≤ k ≤ lam i. This count equals lam i + 1 - j. Since lam is weakly decreasing (an N-partition), so is this count, hence 0 + contentColGeq T j is also weakly decreasing, i.e., an N-partition.

theorem AlgebraicCombinatorics.contentTableau_minimalisticTableau {N : ℕ} (lam : Fin N → ℕ) : contentTableau (minimalisticTableau lam) = lam

The content of the minimalistic tableau equals lam. This follows from contentColGeq_one_eq_contentTableau and contentColGeq_minimalisticTableau: contentTableau T₀ = contentColGeq T₀ 1, and contentColGeq T₀ 1 i = lam i + 1 - 1 = lam i.

theorem AlgebraicCombinatorics.yamanouchi_rightmost_entry {N : ℕ} {lam : Fin N → ℕ} (hlam : IsNPartition lam) (T : Tableau lam zeroTuple) (hT : IsYamanouchi zeroTuple T) (i : Fin N) (hi : lam i > 0) : have hright_mem := ⋯; T ⟨(i, lam i), hright_mem⟩ = i

Helper: for 0-Yamanouchi T of shape lam/0, the entry at the rightmost cell of row i equals i. This is the key to proving uniqueness.

theorem AlgebraicCombinatorics.minimalisticTableau_unique {N : ℕ} (lam : Fin N → ℕ) (hlam : IsNPartition lam) (T : Tableau lam zeroTuple) (hT : IsYamanouchi zeroTuple T) : T = minimalisticTableau lam

The minimalistic tableau is the unique 0-Yamanouchi semistandard tableau of shape lam/0. (Observation 2 in proof)

theorem AlgebraicCombinatorics.schurPoly_eq_alternant_div {R : Type u_1} [CommRing R] {N : ℕ} (lam : Fin N → ℕ) (hlam : IsNPartition lam) : alternant (lam + rho N) = alternant (rho N) * schurPoly lam

Theorem (thm.sf.schur-symm (b)): The fundamental relation between Schur polynomials and alternants: a_{lam+ρ} = a_ρ · s_lam.

Proof Strategy

The proof derives this from Stembridge's Lemma by setting μ = 0 and ν = 0:

1. By Stembridge's Lemma: a_{0+ρ} · s_{λ/0} = ∑{T 0-Yamanouchi} a{0+cont(T)+ρ}
2. The only 0-Yamanouchi semistandard tableau of shape λ/0 is the minimalistic tableau T₀ (where each row i contains only i's).
3. The content of T₀ equals λ.
4. Therefore: a_ρ · s_λ = a_{λ+ρ}

This is equivalent to: a_{λ+ρ} = a_ρ · s_λ.

theorem AlgebraicCombinatorics.littlewoodRichardson {R : Type u_1} [CommRing R] {N : ℕ} [IsDomain R] (lam mu nu : Fin N → ℕ) (hlam : IsNPartition lam) (hmu : IsNPartition mu) (hnu : IsNPartition nu) : schurPoly nu * skewSchurPoly lam mu = ∑ T : { T : Tableau lam mu // IsYamanouchi nu T }, schurPoly (nu + contentTableau ↑T)

Zelevinsky's generalized Littlewood-Richardson rule (thm.sf.lr-zy):

For N-partitions lam, mu, nu: s_nu · s_{lam/mu} = ∑{T nu-Yamanouchi of shape lam/mu} s{nu + cont(T)}

This expresses the product of a Schur polynomial with a skew Schur polynomial as a sum of Schur polynomials. Setting mu = 0 gives the classical Littlewood-Richardson rule for products of two Schur polynomials.

Note: For each nu-Yamanouchi tableau T, the tuple nu + cont(T) is automatically an N-partition (this follows from the definition of Yamanouchi with j=1).

Proof Strategy (from the textbook)

The proof derives thm.sf.lr-zy from Stembridge's Lemma (lem.sf.stemb-lem):

Step 1: By Theorem thm.sf.schur-symm (b) applied to ν instead of λ: a_{ν+ρ} = a_ρ · s_ν

Step 2: By Stembridge's Lemma (lem.sf.stemb-lem): a_{ν+ρ} · s_{λ/μ} = ∑{T ν-Yamanouchi} a{ν+cont(T)+ρ}

Step 3: For each ν-Yamanouchi tableau T, ν+cont(T) is an N-partition (by the j=1 case of the Yamanouchi condition), so by thm.sf.schur-symm (b): a_{ν+cont(T)+ρ} = a_ρ · s_{ν+cont(T)}

Step 4: Substituting Steps 1 and 3 into Step 2: a_ρ · s_ν · s_{λ/μ} = a_ρ · ∑{T ν-Yamanouchi} s{ν+cont(T)}

Step 5: Since a_ρ is regular (lem.sf.arho-reg), we can cancel it (using lem.cring.reg.cancel) to obtain: s_ν · s_{λ/μ} = ∑{T ν-Yamanouchi} s{ν+cont(T)}

This completes the proof.

Examples

The Littlewood-Richardson coefficients

The coefficients c(nu, lam, omega) appearing in the expansion s_nu · s_lam = ∑_omega c(nu, lam, omega) · s_omega are called the Littlewood-Richardson coefficients. They have deep connections to representation theory: they are the multiplicities in the tensor product decomposition V_nu ⊗ V_lam ≅ ⊕_omega V_omega^{c(nu,lam,omega)} of irreducible polynomial representations of GL_N(ℂ).

noncomputable def AlgebraicCombinatorics.littlewoodRichardsonCoeff {N : ℕ} (nu lam omega : Fin N → ℕ) : ℕ

The Littlewood-Richardson coefficient c(nu, lam, omega) counts the number of nu-Yamanouchi semistandard tableaux T of shape lam/0 such that nu + cont(T) = omega.

This is a finite count since there are finitely many semistandard tableaux of any shape.

Equations

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

theorem AlgebraicCombinatorics.schurPoly_mul_expansion {R : Type u_1} [CommRing R] {N : ℕ} [IsDomain R] (nu lam : Fin N → ℕ) (hnu : IsNPartition nu) (hlam : IsNPartition lam) : schurPoly nu * schurPoly lam = ∑ T : { T : Tableau lam 0 // IsYamanouchi nu T }, schurPoly (nu + contentTableau ↑T)

The product s_nu · s_lam expands as ∑_omega c(nu, lam, omega) · s_omega.

This is a corollary of the Littlewood-Richardson rule with mu = 0.