The Robinson--Schensted correspondence for words

Inserting the letters of a word w = w₁ w₂ ⋯ wₙ one after another into the empty tableau by Schensted row insertion gives its insertion tableau P(w) = (⋯((∅ ← w₁) ← w₂) ⋯) ← wₙ. Recording, for each k, the row rₖ in which the insertion of wₖ adds its new cell gives its recording word r₁ r₂ ⋯ rₙ. The recording word is the row-by-row record of the usual recording tableau Q(w), the standard tableau with the entry k in the cell added at step k: a standard tableau is determined by the row of each of its entries, and the words arising this way from standard tableaux of shape λ are exactly the lattice words in which each letter i occurs λᵢ times.

The Robinson--Schensted correspondence TauCeti.robinsonSchenstedEquiv says that w ↦ (P(w), r(w)) is a bijection from words onto the pairs of a semistandard tableau P and a lattice word r such that row i of P has as many cells as r has letters i. Injectivity and surjectivity both follow, one letter at a time, from the fact that a single row insertion is a bijection onto tableaux with a chosen corner (TauCeti.rowInsertEquiv). For a word without repeated letters, such as a permutation in one-line notation, the insertion tableau has distinct entries (TauCeti.flatten_robinsonSchensted_fst_perm); this is the case underlying the classical bijection between permutations and pairs of standard tableaux of the same shape.

Main definitions

• List.IsLatticeWord: a lattice word, in which every prefix contains each letter i at least as often as i + 1; a weakly increasing word is one as soon as the word itself satisfies these inequalities (List.isLatticeWord_of_pairwise_le).
• TauCeti.robinsonSchensted: the insertion tableau and the recording word of a word.
• TauCeti.robinsonSchenstedEquiv: the Robinson--Schensted correspondence, as a bijection.

Main statements

• TauCeti.flatten_robinsonSchensted_fst_perm: the insertion tableau has the letters of the word.
• TauCeti.length_getD_robinsonSchensted_fst: the shape of the insertion tableau is the content of the recording word.
• TauCeti.isLatticeWord_robinsonSchensted_snd: the recording word is a lattice word.
• TauCeti.robinsonSchensted_injective and TauCeti.exists_robinsonSchensted_eq_iff: the correspondence is injective, and its image is described by the three properties above.

References

• W. Fulton, Young Tableaux, Cambridge University Press (1997), Section 4.1.
• B. E. Sagan, The Symmetric Group, 2nd ed., Springer GTM 203 (2001), Sections 3.1 and 3.3.
• C. Schensted, Longest increasing and decreasing subsequences, Canad. J. Math. 13 (1961).

def List.IsLatticeWord (r : List ℕ) : Prop

A lattice word (also called a Yamanouchi word or a ballot sequence) is a word in the letters 0, 1, 2, … every prefix of which contains the letter i at least as often as the letter i + 1.

theorem List.isLatticeWord_iff {r : List ℕ} : r.IsLatticeWord ↔ ∀ (p : List ℕ), p <+: r → ∀ (i : ℕ), count (i + 1) p ≤ count i p

Unfolds List.IsLatticeWord.

@[simp]

theorem List.isLatticeWord_nil : [].IsLatticeWord

The empty word is a lattice word.

theorem List.IsLatticeWord.of_prefix {r s : List ℕ} (h : r.IsLatticeWord) (hs : s <+: r) : s.IsLatticeWord

A prefix of a lattice word is a lattice word.

theorem List.IsLatticeWord.count_succ_le {r : List ℕ} (h : r.IsLatticeWord) (i : ℕ) : count (i + 1) r ≤ count i r

A lattice word contains each letter i at least as often as the letter i + 1.

theorem List.isLatticeWord_of_pairwise_le {r : List ℕ} (hr : Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) r) (hc : ∀ (i : ℕ), count (i + 1) r ≤ count i r) : r.IsLatticeWord

A weakly increasing word is a lattice word as soon as it contains each letter i at least as often as the letter i + 1: a prefix that already contains an i + 1 contains every i of the word.

theorem List.isLatticeWord_append_singleton {r : List ℕ} {k : ℕ} : (r ++ [k]).IsLatticeWord ↔ r.IsLatticeWord ∧ ∀ (i : ℕ), k = i + 1 → count (i + 1) r < count i r

A word ending in the letter k is a lattice word exactly when the rest of it is a lattice word which, if k = i + 1, contains k strictly fewer times than i.

def TauCeti.robinsonSchensted {α : Type u_1} [LinearOrder α] (w : List α) : List (List α) × List ℕ

The Robinson--Schensted correspondence of a word w₁ w₂ ⋯ wₙ: the rows of its insertion tableau (⋯((∅ ← w₁) ← w₂) ⋯) ← wₙ, together with its recording word, whose k-th letter is the row in which the insertion of wₖ adds its new cell.

@[simp]

theorem TauCeti.robinsonSchensted_nil {α : Type u_1} [LinearOrder α] : robinsonSchensted [] = ([], [])

The empty word has the empty tableau and the empty recording word.

@[simp]

theorem TauCeti.robinsonSchensted_append_singleton {α : Type u_1} [LinearOrder α] (w : List α) (x : α) : robinsonSchensted (w ++ [x]) = (rowInsert x (robinsonSchensted w).1, (robinsonSchensted w).2 ++ [rowInsertIndex x (robinsonSchensted w).1])

Appending a letter x to a word inserts x into its insertion tableau, and appends to its recording word the row of the new cell.

theorem TauCeti.isTableauRows_robinsonSchensted_fst {α : Type u_1} [LinearOrder α] (w : List α) : (robinsonSchensted w).1.IsTableauRows

The insertion tableau of a word is a tableau.

theorem TauCeti.flatten_robinsonSchensted_fst_perm {α : Type u_1} [LinearOrder α] (w : List α) : (robinsonSchensted w).1.flatten.Perm w

The insertion tableau has the letters of the word.

@[simp]

theorem TauCeti.length_robinsonSchensted_snd {α : Type u_1} [LinearOrder α] (w : List α) : (robinsonSchensted w).2.length = w.length

The recording word has one letter for each letter of the word.

theorem TauCeti.robinsonSchensted_snd_prefix_append {α : Type u_1} [LinearOrder α] (u v : List α) : (robinsonSchensted u).2 <+: (robinsonSchensted (u ++ v)).2

The recording word of a word extends the recording word of each of its prefixes.

theorem TauCeti.getElem_robinsonSchensted_snd {α : Type u_1} [LinearOrder α] (w : List α) (i : ℕ) (hi : i < (robinsonSchensted w).2.length) : (robinsonSchensted w).2[i] = rowInsertIndex w[i] (robinsonSchensted (List.take i w)).1

The i-th letter of the recording word is the row of the new cell when the i-th letter is inserted into the insertion tableau of the preceding letters.

theorem TauCeti.length_getD_robinsonSchensted_fst {α : Type u_1} [LinearOrder α] (w : List α) (i : ℕ) : ((robinsonSchensted w).1.getD i []).length = List.count i (robinsonSchensted w).2

The shape of the insertion tableau is the content of the recording word: row i of the insertion tableau has as many cells as the recording word has letters i.

theorem TauCeti.isLatticeWord_robinsonSchensted_snd {α : Type u_1} [LinearOrder α] (w : List α) : (robinsonSchensted w).2.IsLatticeWord

The recording word is a lattice word.

theorem TauCeti.robinsonSchensted_injective {α : Type u_1} [LinearOrder α] : Function.Injective robinsonSchensted

The Robinson--Schensted correspondence is injective: a word is determined by its insertion tableau and its recording word.

theorem TauCeti.exists_robinsonSchensted_eq_iff {α : Type u_1} [LinearOrder α] {p : List (List α) × List ℕ} : (∃ (w : List α), robinsonSchensted w = p) ↔ p.1.IsTableauRows ∧ p.2.IsLatticeWord ∧ ∀ (i : ℕ), (p.1.getD i []).length = List.count i p.2

The image of the Robinson--Schensted correspondence: a pair of a list of rows and a word of row indices consists of the insertion tableau and the recording word of some word exactly when the rows form a tableau, the word is a lattice word, and row i has as many cells as the word has letters i.

noncomputable def TauCeti.robinsonSchenstedEquiv {α : Type u_1} [LinearOrder α] : List α ≃ { p : List (List α) × List ℕ // p.1.IsTableauRows ∧ p.2.IsLatticeWord ∧ ∀ (i : ℕ), (p.1.getD i []).length = List.count i p.2 }

The Robinson--Schensted correspondence: inserting the letters of a word into the empty tableau and recording the rows of the new cells is a bijection from words onto the pairs of a tableau and a lattice word such that row i of the tableau has as many cells as the lattice word has letters i.

@[simp]

theorem TauCeti.robinsonSchenstedEquiv_apply_coe {α : Type u_1} [LinearOrder α] (w : List α) : ↑(robinsonSchenstedEquiv w) = robinsonSchensted w

robinsonSchenstedEquiv sends a word to its insertion tableau and recording word.