The Pieri Rules and Jacobi-Trudi Identities

This file formalizes the Pieri rules for multiplying Schur polynomials by complete homogeneous or elementary symmetric polynomials, and the Jacobi-Trudi identities expressing skew Schur polynomials as determinants.

Main definitions

• NPartition: An N-partition is a weakly decreasing N-tuple of nonnegative integers
• NPartition.IsTranspose: Predicate asserting that two partitions are transposes
• SkewPartition: A skew partition λ/μ is a pair of partitions with μ ⊆ λ
• SkewPartition.isHorizontalStrip: A skew partition is a horizontal strip if no two boxes in Y(λ/μ) lie in the same column
• SkewPartition.isVerticalStrip: A skew partition is a vertical strip if no two boxes in Y(λ/μ) lie in the same row
• SkewPartition.isHorizontalNStrip: A horizontal n-strip has exactly n boxes
• SkewPartition.isVerticalNStrip: A vertical n-strip has exactly n boxes
• isHorizontalStripFun: Canonical unbundled horizontal strip predicate with (lam, mu) order
• isVerticalStripFun: Canonical unbundled vertical strip predicate with (lam, mu) order
• SSYT: A semistandard Young tableau of shape λ
• SkewSSYT: A semistandard Young tableau of skew shape λ/μ
• LatticePath: A lattice path in ℤ² using north and east steps
• Nipat: A non-intersecting path tuple (for LGV lemma connection)

Main results

• pieri_horizontal: h_n · s_μ = ∑_{λ/μ is horizontal n-strip} s_λ (Theorem thm.sf.pieri(a))
• pieri_vertical: e_n · s_μ = ∑_{λ/μ is vertical n-strip} s_λ (Theorem thm.sf.pieri(b))
• horizontalStrip_iff_entries: Characterization of horizontal strips via partition entries (Proposition prop.sf.strips.entries(a))
• verticalStrip_iff_entries: Characterization of vertical strips via partition entries (Proposition prop.sf.strips.entries(b))
• jacobiTrudi_h: s_{λ/μ} = det(h_{λᵢ - μⱼ - i + j}) (Theorem thm.sf.jt-h)
• jacobiTrudi_e: s_{λ/μ} = det(e_{λᵢᵗ - μⱼᵗ - i + j}) (Theorem thm.sf.jt-e)

References

• Source: AlgebraicCombinatorics/tex/SymmetricFunctions/PieriJacobiTrudi.tex
• [Stanley, Enumerative Combinatorics, Vol. 2][Stanley-EC2]
• [Grinberg-Reiner, Hopf algebras in combinatorics][GriRei]

Implementation notes

We work with N-partitions as length-N lists of weakly decreasing nonnegative integers. Schur polynomials are defined via semistandard Young tableaux (SSYT). The Jacobi-Trudi identities are proved using the Lindström-Gessel-Viennot lemma (see AlgebraicCombinatorics/Determinants/LGV2.lean).

For h_n and e_n with negative n, we use the convention h_n = 0 and e_n = 0.

Note: In the source, M is the length of the partition tuples (for Jacobi-Trudi), while N is the number of variables (entries in tableaux come from [N]). We use a single parameter N for simplicity in this formalization.

Strip Definition Conventions

There are three representations for horizontal/vertical strip predicates:

1. Bundled (SkewPartition.isHorizontalStrip): Takes a SkewPartition N directly. Use when working with bundled skew partitions.

2. Unbundled canonical (isHorizontalStripFun): Takes (lam mu : Fin N → ℕ) with argument order matching the mathematical notation λ/μ. Preferred for new code.

See SkewPartition.isHorizontalStrip_iff_isHorizontalStripFun for the equivalence lemma.

N-Partitions

An N-partition is a weakly decreasing N-tuple of nonnegative integers.

DEPRECATION NOTE: This is a local definition within the SymmetricFunctions namespace. A canonical definition exists at the top level in NPartition.lean (see AlgebraicCombinatorics/SymmetricFunctions/NPartition.lean). New code should prefer the canonical definition. This local definition uses weaklyDecreasing as the field name, while the canonical definition uses antitone (which matches Mathlib conventions). Both are semantically equivalent.

Migration support: An equivalence NPartition.equivShared is provided below to convert between the local and shared definitions. This enables gradual migration:

• Use NPartition.toShared to convert local → shared
• Use NPartition.ofShared to convert shared → local
• Both preserve parts, size, and the ≤ relation

Note: MonomialSymmetric.lean and SchurBasics.lean have been migrated to use the canonical definition. This file retains the local definition to avoid large refactoring of the extensive APIs built on top of it.

structure SymmetricFunctions.NPartition (N : ℕ) : Type

An N-partition is a list of length N with weakly decreasing nonnegative entries. This corresponds to Definition def.sf.N-par in the source.

Note: This is SymmetricFunctions.NPartition, a local definition. A canonical top-level NPartition exists in NPartition.lean with the same semantics (using antitone as the field name instead of weaklyDecreasing). See the section docstring for details.

• parts : Fin N → ℕ

  The parts of the partition

• weaklyDecreasing (i j : Fin N) : i ≤ j → self.parts j ≤ self.parts i

  The parts are weakly decreasing

theorem SymmetricFunctions.NPartition.ext {N : ℕ} {lam mu : NPartition N} (h : lam.parts = mu.parts) : lam = mu

Two N-partitions are equal if their parts are equal.

theorem SymmetricFunctions.NPartition.ext_iff {N : ℕ} {lam mu : NPartition N} : lam = mu ↔ lam.parts = mu.parts

instance SymmetricFunctions.NPartition.instDecidableEq {N : ℕ} : DecidableEq (NPartition N)

Decidable equality for N-partitions.

Equations

• lam.instDecidableEq mu = decidable_of_iff (lam.parts = mu.parts) ⋯

def SymmetricFunctions.NPartition.zero (N : ℕ) : NPartition N

The zero partition (0, 0, ..., 0)

Equations

• SymmetricFunctions.NPartition.zero N = { parts := fun (x : Fin N) => 0, weaklyDecreasing := ⋯ }

instance SymmetricFunctions.NPartition.instZero {N : ℕ} : Zero (NPartition N)

Equations

• SymmetricFunctions.NPartition.instZero = { zero := SymmetricFunctions.NPartition.zero N }

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

The size (sum of parts) of an N-partition

Equations

• lam.size = ∑ i : Fin N, lam.parts i

def SymmetricFunctions.NPartition.partLE {N : ℕ} (mu lam : NPartition N) : Prop

Containment of partitions: μ ⊆ λ means μᵢ ≤ λᵢ for all i

Equations

• mu.partLE lam = ∀ (i : Fin N), mu.parts i ≤ lam.parts i

instance SymmetricFunctions.NPartition.instLE {N : ℕ} : LE (NPartition N)

Equations

• SymmetricFunctions.NPartition.instLE = { le := SymmetricFunctions.NPartition.partLE }

theorem SymmetricFunctions.NPartition.le_def {N : ℕ} (mu lam : NPartition N) : mu ≤ lam ↔ ∀ (i : Fin N), mu.parts i ≤ lam.parts i

instance SymmetricFunctions.NPartition.instDecidableLE {N : ℕ} : DecidableRel fun (a b : NPartition N) => a ≤ b

Decidable instance for partition containment.

Equations

• x✝¹.instDecidableLE x✝ = Fintype.decidableForallFintype

noncomputable def SymmetricFunctions.NPartition.transpose {N : ℕ} (lam : NPartition N) (hN : 0 < N) : NPartition (lam.parts ⟨0, hN⟩)

The transpose of a partition. See Exercise exe.pars.transpose in the source. The transpose λᵗ satisfies: (λᵗ)ᵢ = |{j : λⱼ ≥ i+1}| for each i. The length of the transpose equals the first (largest) part of λ.

Equations

• lam.transpose hN = { parts := fun (i : Fin (lam.parts ⟨0, hN⟩)) => {j : Fin N | ↑i + 1 ≤ lam.parts j}.card, weaklyDecreasing := ⋯ }

def SymmetricFunctions.NPartition.IsTranspose {N M : ℕ} (lam : Fin N → ℕ) (lamt : Fin M → ℕ) : Prop

Predicate asserting that lamt is the transpose of lam. The transpose λᵗ of a partition λ satisfies: (λᵗ)ᵢ = |{j : λⱼ ≥ i}| for each i.

Since we work with fixed-length tuples, this predicate captures when two tuples represent transpose partitions (possibly with trailing zeros).

Equations

• SymmetricFunctions.NPartition.IsTranspose lam lamt = ((∀ (i : Fin M), lamt i = {j : Fin N | ↑i + 1 ≤ lam j}.card) ∧ ∀ (j : Fin N), lam j = {i : Fin M | ↑j + 1 ≤ lamt i}.card)

theorem SymmetricFunctions.NPartition.zero_isTranspose {N : ℕ} : IsTranspose (fun (x : Fin N) => 0) fun (x : Fin N) => 0

The zero partition is its own transpose.

Transpose Box Equivalence

For Young tableaux, the transpose property gives a key equivalence: a box (i, j) is in the diagram λ iff box (j, i) is in the transpose λᵗ. In the counting formulation: j + 1 ≤ λ_i iff i + 1 ≤ λᵗ_j.

This equivalence is fundamental for proving that the transpose preserves the number of boxes and for the Bender-Knuth bijection.

theorem SymmetricFunctions.NPartition.IsTranspose.box_equiv {N M : ℕ} {lam : Fin N → ℕ} {lamt : Fin M → ℕ} (hlam_mono : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hlamt_mono : ∀ (i j : Fin M), i ≤ j → lamt j ≤ lamt i) (htranspose : IsTranspose lam lamt) (i : Fin N) (j : Fin M) : ↑j + 1 ≤ lam i ↔ ↑i + 1 ≤ lamt j

The transpose box equivalence: for weakly decreasing partitions λ and λᵗ satisfying the transpose property, box (i, j) is in λ iff (j, i) is in λᵗ.

This is the key lemma that relates the two counting conditions: j + 1 ≤ λ_i ↔ i + 1 ≤ λᵗ_j

The proof uses the weakly decreasing property: if j + 1 ≤ λ_i, then all rows 0, 1, ..., i have at least j + 1 boxes, so λᵗ_j ≥ i + 1.

theorem SymmetricFunctions.NPartition.IsTranspose.sum_eq {N M : ℕ} {lam : Fin N → ℕ} {lamt : Fin M → ℕ} (hlam_mono : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hlamt_mono : ∀ (i j : Fin M), i ≤ j → lamt j ≤ lamt i) (htranspose : IsTranspose lam lamt) : ∑ i : Fin N, lam i = ∑ j : Fin M, lamt j

The transpose of a partition preserves the sum of parts (number of boxes).

This is a fundamental property of Young tableau transposition: |λ| = |λᵗ| (the size of the partition equals the size of its transpose).

The proof uses double counting: both ∑ᵢ λᵢ and ∑ⱼ λᵗⱼ count the total number of boxes in the Young diagram, just organized differently.

Row and Column Partitions

Special partitions consisting of a single row or column, used in the alternative proof of Pieri rules via Littlewood-Richardson.

def SymmetricFunctions.NPartition.rowPartition (N n : ℕ) (_hN : 0 < N) : NPartition N

The row partition (n, 0, 0, ..., 0) with n boxes in the first row. This is the partition corresponding to h_n (complete homogeneous symmetric polynomial). Requires N > 0 to have at least one row.

Equations

• SymmetricFunctions.NPartition.rowPartition N n _hN = { parts := fun (i : Fin N) => if ↑i = 0 then n else 0, weaklyDecreasing := ⋯ }

@[simp]

theorem SymmetricFunctions.NPartition.rowPartition_size (N n : ℕ) (hN : 0 < N) : (rowPartition N n hN).size = n

The row partition has size n.

@[simp]

theorem SymmetricFunctions.NPartition.rowPartition_parts_zero (N n : ℕ) (hN : 0 < N) : (rowPartition N n hN).parts ⟨0, hN⟩ = n

The first part of the row partition is n.

@[simp]

theorem SymmetricFunctions.NPartition.rowPartition_parts_pos (N n : ℕ) (hN : 0 < N) (i : Fin N) (hi : 0 < ↑i) : (rowPartition N n hN).parts i = 0

All other parts of the row partition are 0.

def SymmetricFunctions.NPartition.colPartition (N n : ℕ) (_hn : n ≤ N) : NPartition N

The column partition (1, 1, ..., 1, 0, ..., 0) with n ones (n boxes in first column). This is the partition corresponding to e_n (elementary symmetric polynomial). Requires n ≤ N (can't have more rows than N).

Equations

• SymmetricFunctions.NPartition.colPartition N n _hn = { parts := fun (i : Fin N) => if ↑i < n then 1 else 0, weaklyDecreasing := ⋯ }

@[simp]

theorem SymmetricFunctions.NPartition.colPartition_size (N n : ℕ) (hn : n ≤ N) : (colPartition N n hn).size = n

The column partition has size n.

@[simp]

theorem SymmetricFunctions.NPartition.colPartition_parts_lt (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : ↑i < n) : (colPartition N n hn).parts i = 1

The first n parts of the column partition are 1.

@[simp]

theorem SymmetricFunctions.NPartition.colPartition_parts_ge (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : n ≤ ↑i) : (colPartition N n hn).parts i = 0

Parts beyond n in the column partition are 0.

NPartition Type Equivalence

This section provides an equivalence between the local SymmetricFunctions.NPartition and the shared _root_.NPartition definition from NPartition.lean.

This enables gradual migration: code can use the local definition while having access to theorems proved about the shared definition (and vice versa).

def SymmetricFunctions.NPartition.toShared {N : ℕ} (μ : NPartition N) : _root_.NPartition N

Convert a local SymmetricFunctions.NPartition to the shared _root_.NPartition.

Equations

• μ.toShared = NPartition.mk' μ.parts ⋯

def SymmetricFunctions.NPartition.ofShared {N : ℕ} (μ : _root_.NPartition N) : NPartition N

Convert a shared _root_.NPartition to the local SymmetricFunctions.NPartition.

Equations

• SymmetricFunctions.NPartition.ofShared μ = { parts := μ.parts, weaklyDecreasing := ⋯ }

@[simp]

theorem SymmetricFunctions.NPartition.ofShared_toShared {N : ℕ} (μ : NPartition N) : ofShared μ.toShared = μ

Converting to shared and back is the identity.

@[simp]

theorem SymmetricFunctions.NPartition.toShared_ofShared {N : ℕ} (μ : _root_.NPartition N) : (ofShared μ).toShared = μ

Converting from shared and back is the identity.

def SymmetricFunctions.NPartition.equivShared {N : ℕ} : NPartition N ≃ _root_.NPartition N

The equivalence between local and shared NPartition types.

Equations

• SymmetricFunctions.NPartition.equivShared = { toFun := SymmetricFunctions.NPartition.toShared, invFun := SymmetricFunctions.NPartition.ofShared, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SymmetricFunctions.NPartition.toShared_parts {N : ℕ} (μ : NPartition N) : μ.toShared.parts = μ.parts

Converting to shared preserves parts.

@[simp]

theorem SymmetricFunctions.NPartition.ofShared_parts {N : ℕ} (μ : _root_.NPartition N) : (ofShared μ).parts = μ.parts

Converting from shared preserves parts.

@[simp]

theorem SymmetricFunctions.NPartition.toShared_size {N : ℕ} (μ : NPartition N) : μ.toShared.size = μ.size

Converting to shared preserves size.

@[simp]

theorem SymmetricFunctions.NPartition.ofShared_size {N : ℕ} (μ : _root_.NPartition N) : (ofShared μ).size = μ.size

Converting from shared preserves size.

@[simp]

theorem SymmetricFunctions.NPartition.toShared_zero {N : ℕ} : toShared 0 = 0

The zero partitions correspond under the equivalence.

@[simp]

theorem SymmetricFunctions.NPartition.ofShared_zero {N : ℕ} : ofShared 0 = 0

The zero partitions correspond under the equivalence.

theorem SymmetricFunctions.NPartition.toShared_le_iff {N : ℕ} (μ ν : NPartition N) : μ.toShared ≤ ν.toShared ↔ μ ≤ ν

The equivalence preserves the LE relation.

theorem SymmetricFunctions.NPartition.ofShared_le_iff {N : ℕ} (μ ν : _root_.NPartition N) : ofShared μ ≤ ofShared ν ↔ μ ≤ ν

The equivalence preserves the LE relation.

Transpose Bridge Lemmas

These lemmas connect the local SymmetricFunctions.NPartition.transpose with the canonical _root_.NPartition.transpose via the toShared/ofShared equivalence.

Both definitions compute the same thing: (λᵗ)ᵢ = |{j : λⱼ ≥ i+1}| for each i. The bridge lemmas make this equivalence explicit, enabling code using the local definition to interoperate with theorems proved about the canonical definition.

theorem SymmetricFunctions.NPartition.transpose_toShared_eq {N : ℕ} (lam : NPartition N) (hN : 0 < N) : (lam.transpose hN).toShared = lam.toShared.transpose hN

The transpose of the local SymmetricFunctions.NPartition equals the transpose of the shared _root_.NPartition (via the toShared/ofShared equivalence).

This is the bridge lemma connecting the two transpose definitions. Since both definitions compute (λᵗ)ᵢ = |{j : λⱼ ≥ i+1}|, they are definitionally equal when the parts are the same.

theorem SymmetricFunctions.NPartition.ofShared_transpose_eq {N : ℕ} (lam : _root_.NPartition N) (hN : 0 < N) : ofShared (lam.transpose hN) = (ofShared lam).transpose hN

The transpose of a shared _root_.NPartition converted to local equals the local transpose of the converted partition.

This is the inverse direction of the bridge lemma.

theorem SymmetricFunctions.NPartition.equivShared_transpose {N : ℕ} (lam : NPartition N) (hN : 0 < N) : equivShared (lam.transpose hN) = (equivShared lam).transpose hN

The transpose commutes with the equivalence.

Helper Lemmas for Sym-SSYT Bijection

These lemmas establish the connection between Sym (Fin N) n (multisets of size n) and weakly increasing sequences, which is key for proving that h_n equals the Schur polynomial of the row partition.

def SymmetricFunctions.symToWeaklyIncreasing {N : ℕ} (n : ℕ) (s : Sym (Fin N) n) : { f : Fin n → Fin N // ∀ (i j : Fin n), i ≤ j → f i ≤ f j }

Convert a Sym to a weakly increasing function. The sorted list of a multiset gives a canonical weakly increasing sequence.

Equations

• SymmetricFunctions.symToWeaklyIncreasing n s = ⟨fun (i : Fin n) => ((↑s).sort fun (x1 x2 : Fin N) => x1 ≤ x2).get ⟨↑i, ⋯⟩, ⋯⟩

theorem SymmetricFunctions.sym_monomial_eq_weaklyIncreasing_prod {N : ℕ} {R : Type u_2} [CommRing R] (n : ℕ) (s : Sym (Fin N) n) : (Multiset.map MvPolynomial.X ↑s).prod = ∏ j : Fin n, MvPolynomial.X (↑(symToWeaklyIncreasing n s) j)

The monomial from a Sym equals the product over its weakly increasing representation. This is a key lemma for connecting h_n to Schur polynomials.

def SymmetricFunctions.weaklyIncreasingToSym {N : ℕ} (n : ℕ) (f : Fin n → Fin N) : Sym (Fin N) n

Convert a weakly increasing function back to a Sym. This is the inverse of symToWeaklyIncreasing.

Equations

• SymmetricFunctions.weaklyIncreasingToSym n f = ⟨↑(List.map f (List.finRange n)), ⋯⟩

theorem SymmetricFunctions.weaklyIncreasingToSym_symToWeaklyIncreasing {N : ℕ} (n : ℕ) (s : Sym (Fin N) n) : weaklyIncreasingToSym n ↑(symToWeaklyIncreasing n s) = s

The round-trip from Sym to weakly increasing and back gives the same Sym. This shows that symToWeaklyIncreasing and weaklyIncreasingToSym form a bijection.

Skew Partitions and Strips

Definition def.sf.strips: A skew partition λ/μ is a pair (μ, λ) of N-partitions. Horizontal and vertical strips are special cases where the skew diagram has no two boxes in the same column or row, respectively.

structure SymmetricFunctions.SkewPartition (N : ℕ) : Type

A skew partition λ/μ is a pair of N-partitions with μ ⊆ λ. Definition def.sf.strips(a).

• outer : NPartition N

  The outer partition λ

• inner : NPartition N

  The inner partition μ

• contained : self.inner ≤ self.outer

  The containment condition μ ⊆ λ

def SymmetricFunctions.SkewPartition.size {N : ℕ} (s : SkewPartition N) : ℕ

The size of a skew partition |Y(λ/μ)| = |λ| - |μ|

Equations

• s.size = s.outer.size - s.inner.size

def SymmetricFunctions.SkewPartition.isHorizontalStrip {N : ℕ} (s : SkewPartition N) : Prop

A skew partition λ/μ is a horizontal strip if no two boxes of Y(λ/μ) lie in the same column. Definition def.sf.strips(b).

Bundled definition: This is the preferred version when working with SkewPartition N.

Related definitions:

• isHorizontalStripFun: Canonical unbundled version with (lam, mu) argument order

Equivalence: s.isHorizontalStrip ↔ isHorizontalStripFun s.outer.parts s.inner.parts (see SkewPartition.isHorizontalStrip_iff_isHorizontalStripFun)

Equations

• s.isHorizontalStrip = ∀ (i : Fin N) (hi : ↑i + 1 < N), s.inner.parts i ≥ s.outer.parts ⟨↑i + 1, hi⟩

def SymmetricFunctions.SkewPartition.isVerticalStrip {N : ℕ} (s : SkewPartition N) : Prop

A skew partition λ/μ is a vertical strip if no two boxes of Y(λ/μ) lie in the same row. Definition def.sf.strips(c).

Bundled definition: This is the preferred version when working with SkewPartition N.

Related definitions:

• isVerticalStripFun: Canonical unbundled version with (lam, mu) argument order

Equivalence: s.isVerticalStrip ↔ isVerticalStripFun s.outer.parts s.inner.parts (see SkewPartition.isVerticalStrip_iff_isVerticalStripFun)

Equations

• s.isVerticalStrip = ∀ (i : Fin N), s.outer.parts i ≤ s.inner.parts i + 1

def SymmetricFunctions.SkewPartition.isHorizontalNStrip {N : ℕ} (s : SkewPartition N) (n : ℕ) : Prop

A skew partition is a horizontal n-strip if it is a horizontal strip with |Y(λ/μ)| = n. Definition def.sf.strips(d).

Equations

• s.isHorizontalNStrip n = (s.isHorizontalStrip ∧ s.size = n)

def SymmetricFunctions.SkewPartition.isVerticalNStrip {N : ℕ} (s : SkewPartition N) (n : ℕ) : Prop

A skew partition is a vertical n-strip if it is a vertical strip with |Y(λ/μ)| = n. Definition def.sf.strips(e).

Equations

• s.isVerticalNStrip n = (s.isVerticalStrip ∧ s.size = n)

Characterization of Strips

Proposition prop.sf.strips.entries: Horizontal and vertical strips can be characterized in terms of the entries of the partitions.

theorem SymmetricFunctions.SkewPartition.horizontalStrip_iff_entries {N : ℕ} (s : SkewPartition N) : s.isHorizontalStrip ↔ ∀ (i : Fin N) (hi : ↑i + 1 < N), s.outer.parts i ≥ s.inner.parts i ∧ s.inner.parts i ≥ s.outer.parts ⟨↑i + 1, hi⟩

Horizontal strip characterization (Proposition prop.sf.strips.entries(a)) Label: prop.sf.strips.entries

A skew partition λ/μ is a horizontal strip iff λ₁ ≥ μ₁ ≥ λ₂ ≥ μ₂ ≥ ⋯ ≥ λ_N ≥ μ_N.

theorem SymmetricFunctions.SkewPartition.verticalStrip_iff_entries {N : ℕ} (s : SkewPartition N) : s.isVerticalStrip ↔ ∀ (i : Fin N), s.inner.parts i ≤ s.outer.parts i ∧ s.outer.parts i ≤ s.inner.parts i + 1

Vertical strip characterization (Proposition prop.sf.strips.entries(b)) Label: prop.sf.strips.entries

A skew partition λ/μ is a vertical strip iff μᵢ ≤ λᵢ ≤ μᵢ + 1 for each i ∈ [N].

Decidability and Basic API for Strips

These instances and lemmas make the strip predicates computable and provide basic API for working with strips.

instance SymmetricFunctions.SkewPartition.instDecidableIsHorizontalStrip {N : ℕ} (s : SkewPartition N) : Decidable s.isHorizontalStrip

Decidable instance for isHorizontalStrip.

Equations

• s.instDecidableIsHorizontalStrip = Fintype.decidableForallFintype

instance SymmetricFunctions.SkewPartition.instDecidableIsVerticalStrip {N : ℕ} (s : SkewPartition N) : Decidable s.isVerticalStrip

Decidable instance for isVerticalStrip.

Equations

• s.instDecidableIsVerticalStrip = Fintype.decidableForallFintype

instance SymmetricFunctions.SkewPartition.instDecidableIsHorizontalNStrip {N : ℕ} (s : SkewPartition N) (n : ℕ) : Decidable (s.isHorizontalNStrip n)

Decidable instance for isHorizontalNStrip.

Equations

• s.instDecidableIsHorizontalNStrip n = instDecidableAnd

instance SymmetricFunctions.SkewPartition.instDecidableIsVerticalNStrip {N : ℕ} (s : SkewPartition N) (n : ℕ) : Decidable (s.isVerticalNStrip n)

Decidable instance for isVerticalNStrip.

Equations

• s.instDecidableIsVerticalNStrip n = instDecidableAnd

theorem SymmetricFunctions.SkewPartition.isHorizontalNStrip.size_eq {N : ℕ} {s : SkewPartition N} {n : ℕ} (h : s.isHorizontalNStrip n) : s.size = n

A horizontal n-strip has size n.

theorem SymmetricFunctions.SkewPartition.isVerticalNStrip.size_eq {N : ℕ} {s : SkewPartition N} {n : ℕ} (h : s.isVerticalNStrip n) : s.size = n

A vertical n-strip has size n.

theorem SymmetricFunctions.SkewPartition.isHorizontalNStrip.isHorizontalStrip {N : ℕ} {s : SkewPartition N} {n : ℕ} (h : s.isHorizontalNStrip n) : s.isHorizontalStrip

A horizontal n-strip is a horizontal strip.

theorem SymmetricFunctions.SkewPartition.isVerticalNStrip.isVerticalStrip {N : ℕ} {s : SkewPartition N} {n : ℕ} (h : s.isVerticalNStrip n) : s.isVerticalStrip

A vertical n-strip is a vertical strip.

theorem SymmetricFunctions.SkewPartition.empty_isHorizontalNStrip {N : ℕ} (lam : NPartition N) : { outer := lam, inner := lam, contained := ⋯ }.isHorizontalNStrip 0

The empty skew partition (λ = μ) is a horizontal 0-strip.

theorem SymmetricFunctions.SkewPartition.empty_isVerticalNStrip {N : ℕ} (lam : NPartition N) : { outer := lam, inner := lam, contained := ⋯ }.isVerticalNStrip 0

The empty skew partition (λ = μ) is a vertical 0-strip.

Examples from the textbook

These examples verify that our definitions match Definition def.sf.strips from the source (AlgebraicCombinatorics/tex/SymmetricFunctions/PieriJacobiTrudi.tex).

def SymmetricFunctions.SkewPartition.exampleA_outer : NPartition 4

Example (a) from the textbook: λ = (8,7,4,3), μ = (7,4,4,1). This is a horizontal 6-strip but NOT a vertical strip.

Equations

• SymmetricFunctions.SkewPartition.exampleA_outer = { parts := ![8, 7, 4, 3], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleA_outer._proof_1 }

def SymmetricFunctions.SkewPartition.exampleA_inner : NPartition 4

Equations

• SymmetricFunctions.SkewPartition.exampleA_inner = { parts := ![7, 4, 4, 1], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleA_inner._proof_1 }

def SymmetricFunctions.SkewPartition.exampleA : SkewPartition 4

Equations

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

def SymmetricFunctions.SkewPartition.exampleB_outer : NPartition 4

Example (b) from the textbook: λ = (3,3,2,1), μ = (2,2,1,0). This is a vertical 4-strip but NOT a horizontal strip.

Equations

• SymmetricFunctions.SkewPartition.exampleB_outer = { parts := ![3, 3, 2, 1], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleB_outer._proof_1 }

def SymmetricFunctions.SkewPartition.exampleB_inner : NPartition 4

Equations

• SymmetricFunctions.SkewPartition.exampleB_inner = { parts := ![2, 2, 1, 0], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleB_inner._proof_1 }

def SymmetricFunctions.SkewPartition.exampleB : SkewPartition 4

Equations

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

def SymmetricFunctions.SkewPartition.exampleC_outer : NPartition 4

Example (c) from the textbook: λ = (4,3,1,1), μ = (3,2,1,0). This is BOTH a horizontal 3-strip AND a vertical 3-strip.

Equations

• SymmetricFunctions.SkewPartition.exampleC_outer = { parts := ![4, 3, 1, 1], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleC_outer._proof_1 }

def SymmetricFunctions.SkewPartition.exampleC_inner : NPartition 4

Equations

• SymmetricFunctions.SkewPartition.exampleC_inner = { parts := ![3, 2, 1, 0], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleC_inner._proof_1 }

def SymmetricFunctions.SkewPartition.exampleC : SkewPartition 4

Equations

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

def SymmetricFunctions.SkewPartition.exampleD_outer : NPartition 4

Example (d) from the textbook: λ = (3,3,2,1), μ = (1,1,1,1). This is NEITHER a horizontal strip NOR a vertical strip.

Equations

• SymmetricFunctions.SkewPartition.exampleD_outer = { parts := ![3, 3, 2, 1], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleB_outer._proof_1 }

def SymmetricFunctions.SkewPartition.exampleD_inner : NPartition 4

Equations

• SymmetricFunctions.SkewPartition.exampleD_inner = { parts := ![1, 1, 1, 1], weaklyDecreasing := SymmetricFunctions.SkewPartition.exampleD_inner._proof_1 }

def SymmetricFunctions.SkewPartition.exampleD : SkewPartition 4

Equations

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

Schur Polynomials

We use Mathlib's symmetric polynomial infrastructure and define Schur polynomials via semistandard Young tableaux (SSYT).

structure SymmetricFunctions.SSYT {N : ℕ} (lam : NPartition N) : Type

A semistandard Young tableau (SSYT) of shape λ with entries in [N]. The entries are weakly increasing along rows and strictly increasing down columns. Definition def.sf.ssyt.

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

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

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

When to use which:

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

• entries (i : Fin N) (j : Fin (lam.parts i)) : Fin N

  The entries of the tableau

• rowWeak (i : Fin N) (j k : Fin (lam.parts i)) : j ≤ k → self.entries i j ≤ self.entries i k

  Entries are weakly increasing along rows

• colStrict (i : Fin N) (hi : ↑i + 1 < N) (j : Fin (lam.parts i)) (hj : ↑j < lam.parts ⟨↑i + 1, hi⟩) : self.entries i j < self.entries ⟨↑i + 1, hi⟩ ⟨↑j, hj⟩

  Entries are strictly increasing down columns

structure SymmetricFunctions.SkewSSYT {N : ℕ} (s : SkewPartition N) : Type

A semistandard Young tableau of skew shape λ/μ with entries in [N]. Definition def.sf.skew-schur.

For a skew tableau, the column-strict condition requires that entries are strictly increasing down columns, where column j of Y(λ/μ) consists of boxes (i, j) with μᵢ < j ≤ λᵢ.

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

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

See SSYTEquiv.lean for conversions between representations.

• entries (i : Fin N) (k : Fin (s.outer.parts i - s.inner.parts i)) : Fin N

  The entries of the tableau, only for boxes in Y(λ/μ). Entry (i, k) corresponds to box (i, μᵢ + k + 1) in Y(λ/μ).

• rowWeak (i : Fin N) (j k : Fin (s.outer.parts i - s.inner.parts i)) : j ≤ k → self.entries i j ≤ self.entries i k

  Entries are weakly increasing along rows

• colStrict (i : Fin N) (hi : ↑i + 1 < N) (k : Fin (s.outer.parts i - s.inner.parts i)) (_hcol : s.inner.parts i + ↑k + 1 > s.inner.parts ⟨↑i + 1, hi⟩ ∧ s.inner.parts i + ↑k + 1 ≤ s.outer.parts ⟨↑i + 1, hi⟩) : let k' := s.inner.parts i + ↑k - s.inner.parts ⟨↑i + 1, hi⟩; ∀ (hk' : k' < s.outer.parts ⟨↑i + 1, hi⟩ - s.inner.parts ⟨↑i + 1, hi⟩), self.entries i k < self.entries ⟨↑i + 1, hi⟩ ⟨k', hk'⟩

  Entries are strictly increasing down columns. If boxes (i, c) and (i', c) are both in Y(λ/μ) with i < i', then T(i, c) < T(i', c). Here c = μᵢ + k + 1 for some k. The condition checks: for row i and column offset k, if row i+1 also contains column μᵢ + k + 1 (i.e., μᵢ + k + 1 > μᵢ₊₁ and μᵢ + k + 1 ≤ λᵢ₊₁), then the entry in row i is strictly less than the entry in row i+1.

noncomputable def SymmetricFunctions.SSYT.toMonomial {N : ℕ} {R : Type u_1} [CommRing R] {lam : NPartition N} (T : SSYT lam) : MvPolynomial (Fin N) R

The monomial x^T associated to a tableau T. x_T = ∏{(i,j) ∈ Y(λ)} x{T(i,j)}

Equations

• T.toMonomial = ∏ i : Fin N, ∏ j : Fin (lam.parts i), MvPolynomial.X (T.entries i j)

theorem SymmetricFunctions.SkewSSYT.eq_of_entries_eq {N : ℕ} {s : SkewPartition N} {T1 T2 : SkewSSYT s} (h : T1.entries = T2.entries) : T1 = T2

Two skew SSYT are equal if their entries are equal.

instance SymmetricFunctions.SkewSSYT.instSubsingletonOne (s : SkewPartition 1) : Subsingleton (SkewSSYT s)

For N = 1, all SkewSSYT of a given shape are equal. This is because all entries must be in Fin 1 = {0}, so there's only one possible entry. This is useful for proving special cases of the Bender-Knuth bijection.

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

Two SSYT are equal if their entries are equal.

noncomputable def SymmetricFunctions.SkewSSYT.toMonomial {N : ℕ} {R : Type u_1} [CommRing R] {s : SkewPartition N} (T : SkewSSYT s) : MvPolynomial (Fin N) R

The monomial x^T associated to a skew tableau T.

Equations

• T.toMonomial = ∏ i : Fin N, ∏ j : Fin (s.outer.parts i - s.inner.parts i), MvPolynomial.X (T.entries i j)

theorem SymmetricFunctions.SkewSSYT.colStrict_nonadjacent {N : ℕ} {s : SkewPartition N} (T : SkewSSYT s) (i j : Fin N) (hij : i < j) (k : Fin (s.outer.parts i - s.inner.parts i)) (k' : Fin (s.outer.parts j - s.inner.parts j)) (hcol_eq : s.inner.parts i + ↑k = s.inner.parts j + ↑k') : T.entries i k < T.entries j k'

Column-strictness extends to non-adjacent rows. If column c appears in rows i and j with i < j, then T(i, c) < T(j, c).

This is a key lemma for the nipat-SSYT bijection: it shows that the column-strict condition for adjacent rows implies strict inequality for any two rows that share a column. The proof uses strong induction on the row distance j - i, with the base case being adjacent rows (directly using T.colStrict) and the inductive case going through an intermediate row j' = j - 1.

Finiteness of SSYT

The set of semistandard Young tableaux of a given shape is finite because:

1. The shape has finitely many cells
2. Each cell can contain one of finitely many values (elements of Fin N)
3. The SSYT conditions (row-weak, column-strict) define a subset of all fillings

@[reducible, inline]

abbrev SymmetricFunctions.SkewFilling {N : ℕ} (s : SkewPartition N) : Type

A filling of a skew shape is a function assigning a value in Fin N to each cell. We use abbrev instead of def to ensure type class inference can see through this.

Equations

• SymmetricFunctions.SkewFilling s = ((i : Fin N) → Fin (s.outer.parts i - s.inner.parts i) → Fin N)

instance SymmetricFunctions.skewFilling_fintype {N : ℕ} (s : SkewPartition N) : Fintype (SkewFilling s)

The type of fillings of a skew shape is finite.

Equations

• SymmetricFunctions.skewFilling_fintype s = inferInstance

def SymmetricFunctions.isRowWeak {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Prop

Predicate for a filling satisfying the SSYT row-weak condition.

Equations

• SymmetricFunctions.isRowWeak s f = ∀ (i : Fin N) (j k : Fin (s.outer.parts i - s.inner.parts i)), j ≤ k → f i j ≤ f i k

def SymmetricFunctions.isColStrict {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Prop

Predicate for a filling satisfying the SSYT column-strict condition. This is a simplified version that checks the condition for adjacent rows.

Equations

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

def SymmetricFunctions.isSSYTFilling {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Prop

Combined predicate for SSYT conditions.

Equations

• SymmetricFunctions.isSSYTFilling s f = (SymmetricFunctions.isRowWeak s f ∧ SymmetricFunctions.isColStrict s f)

instance SymmetricFunctions.isRowWeak_decidable {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Decidable (isRowWeak s f)

The row-weak predicate is decidable.

Equations

• SymmetricFunctions.isRowWeak_decidable s f = Fintype.decidableForallFintype

instance SymmetricFunctions.isColStrict_decidable {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Decidable (isColStrict s f)

The column-strict predicate is decidable.

Equations

• SymmetricFunctions.isColStrict_decidable s f = Fintype.decidableForallFintype

instance SymmetricFunctions.isSSYTFilling_decidable {N : ℕ} (s : SkewPartition N) (f : SkewFilling s) : Decidable (isSSYTFilling s f)

The SSYT predicate is decidable.

Equations

• SymmetricFunctions.isSSYTFilling_decidable s f = instDecidableAnd

noncomputable def SymmetricFunctions.ssytFillingFinset {N : ℕ} (s : SkewPartition N) : Finset (SkewFilling s)

The finite set of all fillings satisfying SSYT conditions.

Equations

• SymmetricFunctions.ssytFillingFinset s = Finset.filter (SymmetricFunctions.isSSYTFilling s) Finset.univ

def SymmetricFunctions.SkewSSYT.toFilling {N : ℕ} {s : SkewPartition N} (T : SkewSSYT s) : SkewFilling s

Convert a SkewSSYT to a filling.

Equations

• T.toFilling = T.entries

def SymmetricFunctions.fillingToSkewSSYT {N : ℕ} {s : SkewPartition N} (f : SkewFilling s) (hf : isSSYTFilling s f) : SkewSSYT s

A filling satisfying SSYT conditions can be converted to a SkewSSYT.

Equations

• SymmetricFunctions.fillingToSkewSSYT f hf = { entries := f, rowWeak := ⋯, colStrict := ⋯ }

@[reducible, inline]

abbrev SymmetricFunctions.Filling {N : ℕ} (lam : NPartition N) : Type

A filling of a non-skew shape λ.

Equations

• SymmetricFunctions.Filling lam = ((i : Fin N) → Fin (lam.parts i) → Fin N)

instance SymmetricFunctions.filling_fintype {N : ℕ} (lam : NPartition N) : Fintype (Filling lam)

Fintype instance for fillings of non-skew shapes.

Equations

• SymmetricFunctions.filling_fintype lam = inferInstance

def SymmetricFunctions.isRowWeakFilling {N : ℕ} (lam : NPartition N) (f : Filling lam) : Prop

Row-weak predicate for fillings of non-skew shapes.

Equations

• SymmetricFunctions.isRowWeakFilling lam f = ∀ (i : Fin N) (j k : Fin (lam.parts i)), j ≤ k → f i j ≤ f i k

def SymmetricFunctions.isColStrictFilling {N : ℕ} (lam : NPartition N) (f : Filling lam) : Prop

Column-strict predicate for fillings of non-skew shapes.

Equations

• SymmetricFunctions.isColStrictFilling lam f = ∀ (i : Fin N) (hi : ↑i + 1 < N) (j : Fin (lam.parts i)) (hj : ↑j < lam.parts ⟨↑i + 1, hi⟩), f i j < f ⟨↑i + 1, hi⟩ ⟨↑j, hj⟩

def SymmetricFunctions.isSSYTFillingNonSkew {N : ℕ} (lam : NPartition N) (f : Filling lam) : Prop

Combined SSYT predicate for non-skew fillings.

Equations

• SymmetricFunctions.isSSYTFillingNonSkew lam f = (SymmetricFunctions.isRowWeakFilling lam f ∧ SymmetricFunctions.isColStrictFilling lam f)

instance SymmetricFunctions.isRowWeakFilling_decidable {N : ℕ} (lam : NPartition N) (f : Filling lam) : Decidable (isRowWeakFilling lam f)

Decidability of row-weak for non-skew fillings.

Equations

• SymmetricFunctions.isRowWeakFilling_decidable lam f = Fintype.decidableForallFintype

instance SymmetricFunctions.isColStrictFilling_decidable {N : ℕ} (lam : NPartition N) (f : Filling lam) : Decidable (isColStrictFilling lam f)

Decidability of column-strict for non-skew fillings.

Equations

• SymmetricFunctions.isColStrictFilling_decidable lam f = Fintype.decidableForallFintype

instance SymmetricFunctions.isSSYTFillingNonSkew_decidable {N : ℕ} (lam : NPartition N) (f : Filling lam) : Decidable (isSSYTFillingNonSkew lam f)

Decidability of SSYT predicate for non-skew fillings.

Equations

• SymmetricFunctions.isSSYTFillingNonSkew_decidable lam f = instDecidableAnd

noncomputable def SymmetricFunctions.ssytFillingFinsetNonSkew {N : ℕ} (lam : NPartition N) : Finset (Filling lam)

Finset of valid fillings for non-skew shapes.

Equations

• SymmetricFunctions.ssytFillingFinsetNonSkew lam = Finset.filter (SymmetricFunctions.isSSYTFillingNonSkew lam) Finset.univ

def SymmetricFunctions.fillingToSSYT {N : ℕ} (lam : NPartition N) (f : Filling lam) (hf : isSSYTFillingNonSkew lam f) : SSYT lam

Convert a valid filling to an SSYT.

Equations

• SymmetricFunctions.fillingToSSYT lam f hf = { entries := f, rowWeak := ⋯, colStrict := ⋯ }

theorem SymmetricFunctions.SSYT.entries_isSSYTFillingNonSkew {N : ℕ} {lam : NPartition N} (T : SSYT lam) : isSSYTFillingNonSkew lam T.entries

An SSYT's entries form a valid filling.

theorem SymmetricFunctions.SSYT.entries_mem_ssytFillingFinsetNonSkew {N : ℕ} {lam : NPartition N} (T : SSYT lam) : T.entries ∈ ssytFillingFinsetNonSkew lam

An SSYT's entries are in the valid filling finset.

noncomputable def SymmetricFunctions.ssytFinset {N : ℕ} (lam : NPartition N) : Finset (SSYT lam)

The set of all SSYT of shape λ. This is finite because it's a subset of all fillings, which is finite.

Equations

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

theorem SymmetricFunctions.ssytFinset_mem {N : ℕ} (lam : NPartition N) (T : SSYT lam) : T ∈ ssytFinset lam

Every SSYT is in ssytFinset.

noncomputable def SymmetricFunctions.skewSSYTFinset {N : ℕ} (s : SkewPartition N) : Finset (SkewSSYT s)

The set of all skew SSYT of shape λ/μ. This is finite because it's a subset of all fillings, which is finite.

Equations

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

theorem SymmetricFunctions.SkewSSYT.toFilling_isSSYTFilling {N : ℕ} {s : SkewPartition N} (T : SkewSSYT s) : isSSYTFilling s T.toFilling

A SkewSSYT's entries form a valid SSYT filling.

theorem SymmetricFunctions.SkewSSYT.entries_mem_ssytFillingFinset {N : ℕ} {s : SkewPartition N} (T : SkewSSYT s) : T.entries ∈ ssytFillingFinset s

A SkewSSYT's entries are in ssytFillingFinset.

theorem SymmetricFunctions.skewSSYTFinset_mem {N : ℕ} (s : SkewPartition N) (T : SkewSSYT s) : T ∈ skewSSYTFinset s

Every skew SSYT is a member of skewSSYTFinset. This follows from the definition of skewSSYTFinset as the set of ALL skew SSYT.

noncomputable def SymmetricFunctions.schur {N : ℕ} {R : Type u_1} [CommRing R] (lam : NPartition N) : MvPolynomial (Fin N) R

The Schur polynomial s_λ defined as the sum over all SSYT of shape λ. Definition def.sf.schur.

Equations

• SymmetricFunctions.schur lam = ∑ T ∈ SymmetricFunctions.ssytFinset lam, T.toMonomial

The Schur polynomial of the zero partition

For the zero partition (0, 0, ..., 0), all rows have 0 entries, so there is exactly one SSYT of this shape (the empty tableau). Its monomial is 1.

def SymmetricFunctions.SSYT.unique {N : ℕ} : SSYT 0

The unique SSYT of shape 0 (the empty tableau). Since all rows have 0 entries, the entries function is vacuously defined.

Equations

• SymmetricFunctions.SSYT.unique = { entries := fun (x : Fin N) (j : Fin (SymmetricFunctions.NPartition.parts 0 x)) => j.elim0, rowWeak := ⋯, colStrict := ⋯ }

theorem SymmetricFunctions.SSYT.eq_unique {N : ℕ} (T : SSYT 0) : T = unique

Any SSYT of shape 0 equals the unique empty tableau.

@[simp]

theorem SymmetricFunctions.SSYT.toMonomial_unique {N : ℕ} {R : Type u_1} [CommRing R] : unique.toMonomial = 1

The monomial of the unique SSYT of shape 0 is 1.

theorem SymmetricFunctions.ssytFinset_zero {N : ℕ} : ssytFinset 0 = {SSYT.unique}

The finite set of SSYT of shape 0 is the singleton containing the unique empty tableau.

@[simp]

theorem SymmetricFunctions.schur_zero {N : ℕ} {R : Type u_1} [CommRing R] : schur 0 = 1

The Schur polynomial of the zero partition is 1. This is because the only SSYT of shape 0 is the empty tableau with monomial 1.

noncomputable def SymmetricFunctions.skewSchur {N : ℕ} {R : Type u_1} [CommRing R] (s : SkewPartition N) : MvPolynomial (Fin N) R

The skew Schur polynomial s_{λ/μ} defined as the sum over all skew SSYT. Definition def.sf.skew-schur.

Equations

• SymmetricFunctions.skewSchur s = ∑ T ∈ SymmetricFunctions.skewSSYTFinset s, T.toMonomial

def SymmetricFunctions.ssytToSkewSSYT {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (T : SSYT { parts := lam, weaklyDecreasing := hlam }) : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := fun (x : Fin N) => 0, weaklyDecreasing := ⋯ }, contained := ⋯ }

Convert an SSYT to a SkewSSYT when the inner partition is zero. This is an identity on entries since lam i - 0 = lam i definitionally.

Equations

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

def SymmetricFunctions.skewSSYTToSSYT {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := fun (x : Fin N) => 0, weaklyDecreasing := ⋯ }, contained := ⋯ }) : SSYT { parts := lam, weaklyDecreasing := hlam }

Convert a SkewSSYT to an SSYT when the inner partition is zero. This is the inverse of ssytToSkewSSYT.

Equations

• SymmetricFunctions.skewSSYTToSSYT lam hlam T = { entries := fun (i : Fin N) (j : Fin ({ parts := lam, weaklyDecreasing := hlam }.parts i)) => T.entries i j, rowWeak := ⋯, colStrict := ⋯ }

theorem SymmetricFunctions.ssytToSkewSSYT_skewSSYTToSSYT {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (T : SSYT { parts := lam, weaklyDecreasing := hlam }) : skewSSYTToSSYT lam hlam (ssytToSkewSSYT lam hlam T) = T

ssytToSkewSSYT and skewSSYTToSSYT are inverses (direction 1).

theorem SymmetricFunctions.skewSSYTToSSYT_ssytToSkewSSYT {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := fun (x : Fin N) => 0, weaklyDecreasing := ⋯ }, contained := ⋯ }) : ssytToSkewSSYT lam hlam (skewSSYTToSSYT lam hlam T) = T

ssytToSkewSSYT and skewSSYTToSSYT are inverses (direction 2).

theorem SymmetricFunctions.ssytToSkewSSYT_toMonomial {N : ℕ} {R : Type u_1} [CommRing R] (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (T : SSYT { parts := lam, weaklyDecreasing := hlam }) : (ssytToSkewSSYT lam hlam T).toMonomial = T.toMonomial

ssytToSkewSSYT preserves monomials.

theorem SymmetricFunctions.skewSchur_zero_eq_schur {N : ℕ} {R : Type u_1} [CommRing R] (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) : skewSchur { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := fun (x : Fin N) => 0, weaklyDecreasing := ⋯ }, contained := ⋯ } = schur { parts := lam, weaklyDecreasing := hlam }

When the inner partition is zero, the skew Schur polynomial equals the regular Schur polynomial. This is because the skew shape λ/0 is just the shape λ.

The Pieri Rules

Theorem thm.sf.pieri: The Pieri rules express products h_n · s_μ and e_n · s_μ as sums of Schur polynomials.

Enumeration of Horizontal and Vertical Strip Partitions

For a fixed N-partition μ and size n, we enumerate all N-partitions λ such that λ/μ is a horizontal (resp. vertical) n-strip. The key observation is that each λ_i is bounded:

• Lower bound: λ_i ≥ μ_i (containment)
• Upper bound: λ_i ≤ μ_{i-1} for i > 0 (horizontal strip condition)
• Upper bound: λ_0 ≤ μ_0 + n (since |λ| = |μ| + n)

This makes the enumeration finite.

def SymmetricFunctions.horizontalStripUpperBound {N : ℕ} (mu : NPartition N) (n : ℕ) (i : Fin N) : ℕ

The bound for each λ_i when forming a horizontal strip with μ. λ_i must satisfy μ_i ≤ λ_i ≤ bound_i where:

• For i = 0: bound_0 = μ_0 + n (since |λ| - |μ| = n and all parts are bounded by λ_0)
• For i > 0: bound_i = μ_{i-1} (horizontal strip condition: μ_{i-1} ≥ λ_i)

Equations

• SymmetricFunctions.horizontalStripUpperBound mu n i = if h : ↑i = 0 then mu.parts ⟨0, ⋯⟩ + n else mu.parts ⟨↑i - 1, ⋯⟩

def SymmetricFunctions.potentialHorizontalStrips {N : ℕ} (mu : NPartition N) (n : ℕ) : Finset (Fin N → ℕ)

A function from Fin N to ℕ that could potentially form a horizontal n-strip with μ. This is the set of all functions bounded by the horizontal strip constraints.

Equations

• SymmetricFunctions.potentialHorizontalStrips mu n = Fintype.piFinset fun (i : Fin N) => Finset.Icc (mu.parts i) (SymmetricFunctions.horizontalStripUpperBound mu n i)

def SymmetricFunctions.isWeaklyDecreasing {N : ℕ} (f : Fin N → ℕ) : Prop

Check if a function forms a valid N-partition (weakly decreasing).

Equations

• SymmetricFunctions.isWeaklyDecreasing f = ∀ (i j : Fin N), i ≤ j → f j ≤ f i

instance SymmetricFunctions.instDecidableIsWeaklyDecreasing {N : ℕ} (f : Fin N → ℕ) : Decidable (isWeaklyDecreasing f)

Equations

• SymmetricFunctions.instDecidableIsWeaklyDecreasing f = Fintype.decidableForallFintype

def SymmetricFunctions.hasSizeDiff {N : ℕ} (mu lam : Fin N → ℕ) (n : ℕ) : Prop

Check if |λ| - |μ| = n.

Equations

• SymmetricFunctions.hasSizeDiff mu lam n = (∑ i : Fin N, lam i = ∑ i : Fin N, mu i + n)

instance SymmetricFunctions.instDecidableHasSizeDiff {N : ℕ} (mu lam : Fin N → ℕ) (n : ℕ) : Decidable (hasSizeDiff mu lam n)

Equations

• SymmetricFunctions.instDecidableHasSizeDiff mu lam n = inferInstanceAs (Decidable (∑ i : Fin N, lam i = ∑ i : Fin N, mu i + n))

def SymmetricFunctions.isHorizontalStripFun {N : ℕ} (lam mu : Fin N → ℕ) : Prop

A skew partition λ/μ is a horizontal strip if no two boxes lie in the same column. Equivalently: μ_i ≥ λ_{i+1} for all i.

The argument order (lam, mu) matches standard mathematical notation λ/μ.

Related definitions:

• SkewPartition.isHorizontalStrip: Bundled version for SkewPartition N

Equations

• SymmetricFunctions.isHorizontalStripFun lam mu = ∀ (i : Fin N) (hi : ↑i + 1 < N), mu i ≥ lam ⟨↑i + 1, hi⟩

def SymmetricFunctions.isVerticalStripFun {N : ℕ} (lam mu : Fin N → ℕ) : Prop

A skew partition λ/μ is a vertical strip if no two boxes lie in the same row. Equivalently: λ_i ≤ μ_i + 1 for all i.

The argument order (lam, mu) matches standard mathematical notation λ/μ.

Related definitions:

• SkewPartition.isVerticalStrip: Bundled version for SkewPartition N

Equations

• SymmetricFunctions.isVerticalStripFun lam mu = ∀ (i : Fin N), lam i ≤ mu i + 1

instance SymmetricFunctions.instDecidableIsHorizontalStripFun {N : ℕ} (lam mu : Fin N → ℕ) : Decidable (isHorizontalStripFun lam mu)

Decidable instance for horizontal strip predicate.

Equations

• SymmetricFunctions.instDecidableIsHorizontalStripFun lam mu = Fintype.decidableForallFintype

instance SymmetricFunctions.instDecidableIsVerticalStripFun {N : ℕ} (lam mu : Fin N → ℕ) : Decidable (isVerticalStripFun lam mu)

Decidable instance for vertical strip predicate.

Equations

• SymmetricFunctions.instDecidableIsVerticalStripFun lam mu = Fintype.decidableForallFintype

def SymmetricFunctions.toNPartition {N : ℕ} (f : Fin N → ℕ) (hf : isWeaklyDecreasing f) : NPartition N

Convert a valid function to an NPartition.

Equations

• SymmetricFunctions.toNPartition f hf = { parts := f, weaklyDecreasing := hf }

def SymmetricFunctions.horizontalNStripPartitions {N : ℕ} (mu : NPartition N) (n : ℕ) : Finset (NPartition N)

The set of N-partitions λ such that λ/μ is a horizontal n-strip.

This is the set of all N-partitions λ satisfying:

1. μ ⊆ λ (containment): μ_i ≤ λ_i for all i
2. Horizontal strip: μ_i ≥ λ_{i+1} for all i < N
3. Size: |λ| - |μ| = n

The set is finite because each λ_i is bounded.

Equations

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

def SymmetricFunctions.verticalStripUpperBound {N : ℕ} (mu : NPartition N) (i : Fin N) : ℕ

The bound for each λ_i when forming a vertical strip with μ. λ_i must satisfy μ_i ≤ λ_i ≤ μ_i + 1 (vertical strip condition).

Equations

• SymmetricFunctions.verticalStripUpperBound mu i = mu.parts i + 1

def SymmetricFunctions.potentialVerticalStrips {N : ℕ} (mu : NPartition N) : Finset (Fin N → ℕ)

A function from Fin N to ℕ that could potentially form a vertical n-strip with μ.

Equations

• SymmetricFunctions.potentialVerticalStrips mu = Fintype.piFinset fun (i : Fin N) => Finset.Icc (mu.parts i) (SymmetricFunctions.verticalStripUpperBound mu i)

def SymmetricFunctions.verticalNStripPartitions {N : ℕ} (mu : NPartition N) (n : ℕ) : Finset (NPartition N)

The set of N-partitions λ such that λ/μ is a vertical n-strip.

This is the set of all N-partitions λ satisfying:

1. μ ⊆ λ (containment): μ_i ≤ λ_i for all i
2. Vertical strip: λ_i ≤ μ_i + 1 for all i
3. Size: |λ| - |μ| = n

The set is finite because each λ_i ∈ {μ_i, μ_i + 1}.

Equations

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

Properties of Horizontal Strip Partitions

theorem SymmetricFunctions.horizontalNStripPartitions_contained {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ horizontalNStripPartitions mu n) : mu ≤ lam

If λ ∈ horizontalNStripPartitions μ n, then μ ⊆ λ.

theorem SymmetricFunctions.horizontalNStripPartitions_isHorizontalStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ horizontalNStripPartitions mu n) : { outer := lam, inner := mu, contained := ⋯ }.isHorizontalStrip

If λ ∈ horizontalNStripPartitions μ n, then λ/μ is a horizontal strip.

theorem SymmetricFunctions.horizontalNStripPartitions_size {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ horizontalNStripPartitions mu n) : lam.size - mu.size = n

If λ ∈ horizontalNStripPartitions μ n, then |λ| - |μ| = n.

theorem SymmetricFunctions.horizontalNStripPartitions_isHorizontalNStrip' {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ horizontalNStripPartitions mu n) : { outer := lam, inner := mu, contained := ⋯ }.isHorizontalNStrip n

If λ ∈ horizontalNStripPartitions μ n, then the skew partition λ/μ is a horizontal n-strip. This combines the horizontal strip condition and size condition into a single predicate.

Properties of Vertical Strip Partitions

theorem SymmetricFunctions.verticalNStripPartitions_contained {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ verticalNStripPartitions mu n) : mu ≤ lam

If λ ∈ verticalNStripPartitions μ n, then μ ⊆ λ.

theorem SymmetricFunctions.verticalNStripPartitions_isVerticalStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ verticalNStripPartitions mu n) : { outer := lam, inner := mu, contained := ⋯ }.isVerticalStrip

If λ ∈ verticalNStripPartitions μ n, then λ/μ is a vertical strip.

theorem SymmetricFunctions.verticalNStripPartitions_size {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ verticalNStripPartitions mu n) : lam.size - mu.size = n

If λ ∈ verticalNStripPartitions μ n, then |λ| - |μ| = n.

theorem SymmetricFunctions.verticalNStripPartitions_isVerticalNStrip' {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hlam : lam ∈ verticalNStripPartitions mu n) : { outer := lam, inner := mu, contained := ⋯ }.isVerticalNStrip n

If λ ∈ verticalNStripPartitions μ n, then the skew partition λ/μ is a vertical n-strip. This combines the vertical strip condition and size condition into a single predicate.

Membership Characterization for Strip Partitions

These theorems provide complete characterizations of membership in horizontalNStripPartitions and verticalNStripPartitions, useful for proving that specific partitions belong to these sets.

theorem SymmetricFunctions.mem_horizontalNStripPartitions_iff {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) : lam ∈ horizontalNStripPartitions mu n ↔ (∀ (i : Fin N), mu.parts i ≤ lam.parts i) ∧ isHorizontalStripFun lam.parts mu.parts ∧ hasSizeDiff mu.parts lam.parts n ∧ ∀ (i : Fin N), lam.parts i ≤ horizontalStripUpperBound mu n i

Complete characterization of membership in horizontalNStripPartitions.

An N-partition λ is in horizontalNStripPartitions μ n if and only if:

1. μ ⊆ λ (containment): μ_i ≤ λ_i for all i
2. λ/μ is a horizontal strip: μ_i ≥ λ_{i+1} for all i < N
3. |λ| - |μ| = n (size constraint)
4. Each λ_i is bounded by horizontalStripUpperBound μ n i

This characterization is useful for proving that specific partitions belong to horizontalNStripPartitions μ n.

theorem SymmetricFunctions.mem_verticalNStripPartitions_iff {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) : lam ∈ verticalNStripPartitions mu n ↔ (∀ (i : Fin N), mu.parts i ≤ lam.parts i) ∧ isVerticalStripFun lam.parts mu.parts ∧ hasSizeDiff mu.parts lam.parts n

Complete characterization of membership in verticalNStripPartitions.

An N-partition λ is in verticalNStripPartitions μ n if and only if:

1. μ ⊆ λ (containment): μ_i ≤ λ_i for all i
2. λ/μ is a vertical strip: λ_i ≤ μ_i + 1 for all i
3. |λ| - |μ| = n (size constraint)

This characterization is useful for proving that specific partitions belong to verticalNStripPartitions μ n.

theorem SymmetricFunctions.hasSizeDiff_of_isHorizontalNStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hcontained : mu ≤ lam) (hstrip : { outer := lam, inner := mu, contained := hcontained }.isHorizontalNStrip n) : hasSizeDiff mu.parts lam.parts n

Helper lemma relating SkewPartition.size to hasSizeDiff for horizontal strips.

theorem SymmetricFunctions.hasSizeDiff_of_isVerticalNStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hcontained : mu ≤ lam) (hstrip : { outer := lam, inner := mu, contained := hcontained }.isVerticalNStrip n) : hasSizeDiff mu.parts lam.parts n

Helper lemma relating SkewPartition.size to hasSizeDiff for vertical strips.

theorem SymmetricFunctions.mem_horizontalNStripPartitions_of_isHorizontalNStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hcontained : mu ≤ lam) (hstrip : { outer := lam, inner := mu, contained := hcontained }.isHorizontalNStrip n) (hbound : ∀ (i : Fin N), lam.parts i ≤ horizontalStripUpperBound mu n i) : lam ∈ horizontalNStripPartitions mu n

Simplified membership criterion for horizontal strip partitions using SkewPartition API.

This theorem bridges the gap between the horizontalNStripPartitions finset and the SkewPartition.isHorizontalNStrip predicate.

theorem SymmetricFunctions.mem_verticalNStripPartitions_of_isVerticalNStrip {N : ℕ} (mu : NPartition N) (n : ℕ) (lam : NPartition N) (hcontained : mu ≤ lam) (hstrip : { outer := lam, inner := mu, contained := hcontained }.isVerticalNStrip n) : lam ∈ verticalNStripPartitions mu n

Simplified membership criterion for vertical strip partitions using SkewPartition API.

This theorem bridges the gap between the verticalNStripPartitions finset and the SkewPartition.isVerticalNStrip predicate.

Infrastructure for Pieri Rule Proofs

The Pieri rules require a bijection between:

• Domain: Sym (Fin N) n × SSYT μ (multisets of size n paired with tableaux of shape μ)
• Codomain: ⨆_{λ ∈ horizontalNStripPartitions μ n} SSYT λ (tableaux of shapes forming horizontal n-strips)

This bijection is the RSK row insertion. Below we provide lemmas that show how the RHS of the Pieri rule can be rewritten as a sum over a sigma type, making the structure of the proof clear.

Alternative Approach: Pieri Rules via Littlewood-Richardson

An alternative proof of the Pieri rules derives them from the Littlewood-Richardson rule. The key observations are:

1. h_n = s_{(n,0,...,0)}: The complete homogeneous symmetric polynomial h_n equals the Schur polynomial indexed by the row partition (n, 0, ..., 0).

2. e_n = s_{(1,1,...,1,0,...,0)}: The elementary symmetric polynomial e_n equals the Schur polynomial indexed by the column partition with n ones.

3. Littlewood-Richardson specialization: When ν = (n, 0, ..., 0), the ν-Yamanouchi tableaux of shape λ/μ correspond exactly to horizontal n-strips (or vertical n-strips for the column partition case).

The infrastructure for this approach requires:

• NPartition.rowPartition: The partition (n, 0, ..., 0) ✓ (defined above)
• NPartition.colPartition: The partition (1, 1, ..., 1, 0, ..., 0) ✓ (defined above)
• hsymm_eq_schur_rowPartition: h_n = s_{rowPartition} ✓ (proved below)
• esymm_eq_schur_colPartition: e_n = s_{colPartition} ✓ (proved below)
• Characterization of Yamanouchi tableaux for row/column partitions (partial: reverse direction proved)

This approach is documented in Exercise exe.sf.pieri of the source text. The Pieri rules themselves are left as exercises (see pieri_horizontal, pieri_vertical).

Yamanouchi Tableaux Infrastructure for Row/Column Partitions

This section provides infrastructure for working with row and column partitions in the context of Yamanouchi tableaux (defined in LittlewoodRichardson.lean).

Mathematical Background:

The key insight connecting the Littlewood-Richardson rule to Pieri rules is that Yamanouchi tableaux for row and column partitions have a simple characterization:

For row partition ν = (n, 0, ..., 0): A semistandard tableau T of shape λ/μ is ν-Yamanouchi iff:

1. All entries of T are 0 (the first row index)
2. λ/μ is a horizontal strip (no two cells in same column)

This is because:

• The Yamanouchi condition requires ν + cont(col_{≥j}(T)) to be weakly decreasing for all j > 0
• For ν = (n, 0, ..., 0), adding any content to position i > 0 would violate this
• So all entries must be 0, and semistandardness forces at most one cell per column

For column partition ν = (1, 1, ..., 1, 0, ..., 0) with n ones: A semistandard tableau T of shape λ/μ is ν-Yamanouchi iff:

1. Entries form a valid "staircase" pattern (entry in row i is at least i)
2. λ/μ is a vertical strip (no two cells in same row)

This is because:

• The Yamanouchi condition with column partition ensures votes are spread across rows
• Semistandardness with at most one entry per row gives vertical strip

What's provided here:

• rowPartitionFun, colPartitionFun: Functions extracting partition parts
• Simp lemmas for accessing row/column partition values
• Proofs that these are valid N-partitions

Note: The reverse direction allEntriesZero_implies_isYamanouchi_rowPartition is proved below: for row partition ν = (n, 0, ..., 0), if all entries of a semistandard tableau are 0, then it is ν-Yamanouchi.

def SymmetricFunctions.rowPartitionFun (N n : ℕ) (hN : 0 < N) : Fin N → ℕ

Row partition as a function (for use with LittlewoodRichardson.IsYamanouchi).

Equations

• SymmetricFunctions.rowPartitionFun N n hN = (SymmetricFunctions.NPartition.rowPartition N n hN).parts

def SymmetricFunctions.colPartitionFun (N n : ℕ) (hn : n ≤ N) : Fin N → ℕ

Column partition as a function (for use with LittlewoodRichardson.IsYamanouchi).

Equations

• SymmetricFunctions.colPartitionFun N n hn = (SymmetricFunctions.NPartition.colPartition N n hn).parts

@[simp]

theorem SymmetricFunctions.rowPartitionFun_zero (N n : ℕ) (hN : 0 < N) : rowPartitionFun N n hN ⟨0, hN⟩ = n

The row partition function has n at position 0 and 0 elsewhere.

@[simp]

theorem SymmetricFunctions.rowPartitionFun_pos (N n : ℕ) (hN : 0 < N) (i : Fin N) (hi : 0 < ↑i) : rowPartitionFun N n hN i = 0

@[simp]

theorem SymmetricFunctions.colPartitionFun_lt (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : ↑i < n) : colPartitionFun N n hn i = 1

The column partition function has 1 at positions < n and 0 elsewhere.

@[simp]

theorem SymmetricFunctions.colPartitionFun_ge (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : n ≤ ↑i) : colPartitionFun N n hn i = 0

theorem SymmetricFunctions.rowPartitionFun_isNPartition (N n : ℕ) (hN : 0 < N) : IsNPartition (rowPartitionFun N n hN)

The row partition function is an N-partition (weakly decreasing).

theorem SymmetricFunctions.colPartitionFun_isNPartition (N n : ℕ) (hn : n ≤ N) : IsNPartition (colPartitionFun N n hn)

The column partition function is an N-partition (weakly decreasing).

Yamanouchi Tableaux Characterization for Row/Column Partitions

This section provides the key characterization theorems connecting Yamanouchi tableaux with horizontal and vertical strips. These theorems enable the alternative proof of Pieri rules via the Littlewood-Richardson rule.

Mathematical Background:

For the row partition ν = (n, 0, ..., 0):

• A semistandard tableau T of shape λ/μ is ν-Yamanouchi iff all entries are 0 and λ/μ is a horizontal strip.
• This is because adding any content to position i > 0 would violate the weakly decreasing property of ν + cont(col_{≥j}(T)).

For the column partition ν = (1, 1, ..., 1, 0, ..., 0) with n ones:

• A semistandard tableau T of shape λ/μ is ν-Yamanouchi iff entries follow a specific pattern and λ/μ is a vertical strip.

Equivalences Between Strip Definitions

The following lemmas establish equivalences between the bundled and unbundled representations of horizontal/vertical strip predicates:

1. Bundled: SkewPartition.isHorizontalStrip / SkewPartition.isVerticalStrip

   • Input: SkewPartition N (bundled outer/inner partitions)
   • Used in: Main theorems like pieri_horizontal, pieri_vertical

2. Unbundled (canonical): isHorizontalStripFun / isVerticalStripFun

   • Input: (lam mu : Fin N → ℕ) with argument order (lam, mu) matching λ/μ notation
   • Used in: horizontalNStripPartitions, verticalNStripPartitions, and integration with LittlewoodRichardson.Tableau

theorem SymmetricFunctions.SkewPartition.isHorizontalStrip_iff_isHorizontalStripFun {N : ℕ} (s : SkewPartition N) : s.isHorizontalStrip ↔ isHorizontalStripFun s.outer.parts s.inner.parts

The bundled SkewPartition.isHorizontalStrip is equivalent to the canonical unbundled isHorizontalStripFun applied to the outer and inner partitions.

theorem SymmetricFunctions.SkewPartition.isVerticalStrip_iff_isVerticalStripFun {N : ℕ} (s : SkewPartition N) : s.isVerticalStrip ↔ isVerticalStripFun s.outer.parts s.inner.parts

The bundled SkewPartition.isVerticalStrip is equivalent to the canonical unbundled isVerticalStripFun applied to the outer and inner partitions.

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

All entries of a tableau are 0 (the first row index). This is the key property for row partition Yamanouchi tableaux.

Equations

• SymmetricFunctions.allEntriesZero T = ∀ (c : { c : Fin N × ℕ // c ∈ AlgebraicCombinatorics.skewYoungDiagram lam mu }), ↑(T c) = 0

noncomputable instance SymmetricFunctions.instDecidableAllEntriesZero {N : ℕ} {lam mu : Fin N → ℕ} (T : AlgebraicCombinatorics.Tableau lam mu) : Decidable (allEntriesZero T)

Decidable instance for allEntriesZero when the diagram is finite.

Equations

• SymmetricFunctions.instDecidableAllEntriesZero T = Fintype.decidableForallFintype

theorem SymmetricFunctions.contentColGeq_zero_of_allEntriesZero {N : ℕ} {lam mu : Fin N → ℕ} (T : AlgebraicCombinatorics.Tableau lam mu) (hZero : allEntriesZero T) (j : ℕ) (k : Fin N) (hk : 0 < ↑k) : AlgebraicCombinatorics.contentColGeq T j k = 0

When all entries of a tableau are 0, the content at any position k > 0 is 0. This is because no cell has entry k when all entries are 0.

theorem SymmetricFunctions.allEntriesZero_implies_isYamanouchi_rowPartition {N : ℕ} {lam mu : Fin N → ℕ} (hN : 0 < N) (T : AlgebraicCombinatorics.Tableau lam mu) (hSS : AlgebraicCombinatorics.IsSemistandard T) (hZero : allEntriesZero T) (n : ℕ) : AlgebraicCombinatorics.IsYamanouchi (rowPartitionFun N n hN) T

Row partition Yamanouchi characterization (reverse direction): If all entries of T are 0 and T is semistandard, then T is ν-Yamanouchi for ν = (n, 0, ..., 0).

Note on Horizontal Strips and Semistandard Tableaux

WARNING: The statement "horizontal strip + semistandard ⟹ all entries 0" is FALSE.

Counterexample: N = 2, λ = (2, 1), μ = (1, 0)

• This is a horizontal strip: μ₀ = 1 ≥ λ₁ = 1 ✓
• Cells: (0, 2) and (1, 1) — in different columns
• Any assignment is semistandard (vacuously, since no two cells share a row or column)
• In particular, T(0, 2) = 1 gives a non-zero entry

WARNING: The statement "Yamanouchi w.r.t. row partition ⟹ all entries 0" is also FALSE without the horizontal strip hypothesis!

Counterexample: N = 3, λ = (2, 2, 0), μ = (0, 0, 0), n = 1, ν = (1, 0, 0)

• This is NOT a horizontal strip (both row 0 and row 1 have 2 cells)
• The tableau T with T(0,1) = 0, T(0,2) = 1, T(1,1) = 1, T(1,2) = 2 is semistandard
• At j = 1: ν + contentColGeq T 1 = (1, 0, 0) + (1, 2, 1) = (2, 2, 1), an N-partition ✓
• At j = 2: ν + contentColGeq T 2 = (1, 0, 0) + (0, 1, 1) = (1, 1, 1), an N-partition ✓
• So T is (1, 0, 0)-Yamanouchi, but has positive entries 1 and 2!

The correct characterization requires BOTH being a horizontal strip AND being Yamanouchi with respect to a row partition.

def SymmetricFunctions.symToRowSSYT {N : ℕ} (hN : 0 < N) (n : ℕ) (s : Sym (Fin N) n) : SSYT (NPartition.rowPartition N n hN)

Convert a Sym to an SSYT of row partition shape. The sorted multiset gives a weakly increasing sequence for row 0.

Equations

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

def SymmetricFunctions.rowSSYTToSym {N : ℕ} (hN : 0 < N) (n : ℕ) (T : SSYT (NPartition.rowPartition N n hN)) : Sym (Fin N) n

Convert an SSYT of row partition shape back to a Sym. Row 0 entries form a weakly increasing sequence which gives a multiset.

Equations

• SymmetricFunctions.rowSSYTToSym hN n T = SymmetricFunctions.weaklyIncreasingToSym n fun (j : Fin n) => T.entries ⟨0, hN⟩ ⟨↑j, ⋯⟩

theorem SymmetricFunctions.rowSSYTToSym_symToRowSSYT {N : ℕ} (hN : 0 < N) (n : ℕ) (s : Sym (Fin N) n) : rowSSYTToSym hN n (symToRowSSYT hN n s) = s

symToRowSSYT and rowSSYTToSym are inverses (Sym → SSYT → Sym).

theorem SymmetricFunctions.symToRowSSYT_toMonomial {N : ℕ} {R : Type u_1} [CommRing R] (hN : 0 < N) (n : ℕ) (s : Sym (Fin N) n) : (symToRowSSYT hN n s).toMonomial = (Multiset.map MvPolynomial.X ↑s).prod

symToRowSSYT preserves monomials.

theorem SymmetricFunctions.hsymm_eq_schur_rowPartition {N : ℕ} {R : Type u_1} [CommRing R] (hN : 0 < N) (n : ℕ) : MvPolynomial.hsymm (Fin N) R n = schur (NPartition.rowPartition N n hN)

The complete homogeneous symmetric polynomial h_n equals the Schur polynomial indexed by the row partition (n, 0, ..., 0).

This is because:

• The only SSYT of shape (n, 0, ..., 0) is a single row of n boxes
• A single row SSYT with entries from Fin N is exactly a weakly increasing sequence
• Such sequences correspond to multisets of size n from Fin N
• The monomial of such a tableau is exactly (s.1.map X).prod for s : Sym (Fin N) n

This lemma enables deriving the horizontal Pieri rule from Littlewood-Richardson.

def SymmetricFunctions.finsetToColSSYT {N : ℕ} (n : ℕ) (hn : n ≤ N) (s : Finset (Fin N)) (hs : s.card = n) : SSYT (NPartition.colPartition N n hn)

Convert a subset of size n to an SSYT of column partition shape. The sorted subset gives a strictly increasing sequence for column 0.

Equations

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

def SymmetricFunctions.colSSYTEntry {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) (k : ℕ) (hk : k < n) : Fin N

Helper for extracting entry from column SSYT

Equations

• SymmetricFunctions.colSSYTEntry n hn T k hk = T.entries ⟨k, ⋯⟩ ⟨0, ⋯⟩

def SymmetricFunctions.colSSYTToFinset {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) : Finset (Fin N)

Inverse bijection: SSYT(colPartition) → Finset

Equations

• SymmetricFunctions.colSSYTToFinset n hn T = Finset.image (fun (k : Fin n) => SymmetricFunctions.colSSYTEntry n hn T ↑k ⋯) Finset.univ

theorem SymmetricFunctions.colSSYTEntry_succ_lt {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) (k : ℕ) (hk : k < n) (hk1 : k + 1 < n) : colSSYTEntry n hn T k hk < colSSYTEntry n hn T (k + 1) hk1

Column entries are strictly increasing - consecutive case

theorem SymmetricFunctions.colSSYTEntry_strictMono {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) (k₁ k₂ : ℕ) (hk₁ : k₁ < n) (hk₂ : k₂ < n) (hlt : k₁ < k₂) : colSSYTEntry n hn T k₁ hk₁ < colSSYTEntry n hn T k₂ hk₂

Column entries are strictly increasing - general case

theorem SymmetricFunctions.colSSYTToFinset_card {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) : (colSSYTToFinset n hn T).card = n

The image has cardinality n because entries are strictly increasing

theorem SymmetricFunctions.colSSYTToFinset_sort_eq {N : ℕ} (n : ℕ) (hn : n ≤ N) (T : SSYT (NPartition.colPartition N n hn)) : ((colSSYTToFinset n hn T).sort fun (x1 x2 : Fin N) => x1 ≤ x2) = List.ofFn fun (k : Fin n) => colSSYTEntry n hn T ↑k ⋯

Sorting colSSYTToFinset gives back the original entries as a list

theorem SymmetricFunctions.finsetToColSSYT_toMonomial {N : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) (hn : n ≤ N) (s : Finset (Fin N)) (hs : s.card = n) : (finsetToColSSYT n hn s hs).toMonomial = ∏ i ∈ s, MvPolynomial.X i

finsetToColSSYT preserves monomials

theorem SymmetricFunctions.esymm_eq_schur_colPartition {N : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) (hn : n ≤ N) : MvPolynomial.esymm (Fin N) R n = schur (NPartition.colPartition N n hn)

The elementary symmetric polynomial e_n equals the Schur polynomial indexed by the column partition (1, 1, ..., 1, 0, ..., 0) with n ones.

This is because:

• The only SSYT of shape (1, 1, ..., 1, 0, ..., 0) is a single column of n boxes
• A single column SSYT with entries from Fin N must have strictly increasing entries
• Such sequences correspond to subsets of size n from Fin N
• The monomial of such a tableau is exactly ∏_{i ∈ s} X_i for s : Finset (Fin N)

This lemma enables deriving the vertical Pieri rule from Littlewood-Richardson.

Proof structure:

1. Both sides are sums of monomials
2. esymm sums over powersetCard n univ with monomial ∏_{i ∈ s} X_i
3. schur sums over SSYT of shape (1,...,1,0,...,0) with monomial T.toMonomial
4. For column partition, SSYT entries in column 0 form strictly increasing sequences
5. The bijection: s ↦ SSYT with entries = sorted(s) in column 0
6. Weight preservation: ∏_{i ∈ s} X_i = T.toMonomial

theorem SymmetricFunctions.pieri_horizontal {N : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) (mu : NPartition N) : MvPolynomial.hsymm (Fin N) R n * schur mu = ∑ lam ∈ horizontalNStripPartitions mu n, schur lam

First Pieri rule (Theorem thm.sf.pieri(a)) Label: exe.sf.pieri

h_n · s_μ = ∑_{λ/μ is horizontal n-strip} s_λ

where h_n is the n-th complete homogeneous symmetric polynomial.

This is Exercise exe.sf.pieri in the TeX source. The proof requires the Robinson-Schensted-Knuth (RSK) row insertion bijection, which is not yet formalized in this project.

theorem SymmetricFunctions.pieri_vertical {N : ℕ} {R : Type u_1} [CommRing R] (n : ℕ) (mu : NPartition N) : MvPolynomial.esymm (Fin N) R n * schur mu = ∑ lam ∈ verticalNStripPartitions mu n, schur lam

Second Pieri rule (Theorem thm.sf.pieri(b)) Label: exe.sf.pieri

e_n · s_μ = ∑_{λ/μ is vertical n-strip} s_λ

where e_n is the n-th elementary symmetric polynomial.

This is Exercise exe.sf.pieri in the TeX source. The proof requires the Robinson-Schensted-Knuth (RSK) column insertion bijection, or alternatively can be derived from pieri_horizontal via the ω-involution.

The Jacobi-Trudi Identities

The Jacobi-Trudi identities express skew Schur polynomials as determinants of matrices involving h_n or e_n.

noncomputable def SymmetricFunctions.hsymmExt {N : ℕ} {R : Type u_1} [CommRing R] (n : ℤ) : MvPolynomial (Fin N) R

Extended h_n: h_n = 0 for n < 0, h_0 = 1. This is needed since the Jacobi-Trudi formula may have negative indices.

Equations

• SymmetricFunctions.hsymmExt n = if 0 ≤ n then MvPolynomial.hsymm (Fin N) R n.toNat else 0

theorem SymmetricFunctions.hsymmExt_isSymmetric {N : ℕ} {R : Type u_1} [CommRing R] (n : ℤ) : (hsymmExt n).IsSymmetric

hsymmExt is symmetric.

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

The Jacobi-Trudi matrix for h (first Jacobi-Trudi formula). Entry (i,j) is h_{λᵢ - μⱼ - i + j}.

Equations

• SymmetricFunctions.jacobiTrudiMatrixH lam mu = Matrix.of fun (i j : Fin N) => SymmetricFunctions.hsymmExt (↑(lam i) - ↑(mu j) - ↑↑i + ↑↑j)

theorem SymmetricFunctions.jacobiTrudi_e {N : ℕ} {R : Type u_1} [CommRing R] (lam mu lamt muT : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hlamt : ∀ (i j : Fin N), i ≤ j → lamt j ≤ lamt i) (hmuT : ∀ (i j : Fin N), i ≤ j → muT j ≤ muT i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) (htranspose_lam : NPartition.IsTranspose lam lamt) (htranspose_mu : NPartition.IsTranspose mu muT) : skewSchur { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ } = (Matrix.of fun (i j : Fin N) => have n := ↑(lamt i) - ↑(muT j) - ↑↑i + ↑↑j; if 0 ≤ n then MvPolynomial.esymm (Fin N) R n.toNat else 0).det

Second Jacobi-Trudi formula (Exercise exe.sf.jt-e) Label: thm.sf.jt-e Status: EXERCISE (exe.sf.jt-e in tex source)

s_{λ/μ} = det((e_{λᵢᵗ - μⱼᵗ - i + j})_{1 ≤ i,j ≤ N})

where λᵗ and μᵗ are the transposes of λ and μ, and e_n denotes the n-th elementary symmetric polynomial (with e_n = 0 for n < 0).

This is a 6-point exercise with no hint provided in the TeX source.

References

• [Stanley, EC2, Theorem 7.16.1]
• [Grinberg-Reiner, Section 2.4]
• [Fulton, Young Tableaux, Section 4.3]

LGV Lemma Connection

The proof of the first Jacobi-Trudi formula uses the LGV lemma. We outline the key constructions here.

Source and Target Vertices for Jacobi-Trudi

For the Jacobi-Trudi identity, we define:

• Source vertices: Aᵢ = (μᵢ - i, 1) for i ∈ [N]
• Target vertices: Bⱼ = (λⱼ - j, N) for j ∈ [N]

These vertices satisfy the sorting conditions required by the LGV lemma (Corollary cor.lgv.kpaths.wt-np):

• x-coordinates are weakly decreasing: x(A₁) ≥ x(A₂) ≥ ... ≥ x(Aₖ)
• y-coordinates are constant (trivially weakly increasing)

def SymmetricFunctions.jacobiTrudiSourceX {N : ℕ} (mu : Fin N → ℕ) (i : Fin N) : ℤ

The source vertex A_i = (μ_i - i, 1) for the Jacobi-Trudi LGV setup. Here 1 represents the "starting height" in the lattice.

Equations

• SymmetricFunctions.jacobiTrudiSourceX mu i = ↑(mu i) - ↑↑i

def SymmetricFunctions.jacobiTrudiTargetX {N : ℕ} (lam : Fin N → ℕ) (j : Fin N) : ℤ

The target vertex B_j = (λ_j - j, N) for the Jacobi-Trudi LGV setup. Here N represents the "ending height" in the lattice.

Equations

• SymmetricFunctions.jacobiTrudiTargetX lam j = ↑(lam j) - ↑↑j

theorem SymmetricFunctions.jacobiTrudiSourceX_antitone {N : ℕ} (mu : Fin N → ℕ) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (i j : Fin N) : i ≤ j → jacobiTrudiSourceX mu j ≤ jacobiTrudiSourceX mu i

The source x-coordinates are weakly decreasing. This follows from the partition being weakly decreasing: μᵢ - i ≥ μⱼ - j when i ≤ j, since μᵢ ≥ μⱼ and i ≤ j.

theorem SymmetricFunctions.jacobiTrudiTargetX_antitone {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (i j : Fin N) : i ≤ j → jacobiTrudiTargetX lam j ≤ jacobiTrudiTargetX lam i

The target x-coordinates are weakly decreasing. This follows from the partition being weakly decreasing.

theorem SymmetricFunctions.jacobiTrudiPathLength {N : ℕ} (lam mu : Fin N → ℕ) (i j : Fin N) : jacobiTrudiTargetX lam j - jacobiTrudiSourceX mu i = ↑(lam j) - ↑(mu i) - ↑↑j + ↑↑i

The path from A_i to B_j has length λ_j - μ_i - j + i (when non-negative). This equals the index of h in the Jacobi-Trudi matrix entry (j, i).

theorem SymmetricFunctions.jacobiTrudiMatrixH_eq_pathLength {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (i j : Fin N) : jacobiTrudiMatrixH lam mu i j = hsymmExt (jacobiTrudiTargetX lam i - jacobiTrudiSourceX mu j)

The Jacobi-Trudi matrix entry (i, j) equals h_{path length from A_j to B_i}. Note: The path is from source A_j to target B_i. This matches the LGV convention where M_{i,j} = ∑_{p : A_i → B_j} w(p), but with the matrix transposed. Equivalently, the Jacobi-Trudi matrix is the transpose of the LGV path weight matrix.

structure SymmetricFunctions.LatticePath {N : ℕ} (a c : ℤ) : Type

A lattice path in ℤ² from (a, 1) to (c, N) using north and east steps. This is the type of paths relevant for the Jacobi-Trudi proof.

• eastStepHeights : List (Fin N)

  The sequence of heights at which east-steps are taken. A path from (a, 1) to (c, N) has exactly (c - a) east-steps (when c ≥ a), and each east-step occurs at some height in [1, N].

• weaklyIncreasing : List.IsChain (fun (x1 x2 : Fin N) => x1 ≤ x2) self.eastStepHeights

  The heights form a weakly increasing sequence (path goes north or east)

• length_eq : self.eastStepHeights.length = (c - a).toNat

  The number of east-steps equals c - a (when non-negative)

noncomputable def SymmetricFunctions.LatticePath.weight {N : ℕ} {R : Type u_1} [CommRing R] {a c : ℤ} (p : LatticePath a c) : MvPolynomial (Fin N) R

The weight of a lattice path is the product of x_j for each east-step at height j. This corresponds to the weight function w in the source.

Equations

• p.weight = (List.map (fun (j : Fin N) => MvPolynomial.X j) p.eastStepHeights).prod

theorem SymmetricFunctions.LatticePath.ext {N : ℕ} {a c : ℤ} {p q : LatticePath a c} (h : p.eastStepHeights = q.eastStepHeights) : p = q

Extensionality lemma for lattice paths.

theorem SymmetricFunctions.LatticePath.ext_iff {N : ℕ} {a c : ℤ} {p q : LatticePath a c} : p = q ↔ p.eastStepHeights = q.eastStepHeights

def SymmetricFunctions.LatticePath.toSym {N : ℕ} {a c : ℤ} (p : LatticePath a c) : Sym (Fin N) (c - a).toNat

Convert a lattice path to a Sym element (multiset of heights).

Equations

• p.toSym = ⟨↑p.eastStepHeights, ⋯⟩

noncomputable def SymmetricFunctions.symToLatticePath {N : ℕ} {a c : ℤ} (s : Sym (Fin N) (c - a).toNat) : LatticePath a c

Convert a Sym element (multiset) to a lattice path by sorting.

Equations

• SymmetricFunctions.symToLatticePath s = { eastStepHeights := (↑s).sort fun (x1 x2 : Fin N) => x1 ≤ x2, weaklyIncreasing := ⋯, length_eq := ⋯ }

theorem SymmetricFunctions.symToLatticePath_toSym {N : ℕ} {a c : ℤ} (p : LatticePath a c) : symToLatticePath p.toSym = p

Converting a path to Sym and back gives the original path.

theorem SymmetricFunctions.toSym_symToLatticePath {N : ℕ} {a c : ℤ} (s : Sym (Fin N) (c - a).toNat) : (symToLatticePath s).toSym = s

Converting a Sym to a path and back gives the original Sym.

noncomputable def SymmetricFunctions.latticePathSymEquiv {N : ℕ} {a c : ℤ} : LatticePath a c ≃ Sym (Fin N) (c - a).toNat

The equivalence between lattice paths and Sym (multisets).

Equations

• SymmetricFunctions.latticePathSymEquiv = { toFun := SymmetricFunctions.LatticePath.toSym, invFun := SymmetricFunctions.symToLatticePath, left_inv := ⋯, right_inv := ⋯ }

noncomputable instance SymmetricFunctions.instFintypeLatticePath {N : ℕ} {a c : ℤ} : Fintype (LatticePath a c)

Fintype instance for LatticePath via the equivalence with Sym.

Equations

• SymmetricFunctions.instFintypeLatticePath = Fintype.ofEquiv (Sym (Fin N) (c - a).toNat) SymmetricFunctions.latticePathSymEquiv.symm

theorem SymmetricFunctions.symToLatticePath_weight {N : ℕ} {R : Type u_1} [CommRing R] {a c : ℤ} (s : Sym (Fin N) (c - a).toNat) : (symToLatticePath s).weight = (Multiset.map (fun (j : Fin N) => MvPolynomial.X j) ↑s).prod

The weight of a path obtained from sorting a Sym equals the Sym product.

noncomputable def SymmetricFunctions.latticePathFinset {N : ℕ} (a c : ℤ) : Finset (LatticePath a c)

The set of all lattice paths from (a, 1) to (c, N). Empty when c < a (no valid paths), otherwise all paths.

Equations

• SymmetricFunctions.latticePathFinset a c = if 0 ≤ c - a then Finset.univ else ∅

theorem SymmetricFunctions.pathWeightSum_eq_hsymm {N : ℕ} {R : Type u_1} [CommRing R] (a c : ℤ) : ∑ p ∈ latticePathFinset a c, p.weight = hsymmExt (c - a)

Observation 1 from the proof of Theorem thm.sf.jt-h: The sum of path weights from (a, 1) to (c, N) in ℤ² equals h_{c-a}.

This follows from Proposition prop.lgv.1-paths.ct. The key insight is that the weakly increasing sequences of length n with entries in [N] are in bijection with multisets of size n from [N], which are exactly what h_n counts.

structure SymmetricFunctions.Nipat {N : ℕ} (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : Type

A non-intersecting path tuple (nipat) from sources A to targets B. For Jacobi-Trudi, A_i = (μᵢ - i, 1) and B_i = (λᵢ - i, N).

• paths (i : Fin N) : LatticePath (↑(mu i) - ↑↑i) (↑(lam i) - ↑↑i)

  The tuple of paths, one for each i ∈ [N]

• colStrictPaths (i j : Fin N) : i < j → ∀ (k : ℕ) (hk : k < (self.paths i).eastStepHeights.length) (k' : ℕ) (hk' : k' < (self.paths j).eastStepHeights.length), mu i + k = mu j + k' → (self.paths i).eastStepHeights[k] < (self.paths j).eastStepHeights[k']

  The paths satisfy column-strictness: for i < j, if east steps k (in path i) and k' (in path j) correspond to the same tableau column (mu i + k = mu j + k'), then the height of path i at step k is strictly less than the height of path j at step k'. This is the key property that makes the nipat-SSYT bijection work.

noncomputable def SymmetricFunctions.Nipat.weight {N : ℕ} {R : Type u_1} [CommRing R] {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) : MvPolynomial (Fin N) R

The weight of a nipat is the product of the weights of its component paths.

Equations

• np.weight = ∏ i : Fin N, (np.paths i).weight

noncomputable def SymmetricFunctions.nipatToSSYT {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }

The bijection between nipats and SSYT, sending a nipat to the tableau whose i-th row contains the heights of east-steps in path i.

Equations

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

def SymmetricFunctions.mkLatticePathFromEntries {N : ℕ} (lam mu i : ℕ) (entries : Fin (lam - mu) → Fin N) (hrowWeak : ∀ (j k : Fin (lam - mu)), j ≤ k → entries j ≤ entries k) : LatticePath (↑mu - ↑i) (↑lam - ↑i)

Helper to create a LatticePath from tableau entries for a single row. Given entries for row i of a tableau, creates the corresponding lattice path with east-steps at the heights given by the entries.

Equations

• SymmetricFunctions.mkLatticePathFromEntries lam mu i entries hrowWeak = { eastStepHeights := List.ofFn entries, weaklyIncreasing := ⋯, length_eq := ⋯ }

noncomputable def SymmetricFunctions.ssytToNipat {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }) : Nipat lam mu hlam hmu hcontained

The inverse bijection from SSYT to nipats, sending a tableau to the nipat whose i-th path has east-steps at the heights given by row i of the tableau.

Equations

• SymmetricFunctions.ssytToNipat T = { paths := fun (i : Fin N) => SymmetricFunctions.mkLatticePathFromEntries (lam i) (mu i) (↑i) (T.entries i) ⋯, colStrictPaths := ⋯ }

theorem SymmetricFunctions.Nipat.eq_of_paths_eq {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np1 np2 : Nipat lam mu hlam hmu hcontained) (h : np1.paths = np2.paths) : np1 = np2

Two nipats with equal paths are equal.

theorem SymmetricFunctions.ssytToNipat_nipatToSSYT {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) : ssytToNipat (nipatToSSYT np) = np

ssytToNipat is a left inverse of nipatToSSYT.

theorem SymmetricFunctions.nipat_path_length {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) (i : Fin N) : (np.paths i).eastStepHeights.length = lam i - mu i

The length of path i's eastStepHeights equals lam i - mu i.

theorem SymmetricFunctions.nipatToSSYT_entries {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) (i : Fin N) (k : Fin (lam i - mu i)) : (nipatToSSYT np).entries i k = (np.paths i).eastStepHeights.get ⟨↑k, ⋯⟩

Specification lemma for nipatToSSYT: the entries of row i are the heights of the east-steps in path i. This captures the key property of the bijection.

theorem SymmetricFunctions.ssytToNipat_paths {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }) (i : Fin N) (k : Fin (lam i - mu i)) : ((ssytToNipat T).paths i).eastStepHeights.get ⟨↑k, ⋯⟩ = T.entries i k

Specification lemma for ssytToNipat: the east-step heights of path i are the entries of row i of the tableau. This is the inverse specification to nipatToSSYT_entries.

theorem SymmetricFunctions.nipatToSSYT_ssytToNipat {N : ℕ} {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }) : nipatToSSYT (ssytToNipat T) = T

nipatToSSYT is a left inverse of ssytToNipat.

theorem SymmetricFunctions.nipatToSSYT_weight {N : ℕ} {R : Type u_1} [CommRing R] {lam mu : Fin N → ℕ} {hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i} {hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i} {hcontained : ∀ (i : Fin N), mu i ≤ lam i} (np : Nipat lam mu hlam hmu hcontained) : np.weight = (nipatToSSYT np).toMonomial

The weight of a nipat equals the monomial of the corresponding tableau.

theorem SymmetricFunctions.nipat_ssyt_bijection {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : ∃ (f : Nipat lam mu hlam hmu hcontained → SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }), Function.Bijective f ∧ ∀ (np : Nipat lam mu hlam hmu hcontained), np.weight = (f np).toMonomial

Observation 2 from the proof of Theorem thm.sf.jt-h: There is a bijection between nipats from 𝐀 to 𝐁 and SSYT(λ/μ).

The bijection sends a nipat 𝐩 = (p₁, ..., pₖ) to the tableau T(𝐩) where the entries in row i are the heights of the east-steps of pᵢ.

Moreover, the weight of a nipat equals the monomial x_T of the corresponding tableau.

Fintype instance for Nipat via the bijection with SkewSSYT

The Nipat type is finite because it is in bijection with SkewSSYT, which is finite. We establish this by constructing an equivalence using nipatToSSYT and ssytToNipat.

noncomputable instance SymmetricFunctions.SkewSSYT.fintype {N : ℕ} (s : SkewPartition N) : Fintype (SkewSSYT s)

Fintype instance for SkewSSYT via the equivalence with valid fillings.

Equations

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

noncomputable def SymmetricFunctions.nipatSSYTEquiv {N : ℕ} (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : Nipat lam mu hlam hmu hcontained ≃ SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }

The equivalence between Nipat and SkewSSYT, established by the bijection functions.

Equations

• SymmetricFunctions.nipatSSYTEquiv lam mu hlam hmu hcontained = { toFun := SymmetricFunctions.nipatToSSYT, invFun := SymmetricFunctions.ssytToNipat, left_inv := ⋯, right_inv := ⋯ }

noncomputable instance SymmetricFunctions.Nipat.fintype {N : ℕ} (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : Fintype (Nipat lam mu hlam hmu hcontained)

Fintype instance for Nipat via the equivalence with SkewSSYT.

Equations

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

noncomputable def SymmetricFunctions.nipatFinset' {N : ℕ} (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : Finset (Nipat lam mu hlam hmu hcontained)

The finite set of all nipats for given partitions λ/μ.

Equations

• SymmetricFunctions.nipatFinset' lam mu hlam hmu hcontained = Finset.univ

theorem SymmetricFunctions.nipatWeightSum_eq_ssytSum {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : ∑ np : Nipat lam mu hlam hmu hcontained, np.weight = ∑ T : SkewSSYT { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }, T.toMonomial

The sum of nipat weights equals the sum of SSYT monomials. This follows from the bijection and weight preservation.

theorem SymmetricFunctions.nipatWeightSum_eq_skewSchur {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : ∑ np : Nipat lam mu hlam hmu hcontained, np.weight = skewSchur { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }

The sum of nipat weights equals skewSchur. This combines the bijection with the definition of skewSchur.

LGV Infrastructure for Jacobi-Trudi

The proof of det_jacobiTrudiMatrixH_eq_nipatSum requires bridging this file's LatticePath and Nipat types with the LGV infrastructure in LGV2.lean.

We define:

1. Source vertices A_i = (μ_i - i, 1) and target vertices B_j = (λ_j - j, N) in ℤ²
2. An arc weight function that assigns X_j to east-steps at height j
3. Helper lemmas connecting the path weight sum to h_n

The key insight is that:

• The Jacobi-Trudi matrix entry (i, j) = h_{λᵢ - μⱼ - i + j}
• This equals the sum of path weights from A_j to B_i
• By LGV nonpermutable, det = sum over non-intersecting path tuples
• Non-intersecting path tuples correspond exactly to our Nipat type

def SymmetricFunctions.jacobiTrudiSourceVertex {N : ℕ} (mu : Fin N → ℕ) : LGV.kVertex (ℤ × ℤ) N

The source k-vertex for the Jacobi-Trudi LGV setup: A_i = (μ_i - i, 1). The y-coordinate 1 represents the starting height in the lattice.

Equations

• SymmetricFunctions.jacobiTrudiSourceVertex mu i = (SymmetricFunctions.jacobiTrudiSourceX mu i, 1)

def SymmetricFunctions.jacobiTrudiTargetVertex {N : ℕ} (lam : Fin N → ℕ) : LGV.kVertex (ℤ × ℤ) N

The target k-vertex for the Jacobi-Trudi LGV setup: B_j = (λ_j - j, N). The y-coordinate N represents the ending height in the lattice.

Equations

• SymmetricFunctions.jacobiTrudiTargetVertex lam j = (SymmetricFunctions.jacobiTrudiTargetX lam j, ↑N)

theorem SymmetricFunctions.jacobiTrudiSourceVertex_xDecreasing {N : ℕ} (mu : Fin N → ℕ) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) : LGV.xDecreasing (jacobiTrudiSourceVertex mu)

The source vertices have x-coordinates that are weakly decreasing.

theorem SymmetricFunctions.jacobiTrudiSourceVertex_yIncreasing {N : ℕ} (mu : Fin N → ℕ) : LGV.yIncreasing (jacobiTrudiSourceVertex mu)

The source vertices have y-coordinates that are constant (trivially increasing).

theorem SymmetricFunctions.jacobiTrudiTargetVertex_xDecreasing {N : ℕ} (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) : LGV.xDecreasing (jacobiTrudiTargetVertex lam)

The target vertices have x-coordinates that are weakly decreasing.

theorem SymmetricFunctions.jacobiTrudiTargetVertex_yIncreasing {N : ℕ} (lam : Fin N → ℕ) : LGV.yIncreasing (jacobiTrudiTargetVertex lam)

The target vertices have y-coordinates that are constant (trivially increasing).

noncomputable def SymmetricFunctions.jacobiTrudiArcWeight {N : ℕ} {R : Type u_1} [CommRing R] : LGV.ArcWeight LGV.integerLattice (MvPolynomial (Fin N) R)

The arc weight function for the Jacobi-Trudi proof. East-steps at height j (where 1 ≤ j ≤ N) are weighted by X_{j-1}. North-steps are weighted by 1.

Note: The lattice uses y-coordinates 1 to N, but Fin N uses 0 to N-1. An east-step at y-coordinate y gets weight X_{y-1} when 1 ≤ y ≤ N.

Equations

• SymmetricFunctions.jacobiTrudiArcWeight u v x✝ = if v.1 = u.1 + 1 ∧ v.2 = u.2 then if h : 1 ≤ u.2 ∧ u.2 ≤ ↑N then MvPolynomial.X ⟨(u.2 - 1).toNat, ⋯⟩ else 1 else 1

def SymmetricFunctions.extractEastStepYCoords (vertices : List (ℤ × ℤ)) : List ℤ

Extract y-coordinates at east-step positions from a path vertex list. For a path from (a, 1) to (c, N), this gives the sequence of y-coordinates where east-steps occur. The sequence is weakly increasing and has length (c - a).

This is a helper function for constructing the bijection between LGV paths and Sym.

Equations

• One or more equations did not get rendered due to their size.
• SymmetricFunctions.extractEastStepYCoords [] = []
• SymmetricFunctions.extractEastStepYCoords [head] = []

LGV-Nipat Bijection Infrastructure

The following lemmas establish the connection between LGV's PathTuple.isNonIntersecting and our Nipat.colStrictPaths. This is needed for step 4 of the Jacobi-Trudi proof.

The key insight is that for lattice paths from (μᵢ - i, 1) to (λᵢ - i, N):

• Two paths intersect (share a vertex) iff they share a point (x, y) for some x, y
• In the integer lattice, paths can only go north or east
• If path i and path j (with i < j) share a vertex, then at some column c, they have the same height
• This violates column-strictness (which requires path j to be strictly higher than path i at the same column)

Conversely, column-strictness implies non-intersection.

Bijection Overview

The bijection between LGV paths and our LatticePath works as follows:

LGV Path → LatticePath: An LGV path from (a, 1) to (c, N) in the integer lattice is a sequence of vertices where each step is either east (+1 in x) or north (+1 in y). We extract the y-coordinates at which east-steps occur (converted to Fin N by subtracting 1).

LatticePath → LGV Path: A LatticePath has eastStepHeights : List (Fin N) which is weakly increasing. We construct the LGV path by starting at (a, 1) and making north-steps until we reach the first east-step height + 1, then east, then more north-steps, etc.

Weight Preservation:

• jacobiTrudiArcWeight assigns X_{y-1} to east-steps at height y (for 1 ≤ y ≤ N)
• North-steps are assigned weight 1
• LatticePath.weight = ∏ h ∈ eastStepHeights, X_h
• These match since the bijection maps y-coordinate y to height h = y - 1

Non-intersection ↔ Column-strictness: For paths from sources A_i = (μ_i - i, 1) to targets B_i = (λ_i - i, N):

• Two LGV paths intersect iff they share a vertex (x, y)
• At any x-coordinate, path i has a well-defined y-coordinate (height)
• If paths i < j share vertex (x, y), then at column (x - (μ_i - i)) in path i and column (x - (μ_j - j)) in path j, both paths have height y
• Since μ_i - i > μ_j - j (by sorting), the column indices satisfy: col_i = x - μ_i + i and col_j = x - μ_j + j If μ_i + col_i = μ_j + col_j (same tableau column), then col_i = col_j + (μ_j - μ_i)
• Column-strictness requires height_i < height_j at same tableau column
• Intersection would give height_i = height_j = y, violating column-strictness

def SymmetricFunctions.lgvPathEastStepYCoords (vertices : List (ℤ × ℤ)) : List ℤ

Extract the y-coordinates of east-steps from an LGV path vertex list. For a path from (a, 1) to (c, N), this returns the y-coordinates at which each east-step occurs.

Equations

• One or more equations did not get rendered due to their size.
• SymmetricFunctions.lgvPathEastStepYCoords [] = []
• SymmetricFunctions.lgvPathEastStepYCoords [head] = []

theorem SymmetricFunctions.lgvPathEastStepYCoords_length_eq_xDisplacement (vertices : List (ℤ × ℤ)) (h_ne : vertices ≠ []) (h_arcs : ∀ (i : ℕ) (hi : i + 1 < vertices.length), LGV.integerLattice.arc (vertices.get ⟨i, ⋯⟩) (vertices.get ⟨i + 1, hi⟩)) : (lgvPathEastStepYCoords vertices).length = ((vertices.getLast h_ne).1 - (vertices.head h_ne).1).toNat

The number of east-steps equals the x-displacement. This is a key property for the bijection.

theorem SymmetricFunctions.lgvPathEastStepYCoords_weaklyIncreasing (vertices : List (ℤ × ℤ)) (h_arcs : ∀ (i : ℕ) (hi : i + 1 < vertices.length), LGV.integerLattice.arc (vertices.get ⟨i, ⋯⟩) (vertices.get ⟨i + 1, hi⟩)) : List.IsChain (fun (x1 x2 : ℤ) => x1 ≤ x2) (lgvPathEastStepYCoords vertices)

East-step y-coordinates are weakly increasing (paths go north or east).

theorem SymmetricFunctions.lgvPathEastStepYCoords_bounded (vertices : List (ℤ × ℤ)) (h_ne : vertices ≠ []) (h_arcs : ∀ (i : ℕ) (hi : i + 1 < vertices.length), LGV.integerLattice.arc (vertices.get ⟨i, ⋯⟩) (vertices.get ⟨i + 1, hi⟩)) (y : ℤ) (hy : y ∈ lgvPathEastStepYCoords vertices) : (vertices.head h_ne).2 ≤ y ∧ y ≤ (vertices.getLast h_ne).2

East-step y-coordinates are bounded between start and end y-coordinates.

theorem SymmetricFunctions.lgvPathEastStepYCoords_at_x (p : LGV.integerLattice.Path) (k : ℕ) (hk : k < (lgvPathEastStepYCoords p.vertices).length) : ∃ (idx : ℕ) (hidx : idx < p.vertices.length), (p.vertices.get ⟨idx, hidx⟩).1 = p.start.1 + ↑k ∧ (p.vertices.get ⟨idx, hidx⟩).2 = (lgvPathEastStepYCoords p.vertices)[k]

The k-th east-step y-coordinate equals the y-coordinate at x = start_x + k.

This lemma establishes that lgvPathEastStepYCoords[k] is the y-coordinate of the path at x-coordinate start_x + k, where start_x is the x-coordinate of the first vertex.

The k-th east step occurs at x = start_x + k because:

• The path starts at x = start_x
• Each east step increases x by 1
• The k-th east step is preceded by exactly k east steps (indices 0, 1, ..., k-1)
• So the k-th east step starts at x = start_x + k

theorem SymmetricFunctions.lgvPathEastStepYCoords_at_x_is_east_step (p : LGV.integerLattice.Path) (k : ℕ) (hk : k < (lgvPathEastStepYCoords p.vertices).length) (idx : ℕ) (hidx : idx < p.vertices.length) (_hx : (p.vertices.get ⟨idx, hidx⟩).1 = p.start.1 + ↑k) (hy : (p.vertices.get ⟨idx, hidx⟩).2 = (lgvPathEastStepYCoords p.vertices)[k]) (hidx_next : idx + 1 < p.vertices.length) : (p.vertices.get ⟨idx + 1, hidx_next⟩).1 = (p.vertices.get ⟨idx, hidx⟩).1 + 1 ∧ (p.vertices.get ⟨idx + 1, hidx_next⟩).2 = (p.vertices.get ⟨idx, hidx⟩).2

The index returned by lgvPathEastStepYCoords_at_x is the start of an east step. If idx + 1 < vertices.length, then the step from idx to idx+1 is an east step.

theorem SymmetricFunctions.paths_above_at_x_stays_above (p p' : LGV.integerLattice.Path) (hni : ∀ v ∈ p.vertices, v ∉ p'.vertices) (x₀ : ℤ) (hx₀_p : ∃ (idx : ℕ) (hidx : idx < p.vertices.length), (p.vertices.get ⟨idx, hidx⟩).1 = x₀) (hx₀_p' : ∃ (idx : ℕ) (hidx : idx < p'.vertices.length), (p'.vertices.get ⟨idx, hidx⟩).1 = x₀) (h_above : ∀ (idx_p : ℕ) (hidx_p : idx_p < p.vertices.length) (idx_p' : ℕ) (hidx_p' : idx_p' < p'.vertices.length), (p.vertices.get ⟨idx_p, hidx_p⟩).1 = x₀ → (p'.vertices.get ⟨idx_p', hidx_p'⟩).1 = x₀ → (p'.vertices.get ⟨idx_p', hidx_p'⟩).2 > (p.vertices.get ⟨idx_p, hidx_p⟩).2) (x₁ : ℤ) (hx₁ : x₁ ≥ x₀) (hx₁_p : ∃ (idx : ℕ) (hidx : idx < p.vertices.length), (p.vertices.get ⟨idx, hidx⟩).1 = x₁) (hx₁_p' : ∃ (idx : ℕ) (hidx : idx < p'.vertices.length), (p'.vertices.get ⟨idx, hidx⟩).1 = x₁) (idx_p : ℕ) (hidx_p : idx_p < p.vertices.length) (idx_p' : ℕ) (hidx_p' : idx_p' < p'.vertices.length) : (p.vertices.get ⟨idx_p, hidx_p⟩).1 = x₁ → (p'.vertices.get ⟨idx_p', hidx_p'⟩).1 = x₁ → (p'.vertices.get ⟨idx_p', hidx_p'⟩).2 > (p.vertices.get ⟨idx_p, hidx_p⟩).2

Key lemma: for two non-intersecting paths, if one is above the other at some x-coordinate, it stays above at all greater x-coordinates where both paths have vertices.

This is the "paths don't cross" property for x-coordinates. The proof uses discrete IVT: if the y-difference ever becomes ≤ 0, there must be a point where it equals 0, meaning the paths share a vertex (contradiction).

LGV Path to LatticePath Bijection

We now construct the explicit bijection between LGV paths from (a, 1) to (c, N) and our LatticePath a c type. This is needed for lgv_pathWeightSum_eq_hsymmExt.

The bijection:

• LGV Path → LatticePath: Extract east-step y-coordinates using lgvPathEastStepYCoords, then convert from ℤ (in range [1, N]) to Fin N by subtracting 1.
• LatticePath → LGV Path: Given a weakly increasing list of Fin N, construct the unique path that makes east-steps at the specified heights.

Weight preservation follows from the definition of jacobiTrudiArcWeight:

• East-step at y-coordinate y gets weight X_{y-1}
• North-steps get weight 1
• This matches LatticePath.weight = ∏ h ∈ eastStepHeights, X_h

def SymmetricFunctions.lgvYCoordsToFinN {N : ℕ} (ycoords : List ℤ) (h : ∀ y ∈ ycoords, 1 ≤ y ∧ y ≤ ↑N) : List (Fin N)

Convert east-step y-coordinates (in ℤ, range [1, N]) to Fin N elements. This is a helper for the LGV path to LatticePath bijection.

Equations

• SymmetricFunctions.lgvYCoordsToFinN ycoords h = List.pmap (fun (y : ℤ) (hy : y ∈ ycoords) => ⟨(y - 1).toNat, ⋯⟩) ycoords ⋯

theorem SymmetricFunctions.lgvYCoordsToFinN_length {N : ℕ} (ycoords : List ℤ) (h : ∀ y ∈ ycoords, 1 ≤ y ∧ y ≤ ↑N) : (lgvYCoordsToFinN ycoords h).length = ycoords.length

The length of lgvYCoordsToFinN equals the length of the input list.

theorem SymmetricFunctions.lgvYCoordsToFinN_getElem {N : ℕ} (ycoords : List ℤ) (h : ∀ y ∈ ycoords, 1 ≤ y ∧ y ≤ ↑N) (k : ℕ) (hk : k < ycoords.length) (hk' : k < (lgvYCoordsToFinN ycoords h).length := by rw [lgvYCoordsToFinN_length]; exact hk) : ↑↑(lgvYCoordsToFinN ycoords h)[k] + 1 = ycoords[k]

The k-th element of lgvYCoordsToFinN equals (ycoords[k] - 1).toNat. Since ycoords[k] ∈ [1, N], we have (lgvYCoordsToFinN ycoords h)[k].val + 1 = ycoords[k].

theorem SymmetricFunctions.lgvYCoordsToFinN_isChain {N : ℕ} (ycoords : List ℤ) (h : ∀ y ∈ ycoords, 1 ≤ y ∧ y ≤ ↑N) (hchain : List.IsChain (fun (x1 x2 : ℤ) => x1 ≤ x2) ycoords) : List.IsChain (fun (x1 x2 : Fin N) => x1 ≤ x2) (lgvYCoordsToFinN ycoords h)

The converted list preserves the chain property (weakly increasing).

theorem SymmetricFunctions.lgvYCoordsToFinN_injective {N : ℕ} (l₁ l₂ : List ℤ) (h₁ : ∀ y ∈ l₁, 1 ≤ y ∧ y ≤ ↑N) (h₂ : ∀ y ∈ l₂, 1 ≤ y ∧ y ≤ ↑N) (heq : lgvYCoordsToFinN l₁ h₁ = lgvYCoordsToFinN l₂ h₂) : l₁ = l₂

The conversion lgvYCoordsToFinN is injective when both lists have elements in [1, N].

The proof uses the fact that y ↦ (y - 1).toNat is injective on [1, N]: if (y₁ - 1).toNat = (y₂ - 1).toNat and both y₁, y₂ ∈ [1, N], then y₁ = y₂.

Proof sketch:

1. The lengths are equal (pmap preserves length)
2. At each position i, the Fin N values are equal (from heq)
3. Since y ↦ (y - 1).toNat is injective on [1, N], the original values are equal

theorem SymmetricFunctions.lgvYCoordsToFinN_map_val_add_one_eq {N : ℕ} (heights : List (Fin N)) {l : List ℤ} (heq : l = List.map (fun (h : Fin N) => ↑↑h + 1) heights) (h : ∀ y ∈ l, 1 ≤ y ∧ y ≤ ↑N) : lgvYCoordsToFinN l h = heights

Helper: lgvYCoordsToFinN inverts the map (fun h => h.val + 1). If l = heights.map (fun h => h.val + 1), then lgvYCoordsToFinN l h = heights.

noncomputable def SymmetricFunctions.lgvPathToLatticePath {N : ℕ} (a c : ℤ) (p : LGV.integerLattice.Path) (hstart : p.start = (a, 1)) (hfinish : p.finish = (c, ↑N)) : LatticePath a c

Convert an LGV path from (a, 1) to (c, N) to a LatticePath. This extracts the east-step heights and converts them to Fin N.

Equations

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

Injectivity of lgvPathToLatticePath

The key lemma for the bijection is that lgvPathToLatticePath is injective. This follows from the fact that paths in the integer lattice from the same start to the same end are uniquely determined by their east-step y-coordinates.

theorem SymmetricFunctions.lgvPath_vertices_eq_of_eastStepYCoords_eq (p₁ p₂ : LGV.integerLattice.Path) (hstart : p₁.start = p₂.start) (hfinish : p₁.finish = p₂.finish) (hcoords : lgvPathEastStepYCoords p₁.vertices = lgvPathEastStepYCoords p₂.vertices) : p₁.vertices = p₂.vertices

Key uniqueness lemma: Paths in the integer lattice from the same start to the same end with the same east-step y-coordinates must have the same vertices.

This is the fundamental lemma for proving injectivity of lgvPathToLatticePath.

Proof idea: At each vertex (x, y), the next step is uniquely determined:

• If y appears in the remaining east-step y-coordinates, we go east
• Otherwise, we go north Since both paths have the same start and the same east-step y-coordinates, they must make the same choices at each step, hence have the same vertices.

The proof proceeds by strong induction on the total number of steps remaining. At each step, we show the next vertex is determined by whether the current y-coordinate matches the next east-step height.

theorem SymmetricFunctions.lgvPathToLatticePath_injective {N : ℕ} (a c : ℤ) (p₁ p₂ : LGV.integerLattice.Path) (hstart₁ : p₁.start = (a, 1)) (hfinish₁ : p₁.finish = (c, ↑N)) (hstart₂ : p₂.start = (a, 1)) (hfinish₂ : p₂.finish = (c, ↑N)) (heq : lgvPathToLatticePath a c p₁ hstart₁ hfinish₁ = lgvPathToLatticePath a c p₂ hstart₂ hfinish₂) : p₁ = p₂

Corollary: lgvPathToLatticePath is injective on paths with the same start and end.

If two LGV paths from (a, 1) to (c, N) map to the same LatticePath, then they have the same vertices (and hence are equal as paths).

LatticePath to LGV Path Bijection: Inverse Direction

We construct the inverse of lgvPathToLatticePath, converting a LatticePath back to an LGV SimpleDigraph.Path. This completes the bidirectional conversion between the two lattice path representations.

Representation equivalence:

• LGV.LatticePath (in LGV1.lean): List LatticeStep (sequence of east/north steps)
• SymmetricFunctions.LatticePath (here): eastStepHeights : List (Fin N) with constraints

The bijection works because:

1. A path from (a, 1) to (c, N) is uniquely determined by its east-step heights
2. East-step heights form a weakly increasing sequence of length (c - a).toNat
3. This is exactly the data in a LatticePath

Construction algorithm: Given eastStepHeights = [h₀, h₁, ...], construct vertices by:

1. Start at (a, 1)
2. For each height hᵢ (which represents y-coordinate hᵢ.val + 1):
   • Go north until y = hᵢ.val + 1
   • Go east
3. Finally go north until y = N

theorem SymmetricFunctions.lgvPathToLatticePath_weight_eq {N : ℕ} {R : Type u_1} [CommRing R] (a c : ℤ) (p : LGV.integerLattice.Path) (hstart : p.start = (a, 1)) (hfinish : p.finish = (c, ↑N)) : LGV.pathWeight jacobiTrudiArcWeight p = (lgvPathToLatticePath a c p hstart hfinish).weight

theorem SymmetricFunctions.lgv_pathWeightSum_eq_latticePathSum {N : ℕ} {R : Type u_1} [CommRing R] (a c : ℤ) (h : 0 ≤ c - a) (hN : 0 < N) : LGV.pathWeightSum LGV.integerLattice_pathFinite jacobiTrudiArcWeight (a, 1) (c, ↑N) = ∑ lp : LatticePath a c, lp.weight

The LGV path weight sum equals the LatticePath weight sum. This is proved using lgvPathToLatticePath as a bijection.

The proof establishes that lgvPathToLatticePath is a bijection by showing:

1. Injectivity: paths with the same east-step heights are equal
2. Surjectivity: every LatticePath corresponds to an LGV path
3. Weight preservation: lgvPathToLatticePath_weight_eq

The bijection works because:

• A path from (a, 1) to (c, N) is uniquely determined by its east-step heights
• East-step heights form a weakly increasing sequence of length (c - a)
• This is exactly the data in a LatticePath

theorem SymmetricFunctions.lgv_pathWeightSum_eq_hsymmExt {N : ℕ} {R : Type u_1} [CommRing R] (a c : ℤ) (hN : 0 < N) : LGV.pathWeightSum LGV.integerLattice_pathFinite jacobiTrudiArcWeight (a, 1) (c, ↑N) = hsymmExt (c - a)

Key infrastructure lemma: The LGV path weight sum from (a, 1) to (c, N) with jacobiTrudiArcWeight equals hsymmExt(c - a).

This connects the LGV framework (using SimpleDigraph.Path in integerLattice) to our LatticePath representation (using eastStepHeights).

The proof uses lgv_pathWeightSum_eq_latticePathSum to establish a weight-preserving bijection between LGV paths and LatticePaths, then applies pathWeightSum_eq_hsymm.

This is a key infrastructure lemma needed for det_jacobiTrudiMatrixH_eq_nipatSum.

theorem SymmetricFunctions.jacobiTrudiMatrixH_eq_pathWeightMatrix_transpose {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) : jacobiTrudiMatrixH lam mu = (LGV.pathWeightMatrix LGV.integerLattice_pathFinite jacobiTrudiArcWeight (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)).transpose

The Jacobi-Trudi matrix is the transpose of the LGV path weight matrix.

This is a key step in the proof of det_jacobiTrudiMatrixH_eq_nipatSum. The (i,j) entry of jacobiTrudiMatrixH is h_{λᵢ - μⱼ - i + j}, which equals the path weight sum from source A_j to target B_i. This is exactly the (j,i) entry of the path weight matrix, hence the transpose relationship.

The proof uses lgv_pathWeightSum_eq_hsymmExt to connect the LGV path weight sum to hsymmExt, which is how jacobiTrudiMatrixH entries are defined.

theorem SymmetricFunctions.det_jacobiTrudiMatrixH_eq_det_pathWeightMatrix {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) : (jacobiTrudiMatrixH lam mu).det = (LGV.pathWeightMatrix LGV.integerLattice_pathFinite jacobiTrudiArcWeight (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)).det

Corollary: The determinant of jacobiTrudiMatrixH equals the determinant of the path weight matrix. This follows from det(Mᵀ) = det(M).

LGV-Nipat Bijection: PathTuple to Nipat Conversion

The following definitions and lemmas establish the conversion from LGV PathTuples to our Nipat type. This is used to prove lgv_nipatWeightSum_eq_nipatSum.

theorem SymmetricFunctions.lgv_nipatWeightSum_eq_nipatSum {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : LGV.nipatWeightSum LGV.integerLattice_pathFinite jacobiTrudiArcWeight (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam) (Equiv.refl (Fin N)) = ∑ np : Nipat lam mu hlam hmu hcontained, np.weight

The LGV nipat weight sum equals our Nipat weight sum.

This connects the two representations of non-intersecting path tuples:

• LGV: PathTuple with isNonIntersecting (no shared vertices)
• Ours: Nipat with colStrictPaths (column-strictness)

The bijection works as follows:

• An LGV path from (a, 1) to (c, N) is encoded by its east-step heights
• This is exactly our LatticePath type
• Non-intersection of LGV paths ↔ column-strictness of east-step heights

The proof uses pathTupleToNipat to convert LGV nipats to our Nipat type, with weight preservation via pathTupleToNipat_weight.

theorem SymmetricFunctions.det_jacobiTrudiMatrixH_eq_nipatSum {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : (jacobiTrudiMatrixH lam mu).det = ∑ np : Nipat lam mu hlam hmu hcontained, np.weight

Key lemma: The Jacobi-Trudi matrix determinant equals the sum of nipat weights.

This is the core connection between the LGV lemma and the Jacobi-Trudi formula. The proof follows from:

1. jacobiTrudiMatrixH entries are h_{λᵢ - μⱼ - i + j} = pathWeightSum from A_j to B_i
2. By LGV nonpermutable lemma, det(pathWeightMatrix) = sum over nipats
3. The Nipat type captures exactly the non-intersecting path tuples

theorem SymmetricFunctions.jacobiTrudi_h {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : skewSchur { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ } = (jacobiTrudiMatrixH lam mu).det

First Jacobi-Trudi formula (Theorem thm.sf.jt-h) Label: thm.sf.jt-h

s_{λ/μ} = det((h_{λᵢ - μⱼ - i + j})_{1 ≤ i,j ≤ M})

The proof uses the Lindström-Gessel-Viennot lemma with appropriate source and target vertices in the integer lattice ℤ².

Proof Strategy

Step 1: Set up the LGV framework Define source vertices Aᵢ = (μᵢ - i, 1) and target vertices Bⱼ = (λⱼ - j, N) in ℤ². The path weight matrix M_{i,j} = ∑_{p : Aᵢ → Bⱼ} w(p) where w(p) is the product of x_h for each east-step at height h.

Step 2: Identify M with the Jacobi-Trudi matrix By pathWeightSum_eq_hsymm, M_{i,j} = h_{λⱼ - μᵢ - j + i} = h_{λⱼ - μᵢ - (j - i)}. Note: The textbook uses 1-indexed notation; our Lean formalization uses 0-indexed. The matrix entry (i,j) is h_{λᵢ - μⱼ - i + j} in the textbook convention.

Step 3: Apply the LGV lemma By lgv_nonpermutable (Corollary cor.lgv.kpaths.wt-np), since the source and target vertices satisfy the sorting conditions (x-decreasing, y-increasing), we have: det(M) = ∑_{nipats from 𝐀 to 𝐁} w(nipat) where the sum is only over non-intersecting path tuples (nipats).

Step 4: Establish the nipat-SSYT bijection By nipat_ssyt_bijection, there is a weight-preserving bijection between nipats from 𝐀 to 𝐁 and SSYT of skew shape λ/μ:

• The nipat (p₁, ..., pₖ) maps to the tableau T where row i contains the heights of east-steps in path pᵢ (in weakly increasing order).
• Non-intersection of paths ensures column-strictness of the tableau.
• The weight w(nipat) = ∏ᵢ w(pᵢ) equals the monomial x^T.

Step 5: Conclude det(M) = ∑{nipats} w(nipat) = ∑{SSYT T of shape λ/μ} x^T = s_{λ/μ}

Key Lemmas Required

1. pathWeightSum_eq_hsymm: Path weight sums equal h_n (Observation 1)
2. nipat_ssyt_bijection: Bijection between nipats and SSYT (Observation 2)
3. lgv_nonpermutable: LGV lemma for sorted vertices (from LGV2.lean)
4. Sorting conditions on A and B vertices (follows from partition monotonicity)

References

• TeX source: AlgebraicCombinatorics/tex/SymmetricFunctions/PieriJacobiTrudi.tex
• LGV infrastructure: AlgebraicCombinatorics/Determinants/LGV2.lean

Special Cases

When μ = 0 (the empty partition), we get formulas for non-skew Schur polynomials.

theorem SymmetricFunctions.schur_eq_skewSchur_zero {N : ℕ} {R : Type u_1} [CommRing R] (lam : NPartition N) : schur lam = skewSchur { outer := lam, inner := 0, contained := ⋯ }

The Schur polynomial for a partition λ equals the skew Schur polynomial for λ/0. This follows from the fact that a skew partition λ/0 is just the partition λ, so SSYT(λ) and SkewSSYT(λ/0) are in natural bijection.

theorem SymmetricFunctions.jacobiTrudi_h_nonSkew {N : ℕ} {R : Type u_1} [CommRing R] (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) : schur { parts := lam, weaklyDecreasing := hlam } = (jacobiTrudiMatrixH lam fun (x : Fin N) => 0).det

Jacobi-Trudi for non-skew Schur polynomials: s_λ = det((h_{λᵢ - i + j})_{1 ≤ i,j ≤ N})

Symmetry of Skew Schur Polynomials via Jacobi-Trudi

The Jacobi-Trudi formula provides an alternative proof that skew Schur polynomials are symmetric, without relying on the Bender-Knuth involution.

Key insight: The Jacobi-Trudi matrix has entries h_{λᵢ - μⱼ - i + j}, where h_n is the n-th complete homogeneous symmetric polynomial. Since each h_n is symmetric and the determinant is a polynomial in the entries, the determinant is also symmetric.

This provides a sorry-free proof of symmetry for skew Schur polynomials, complementing the Bender-Knuth approach in SchurBasics.lean (which is also sorry-free).

theorem SymmetricFunctions.det_isSymmetric_of_entries_symmetric {N : ℕ} {R : Type u_1} [CommRing R] (M : Matrix (Fin N) (Fin N) (MvPolynomial (Fin N) R)) (h : ∀ (i j : Fin N), (M i j).IsSymmetric) : M.det.IsSymmetric

If all entries of a matrix are symmetric polynomials, then the determinant is symmetric. This is because rename σ commutes with det, and rename σ fixes each symmetric entry.

theorem SymmetricFunctions.jacobiTrudiMatrixH_entries_isSymmetric {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (i j : Fin N) : (jacobiTrudiMatrixH lam mu i j).IsSymmetric

The Jacobi-Trudi matrix (h-version) has symmetric entries.

theorem SymmetricFunctions.jacobiTrudiMatrixH_det_isSymmetric {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) : (jacobiTrudiMatrixH lam mu).det.IsSymmetric

The determinant of the Jacobi-Trudi matrix (h-version) is symmetric.

theorem SymmetricFunctions.skewSchur_isSymmetric_jacobiTrudi {N : ℕ} {R : Type u_1} [CommRing R] (lam mu : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) (hmu : ∀ (i j : Fin N), i ≤ j → mu j ≤ mu i) (hcontained : ∀ (i : Fin N), mu i ≤ lam i) : (skewSchur { outer := { parts := lam, weaklyDecreasing := hlam }, inner := { parts := mu, weaklyDecreasing := hmu }, contained := ⋯ }).IsSymmetric

Skew Schur polynomials are symmetric (via Jacobi-Trudi).

This provides a sorry-free proof of symmetry using the Jacobi-Trudi formula, complementing the Bender-Knuth approach in SchurBasics.lean.

The proof works by:

1. Using jacobiTrudi_h to express skewSchur as det(jacobiTrudiMatrixH)
2. Showing each entry h_{λᵢ - μⱼ - i + j} is symmetric (via hsymmExt_isSymmetric)
3. Concluding the determinant is symmetric (via det_isSymmetric_of_entries_symmetric)

Theorem \ref{thm.sf.skew-schur-symm} in the source.

theorem SymmetricFunctions.schur_isSymmetric_jacobiTrudi {N : ℕ} {R : Type u_1} [CommRing R] (lam : Fin N → ℕ) (hlam : ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i) : (schur { parts := lam, weaklyDecreasing := hlam }).IsSymmetric

Schur polynomials are symmetric (via Jacobi-Trudi).

This is a corollary of skewSchur_isSymmetric_jacobiTrudi with μ = 0.

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