Standard tableaux and lattice recording words

The row word of a standard Young tableau records the row containing each label, in increasing order of labels. It is a lattice word: every prefix contains at least as many entries in row i as in row i + 1. Conversely, a lattice word with μ.rowLen i occurrences of each letter i determines a unique standard tableau of shape μ.

This identifies the recording words of Robinson–Schensted insertion with standard recording tableaux. The bijection uses the existing corner restriction and extension of standard tableaux: the final letter specifies the corner occupied by the largest label.

References

• W. Fulton, Young Tableaux, Cambridge University Press (1997), Section 4.1.
• B. E. Sagan, The Symmetric Group, second edition, Springer GTM 203 (2001), Section 3.1.

def TauCeti.StandardYoungTableau.rowWord {μ : YoungDiagram} (T : StandardYoungTableau μ) : List ℕ

The rows containing the labels 0, …, μ.card - 1, in that order.

theorem TauCeti.StandardYoungTableau.rowWord_def {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.rowWord = List.ofFn T.toTableau.rowIndex

The row word lists the row index of each label.

@[simp]

theorem TauCeti.StandardYoungTableau.length_rowWord {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.rowWord.length = μ.card

A row word has one letter per cell.

@[simp]

theorem TauCeti.StandardYoungTableau.getElem_rowWord {μ : YoungDiagram} (T : StandardYoungTableau μ) (k : ℕ) (hk : k < T.rowWord.length) : T.rowWord[k] = T.toTableau.rowIndex ⟨k, ⋯⟩

The letter at a label's position is the row containing that label.

theorem TauCeti.StandardYoungTableau.rowWord_injective {μ : YoungDiagram} : Function.Injective rowWord

Standard tableaux are determined by their row words.

@[simp]

theorem TauCeti.StandardYoungTableau.rowWord_extend {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) : (extend hc T).rowWord = T.rowWord ++ [c.1]

Restoring a corner appends its row to the row word.

@[simp]

theorem TauCeti.StandardYoungTableau.count_rowWord {μ : YoungDiagram} (T : StandardYoungTableau μ) (i : ℕ) : List.count i T.rowWord = μ.rowLen i

The number of occurrences of a row in the row word is its length.

theorem TauCeti.StandardYoungTableau.isLatticeWord_rowWord {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.rowWord.IsLatticeWord

Every standard tableau has a lattice row word.

theorem TauCeti.StandardYoungTableau.exists_rowWord_eq_iff {μ : YoungDiagram} (r : List ℕ) : (∃ (T : StandardYoungTableau μ), T.rowWord = r) ↔ r.IsLatticeWord ∧ ∀ (i : ℕ), List.count i r = μ.rowLen i

Lattice words with the prescribed row counts are exactly the row words of standard tableaux of that shape.

noncomputable def TauCeti.StandardYoungTableau.latticeWordEquiv (μ : YoungDiagram) : StandardYoungTableau μ ≃ { r : List ℕ // r.IsLatticeWord ∧ ∀ (i : ℕ), List.count i r = μ.rowLen i }

Standard tableaux of shape μ correspond to lattice words containing each row index exactly as many times as that row has cells.

@[simp]

theorem TauCeti.StandardYoungTableau.latticeWordEquiv_apply_val {μ : YoungDiagram} (T : StandardYoungTableau μ) : ↑((latticeWordEquiv μ) T) = T.rowWord

The lattice-word correspondence sends a tableau to its row word.

@[simp]

theorem TauCeti.StandardYoungTableau.rowWord_latticeWordEquiv_symm {μ : YoungDiagram} (r : { r : List ℕ // r.IsLatticeWord ∧ ∀ (i : ℕ), List.count i r = μ.rowLen i }) : ((latticeWordEquiv μ).symm r).rowWord = ↑r

Decoding a lattice word recovers a tableau having exactly that row word.