Equivalence Between SSYT Definitions

This file establishes the equivalence between the two definitions of semistandard Young tableaux (SSYT) in this project:

1. SchurBasics.SSYT: Uses entry : Fin N × ℕ → Fin N with a support condition that entries outside the Young diagram are 0. This representation is more flexible for proofs involving cell coordinates.

2. SymmetricFunctions.SSYT: Uses dependent types entries : (i : Fin N) → (j : Fin (lam.parts i)) → Fin N. This representation is more type-safe but harder to work with for some proofs.

Main Results

• npartitionEquiv: An equivalence between the two NPartition types
• ssytEquiv: An equivalence between the two SSYT types
• toSchurBasicsSSYT: Convert from SymmetricFunctions.SSYT to SchurBasics.SSYT
• toSFSSYT: Convert from SchurBasics.SSYT to SymmetricFunctions.SSYT
• schur_eq_schurPoly_int: Equivalence of Schur polynomial definitions
• schurPoly_eq_schur: Corollary for composing theorems from different files

Implementation Notes

The two definitions also use different NPartition types (with fields monotone vs weaklyDecreasing), so we also provide conversions between these.

The SkewSSYT definitions have a similar relationship and are also addressed here.

Schur Polynomial Equivalence

The project has three Schur polynomial definitions:

• SchurBasics.schurPoly: Takes NPartition N with [NeZero N], coefficient ring ℤ
• SymmetricFunctions.schur: Takes SymmetricFunctions.NPartition N, generic ring R
• AlgebraicCombinatorics.schurPoly: Takes Fin N → ℕ with IsNPartition, generic ring R

This file provides equivalence theorems between the first two definitions. The third definition (in LittlewoodRichardson.lean) is related via the IsNPartition predicate, which is equivalent to the bundled NPartition types.

Design Rationale

Both SSYT definitions are retained in their original files. This file provides the equivalence infrastructure for code that needs both representations.

The two representations serve different purposes:

• SchurBasics.SSYT: Better for proofs using cell coordinates, extends YoungTableau
• SymmetricFunctions.SSYT: Better for type-safe code, no [NeZero N] requirement

NPartition Types

This file bridges between the two NPartition types in this project:

• NPartition N (shared, from NPartition.lean) - uses antitone field
• SymmetricFunctions.NPartition N (local, from PieriJacobiTrudi.lean) - uses weaklyDecreasing field

Both equivalences are provided for API convenience:

• SSYTEquiv.npartitionEquiv: shared → local
• SymmetricFunctions.NPartition.equivShared: local → shared

Tags

semistandard Young tableau, SSYT, equivalence, Young diagram, Schur polynomial

NPartition Conversions

The two files use different NPartition types with different field names:

• NPartition N (shared, from NPartition.lean) - uses antitone field (with monotone alias theorem for compatibility)
• SymmetricFunctions.NPartition N (local, from PieriJacobiTrudi.lean) - uses weaklyDecreasing field

We provide conversions between them. These conversions are trivial (just renaming fields).

Note: PieriJacobiTrudi.lean also provides NPartition.equivShared which is the inverse of npartitionEquiv defined here. Both are retained for API convenience:

• npartitionEquiv: shared → local
• NPartition.equivShared: local → shared

def SSYTEquiv.schurBasicsNPartition_to_SF {N : ℕ} (lam : NPartition N) : SymmetricFunctions.NPartition N

Convert from SchurBasics.NPartition to SymmetricFunctions.NPartition. Note: SchurBasics.lean now uses the shared NPartition from NPartition.lean, which has antitone as its field name (with monotone as an alias theorem).

Equations

• SSYTEquiv.schurBasicsNPartition_to_SF lam = { parts := lam.parts, weaklyDecreasing := ⋯ }

def SSYTEquiv.sfNPartition_to_SchurBasics {N : ℕ} (lam : SymmetricFunctions.NPartition N) : NPartition N

Convert from SymmetricFunctions.NPartition to SchurBasics.NPartition. Note: SchurBasics.lean now uses the shared NPartition from NPartition.lean, which has antitone as its field name.

Equations

• SSYTEquiv.sfNPartition_to_SchurBasics lam = { parts := lam.parts, antitone := ⋯ }

@[simp]

theorem SSYTEquiv.sfNPartition_schurBasics_id {N : ℕ} (lam : NPartition N) : sfNPartition_to_SchurBasics (schurBasicsNPartition_to_SF lam) = lam

The conversions are inverses (direction 1).

@[simp]

theorem SSYTEquiv.schurBasics_sfNPartition_id {N : ℕ} (lam : SymmetricFunctions.NPartition N) : schurBasicsNPartition_to_SF (sfNPartition_to_SchurBasics lam) = lam

The conversions are inverses (direction 2).

@[simp]

theorem SSYTEquiv.schurBasicsNPartition_to_SF_parts {N : ℕ} (lam : NPartition N) : (schurBasicsNPartition_to_SF lam).parts = lam.parts

The parts are preserved by conversion.

@[simp]

theorem SSYTEquiv.sfNPartition_to_SchurBasics_parts {N : ℕ} (lam : SymmetricFunctions.NPartition N) : (sfNPartition_to_SchurBasics lam).parts = lam.parts

def SSYTEquiv.npartitionEquiv {N : ℕ} : NPartition N ≃ SymmetricFunctions.NPartition N

The NPartition types are equivalent. This is the symmetric of SymmetricFunctions.NPartition.equivShared from PieriJacobiTrudi.lean. See npartitionEquiv_eq_equivShared_symm for the relationship.

Equations

• SSYTEquiv.npartitionEquiv = { toFun := SSYTEquiv.schurBasicsNPartition_to_SF, invFun := SSYTEquiv.sfNPartition_to_SchurBasics, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SSYTEquiv.npartitionEquiv_apply {N : ℕ} (lam : NPartition N) : npartitionEquiv lam = schurBasicsNPartition_to_SF lam

@[simp]

theorem SSYTEquiv.npartitionEquiv_symm_apply {N : ℕ} (lam : SymmetricFunctions.NPartition N) : npartitionEquiv.symm lam = sfNPartition_to_SchurBasics lam

theorem SSYTEquiv.npartitionEquiv_eq_equivShared_symm {N : ℕ} : npartitionEquiv = SymmetricFunctions.NPartition.equivShared.symm

The equivalence npartitionEquiv is the symmetric of NPartition.equivShared from PieriJacobiTrudi.lean. This means code can use either:

• npartitionEquiv lam to go from shared → local
• lam.toShared to go from local → shared

SSYT Conversions

The main equivalence between the two SSYT definitions.

theorem SSYTEquiv.sf_ssyt_col_strict_nonadjacent {N : ℕ} {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) {i₁ i₂ : Fin N} {j : ℕ} (hj₁ : j < lam.parts i₁) (hj₂ : j < lam.parts i₂) (hi : i₁ < i₂) : T.entries i₁ ⟨j, hj₁⟩ < T.entries i₂ ⟨j, hj₂⟩

Helper lemma: column-strict property extends to non-adjacent rows for SF SSYT. If j is in rows i₁ and i₂ with i₁ < i₂, then T.entries i₁ j < T.entries i₂ j.

def SSYTEquiv.toSchurBasicsSSYT {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : SSYT (sfNPartition_to_SchurBasics lam)

Convert from SymmetricFunctions.SSYT to SchurBasics.SSYT.

The key insight is that the dependent type (j : Fin (lam.parts i)) in the SF definition corresponds to cells (i, j) where j < lam.parts i, which is exactly the membership condition for the Young diagram in SchurBasics.

Equations

• SSYTEquiv.toSchurBasicsSSYT T = { entry := fun (c : Fin N × ℕ) => if h : c.2 < lam.parts c.1 then T.entries c.1 ⟨c.2, h⟩ else 0, support := ⋯, row_weak := ⋯, col_strict := ⋯ }

def SSYTEquiv.toSFSSYT {N : ℕ} [NeZero N] {lam : NPartition N} (T : SSYT lam) : SymmetricFunctions.SSYT (schurBasicsNPartition_to_SF lam)

Convert from SchurBasics.SSYT to SymmetricFunctions.SSYT.

This requires extracting the entries at valid positions from the total function.

Equations

• SSYTEquiv.toSFSSYT T = { entries := fun (i : Fin N) (j : Fin ((SSYTEquiv.schurBasicsNPartition_to_SF lam).parts i)) => T.entry (i, ↑j), rowWeak := ⋯, colStrict := ⋯ }

theorem SSYTEquiv.SSYT_eq_of_entries_eq {N : ℕ} {lam : SymmetricFunctions.NPartition N} {T1 T2 : SymmetricFunctions.SSYT lam} (h : T1.entries = T2.entries) : T1 = T2

Two SSYTs in the SymmetricFunctions namespace are equal if their entries are equal.

theorem SSYTEquiv.toSFSSYT_toSchurBasicsSSYT {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : toSFSSYT (toSchurBasicsSSYT T) = T

The conversions are inverses (direction 1).

theorem SSYTEquiv.toSchurBasicsSSYT_toSFSSYT {N : ℕ} [NeZero N] {lam : NPartition N} (T : SSYT lam) : toSchurBasicsSSYT (toSFSSYT T) = T

The conversions are inverses (direction 2).

def SSYTEquiv.ssytEquiv {N : ℕ} [NeZero N] (lam : SymmetricFunctions.NPartition N) : SymmetricFunctions.SSYT lam ≃ SSYT (sfNPartition_to_SchurBasics lam)

The equivalence between the two SSYT types.

Equations

• SSYTEquiv.ssytEquiv lam = { toFun := SSYTEquiv.toSchurBasicsSSYT, invFun := SSYTEquiv.toSFSSYT, left_inv := ⋯, right_inv := ⋯ }

Skew SSYT Conversions

Similar conversions for skew semistandard Young tableaux.

def SSYTEquiv.sfSkewPartition_to_SchurBasics {N : ℕ} (s : SymmetricFunctions.SkewPartition N) : NPartition N × NPartition N

Convert a SymmetricFunctions.SkewPartition to a SchurBasics-style skew partition (as a pair of NPartitions).

Equations

• SSYTEquiv.sfSkewPartition_to_SchurBasics s = (SSYTEquiv.sfNPartition_to_SchurBasics s.outer, SSYTEquiv.sfNPartition_to_SchurBasics s.inner)

theorem SSYTEquiv.sfSkewPartition_contained {N : ℕ} (s : SymmetricFunctions.SkewPartition N) : (sfSkewPartition_to_SchurBasics s).2 ≤ (sfSkewPartition_to_SchurBasics s).1

The outer partition contains the inner partition after conversion.

def SSYTEquiv.toSchurBasicsSkewSSYT {N : ℕ} [NeZero N] {s : SymmetricFunctions.SkewPartition N} (T : SymmetricFunctions.SkewSSYT s) : SkewSSYT (sfSkewPartition_to_SchurBasics s).1 (sfSkewPartition_to_SchurBasics s).2

Convert from SymmetricFunctions.SkewSSYT to SchurBasics.SkewSSYT.

Equations

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

Schur Polynomial Equivalences

The following theorems establish that the different Schur polynomial definitions are equivalent.

Summary of definitions:

• SchurBasics.schurPoly: Takes NPartition N with [NeZero N], coefficient ring ℤ
• SymmetricFunctions.schur: Takes SymmetricFunctions.NPartition N, generic coefficient ring R

The key insight is that both definitions sum over the same mathematical objects (SSYT), just represented differently. The ssytEquiv equivalence provides the bijection on tableaux, and we show that monomials are preserved under this bijection.

theorem SSYTEquiv.toSchurBasicsSSYT_monomial_eq {N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : T.toMonomial = ∏ c : { c : Fin N × ℕ // c ∈ (sfNPartition_to_SchurBasics lam).youngDiagram }, MvPolynomial.X ((toSchurBasicsSSYT T).entry ↑c)

The monomial associated to a SymmetricFunctions.SSYT equals the monomial of the corresponding SchurBasics.SSYT (as a product over cells).

This is the key lemma for proving Schur polynomial equivalence. The proof shows that the product over cells is preserved by the bijection.

def SSYTEquiv.sfSSYT_to_Filling {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : Filling (sfNPartition_to_SchurBasics lam)

Convert a SymmetricFunctions.SSYT to a Filling for SchurBasics.schurPoly.

Equations

• SSYTEquiv.sfSSYT_to_Filling T c = T.entries (↑c).1 ⟨(↑c).2, ⋯⟩

def SSYTEquiv.filling_to_sfSSYT {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (f : Filling (sfNPartition_to_SchurBasics lam)) (hf : isSSYTFillingYoung (sfNPartition_to_SchurBasics lam) f) : SymmetricFunctions.SSYT lam

Convert a Filling (satisfying SSYT conditions) to a SymmetricFunctions.SSYT.

Equations

• SSYTEquiv.filling_to_sfSSYT f hf = { entries := fun (i : Fin N) (j : Fin (lam.parts i)) => f ⟨(i, ↑j), ⋯⟩, rowWeak := ⋯, colStrict := ⋯ }

theorem SSYTEquiv.sfSSYT_to_Filling_isSSYT {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : isSSYTFillingYoung (sfNPartition_to_SchurBasics lam) (sfSSYT_to_Filling T)

The conversion from SF SSYT to Filling satisfies the SSYT condition.

theorem SSYTEquiv.filling_sfSSYT_id {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : filling_to_sfSSYT (sfSSYT_to_Filling T) ⋯ = T

The conversions are inverses (SF SSYT → Filling → SF SSYT).

theorem SSYTEquiv.sfSSYT_filling_id {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (f : Filling (sfNPartition_to_SchurBasics lam)) (hf : isSSYTFillingYoung (sfNPartition_to_SchurBasics lam) f) : sfSSYT_to_Filling (filling_to_sfSSYT f hf) = f

The conversions are inverses (Filling → SF SSYT → Filling).

theorem SSYTEquiv.sfSSYT_monomial_eq_filling {N : ℕ} [NeZero N] {lam : SymmetricFunctions.NPartition N} (T : SymmetricFunctions.SSYT lam) : T.toMonomial = fillingMonomialYoung (sfSSYT_to_Filling T)

The monomial of an SF SSYT equals the monomial of the corresponding Filling.

theorem SSYTEquiv.schur_eq_schurPoly_int {N : ℕ} [NeZero N] (lam : SymmetricFunctions.NPartition N) : SymmetricFunctions.schur lam = schurPoly (sfNPartition_to_SchurBasics lam)

The Schur polynomial from PieriJacobiTrudi equals the Schur polynomial from SchurBasics when specialized to coefficient ring ℤ.

This theorem establishes that SymmetricFunctions.schur lam (over ℤ) equals schurPoly (sfNPartition_to_SchurBasics lam).

Note: This theorem requires [NeZero N] because schurPoly requires it. For the generic ring version, see schur_eq_schurPoly_map.

theorem SSYTEquiv.schurPoly_eq_schur {N : ℕ} [NeZero N] (lam : NPartition N) : schurPoly lam = SymmetricFunctions.schur (schurBasicsNPartition_to_SF lam)

Corollary: The two Schur polynomial definitions are equal up to NPartition conversion.

This is the main user-facing theorem for composing results from different files.