# Semistandard Young tableaux #

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 a semistandard Young tableau 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 #

• SemistandardYoungTableau (μ : YoungDiagram): semistandard Young tableaux of shape μ. There is a coe instance such that T i j is value of the (i, j) entry of the semistandard Young tableau T.
• Ssyt.highestWeight (μ : YoungDiagram): the semistandard Young tableau whose ith row consists entirely of is, for each i.

## Tags #

Semistandard Young tableau

## References #

A semistandard Young tableau 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, a semistandard Young tableau is represented as an unrestricted function ℕ → ℕ → ℕ that, for reasons of extensionality, is required to vanish outside μ.

• entry :

entry i j is value of the (i, j) entry of the SSYT μ.

• row_weak' : ∀ {i j1 j2 : }, j1 < j2(i, j2) μself.entry i j1 self.entry i j2

The entries in each row are weakly increasing (left to right).

• col_strict' : ∀ {i1 i2 j : }, i1 < i2(i2, j) μself.entry i1 j < self.entry i2 j

The entries in each column are strictly increasing (top to bottom).

• zeros' : ∀ {i j : }, (i, j)μself.entry i j = 0

entry is required to be zero for all pairs (i, j) ∉ μ.

Instances For
theorem SemistandardYoungTableau.row_weak' {μ : YoungDiagram} (self : ) {i : } {j1 : } {j2 : } :
j1 < j2(i, j2) μself.entry i j1 self.entry i j2

The entries in each row are weakly increasing (left to right).

theorem SemistandardYoungTableau.col_strict' {μ : YoungDiagram} (self : ) {i1 : } {i2 : } {j : } :
i1 < i2(i2, j) μself.entry i1 j < self.entry i2 j

The entries in each column are strictly increasing (top to bottom).

theorem SemistandardYoungTableau.zeros' {μ : YoungDiagram} (self : ) {i : } {j : } :
(i, j)μself.entry i j = 0

entry is required to be zero for all pairs (i, j) ∉ μ.

Equations
• SemistandardYoungTableau.instFunLike = { coe := SemistandardYoungTableau.entry, coe_injective' := }

Helper instance for when there's too many metavariables to apply CoeFun.coe directly.

Equations
• SemistandardYoungTableau.instCoeFunForallNatForall = inferInstance
@[simp]
theorem SemistandardYoungTableau.to_fun_eq_coe {μ : YoungDiagram} {T : } :
T.entry = T
theorem SemistandardYoungTableau.ext {μ : YoungDiagram} {T : } {T' : } (h : ∀ (i j : ), T i j = T' i j) :
T = T'
def SemistandardYoungTableau.copy {μ : YoungDiagram} (T : ) (entry' : ) (h : entry' = T) :

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

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

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

Equations
• = { entry := fun (i j : ) => if (i, j) μ then i else 0, row_weak' := , col_strict' := , zeros' := }
Instances For
@[simp]
theorem SemistandardYoungTableau.highestWeight_apply {μ : YoungDiagram} {i : } {j : } :
= if (i, j) μ then i else 0
Equations
• SemistandardYoungTableau.instInhabited = { default := }