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

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

structure SemistandardYoungTableau (μ : YoungDiagram) : Type

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) ∉ μ.

theorem SemistandardYoungTableau.row_weak' {μ : YoungDiagram} (self : SemistandardYoungTableau μ) {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 : SemistandardYoungTableau μ) {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 : SemistandardYoungTableau μ) {i : ℕ} {j : ℕ} : (i, j) ∉ μ → self.entry i j = 0

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

instance SemistandardYoungTableau.instFunLike {μ : YoungDiagram} : FunLike (SemistandardYoungTableau μ) ℕ (ℕ → ℕ)

Equations

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

instance SemistandardYoungTableau.instCoeFunForallNatForall {μ : YoungDiagram} : CoeFun (SemistandardYoungTableau μ) fun (x : SemistandardYoungTableau μ) => ℕ → ℕ → ℕ

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 : SemistandardYoungTableau μ} : T.entry = ⇑T

theorem SemistandardYoungTableau.ext {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {T' : SemistandardYoungTableau μ} (h : ∀ (i j : ℕ), T i j = T' i j) : T = T'

def SemistandardYoungTableau.copy {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = ⇑T) : SemistandardYoungTableau μ

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' := ⋯ }

@[simp]

theorem SemistandardYoungTableau.coe_copy {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = ⇑T) : ⇑(T.copy entry' h) = entry'

theorem SemistandardYoungTableau.copy_eq {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = ⇑T) : T.copy entry' h = T

theorem SemistandardYoungTableau.row_weak {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i : ℕ} {j1 : ℕ} {j2 : ℕ} (hj : j1 < j2) (hcell : (i, j2) ∈ μ) : T i j1 ≤ T i j2

theorem SemistandardYoungTableau.col_strict {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 : ℕ} {i2 : ℕ} {j : ℕ} (hi : i1 < i2) (hcell : (i2, j) ∈ μ) : T i1 j < T i2 j

theorem SemistandardYoungTableau.zeros {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i : ℕ} {j : ℕ} (not_cell : (i, j) ∉ μ) : T i j = 0

theorem SemistandardYoungTableau.row_weak_of_le {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i : ℕ} {j1 : ℕ} {j2 : ℕ} (hj : j1 ≤ j2) (cell : (i, j2) ∈ μ) : T i j1 ≤ T i j2

theorem SemistandardYoungTableau.col_weak {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 : ℕ} {i2 : ℕ} {j : ℕ} (hi : i1 ≤ i2) (cell : (i2, j) ∈ μ) : T i1 j ≤ T i2 j

def SemistandardYoungTableau.highestWeight (μ : YoungDiagram) : SemistandardYoungTableau μ

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

Equations

• SemistandardYoungTableau.highestWeight μ = { entry := fun (i j : ℕ) => if (i, j) ∈ μ then i else 0, row_weak' := ⋯, col_strict' := ⋯, zeros' := ⋯ }

@[simp]

theorem SemistandardYoungTableau.highestWeight_apply {μ : YoungDiagram} {i : ℕ} {j : ℕ} : (SemistandardYoungTableau.highestWeight μ) i j = if (i, j) ∈ μ then i else 0

instance SemistandardYoungTableau.instInhabited {μ : YoungDiagram} : Inhabited (SemistandardYoungTableau μ)

Equations

• SemistandardYoungTableau.instInhabited = { default := SemistandardYoungTableau.highestWeight μ }