The shuffle of a Young diagram in a box

Let μ be a Young diagram that fits in the box with m rows and n columns. The m numbers μ_{m-1-k} + k for k < m and the n numbers m + j - μ'ⱼ for j < n are complementary in {0, …, m + n - 1} (Macdonald (I.1.7)); the first family is the list of beta-numbers YoungDiagram.betaNumber μ m read upwards. Listing the first family and then the second is a permutation of {0, …, m + n - 1}, the box shuffle of μ. Each family increases, and an index k < m and an index m + j are out of order exactly when the cell (m - 1 - k, j) lies in μ. So the inversions of the box shuffle are in bijection with the cells of μ, and its sign is (-1)^{|μ|}.

This is the combinatorial input to the dual Jacobi--Trudi identity TauCeti.diagramSchurPoly_eq_det_esymmInt.

Main definitions

• YoungDiagram.boxShuffle: the box shuffle of μ with respect to m rows, as a function ℕ → ℕ.
• YoungDiagram.boxShufflePerm: the box shuffle of μ in the m × n box, as a permutation of Fin (m + n).

Main results

• YoungDiagram.boxShuffle_lt_boxShuffle_iff: the inversions of the box shuffle are the cells of μ.
• YoungDiagram.card_inversions_boxShufflePerm: the box shuffle has |μ| inversions.
• YoungDiagram.sign_boxShufflePerm: the sign of the box shuffle is (-1)^{|μ|}.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, (1.7).

def YoungDiagram.boxShuffle (μ : YoungDiagram) (m k : ℕ) : ℕ

The box shuffle attached to a diagram μ with at most m rows: an index k < m goes to μ_{m-1-k} + k, and an index m + j goes to m + j - μ'ⱼ.

theorem YoungDiagram.boxShuffle_def (μ : YoungDiagram) (m k : ℕ) : μ.boxShuffle m k = if k < m then μ.rowLen (m - (k + 1)) + k else k - μ.colLen (k - m)

theorem YoungDiagram.boxShuffle_lt_boxShuffle_iff (μ : YoungDiagram) (m : ℕ) {k k' : ℕ} (hm : μ.colLen 0 ≤ m) (hkk' : k < k') : μ.boxShuffle m k' < μ.boxShuffle m k ↔ k < m ∧ m ≤ k' ∧ (m - (k + 1), k' - m) ∈ μ

The inversions of the box shuffle are the cells of the diagram (Macdonald (I.1.7)).

noncomputable def YoungDiagram.boxShufflePerm {μ : YoungDiagram} {m n : ℕ} (hm : μ.colLen 0 ≤ m) (hn : μ.rowLen 0 ≤ n) : Equiv.Perm (Fin (m + n))

The box shuffle of a diagram in the box with m rows and n columns, as a permutation of Fin (m + n).

@[simp]

theorem YoungDiagram.boxShufflePerm_apply_val {μ : YoungDiagram} {m n : ℕ} (hm : μ.colLen 0 ≤ m) (hn : μ.rowLen 0 ≤ n) (k : Fin (m + n)) : ↑((boxShufflePerm hm hn) k) = μ.boxShuffle m ↑k

@[simp]

theorem YoungDiagram.card_inversions_boxShufflePerm {μ : YoungDiagram} {m n : ℕ} (hm : μ.colLen 0 ≤ m) (hn : μ.rowLen 0 ≤ n) : (Finset.inversions (⇑(boxShufflePerm hm hn)) Finset.univ).card = μ.card

The box shuffle has one inversion for each cell of the diagram.

@[simp]

theorem YoungDiagram.sign_boxShufflePerm {μ : YoungDiagram} {m n : ℕ} (hm : μ.colLen 0 ≤ m) (hn : μ.rowLen 0 ≤ n) : Equiv.Perm.sign (boxShufflePerm hm hn) = (-1) ^ μ.card

The sign of the box shuffle is (-1) to the number of cells of the diagram.