Documentation

Mathlib.Combinatorics.Young.SemistandardTableau

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 #

Tags #

Semistandard Young tableau

References #

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

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

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

    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 : 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

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

      Equations
      Instances For
        @[simp]
        theorem SemistandardYoungTableau.highestWeight_apply {μ : YoungDiagram} {i : } {j : } :
        (SemistandardYoungTableau.highestWeight μ) i j = if (i, j) μ then i else 0
        Equations