The labels of a standard Young tableau, ordered by their cells

A standard Young tableau increases along its rows and down its columns, so the order of two of its labels is decided by their cells as soon as those cells share a row or a column: two labels in one column are ordered as their rows are (TauCeti.StandardYoungTableau.lt_iff_rowIndex_lt), and two labels in one row are ordered as their columns are (TauCeti.StandardYoungTableau.lt_iff_colIndex_lt).

The consequence this file is written for is that a standard Young tableau is determined by the row of each of its labels (TauCeti.StandardYoungTableau.rowIndex_injective): the labels of a row are placed there in increasing order, so nothing is left to choose once the rows are known. Two standard tableaux with the same rows differ by a permutation preserving every row of the first, which restricts to a strictly monotone self-map of that row and is therefore the identity there by Mathlib's StrictMono.apply_eq.

In the language of the Specht modules, the injectivity says that distinct standard tableaux have distinct tabloids, and that is how TauCeti/RepresentationTheory/Symmetric/Specht/StandardBasis.lean uses it.

Main results

• TauCeti.StandardYoungTableau.lt_iff_rowIndex_lt: labels in one column are ordered by row.
• TauCeti.StandardYoungTableau.lt_iff_colIndex_lt: labels in one row are ordered by column.
• TauCeti.exists_standardYoungTableau_toTableau_eq_iff: conversely, a tableau whose labels increase down each column and along each row is standard.
• TauCeti.StandardYoungTableau.rowIndex_injective: a standard Young tableau is determined by the rows of its labels.

References

• B. E. Sagan, The Symmetric Group, Section 2.5, where the standard tableaux are ordered by their tabloids.
• Schur--Weyl roadmap, Layer 5, whose standard basis of the Specht module this serves.

Comparing two labels in a common row or column

theorem TauCeti.StandardYoungTableau.lt_of_rowIndex_lt {μ : YoungDiagram} (T : StandardYoungTableau μ) {x y : Fin μ.card} (hcol : T.toTableau.colIndex x = T.toTableau.colIndex y) (hrow : T.toTableau.rowIndex x < T.toTableau.rowIndex y) : x < y

Of two labels of a standard Young tableau lying in a common column, the one in the earlier row is the smaller.

theorem TauCeti.StandardYoungTableau.lt_of_colIndex_lt {μ : YoungDiagram} (T : StandardYoungTableau μ) {x y : Fin μ.card} (hrow : T.toTableau.rowIndex x = T.toTableau.rowIndex y) (hcol : T.toTableau.colIndex x < T.toTableau.colIndex y) : x < y

Of two labels of a standard Young tableau lying in a common row, the one in the earlier column is the smaller.

theorem TauCeti.StandardYoungTableau.lt_iff_rowIndex_lt {μ : YoungDiagram} (T : StandardYoungTableau μ) {x y : Fin μ.card} (hcol : T.toTableau.colIndex x = T.toTableau.colIndex y) : x < y ↔ T.toTableau.rowIndex x < T.toTableau.rowIndex y

Two labels of a standard Young tableau in a common column are ordered as their rows are.

theorem TauCeti.StandardYoungTableau.lt_iff_colIndex_lt {μ : YoungDiagram} (T : StandardYoungTableau μ) {x y : Fin μ.card} (hrow : T.toTableau.rowIndex x = T.toTableau.rowIndex y) : x < y ↔ T.toTableau.colIndex x < T.toTableau.colIndex y

Two labels of a standard Young tableau in a common row are ordered as their columns are.

Recognising a standard Young tableau

theorem TauCeti.exists_standardYoungTableau_toTableau_eq_iff {μ : YoungDiagram} (t : YoungTableau μ) : (∃ (T : StandardYoungTableau μ), T.toTableau = t) ↔ (∀ (x y : Fin μ.card), t.colIndex x = t.colIndex y → t.rowIndex x < t.rowIndex y → x < y) ∧ ∀ (x y : Fin μ.card), t.rowIndex x = t.rowIndex y → t.colIndex x < t.colIndex y → x < y

A tableau is standard exactly when its labels increase down each column and along each row, read on the row and the column of a label rather than on the cells. This is the converse of TauCeti.StandardYoungTableau.lt_of_rowIndex_lt and TauCeti.StandardYoungTableau.lt_of_colIndex_lt, and it is how a tableau produced by the straightening algorithm is recognised as standard.

A standard Young tableau is determined by the rows of its labels

theorem TauCeti.StandardYoungTableau.rowIndex_injective (μ : YoungDiagram) : Function.Injective fun (T : StandardYoungTableau μ) => T.toTableau.rowIndex

A standard Young tableau is determined by the rows of its labels.