Standard tableaux as lists of rows

StandardYoungTableau.toRows lists the entries of a standard tableau from left to right in each row, with the rows ordered from top to bottom. These rows satisfy List.IsTableauRows, have the prescribed shape, and contain every label exactly once. Conversely, these three properties characterize the lists arising from standard tableaux, giving StandardYoungTableau.rowsEquiv.

This connects bijective cell labelings with the list representation used by Schensted insertion. In particular, an insertion tableau containing each label once can be read as a standard tableau without changing its entries or its shape. Empty shapes are included.

References

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

def TauCeti.StandardYoungTableau.toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) : List (List (Fin μ.card))

The rows of a standard tableau, listed from top to bottom and left to right.

theorem TauCeti.StandardYoungTableau.toRows_def {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.toRows = List.ofFn fun (i : Fin (μ.colLen 0)) => List.ofFn fun (j : Fin (μ.rowLen ↑i)) => T ⟨(↑i, ↑j), ⋯⟩

The row representation enumerates each row in increasing column order.

@[simp]

theorem TauCeti.StandardYoungTableau.length_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.toRows.length = μ.colLen 0

The number of rows is the height of the first column.

@[simp]

theorem TauCeti.StandardYoungTableau.map_length_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) : List.map List.length T.toRows = μ.rowLens

The row lengths of a standard tableau agree with its shape.

@[simp]

theorem TauCeti.StandardYoungTableau.getElem_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) (i : ℕ) (hi : i < T.toRows.length) : T.toRows[i] = List.ofFn fun (j : Fin (μ.rowLen i)) => T ⟨(i, ↑j), ⋯⟩

Reading a row in its natural column order recovers its entries.

@[simp]

theorem TauCeti.StandardYoungTableau.length_getD_getElem?_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) (i : ℕ) : (T.toRows[i]?.getD []).length = μ.rowLen i

Reading a row beyond the shape gives length zero; otherwise it has the shape's row length.

@[simp]

theorem TauCeti.StandardYoungTableau.getElem?_getD_getElem?_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) (c : ↥μ.cells) : (T.toRows[(↑c).1]?.getD [])[(↑c).2]? = some (T c)

Looking up the coordinates of a cell in the row representation recovers its label.

theorem TauCeti.StandardYoungTableau.isTableauRows_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.toRows.IsTableauRows

A standard tableau's row representation is a semistandard tableau.

theorem TauCeti.StandardYoungTableau.flatten_toRows_perm {μ : YoungDiagram} (T : StandardYoungTableau μ) : T.toRows.flatten.Perm (List.finRange μ.card)

The rows contain each label exactly once.

@[simp]

theorem TauCeti.StandardYoungTableau.findIdx?_mem_toRows {μ : YoungDiagram} (T : StandardYoungTableau μ) (l : Fin μ.card) : List.findIdx? (fun (row : List (Fin μ.card)) => decide (l ∈ row)) T.toRows = some (T.toTableau.rowIndex l)

The first row of the row representation containing a label is the row of that label.

theorem TauCeti.StandardYoungTableau.toRows_injective {μ : YoungDiagram} : Function.Injective toRows

The row representation determines a standard tableau.

Decoding a list of rows

theorem TauCeti.StandardYoungTableau.exists_toRows_eq_iff {μ : YoungDiagram} {rows : List (List (Fin μ.card))} : (∃ (T : StandardYoungTableau μ), T.toRows = rows) ↔ rows.IsTableauRows ∧ List.map List.length rows = μ.rowLens ∧ rows.flatten.Perm (List.finRange μ.card)

A list of rows comes from a standard tableau exactly when it is a semistandard tableau of the given shape containing each label exactly once.

noncomputable def TauCeti.StandardYoungTableau.rowsEquiv (μ : YoungDiagram) : StandardYoungTableau μ ≃ { rows : List (List (Fin μ.card)) // rows.IsTableauRows ∧ List.map List.length rows = μ.rowLens ∧ rows.flatten.Perm (List.finRange μ.card) }

Standard tableaux of shape μ correspond to semistandard lists of rows of that shape containing every label exactly once.

@[simp]

theorem TauCeti.StandardYoungTableau.rowsEquiv_apply_coe {μ : YoungDiagram} (T : StandardYoungTableau μ) : ↑((rowsEquiv μ) T) = T.toRows

The forward row equivalence lists the entries of the tableau by rows.

@[simp]

theorem TauCeti.StandardYoungTableau.toRows_rowsEquiv_symm {μ : YoungDiagram} (rows : { rows : List (List (Fin μ.card)) // rows.IsTableauRows ∧ List.map List.length rows = μ.rowLens ∧ rows.flatten.Perm (List.finRange μ.card) }) : ((rowsEquiv μ).symm rows).toRows = ↑rows

Decoding a valid row list and reading it back recovers that list.

@[simp]

theorem TauCeti.StandardYoungTableau.rowsEquiv_symm_apply {μ : YoungDiagram} (rows : { rows : List (List (Fin μ.card)) // rows.IsTableauRows ∧ List.map List.length rows = μ.rowLens ∧ rows.flatten.Perm (List.finRange μ.card) }) (c : ↥μ.cells) : ((rowsEquiv μ).symm rows) c = (↑rows)[(↑c).1][(↑c).2]

The tableau decoded from a valid row list labels each cell by the entry in its row and column.