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 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 (μ : 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 SSYT T.
• Ssyt.highestWeight (μ : YoungDiagram): the semistandard Young tableau whose ith row consists entirely of is, for each i.

Tags

Semistandard Young tableau

References

structure Ssyt (μ : YoungDiagram) : Type

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

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

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

Equations

• Ssyt.instFunLike = { coe := Ssyt.entry, coe_injective' := (_ : ∀ (T T' : Ssyt μ), T.entry = T'.entry → T = T') }

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

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

Equations

• Ssyt.instCoeFunSsytForAllNat = inferInstance

@[simp]

theorem Ssyt.to_fun_eq_coe {μ : YoungDiagram} {T : Ssyt μ} : T.entry = ⇑T

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

def Ssyt.copy {μ : YoungDiagram} (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

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

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

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

instance Ssyt.instInhabitedSsyt {μ : YoungDiagram} : Inhabited (Ssyt μ)

Equations

• Ssyt.instInhabitedSsyt = { default := Ssyt.highestWeight μ }