Young tableaux

A μ-tableau is a bijective filling t : ↥μ.cells ≃ Fin μ.card of the cells of a Young diagram μ by the labels Fin μ.card. This file defines YoungTableau, the row and the column of a label, and identifies the labels lying in a given row, respectively column, with the cells of that row, respectively column, of μ; counting those labels recovers the row lengths of μ (YoungTableau.card_filter_rowIndex_eq) and their partial sums (YoungTableau.card_filter_rowIndex_lt), and the column lengths (YoungTableau.card_filter_colIndex_eq). The latter gives the pigeonhole lemma YoungTableau.exists_ne_and_apply_eq_of_lt_colLen: a filling by fewer values than the length of a column repeats a value on that column. On top of that it proves the counting lemma YoungTableau.colIndex_lt_rowLen_of_injective: if the row of a label together with the column of its image under a permutation u of the labels determine the label, then that pair of indices is again a cell of μ. A second counting lemma, YoungTableau.card_filter_lt_le_card_filter_rowIndex_lt, bounds a filling of the labels that is injective on columns: it takes small values no more often than the row index does, the row filling YoungTableau.rowFilling being the extreme case. It also defines YoungTableau.relabel, the transitive action of the permutations of the labels on the tableaux of a fixed shape, which is how two tableaux of the same shape are compared.

Note that YoungTableau μ is an abbreviation, so that the whole Equiv API applies to a tableau directly. As a consequence dot notation on a tableau resolves in the Equiv namespace, and the declarations below are to be spelled out, as in YoungTableau.rowIndex t.

A μ-tableau is not required to be row- or column-increasing. The strictly row- and column-increasing ones are TauCeti.StandardYoungTableau, whose toTableau field is a μ-tableau in the present sense; Mathlib's SemistandardYoungTableau is a different notion again, a filling of μ by natural numbers that is weakly increasing along each row and strictly increasing down each column (represented as a function ℕ → ℕ → ℕ vanishing outside μ), with no bijectivity requirement. The three notions are kept distinct.

References

• W. Fulton, Young Tableaux, Section 7.1.
• Schur--Weyl roadmap, Layer 0.

@[reducible, inline]

abbrev TauCeti.YoungTableau (μ : YoungDiagram) : Type

A μ-tableau: a bijective filling of the cells of the Young diagram μ by the labels Fin μ.card.

Equations

• TauCeti.YoungTableau μ = (↥μ.cells ≃ Fin μ.card)

def TauCeti.YoungTableau.rowIndex {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) : ℕ

The row of the cell of μ carrying the label k in the tableau t.

Equations

• t.rowIndex k = (↑((Equiv.symm t) k)).1

def TauCeti.YoungTableau.colIndex {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) : ℕ

The column of the cell of μ carrying the label k in the tableau t.

Equations

• t.colIndex k = (↑((Equiv.symm t) k)).2

theorem TauCeti.YoungTableau.rowIndex_def {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) : t.rowIndex k = (↑((Equiv.symm t) k)).1

The row of a label is the first coordinate of the cell carrying it. This is not a simp lemma: rowIndex is the normal form, and rowIndex_apply computes it on a label presented as the value of t.

theorem TauCeti.YoungTableau.colIndex_def {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) : t.colIndex k = (↑((Equiv.symm t) k)).2

The column of a label is the second coordinate of the cell carrying it. As for rowIndex_def, this is not a simp lemma.

@[simp]

theorem TauCeti.YoungTableau.rowIndex_apply {μ : YoungDiagram} (t : YoungTableau μ) (c : ↥μ.cells) : t.rowIndex (t c) = (↑c).1

@[simp]

theorem TauCeti.YoungTableau.colIndex_apply {μ : YoungDiagram} (t : YoungTableau μ) (c : ↥μ.cells) : t.colIndex (t c) = (↑c).2

theorem TauCeti.YoungTableau.rowIndex_colIndex_injective {μ : YoungDiagram} (t : YoungTableau μ) : Function.Injective fun (k : Fin μ.card) => (t.rowIndex k, t.colIndex k)

A cell of a Young diagram is determined by its row together with its column, so a label of a tableau is determined by its row and its column.

def TauCeti.YoungTableau.rowFiberEquiv {μ : YoungDiagram} (t : YoungTableau μ) (i : ℕ) : { k : Fin μ.card // t.rowIndex k = i } ≃ ↥(μ.row i)

The labels lying in row i of a μ-tableau are the cells of the i-th row of μ.

Equations

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

def TauCeti.YoungTableau.colFiberEquiv {μ : YoungDiagram} (t : YoungTableau μ) (j : ℕ) : { k : Fin μ.card // t.colIndex k = j } ≃ ↥(μ.col j)

The labels lying in column j of a μ-tableau are the cells of the j-th column of μ.

Equations

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

@[simp]

theorem TauCeti.YoungTableau.rowFiberEquiv_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (i : ℕ) (k : { k : Fin μ.card // t.rowIndex k = i }) : ↑((t.rowFiberEquiv i) k) = ↑((Equiv.symm t) ↑k)

@[simp]

theorem TauCeti.YoungTableau.colFiberEquiv_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (j : ℕ) (k : { k : Fin μ.card // t.colIndex k = j }) : ↑((t.colFiberEquiv j) k) = ↑((Equiv.symm t) ↑k)

@[simp]

theorem TauCeti.YoungTableau.rowFiberEquiv_symm_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (i : ℕ) (c : ↥(μ.row i)) : ↑((t.rowFiberEquiv i).symm c) = t ⟨↑c, ⋯⟩

The label attached to a cell of row i is the label of that cell in the tableau.

@[simp]

theorem TauCeti.YoungTableau.colFiberEquiv_symm_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (j : ℕ) (c : ↥(μ.col j)) : ↑((t.colFiberEquiv j).symm c) = t ⟨↑c, ⋯⟩

The label attached to a cell of column j is the label of that cell in the tableau.

Cells and labels

theorem TauCeti.YoungTableau.rowIndex_colIndex_mem {μ : YoungDiagram} (t : YoungTableau μ) (x : Fin μ.card) : (t.rowIndex x, t.colIndex x) ∈ μ

The row and the column of a label are the coordinates of a cell of μ.

theorem TauCeti.YoungTableau.colIndex_lt_rowLen {μ : YoungDiagram} (t : YoungTableau μ) (x : Fin μ.card) : t.colIndex x < μ.rowLen (t.rowIndex x)

A label lies in a column strictly to the left of the end of its row.

theorem TauCeti.YoungTableau.rowIndex_lt_colLen_zero {μ : YoungDiagram} (t : YoungTableau μ) (x : Fin μ.card) : t.rowIndex x < μ.colLen 0

The row of a label is below the number of rows. The label lies in its own column, which is no longer than the zeroth one.

theorem TauCeti.YoungTableau.exists_rowIndex_colIndex {μ : YoungDiagram} (t : YoungTableau μ) {i j : ℕ} (h : (i, j) ∈ μ) : ∃ (x : Fin μ.card), t.rowIndex x = i ∧ t.colIndex x = j

Every cell of μ carries a label.

theorem TauCeti.YoungTableau.card_filter_rowIndex_eq {μ : YoungDiagram} (t : YoungTableau μ) (i : ℕ) : {y : Fin μ.card | t.rowIndex y = i}.card = μ.rowLen i

Row i of a μ-tableau carries μ.rowLen i labels.

theorem TauCeti.YoungTableau.card_filter_colIndex_eq {μ : YoungDiagram} (t : YoungTableau μ) (j : ℕ) : {y : Fin μ.card | t.colIndex y = j}.card = μ.colLen j

Column j of a μ-tableau carries μ.colLen j labels.

theorem TauCeti.YoungTableau.exists_ne_and_apply_eq_of_lt_colLen {μ : YoungDiagram} (t : YoungTableau μ) {α : Type u_1} [Fintype α] {j : ℕ} (hn : Fintype.card α < μ.colLen j) (p : Fin μ.card → α) : ∃ (a : Fin μ.card) (b : Fin μ.card), t.colIndex a = j ∧ t.colIndex b = j ∧ a ≠ b ∧ p a = p b

A filling with fewer values than the length of column j repeats a value on that column: two distinct labels of the column have the same image.

theorem TauCeti.YoungTableau.card_filter_rowIndex_lt {μ : YoungDiagram} (t : YoungTableau μ) (k : ℕ) : {x : Fin μ.card | t.rowIndex x < k}.card = (List.take k μ.rowLens).sum

The labels of a tableau lying in one of its first k rows are as many as the cells of the shape in its first k rows.

The counting lemma

theorem TauCeti.YoungTableau.colIndex_lt_rowLen_of_injective {μ : YoungDiagram} (t : YoungTableau μ) (u : Equiv.Perm (Fin μ.card)) (hu : Function.Injective fun (x : Fin μ.card) => (t.rowIndex x, t.colIndex (u x))) (x : Fin μ.card) : t.colIndex (u x) < μ.rowLen (t.rowIndex x)

The counting lemma for rows and columns along a permutation. If the row of a label together with the column of its u-image determine the label, then that pair is again a cell of μ.

Both halves of the count are over the rows of μ: the labels whose u-image lies in one of the first k columns number ∑ᵢ min (μ.rowLen i) k, while row i can contribute at most min (μ.rowLen i) k of them. Upper bounds that add up to the total are equalities, and the case k = μ.rowLen i of the resulting equality is the statement.

Fillings injective on columns

A filling p : Fin μ.card → ℕ of the labels of a μ-tableau is injective on columns when the value p x together with the column of x determines x. The counting lemma TauCeti.YoungTableau.card_filter_lt_le_card_filter_rowIndex_lt is that such a filling takes small values no more often than the row index does: for every m, at most as many labels satisfy p x < m as satisfy rowIndex t x < m. The row index is itself injective on columns (TauCeti.YoungTableau.rowIndex_colIndex_injective), so the bound is sharp.

Reading the labels as the cells carrying them, the filling plays the role of a row function and the tableau that of an injection into the cells, so the lemma is the counting core YoungDiagram.card_filter_le_sum_take_rowLens with the right-hand side counted back by TauCeti.YoungTableau.card_filter_rowIndex_lt.

theorem TauCeti.YoungTableau.card_filter_lt_le_card_filter_rowIndex_lt {μ : YoungDiagram} (t : YoungTableau μ) {p : Fin μ.card → ℕ} (hp : Function.Injective fun (x : Fin μ.card) => (p x, t.colIndex x)) (m : ℕ) : {x : Fin μ.card | p x < m}.card ≤ {x : Fin μ.card | t.rowIndex x < m}.card

A filling injective on columns takes small values no more often than the row index does. For every m, at most as many labels of a μ-tableau satisfy p x < m as lie in one of the first m rows.

As m varies, this gives the dominance bound on the content of such a filling: the content is dominated by the sequence of row lengths of μ, which is the content of the row index itself.

The row filling

def TauCeti.YoungTableau.rowFilling {μ : YoungDiagram} {n : ℕ} (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) (x : Fin μ.card) : Fin n

The row filling of a μ-tableau whose shape has at most n rows: the row index of a label, read as an element of Fin n. It is injective on the columns of t (TauCeti.YoungTableau.rowIndex_colIndex_injective), and the extreme case of the counting lemma above: its content is the sequence of row lengths of μ.

Equations

• t.rowFilling hn x = ⟨t.rowIndex x, ⋯⟩

@[simp]

theorem TauCeti.YoungTableau.val_rowFilling {μ : YoungDiagram} {n : ℕ} (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) (x : Fin μ.card) : ↑(t.rowFilling hn x) = t.rowIndex x

@[simp]

theorem TauCeti.YoungTableau.rowFilling_eq_iff {μ : YoungDiagram} {n : ℕ} (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) (x : Fin μ.card) (j : Fin n) : t.rowFilling hn x = j ↔ t.rowIndex x = ↑j

Relabeling

def TauCeti.YoungTableau.relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : YoungTableau μ

The tableau t with its labels permuted by σ: the cell that t labels k is labelled σ k by relabel σ t.

Relabeling is the left action of Equiv.Perm (Fin μ.card) on YoungTableau μ recorded by relabel_one and relabel_relabel, and it is transitive by exists_relabel_eq. It is not registered as a MulAction instance because YoungTableau μ is an abbreviation for a type of equivalences, so such an instance would fire on equivalences at large, far outside the tableaux it is meant for.

Equations

• TauCeti.YoungTableau.relabel σ t = Equiv.trans t σ

@[simp]

theorem TauCeti.YoungTableau.relabel_apply {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (c : ↥μ.cells) : (relabel σ t) c = σ (t c)

@[simp]

theorem TauCeti.YoungTableau.relabel_symm_apply {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (k : Fin μ.card) : (Equiv.symm (relabel σ t)) k = (Equiv.symm t) (σ⁻¹ k)

@[simp]

theorem TauCeti.YoungTableau.rowIndex_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (k : Fin μ.card) : (relabel σ t).rowIndex k = t.rowIndex (σ⁻¹ k)

Relabeling by σ moves the label k to the row that t gives to σ⁻¹ k.

@[simp]

theorem TauCeti.YoungTableau.colIndex_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (k : Fin μ.card) : (relabel σ t).colIndex k = t.colIndex (σ⁻¹ k)

Relabeling by σ moves the label k to the column that t gives to σ⁻¹ k.

@[simp]

theorem TauCeti.YoungTableau.relabel_one {μ : YoungDiagram} (t : YoungTableau μ) : relabel 1 t = t

@[simp]

theorem TauCeti.YoungTableau.relabel_relabel {μ : YoungDiagram} (σ τ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : relabel σ (relabel τ t) = relabel (σ * τ) t

def TauCeti.YoungTableau.relabelPerm {μ : YoungDiagram} (t t' : YoungTableau μ) : Equiv.Perm (Fin μ.card)

The permutation of the labels carrying the tableau t to the tableau t' of the same shape.

Equations

• t.relabelPerm t' = (Equiv.symm t).trans t'

@[simp]

theorem TauCeti.YoungTableau.relabelPerm_apply {μ : YoungDiagram} (t t' : YoungTableau μ) (k : Fin μ.card) : (t.relabelPerm t') k = t' ((Equiv.symm t) k)

The permutation carrying t to t' sends the label k to the label that t' gives to the cell that t labels k.

@[simp]

theorem TauCeti.YoungTableau.relabel_relabelPerm {μ : YoungDiagram} (t t' : YoungTableau μ) : relabel (t.relabelPerm t') t = t'

theorem TauCeti.YoungTableau.exists_relabel_eq {μ : YoungDiagram} (t t' : YoungTableau μ) : ∃ (σ : Equiv.Perm (Fin μ.card)), relabel σ t = t'

Any two tableaux of the same shape differ by a relabeling.

theorem TauCeti.YoungTableau.nonempty (μ : YoungDiagram) : Nonempty (YoungTableau μ)

Every Young diagram carries a tableau: enumerating its cells is one.

This is a theorem rather than a Nonempty instance because YoungTableau μ is an abbreviation for a type of equivalences, so an instance would fire on equivalences at large.