mathlib3 documentation

combinatorics.young.semistandard_tableau

Semistandard Young tableaux #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A semistandard Young tableau is a filling of a Young diagram by natural numbers, such that the entries are weakly increasing left-to-right along rows (i.e. for fixed i), and strictly-increasing top-to-bottom along columns (i.e. for fixed j).

An example of an SSYT of shape μ = [4, 2, 1] is:

0 0 0 2
1 1
2

We represent an SSYT as a function ℕ → ℕ → ℕ, which is required to be zero for all pairs (i, j) ∉ μ and to satisfy the row-weak and column-strict conditions on μ.

Main definitions #

Tags #

Semistandard Young tableau

References #

https://en.wikipedia.org/wiki/Young_tableau

structure ssyt (μ : young_diagram) :

A semistandard Young tableau (SSYT) is a filling of the cells of a Young diagram by natural numbers, such that the entries in each row are weakly increasing (left to right), and the entries in each column are strictly increasing (top to bottom).

Here, an SSYT is represented as an unrestricted function ℕ → ℕ → ℕ that, for reasons of extensionality, is required to vanish outside μ.

Instances for ssyt
@[protected, instance]
def ssyt.fun_like {μ : young_diagram} :
fun_like (ssyt μ) (λ (_x : ), )
Equations
@[protected, instance]
def ssyt.has_coe_to_fun {μ : young_diagram} :
has_coe_to_fun (ssyt μ) (λ (_x : ssyt μ), )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem ssyt.to_fun_eq_coe {μ : young_diagram} {T : ssyt μ} :
@[ext]
theorem ssyt.ext {μ : young_diagram} {T T' : ssyt μ} (h : (i j : ), T i j = T' i j) :
T = T'
@[protected]
def ssyt.copy {μ : young_diagram} (T : ssyt μ) (entry' : ) (h : entry' = T) :
ssyt μ

Copy of an ssyt μ with a new entry equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem ssyt.coe_copy {μ : young_diagram} (T : ssyt μ) (entry' : ) (h : entry' = T) :
(T.copy entry' h) = entry'
theorem ssyt.copy_eq {μ : young_diagram} (T : ssyt μ) (entry' : ) (h : entry' = T) :
T.copy entry' h = T
theorem ssyt.row_weak {μ : young_diagram} (T : ssyt μ) {i j1 j2 : } (hj : j1 < j2) (hcell : (i, j2) μ) :
T i j1 T i j2
theorem ssyt.col_strict {μ : young_diagram} (T : ssyt μ) {i1 i2 j : } (hi : i1 < i2) (hcell : (i2, j) μ) :
T i1 j < T i2 j
theorem ssyt.zeros {μ : young_diagram} (T : ssyt μ) {i j : } (not_cell : (i, j) μ) :
T i j = 0
theorem ssyt.row_weak_of_le {μ : young_diagram} (T : ssyt μ) {i j1 j2 : } (hj : j1 j2) (cell : (i, j2) μ) :
T i j1 T i j2
theorem ssyt.col_weak {μ : young_diagram} (T : ssyt μ) {i1 i2 j : } (hi : i1 i2) (cell : (i2, j) μ) :
T i1 j T i2 j

The "highest weight" SSYT of a given shape is has all i's in row i, for each i.

Equations
@[simp]
theorem ssyt.highest_weight_apply {μ : young_diagram} {i j : } :
(ssyt.highest_weight μ) i j = ite ((i, j) μ) i 0
@[protected, instance]
Equations