Schensted row insertion into a tableau

A semistandard tableau is recorded here by its list of rows, from top to bottom: every row is nonempty and weakly increasing, and each row sits on top of the next one, being at least as long and strictly smaller in every column (List.IsTableauRows).

Row insertion TauCeti.rowInsert x T inserts the letter x into the first row by TauCeti.rowBump; the letter bumped out of that row is inserted into the second row, and so on, until a letter is appended at the end of a row (possibly a new row at the bottom). This is Schensted's insertion T ← x, the step iterated by the Robinson--Schensted--Knuth correspondence. Its basic properties are:

• the result is again a tableau (List.IsTableauRows.rowInsert);
• it has the letters of T together with x (TauCeti.flatten_rowInsert_perm);
• its shape is that of T with one cell added, at the end of the row TauCeti.rowInsertIndex x T (TauCeti.length_getD_rowInsert), and that cell is a corner (TauCeti.length_getD_succ_rowInsertIndex_lt).

Reverse insertion TauCeti.reverseRowInsert k T removes the last entry of row k and moves it up by TauCeti.reverseRowBump, row by row, ejecting a letter from the first row. It undoes insertion (TauCeti.reverseRowInsert_rowInsert), and conversely, from a corner of a tableau it produces a tableau and a letter whose insertion recovers the original tableau with the new cell at that corner (TauCeti.rowInsert_reverseRowInsert, List.IsTableauRows.reverseRowInsert). So insertion is a bijection between pairs of a tableau and a letter, and tableaux with a chosen corner (TauCeti.rowInsertEquiv). Iterating it over the letters of a word, and recording the new cells, is the Robinson--Schensted--Knuth correspondence.

Main definitions

• List.IsRowAbove: one row can sit directly on top of another in a semistandard tableau.
• List.IsTableauRows: the rows of a semistandard tableau.
• TauCeti.rowInsert: Schensted row insertion of a letter into a tableau.
• TauCeti.rowInsertIndex: the row in which row insertion adds its new cell.
• TauCeti.reverseRowInsert: reverse row insertion from the end of a given row.
• TauCeti.rowInsertEquiv: row insertion as a bijection onto tableaux with a chosen corner.

References

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

structure List.IsRowAbove {α : Type u_1} [LT α] (upper lower : List α) : Prop

The row upper can sit directly on top of the row lower in a semistandard tableau: lower is no longer than upper, and each entry of lower is strictly greater than the entry of upper above it.

• length_le : lower.length ≤ upper.length

  The lower row is no longer than the upper row.

• getElem_lt (j : ℕ) (hu : j < upper.length) (hl : j < lower.length) : upper[j] < lower[j]

  Each entry of the lower row is strictly greater than the entry above it.

@[simp]

theorem List.isRowAbove_nil {α : Type u_1} [LT α] (upper : List α) : upper.IsRowAbove []

Any row can sit on top of the empty row.

theorem List.IsRowAbove.append_right {α : Type u_1} [LT α] {upper lower : List α} (h : upper.IsRowAbove lower) (extra : List α) : (upper ++ extra).IsRowAbove lower

Lengthening the upper row keeps it on top of the lower row.

structure List.IsTableauRows {α : Type u_1} [Preorder α] (rows : List (List α)) : Prop

The rows, listed from top to bottom, of a semistandard tableau: every row is nonempty and weakly increasing, and every row sits on top of the next one in the sense of List.IsRowAbove. So the row lengths weakly decrease and the columns strictly increase.

• nil_notMem : ¬[] ∈ rows

  No row is empty.

• sortedLE (row : List α) : row ∈ rows → row.SortedLE

  Every row is weakly increasing.

• isChain : IsChain IsRowAbove rows

  Every row sits on top of the next one.

@[simp]

theorem List.isTableauRows_nil {α : Type u_1} [Preorder α] : [].IsTableauRows

The empty tableau.

theorem List.isTableauRows_cons {α : Type u_1} [Preorder α] {row : List α} {rows : List (List α)} : (row :: rows).IsTableauRows ↔ row ≠ [] ∧ row.SortedLE ∧ row.IsRowAbove (rows.headD []) ∧ rows.IsTableauRows

A tableau is a nonempty weakly increasing first row on top of a tableau.

theorem List.IsTableauRows.tail {α : Type u_1} [Preorder α] {row : List α} {rows : List (List α)} (h : (row :: rows).IsTableauRows) : rows.IsTableauRows

Deleting the first row of a tableau leaves a tableau.

theorem List.IsTableauRows.length_getD_succ_le {α : Type u_1} [Preorder α] {rows : List (List α)} (h : rows.IsTableauRows) (i : ℕ) : (rows.getD (i + 1) []).length ≤ (rows.getD i []).length

The row lengths of a tableau weakly decrease. Rows beyond the last one are read as empty.

Row insertion

def TauCeti.rowInsert {α : Type u_1} [LinearOrder α] (x : α) : List (List α) → List (List α)

Schensted row insertion T ← x of a letter x into a tableau given by its rows T: insert x into the first row by TauCeti.rowBump, insert the bumped letter into the next row, and so on, until a letter is appended at the end of a row, possibly a new last row.

Equations

• TauCeti.rowInsert x [] = [[x]]
• TauCeti.rowInsert x (row :: rows) = (TauCeti.rowBump x row).1 :: (TauCeti.rowBump x row).2.elim rows fun (x : α) => TauCeti.rowInsert x rows

def TauCeti.rowInsertIndex {α : Type u_1} [LinearOrder α] (x : α) : List (List α) → ℕ

The index of the row in which TauCeti.rowInsert x T adds its new cell.

Equations

• TauCeti.rowInsertIndex x [] = 0
• TauCeti.rowInsertIndex x (row :: rows) = (TauCeti.rowBump x row).2.elim 0 fun (x : α) => TauCeti.rowInsertIndex x rows + 1

@[simp]

theorem TauCeti.rowInsert_nil {α : Type u_1} [LinearOrder α] (x : α) : rowInsert x [] = [[x]]

Inserting into the empty tableau gives a one-cell tableau.

@[simp]

theorem TauCeti.rowInsertIndex_nil {α : Type u_1} [LinearOrder α] (x : α) : rowInsertIndex x [] = 0

Inserting into the empty tableau adds its cell in the first row.

theorem TauCeti.rowInsert_cons_of_eq_none {α : Type u_1} [LinearOrder α] {x : α} {row : List α} (rows : List (List α)) (h : (rowBump x row).2 = none) : rowInsert x (row :: rows) = (rowBump x row).1 :: rows

If nothing is bumped from the first row, insertion stops there.

theorem TauCeti.rowInsert_cons_of_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (rows : List (List α)) (h : (rowBump x row).2 = some y) : rowInsert x (row :: rows) = (rowBump x row).1 :: rowInsert y rows

A letter bumped from the first row is inserted into the remaining rows.

theorem TauCeti.rowInsertIndex_cons_of_eq_none {α : Type u_1} [LinearOrder α] {x : α} {row : List α} (rows : List (List α)) (h : (rowBump x row).2 = none) : rowInsertIndex x (row :: rows) = 0

If nothing is bumped from the first row, the new cell is in the first row.

theorem TauCeti.rowInsertIndex_cons_of_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (rows : List (List α)) (h : (rowBump x row).2 = some y) : rowInsertIndex x (row :: rows) = rowInsertIndex y rows + 1

If a letter is bumped from the first row, the new cell is where its insertion into the remaining rows puts it.

theorem TauCeti.headD_rowInsert {α : Type u_1} [LinearOrder α] (x : α) (rows : List (List α)) : (rowInsert x rows).headD [] = (rowBump x (rows.headD [])).1

The first row of T ← x is the first row of T (empty if T is) after the first bump.

theorem TauCeti.flatten_rowInsert_perm {α : Type u_1} [LinearOrder α] (x : α) (rows : List (List α)) : (rowInsert x rows).flatten.Perm (x :: rows.flatten)

Row insertion conserves the letters: T ← x has the letters of T together with x.

theorem TauCeti.rowInsertIndex_le_length {α : Type u_1} [LinearOrder α] (x : α) (rows : List (List α)) : rowInsertIndex x rows ≤ rows.length

The new cell is in an existing row or in the row just below the last one.

theorem TauCeti.length_getD_rowInsert {α : Type u_1} [LinearOrder α] (x : α) (rows : List (List α)) (i : ℕ) : ((rowInsert x rows).getD i []).length = (rows.getD i []).length + if i = rowInsertIndex x rows then 1 else 0

The shape of T ← x: the row TauCeti.rowInsertIndex x T gains one cell and every other row keeps its length. Rows beyond the last one are read as empty.

theorem TauCeti.length_rowInsert {α : Type u_1} [LinearOrder α] (x : α) (rows : List (List α)) : (rowInsert x rows).length = max rows.length (rowInsertIndex x rows + 1)

T ← x has one more row than T exactly when the new cell starts a new row.

Insertion preserves tableaux

theorem List.IsTableauRows.rowInsert {α : Type u_1} [LinearOrder α] {rows : List (List α)} (h : rows.IsTableauRows) (x : α) : (TauCeti.rowInsert x rows).IsTableauRows

Row insertion preserves tableaux.

theorem TauCeti.length_getD_succ_rowInsertIndex_lt {α : Type u_1} [LinearOrder α] {rows : List (List α)} (h : rows.IsTableauRows) (x : α) : ((rowInsert x rows).getD (rowInsertIndex x rows + 1) []).length < ((rowInsert x rows).getD (rowInsertIndex x rows) []).length

The new cell of T ← x is a corner: the row below it is strictly shorter.

Reverse insertion

def TauCeti.reverseRowInsert {α : Type u_1} [LinearOrder α] : ℕ → List (List α) → List (List α) × Option α

Reverse row insertion from the end of row k: remove the last entry of row k (deleting the row if it becomes empty), insert it into row k - 1 by TauCeti.reverseRowBump, insert the letter returned into row k - 2, and so on up to the first row. The second component is the letter returned by the first row, or none if some step fails, which does not happen at a corner of a tableau.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.reverseRowInsert x✝ [] = ([], none)
• TauCeti.reverseRowInsert 0 (row :: rows) = (if row.dropLast = [] then rows else row.dropLast :: rows, row.getLast?)

@[simp]

theorem TauCeti.reverseRowInsert_nil {α : Type u_1} [LinearOrder α] (k : ℕ) : reverseRowInsert k [] = ([], none)

Reverse insertion into the empty tableau fails.

theorem TauCeti.reverseRowInsert_zero_cons {α : Type u_1} [LinearOrder α] (row : List α) (rows : List (List α)) : reverseRowInsert 0 (row :: rows) = (if row.dropLast = [] then rows else row.dropLast :: rows, row.getLast?)

Reverse insertion from the end of the first row removes its last entry and returns it.

theorem TauCeti.reverseRowInsert_succ_cons_of_eq_some {α : Type u_1} [LinearOrder α] {k : ℕ} {y : α} (row : List α) {rows : List (List α)} (h : (reverseRowInsert k rows).2 = some y) : reverseRowInsert (k + 1) (row :: rows) = ((reverseRowBump y row).1 :: (reverseRowInsert k rows).1, (reverseRowBump y row).2)

A letter returned by reverse insertion into the rows below the first is reverse bumped into the first row.

theorem TauCeti.reverseRowInsert_succ_cons_of_eq_none {α : Type u_1} [LinearOrder α] {k : ℕ} (row : List α) {rows : List (List α)} (h : (reverseRowInsert k rows).2 = none) : reverseRowInsert (k + 1) (row :: rows) = (row :: (reverseRowInsert k rows).1, none)

If reverse insertion into the rows below the first fails, it fails.

theorem TauCeti.reverseRowInsert_rowInsert {α : Type u_1} [LinearOrder α] (x : α) {rows : List (List α)} (hne : ¬[] ∈ rows) (hs : ∀ (row : List α), row ∈ rows → row.SortedLE) : reverseRowInsert (rowInsertIndex x rows) (rowInsert x rows) = (rows, some x)

Reverse insertion undoes insertion: reverse inserting from the new cell of T ← x recovers T and returns x. Only the rows of T being nonempty and weakly increasing is used.

theorem List.IsTableauRows.reverseRowInsert {α : Type u_1} [LinearOrder α] {k : ℕ} {rows : List (List α)} (h : rows.IsTableauRows) (hk : (rows.getD (k + 1) []).length < (rows.getD k []).length) : (TauCeti.reverseRowInsert k rows).1.IsTableauRows

Reverse insertion preserves tableaux at corners: reverse inserting from the end of a row k of a tableau whose next row is strictly shorter yields a tableau.

theorem TauCeti.rowInsert_reverseRowInsert {α : Type u_1} [LinearOrder α] {k : ℕ} {rows : List (List α)} (h : rows.IsTableauRows) (hk : (rows.getD (k + 1) []).length < (rows.getD k []).length) : ∃ (x : α), (reverseRowInsert k rows).2 = some x ∧ rowInsert x (reverseRowInsert k rows).1 = rows ∧ rowInsertIndex x (reverseRowInsert k rows).1 = k

Insertion undoes reverse insertion at a corner. If row k + 1 of a tableau T is strictly shorter than row k, then reverse insertion from the end of row k returns a letter x and a tableau T' such that T' ← x is T, with its new cell in row k.

Insertion as a bijection

def TauCeti.rowInsertEquiv {α : Type u_1} [LinearOrder α] : { rows : List (List α) // rows.IsTableauRows } × α ≃ { p : List (List α) × ℕ // p.1.IsTableauRows ∧ (p.1.getD (p.2 + 1) []).length < (p.1.getD p.2 []).length }

Row insertion is a bijection between pairs of a tableau and a letter, and pairs of a tableau and a row k ending in a corner, that is, whose next row is strictly shorter. It sends (T, x) to T ← x with the row of its new cell; the inverse is reverse row insertion.

Equations

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

@[simp]

theorem TauCeti.rowInsertEquiv_apply_coe {α : Type u_1} [LinearOrder α] (rows : { rows : List (List α) // rows.IsTableauRows }) (x : α) : ↑(rowInsertEquiv (rows, x)) = (rowInsert x ↑rows, rowInsertIndex x ↑rows)

rowInsertEquiv sends (T, x) to T ← x with the row of its new cell.

@[simp]

theorem TauCeti.rowInsertEquiv_symm_apply_fst_coe {α : Type u_1} [LinearOrder α] (p : { p : List (List α) × ℕ // p.1.IsTableauRows ∧ (p.1.getD (p.2 + 1) []).length < (p.1.getD p.2 []).length }) : ↑(rowInsertEquiv.symm p).1 = (reverseRowInsert (↑p).2 (↑p).1).1

The tableau of rowInsertEquiv.symm p is the result of reverse row insertion.

theorem TauCeti.some_rowInsertEquiv_symm_apply_snd {α : Type u_1} [LinearOrder α] (p : { p : List (List α) × ℕ // p.1.IsTableauRows ∧ (p.1.getD (p.2 + 1) []).length < (p.1.getD p.2 []).length }) : some (rowInsertEquiv.symm p).2 = (reverseRowInsert (↑p).2 (↑p).1).2

The letter of rowInsertEquiv.symm p is the letter returned by reverse row insertion.