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.appendToRow: append a letter at the end of a given row of a list of rows.
• TauCeti.dropLastOfRow: remove the last letter of a given row of a list of rows.
• 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.

theorem List.IsRowAbove.append_singleton {α : Type u_1} [LT α] {upper lower : List α} (h : upper.IsRowAbove lower) {a : α} (hlen : lower.length < upper.length) (ha : upper[lower.length] < a) : upper.IsRowAbove (lower ++ [a])

Lengthening the lower row by an entry greater than the entry above it keeps the upper row on top of it.

theorem List.IsRowAbove.trans {α : Type u_1} [LT α] [IsTrans α fun (x1 x2 : α) => x1 < x2] {upper middle lower : List α} (h₁ : upper.IsRowAbove middle) (h₂ : middle.IsRowAbove lower) : upper.IsRowAbove lower

If one row sits above a second, and the second above a third, the first sits above the third.

instance List.instIsTransIsRowAboveOfLt {α : Type u_1} [LT α] [IsTrans α fun (x1 x2 : α) => x1 < x2] : IsTrans (List α) IsRowAbove

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.sortedGE_map_length {α : Type u_1} [Preorder α] {rows : List (List α)} (h : rows.IsTableauRows) : (map length rows).SortedGE

The row lengths of a tableau form a weakly decreasing list.

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.

theorem List.IsTableauRows.length_getD_eq_zero_of_le {α : Type u_1} [Preorder α] {rows : List (List α)} (h : rows.IsTableauRows) {k i : ℕ} (hk : (rows.getD k []).length = 0) (hki : k ≤ i) : (rows.getD i []).length = 0

Every row of a tableau below an empty row is empty. Rows beyond the last one are read as empty.

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

Each row of a tableau sits on top of the next one. Rows beyond the last one are read as empty.

theorem List.IsTableauRows.eq_nil_of_dropLast_eq_nil {α : Type u_1} [Preorder α] {row : List α} {rows : List (List α)} (h : (row :: rows).IsTableauRows) (hk : (rows.getD 0 []).length < row.length) (hd : row.dropLast = []) : rows = []

At a corner of the first row of a tableau, a first row with a single entry is the whole tableau: the row below it is empty.

theorem List.IsTableauRows.length_getD_succ_lt_of_getLast?_eq_some {α : Type u_1} [Preorder α] {rows : List (List α)} (h : rows.IsTableauRows) {a : α} (hmax : ∀ (x : α), x ∈ rows.flatten → x ≤ a) {k : ℕ} (hk : (rows.getD k []).getLast? = some a) : (rows.getD (k + 1) []).length < (rows.getD k []).length

In a nonempty tableau whose largest entry is a, the highest row ending in a ends in a corner: the row below it is strictly shorter.

theorem List.IsTableauRows.exists_getLast?_getD_eq_some {α : Type u_1} [PartialOrder α] {rows : List (List α)} (h : rows.IsTableauRows) {a : α} (ha : a ∈ rows.flatten) (hmax : ∀ (x : α), x ∈ rows.flatten → x ≤ a) : ∃ (i : ℕ), (rows.getD i []).getLast? = some a

In a tableau, the largest entry ends some row.

Appending a letter to a row

def TauCeti.appendToRow {α : Type u_1} (a : α) : ℕ → List (List α) → List (List α)

Append the letter a at the end of row k of a list of rows. If k is at least the number of rows, a starts a new last row.

@[simp]

theorem TauCeti.appendToRow_nil {α : Type u_1} (a : α) (k : ℕ) : appendToRow a k [] = [[a]]

Appending to a row of the empty list of rows starts a new row.

@[simp]

theorem TauCeti.appendToRow_zero_cons {α : Type u_1} (a : α) (row : List α) (rows : List (List α)) : appendToRow a 0 (row :: rows) = (row ++ [a]) :: rows

Appending to row 0 appends the letter to the first row.

@[simp]

theorem TauCeti.appendToRow_succ_cons {α : Type u_1} (a : α) (k : ℕ) (row : List α) (rows : List (List α)) : appendToRow a (k + 1) (row :: rows) = row :: appendToRow a k rows

Appending to row k + 1 appends to row k of the remaining rows.

theorem TauCeti.getD_appendToRow {α : Type u_1} (a : α) {k : ℕ} {rows : List (List α)} (hk : k ≤ rows.length) (i : ℕ) : (appendToRow a k rows).getD i [] = if i = k then rows.getD k [] ++ [a] else rows.getD i []

The rows of TauCeti.appendToRow a k: row k gains the letter a at its end, and every other row is unchanged. Rows beyond the last one are read as empty.

theorem TauCeti.length_appendToRow {α : Type u_1} (a : α) {k : ℕ} {rows : List (List α)} (hk : k ≤ rows.length) : (appendToRow a k rows).length = max rows.length (k + 1)

Appending to row k adds a new row exactly when k is the number of rows.

theorem TauCeti.flatten_appendToRow_perm {α : Type u_1} (a : α) (k : ℕ) (rows : List (List α)) : (appendToRow a k rows).flatten.Perm (rows.flatten ++ [a])

Appending to a row adds the letter to the entries.

@[simp]

theorem TauCeti.findIdx?_mem_appendToRow_self {α : Type u_1} [DecidableEq α] {a : α} {s : ℕ} {rows : List (List α)} (ha : ∀ (row : List α), row ∈ rows → ¬a ∈ row) (hs : s ≤ rows.length) : List.findIdx? (fun (row : List α) => decide (a ∈ row)) (appendToRow a s rows) = some s

Appending a to row s puts a in row s, when a is not already present.

@[simp]

theorem TauCeti.findIdx?_mem_appendToRow_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (hab : b ≠ a) (s : ℕ) (rows : List (List α)) : List.findIdx? (fun (row : List α) => decide (b ∈ row)) (appendToRow a s rows) = List.findIdx? (fun (row : List α) => decide (b ∈ row)) rows

Appending a to a row does not move any other letter.

theorem List.IsTableauRows.appendToRow {α : Type u_1} [Preorder α] {rows : List (List α)} (h : rows.IsTableauRows) {a : α} {k : ℕ} (hle : ∀ (x : α), x ∈ rows.getD k [] → x ≤ a) (habove : ∀ (i : ℕ), k = i + 1 → ∃ (hlen : (rows.getD k []).length < (rows.getD i []).length), (rows.getD i [])[(rows.getD k []).length] < a) : (TauCeti.appendToRow a k rows).IsTableauRows

Appending to a row preserves tableaux when the new cell is a corner of the new shape and its entry fits: it is at least every entry of its row, and greater than the entry above it.

Removing the last letter of a row

def TauCeti.dropLastOfRow {α : Type u_1} : ℕ → List (List α) → List (List α)

Remove the last letter of row k of a list of rows, deleting the row if it becomes empty. At a corner of a tableau this undoes TauCeti.appendToRow.

@[simp]

theorem TauCeti.dropLastOfRow_nil {α : Type u_1} (k : ℕ) : dropLastOfRow k [] = []

Removing a letter from the empty list of rows does nothing.

@[simp]

theorem TauCeti.dropLastOfRow_zero_cons {α : Type u_1} (row : List α) (rows : List (List α)) : dropLastOfRow 0 (row :: rows) = if row.dropLast = [] then rows else row.dropLast :: rows

Removing the last letter of row 0 drops the last letter of the first row, deleting that row if it becomes empty.

@[simp]

theorem TauCeti.dropLastOfRow_succ_cons {α : Type u_1} (k : ℕ) (row : List α) (rows : List (List α)) : dropLastOfRow (k + 1) (row :: rows) = row :: dropLastOfRow k rows

Removing the last letter of row k + 1 removes the last letter of row k of the remaining rows.

@[simp]

theorem TauCeti.dropLastOfRow_appendToRow {α : Type u_1} (a : α) {k : ℕ} {rows : List (List α)} (hne : ¬[] ∈ rows) (hk : k ≤ rows.length) : dropLastOfRow k (appendToRow a k rows) = rows

Removing the letter just appended to a row of a list of nonempty rows recovers the rows.

theorem TauCeti.getD_dropLastOfRow {α : Type u_1} {k : ℕ} {rows : List (List α)} (hk : 0 < (rows.getD k []).length) (hz : (rows.getD k []).length = 1 → ∀ (i : ℕ), k < i → (rows.getD i []).length = 0) (i : ℕ) : (dropLastOfRow k rows).getD i [] = if i = k then (rows.getD k []).dropLast else rows.getD i []

The rows of TauCeti.dropLastOfRow k at a nonempty row: row k loses its last letter, and every other row is unchanged, provided that deleting row k (when it has a single cell) shifts only empty rows. Rows beyond the last one are read as empty.

@[simp]

theorem TauCeti.appendToRow_dropLastOfRow {α : Type u_1} [Preorder α] {k : ℕ} {rows : List (List α)} (h : rows.IsTableauRows) (hk : (rows[k + 1]?.getD []).length < (rows[k]?.getD []).length) {a : α} (ha : (rows[k]?.getD []).getLast? = some a) : appendToRow a k (dropLastOfRow k rows) = rows

At a corner of a tableau, putting back the last letter of row k after removing it recovers the tableau.

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

Removing a corner preserves tableaux: deleting the last letter of a row that is longer than the next one gives a tableau.

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.

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.

@[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.

theorem TauCeti.le_length_rowInsert {α : Type u_1} [LinearOrder α] (x : α) {s : ℕ} {rows : List (List α)} (hs : s ≤ rows.length) : (if rowInsertIndex x rows = s then s + 1 else s) ≤ (rowInsert x rows).length

The row to which TauCeti.rowInsert_appendToRow moves a letter appended to row s of T is a row of T ← x or the row just below its last one: it is s + 1 if the new cell of T ← x is in row s, and s otherwise.

theorem TauCeti.rowInsert_of_forall_le {α : Type u_1} [LinearOrder α] {k : α} {rows : List (List α)} (h : ∀ (z : α), z ∈ rows.headD [] → z ≤ k) : rowInsert k rows = appendToRow k 0 rows

Inserting a letter at least as large as every entry of the first row appends it to the first row.

theorem TauCeti.rowInsertIndex_of_forall_le {α : Type u_1} [LinearOrder α] {k : α} {rows : List (List α)} (h : ∀ (z : α), z ∈ rows.headD [] → z ≤ k) : rowInsertIndex k rows = 0

Inserting a letter at least as large as every entry of the first row adds its cell to the first row.

theorem TauCeti.rowInsert_appendToRow {α : Type u_1} [LinearOrder α] {x k : α} {s : ℕ} {rows : List (List α)} (hx : x < k) (h : ∀ (z : α), z ∈ rows.flatten → z < k) (hs : s ≤ rows.length) : rowInsert x (appendToRow k s rows) = appendToRow k (if rowInsertIndex x rows = s then s + 1 else s) (rowInsert x rows)

Insertion past a larger letter. Let k be strictly larger than x and than every entry of rows, and append k to row s. Inserting x then gives the insertion of x into rows with k appended to row s, unless the insertion of x into rows ends in row s: in that case x's bumping path displaces k, which moves to the end of row s + 1.

theorem TauCeti.rowInsertIndex_appendToRow {α : Type u_1} [LinearOrder α] {x k : α} {s : ℕ} {rows : List (List α)} (hx : x < k) (h : ∀ (z : α), z ∈ rows.flatten → z < k) (hs : s ≤ rows.length) : rowInsertIndex x (appendToRow k s rows) = if rowInsertIndex x rows = s then s + 1 else rowInsertIndex x rows

The new cell of an insertion past a larger letter. In the situation of TauCeti.rowInsert_appendToRow, the new cell is in the same row as for the insertion of x into rows, unless that row is s, in which case it is the cell of k at the end of row s + 1.

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 : (List.map List.length rows).SortedGE) (x : α) : ((rowInsert x rows).getD (rowInsertIndex x rows + 1) []).length < ((rowInsert x rows).getD (rowInsertIndex x rows) []).length

The row below the new cell of T ← x is strictly shorter than the row gaining the cell. Only weakly decreasing original row lengths are needed.

theorem TauCeti.length_getD_succ_lt_of_rowInsertIndex_eq_succ {α : Type u_1} [LinearOrder α] {rows : List (List α)} (h : rows.IsTableauRows) {x : α} {i : ℕ} (hi : rowInsertIndex x rows = i + 1) : (rows.getD (i + 1) []).length < (rows.getD i []).length

A new cell below the first row sits under a longer row: if T ← x adds its cell in row i + 1, then row i + 1 of T is strictly shorter than row i.

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.

@[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.

theorem List.IsTableauRows.exists_forall_le_getLast?_getD_eq_some {α : Type u_1} [LinearOrder α] {Q : List (List α)} (hQ : Q.IsTableauRows) (hQnil : Q ≠ []) : ∃ (a : α), ∃ (k : ℕ), (∀ (x : α), x ∈ Q.flatten → x ≤ a) ∧ (Q.getD k []).getLast? = some a ∧ ∀ (i : ℕ), i < k → (Q.getD i []).getLast? ≠ some a

A nonempty tableau has a largest entry a, and a highest row k ending in a.

theorem TauCeti.length_getD_reverseRowInsert_fst {α : Type u_2} {β : Type u_3} [LinearOrder β] {P : List (List β)} {Q : List (List α)} (hP : P.IsTableauRows) (hshape : ∀ (i : ℕ), (P.getD i []).length = (Q.getD i []).length) {k : ℕ} (hk : (Q.getD (k + 1) []).length < (Q.getD k []).length) (i : ℕ) : ((reverseRowInsert k P).1.getD i []).length = ((dropLastOfRow k Q).getD i []).length

Reverse insertion from a corner of P, and removal of the last letter of the same row of a list of rows Q of the same shape, give two lists of rows of the same shape.

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.

@[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.