The Robinson--Schensted correspondence for permutations

The Robinson--Schensted correspondence sends a permutation of Fin n, written in one-line notation, to its insertion and recording tableaux. Both tableaux are standard, have the same shape, and every pair of standard tableaux of the same shape arises uniquely in this way.

This file packages the word-level correspondence TauCeti.robinsonSchenstedEquiv as the classical equivalence between permutations and pairs of standard Young tableaux. The insertion tableau is decoded from its rows using StandardYoungTableau.rowsEquiv; the recording tableau is decoded from the recording lattice word using StandardYoungTableau.latticeWordEquiv.

References

• W. Fulton, Young Tableaux, Cambridge University Press (1997), Section 4.1.
• B. E. Sagan, The Symmetric Group, second edition, Springer GTM 203 (2001), Section 3.1.

noncomputable def TauCeti.rsk (n : ℕ) : Equiv.Perm (Fin n) ≃ (μ : n.Partition) × StandardYoungTableau (YoungDiagram.ofPartition μ) × StandardYoungTableau (YoungDiagram.ofPartition μ)

The Robinson--Schensted correspondence for permutations: permutations of Fin n correspond to pairs of standard Young tableaux of the same shape, where the shape ranges over the partitions of n.

@[simp]

theorem Equiv.Perm.map_val_toRows_rsk_apply {n : ℕ} (σ : Perm (Fin n)) : List.map (List.map Fin.val) ((TauCeti.rsk n) σ).snd.1.toRows = List.map (List.map Fin.val) (TauCeti.robinsonSchensted (List.ofFn ⇑σ)).1

The entries in the rows of the insertion tableau are the entries produced by word-level Robinson--Schensted insertion. The Fin labels are compared through their natural-number values because the tableau labels are indexed by the cardinality of its inferred shape.

@[simp]

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

The recording tableau of a permutation has the recording word produced by word-level Robinson--Schensted insertion.

theorem Equiv.Perm.rowLens_ofPartition_rsk_apply {n : ℕ} (σ : Perm (Fin n)) : (YoungDiagram.ofPartition ((TauCeti.rsk n) σ).fst).rowLens = List.map List.length (TauCeti.robinsonSchensted (List.ofFn ⇑σ)).1

The shape of the tableaux in rsk n σ is the row-length shape of the insertion tableau.