Kostka numbers

The content of a semistandard Young tableau records how often each natural number is used as an entry, and the Kostka number K_{μ w} counts the semistandard tableaux of shape μ and content w. This file defines both, proves that the tableaux of a given content are finite, and establishes the two facts that make the Kostka numbers a triangular array for the dominance order: the tableau of shape μ whose i-th row consists of is is the only one of content μ.rowLen (so K_{μ μ} = 1), and a tableau of shape μ and content w forces every partial sum ∑_{i < k} w i to be at most the corresponding partial sum of the row lengths of μ (so, for partitions, K_{μ ν} = 0 unless μ dominates ν).

The mechanism behind both is a single observation, SemistandardYoungTableau.le_entry: the entries of a semistandard tableau strictly increase down each column, so the entry in row i is at least i, and therefore the cells carrying an entry smaller than k all lie in the first k rows.

Mathlib's SemistandardYoungTableau fills the cells with natural numbers starting at 0, so the alphabet here is 0, 1, 2, … rather than the classical 1, 2, 3, … and the content of the highest-weight tableau SemistandardYoungTableau.highestWeight μ is μ.rowLen on the nose.

Main definitions

• SemistandardYoungTableau.content: the content (or weight) of a semistandard Young tableau, content T i being the number of cells filled with i.
• TauCeti.BoundedSSYT: the semistandard Young tableaux of a given shape whose entries lie below a given bound, that is, those written in a finite alphabet.
• TauCeti.diagramKostkaNumber: the number of semistandard Young tableaux of a given shape and content.
• TauCeti.kostkaNumber: the Kostka number of two partitions of the same natural number, the shape and the content being read off their Young diagrams.

Main results

• SemistandardYoungTableau.sum_content_le_sum_take_rowLens: the partial sums of the content of a tableau of shape μ are bounded by those of the row lengths of μ.
• SemistandardYoungTableau.eq_highestWeight_of_content_eq_rowLen: a tableau of shape μ and content μ.rowLen is the highest-weight tableau.
• SemistandardYoungTableau.finite_content_eq: the tableaux of a fixed shape and content are finite, so the Kostka number counts them faithfully.
• TauCeti.finite_boundedSSYT: likewise the tableaux of a fixed shape written in a finite alphabet, TauCeti.BoundedSSYT, are finite.
• TauCeti.BoundedSSYT.isEmpty_of_lt_colLen: a shape taller than its alphabet admits no tableau.
• TauCeti.kostkaNumber_self: K_{μ μ} = 1.
• TauCeti.kostkaNumber_eq_zero_of_not_dominates: K_{μ ν} = 0 unless μ dominates ν.

References

• W. Fulton, Young Tableaux, Section 2.2.
• Schur--Weyl roadmap, Layer 1.

noncomputable def SemistandardYoungTableau.content {μ : YoungDiagram} (T : SemistandardYoungTableau μ) : ℕ →₀ ℕ

The content, or weight, of a semistandard Young tableau: the multiset of its entries, read as a finitely supported multiplicity function, so content T i is the number of cells of the shape whose entry is i.

Equations

• T.content = Multiset.toFinsupp (Multiset.map (fun (c : ℕ × ℕ) => T c.1 c.2) μ.cells.val)

theorem SemistandardYoungTableau.content_apply {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i : ℕ) : T.content i = {c ∈ μ.cells | T c.1 c.2 = i}.card

The content of a tableau counts the cells of its shape carrying a given entry.

@[simp]

theorem SemistandardYoungTableau.support_content {μ : YoungDiagram} (T : SemistandardYoungTableau μ) : T.content.support = Finset.image (fun (c : ℕ × ℕ) => T c.1 c.2) μ.cells

The support of the content of a tableau is the set of entries it uses.

theorem SemistandardYoungTableau.le_entry {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j : ℕ} (h : (i, j) ∈ μ) : i ≤ T i j

The entries of a semistandard Young tableau increase strictly down a column, so the entry in row i is at least i.

theorem SemistandardYoungTableau.filter_entry_lt_subset_filter_fst_lt {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (k : ℕ) : {c ∈ μ.cells | T c.1 c.2 < k} ⊆ {c ∈ μ.cells | c.1 < k}

The cells carrying an entry smaller than k all lie in the first k rows.

theorem SemistandardYoungTableau.sum_content_eq_card_filter {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (k : ℕ) : ∑ i ∈ Finset.range k, T.content i = {c ∈ μ.cells | T c.1 c.2 < k}.card

The first k values of the content of a tableau count the cells carrying an entry smaller than k.

theorem SemistandardYoungTableau.sum_content_eq_card {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {N : ℕ} (hN : ∀ c ∈ μ.cells, T c.1 c.2 < N) : ∑ i ∈ Finset.range N, T.content i = μ.card

The content of a tableau of shape μ is a composition of the number of cells of μ, once the range of summation covers all the entries.

theorem SemistandardYoungTableau.sum_content_le_sum_take_rowLens {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (k : ℕ) : ∑ i ∈ Finset.range k, T.content i ≤ (List.take k μ.rowLens).sum

Dominance bound for the content of a tableau: the partial sums of the content of a semistandard tableau of shape μ never exceed the partial sums of the row lengths of μ.

@[simp]

theorem SemistandardYoungTableau.content_highestWeight (μ : YoungDiagram) : ⇑(highestWeight μ).content = μ.rowLen

The highest-weight tableau, whose i-th row consists of is, has content the row lengths of its shape.

theorem SemistandardYoungTableau.eq_highestWeight_of_content_eq_rowLen {μ : YoungDiagram} {T : SemistandardYoungTableau μ} (h : ⇑T.content = μ.rowLen) : T = highestWeight μ

Uniqueness of the highest-weight tableau: a semistandard tableau of shape μ whose content is the row lengths of μ has an i in every cell of row i, so it is SemistandardYoungTableau.highestWeight μ.

instance SemistandardYoungTableau.finite_content_eq (μ : YoungDiagram) (w : ℕ → ℕ) : Finite { T : SemistandardYoungTableau μ // ⇑T.content = w }

The semistandard tableaux of a fixed shape and content are finite.

@[reducible, inline]

abbrev TauCeti.BoundedSSYT (n : ℕ) (μ : YoungDiagram) : Type

The semistandard Young tableaux of shape μ written in the alphabet {0, …, n - 1}, that is, those all of whose entries are smaller than n. Mathlib's SemistandardYoungTableau μ allows arbitrary natural-number entries and is infinite for a nonempty μ, so bounding the alphabet is what makes the tableaux of a fixed shape finitely many.

Equations

• TauCeti.BoundedSSYT n μ = { T : SemistandardYoungTableau μ // ∀ (i c : ℕ), (i, c) ∈ μ → T i c < n }

theorem TauCeti.BoundedSSYT.entry_lt {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT n μ) {i c : ℕ} (h : (i, c) ∈ μ) : ↑T i c < n

The entries of a tableau written in the alphabet {0, …, n - 1} all use letters of that alphabet.

theorem TauCeti.BoundedSSYT.isEmpty_of_lt_colLen {n : ℕ} {μ : YoungDiagram} (h : n < μ.colLen 0) : IsEmpty (BoundedSSYT n μ)

A shape taller than its alphabet admits no tableau: entries increase strictly down a column, so a column of more than n cells cannot be filled from an n-letter alphabet.

@[instance_reducible]

instance TauCeti.BoundedSSYT.instUniqueBotYoungDiagram (n : ℕ) : Unique (BoundedSSYT n ⊥)

The empty shape has a unique tableau, the empty one.

Equations

• TauCeti.BoundedSSYT.instUniqueBotYoungDiagram n = { default := ⟨SemistandardYoungTableau.highestWeight ⊥, ⋯⟩, uniq := ⋯ }

instance TauCeti.finite_boundedSSYT (n : ℕ) (μ : YoungDiagram) : Finite (BoundedSSYT n μ)

Bounded semistandard tableaux of a fixed shape are finitely many: such a tableau is determined by its restriction to the finitely many cells of μ, where it takes one of n values. Mathlib's SemistandardYoungTableau μ allows unbounded entries and is infinite for a nonempty μ, so the bound is what makes the count finite. No relation between n and the number of rows of μ is needed: for a shape taller than n the type is empty, columns being strict.

@[instance_reducible]

noncomputable instance TauCeti.instFintypeBoundedSSYT (n : ℕ) (μ : YoungDiagram) : Fintype (BoundedSSYT n μ)

Equations

• TauCeti.instFintypeBoundedSSYT n μ = Fintype.ofFinite (TauCeti.BoundedSSYT n μ)

noncomputable def TauCeti.diagramKostkaNumber (μ : YoungDiagram) (w : ℕ → ℕ) : ℕ

The Kostka number K_{μ w} of a shape and a weight function: the number of semistandard Young tableaux of shape μ whose content is w.

Equations

• TauCeti.diagramKostkaNumber μ w = Nat.card { T : SemistandardYoungTableau μ // ⇑T.content = w }

theorem TauCeti.diagramKostkaNumber_def (μ : YoungDiagram) (w : ℕ → ℕ) : diagramKostkaNumber μ w = Nat.card { T : SemistandardYoungTableau μ // ⇑T.content = w }

The Kostka number of a shape and a weight function counts the semistandard tableaux of that shape whose content is that weight.

theorem TauCeti.diagramKostkaNumber_ne_zero_iff {μ : YoungDiagram} {w : ℕ → ℕ} : diagramKostkaNumber μ w ≠ 0 ↔ ∃ (T : SemistandardYoungTableau μ), ⇑T.content = w

A Kostka number is nonzero exactly when a tableau of the prescribed shape and content exists.

@[simp]

theorem TauCeti.diagramKostkaNumber_rowLen (μ : YoungDiagram) : diagramKostkaNumber μ μ.rowLen = 1

The diagonal Kostka number is 1: the highest-weight tableau is the only semistandard tableau of shape μ whose content is the row lengths of μ.

theorem TauCeti.sum_le_sum_take_rowLens_of_diagramKostkaNumber_ne_zero {μ : YoungDiagram} {w : ℕ → ℕ} (h : diagramKostkaNumber μ w ≠ 0) (k : ℕ) : ∑ i ∈ Finset.range k, w i ≤ (List.take k μ.rowLens).sum

Partial-sum bound for a nonzero Kostka number: if K_{μ w} ≠ 0 then every partial sum of w is bounded by the corresponding partial sum of the row lengths of μ. For partitions this becomes the dominance statement TauCeti.dominates_of_kostkaNumber_ne_zero.

noncomputable def TauCeti.kostkaNumber {n : ℕ} (μ ν : n.Partition) : ℕ

The Kostka number K_{μ ν} of two partitions of the same natural number: the number of semistandard tableaux of the shape of μ whose content is the row lengths of the diagram of ν, that is (by TauCeti.rowLen_diagramOf), the tableaux using the entry i exactly as often as the i-th largest part of ν prescribes.

Equations

• TauCeti.kostkaNumber μ ν = TauCeti.diagramKostkaNumber (TauCeti.diagramOf μ) (TauCeti.diagramOf ν).rowLen

theorem TauCeti.kostkaNumber_def {n : ℕ} (μ ν : n.Partition) : kostkaNumber μ ν = diagramKostkaNumber (diagramOf μ) (diagramOf ν).rowLen

The Kostka number of two partitions is the Kostka number of the diagram of μ together with the row lengths of the diagram of ν.

theorem TauCeti.kostkaNumber_ne_zero_iff {n : ℕ} {μ ν : n.Partition} : kostkaNumber μ ν ≠ 0 ↔ ∃ (T : SemistandardYoungTableau (diagramOf μ)), ⇑T.content = (diagramOf ν).rowLen

A Kostka number of two partitions is nonzero exactly when a tableau of shape μ and content ν exists.

@[simp]

theorem TauCeti.kostkaNumber_self {n : ℕ} (μ : n.Partition) : kostkaNumber μ μ = 1

A partition contributes exactly one tableau to its own Kostka number.

theorem TauCeti.dominates_of_kostkaNumber_ne_zero {n : ℕ} {μ ν : n.Partition} (h : kostkaNumber μ ν ≠ 0) : Dominates μ ν

The Kostka numbers are triangular for the dominance order: K_{μ ν} ≠ 0 forces μ to dominate ν.

theorem TauCeti.kostkaNumber_eq_zero_of_not_dominates {n : ℕ} {μ ν : n.Partition} (h : ¬Dominates μ ν) : kostkaNumber μ ν = 0

The Kostka numbers vanish off the dominance order: there is no semistandard tableau of shape μ and content ν unless μ dominates ν.