The symmetry of the Robinson--Schensted correspondence

Schützenberger's symmetry theorem: the Robinson--Schensted correspondence of the inverse permutation σ⁻¹ is that of σ with the insertion and recording tableaux exchanged, Equiv.Perm.rsk_inv.

The proof is Fomin's growth-diagram argument. For a word w of distinct letters, consider the insertion tableaux G(i, k) of the subwords formed by those of the first i letters whose value is below k. Passing from G(i, k) to G(i + 1, k) adds at most one cell, in the row where the i-th letter is inserted; passing from G(i, k) to G(i, k + 1) adds at most one cell, the cell of the letter k. Label each edge of the (i, k) grid by the row of the added cell, if any. The comparison TauCeti.rowInsert_appendToRow of inserting a letter into a tableau with and without a strictly larger letter at the end of one of its rows shows that the labels of the top and right edges of each unit square are given by Fomin's local rule from the labels of its bottom and left edges, and this rule is symmetric under exchanging the two. Exchanging positions and values transposes the grid, so the recording word of σ⁻¹, read off the top edge of the transposed grid, lists the rows of the labels of the insertion tableau of σ, read off the right edge of the original grid.

Main results

• Equiv.Perm.findIdx?_robinsonSchensted_ofFn_eq_some: the label k lies in row r of the insertion tableau of σ, where r is the k-th letter of the recording word of σ⁻¹.
• Equiv.Perm.rowWord_snd_fst_rsk_apply: the row word of the insertion tableau of σ is the recording word of σ⁻¹.
• Equiv.Perm.rsk_inv: rsk n σ⁻¹ exchanges the two tableaux of rsk n σ.

References

• M.-P. Schützenberger, Quelques remarques sur une construction de Schensted, Math. Scand. 12 (1963), 117--128.
• S. Fomin, Schensted algorithms for dual graded graphs, J. Algebraic Combin. 4 (1995), 5--45.
• R. P. Stanley, Enumerative Combinatorics, Volume 2, Cambridge University Press (1999), Section 7.13.

The growth diagram of a word of distinct letters

theorem Equiv.Perm.findIdx?_robinsonSchensted_ofFn_eq_some {n : ℕ} (σ : Perm (Fin n)) (k : Fin n) : List.findIdx? (fun (row : List (Fin n)) => decide (k ∈ row)) (TauCeti.robinsonSchensted (List.ofFn ⇑σ)).1 = some (TauCeti.robinsonSchensted (List.ofFn ⇑σ⁻¹)).2[↑k]

The symmetry of the Robinson--Schensted correspondence, at the level of words: the label k lies in the row of the insertion tableau of σ given by the k-th letter of the recording word of σ⁻¹.

theorem Equiv.Perm.rowWord_snd_fst_rsk_apply {n : ℕ} (σ : Perm (Fin n)) : ((TauCeti.rsk n) σ).snd.1.rowWord = (TauCeti.robinsonSchensted (List.ofFn ⇑σ⁻¹)).2

The insertion tableau of σ has the recording word of σ⁻¹ as its row word.

theorem Equiv.Perm.rsk_inv {n : ℕ} (σ : Perm (Fin n)) : (TauCeti.rsk n) σ⁻¹ = ⟨((TauCeti.rsk n) σ).fst, (((TauCeti.rsk n) σ).snd.2, ((TauCeti.rsk n) σ).snd.1)⟩

Schützenberger's symmetry theorem. The Robinson--Schensted correspondence of the inverse permutation exchanges the insertion and recording tableaux.