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 #

ssyt (μ : young_diagram) : semistandard Young tableaux of shape μ. There is a has_coe_to_fun instance such that T i j is value of the (i, j) entry of the SSYT T.
ssyt.highest_weight (μ : young_diagram): 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 ssyt (μ : young_diagram) :

entry : ℕ → ℕ → ℕ
row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → self.entry i j1 ≤ self.entry i j2
col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → self.entry i1 j < self.entry i2 j
zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → self.entry i j = 0

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

ssyt.fun_like = {coe := ssyt.entry μ, coe_injective' := _}

@[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

ssyt.has_coe_to_fun = fun_like.has_coe_to_fun

@[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) :

Copy of an ssyt μ 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 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

def ssyt.highest_weight (μ : young_diagram) :

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

Equations

ssyt.highest_weight μ = {entry := λ (i j : ℕ), ite ((i, j) ∈ μ) i 0, row_weak' := _, col_strict' := _, zeros' := _}

@[simp]

theorem ssyt.highest_weight_apply {μ : young_diagram} {i j : ℕ} :

⇑(ssyt.highest_weight μ) i j = ite ((i, j) ∈ μ) i 0

@[protected, instance]

def ssyt.inhabited {μ : young_diagram} :

inhabited (ssyt μ)

Equations

ssyt.inhabited = {default := ssyt.highest_weight μ}