Rim hooks of a Young diagram

A rim hook (border strip, ribbon) of a Young diagram μ is a skew shape μ / ν that is edge-connected and contains no 2 × 2 block. Removing rim hooks is the recursion behind the Murnaghan--Nakayama rule for the characters of the symmetric group, and the same move read on beta-numbers is the abacus.

The definition, and why it is the geometric one

The rows of a skew shape are intervals: row i of μ / ν is the set of columns [ν.rowLen i, μ.rowLen i). So μ / ν is edge-connected exactly when the rows it meets form an interval and two consecutive such rows overlap in a column, ν.rowLen i < μ.rowLen (i + 1); and it contains no 2 × 2 block exactly when two consecutive such rows overlap in at most one column, μ.rowLen (i + 1) ≤ ν.rowLen i + 1. YoungDiagram.IsRimHook therefore asks for ν ≤ μ with ν ≠ μ, for the rows met by μ / ν to be Set.OrdConnected, and for μ.rowLen (i + 1) = ν.rowLen i + 1 at two consecutive rows the shape meets.

That the definition really says "connected, and no 2 × 2 block" is not left to the prose. The two geometric conditions are proved from it in YoungDiagram.IsRimHook.mem_succ_succ_of_notMem (no cell of μ / ν has its diagonal neighbour in μ / ν, which for a skew shape is exactly 2 × 2-freeness, since a 2 × 2 block contains such a pair) and YoungDiagram.IsRimHook.mem_succ_rowLen (consecutive rows met by the shape share a column, so the shape is connected), and YoungDiagram.isRimHook_of_forall recovers the definition from them.

Removing a rim hook is a move of one beta-number

Let μ / ν be a rim hook occupying the rows a ≤ i ≤ b. Its row lengths satisfy ν.rowLen i = μ.rowLen (i + 1) - 1 for a ≤ i < b, so the beta-numbers of ν relative to a bound r > b are those of μ with the value at a deleted, the values between shifted up by one index, and the single new value

ν.betaNumber r b = μ.betaNumber r a - (μ.card - ν.card).

Removing a rim hook of size s is thus exactly the move of one bead down s places on the abacus, and the height b - a of the rim hook, one less than the number of rows it meets, counts the beads the moving bead jumps over. Both statements are proved here: YoungDiagram.IsRimHook.card_add_betaNumber and YoungDiagram.IsRimHook.card_filter_betaNumber.

Main definitions

• YoungDiagram.IsRimHook: the skew shape μ / ν is a rim hook. As in YoungDiagram.InterlacedBy, the ambient shape is written first.
• YoungDiagram.rimHookRows: the rows met by μ / ν.
• YoungDiagram.rimHookHeight: one less than the number of rows met by μ / ν.

Main results

• YoungDiagram.IsCorner.isRimHook_erase and YoungDiagram.IsRimHook.exists_isCorner_of_card_succ: the rim hooks with one cell are exactly the erasures of corners.
• YoungDiagram.IsRimHook.mem_succ_succ_of_notMem, YoungDiagram.IsRimHook.mem_succ_rowLen and YoungDiagram.isRimHook_of_forall: the geometric reading of the definition.
• YoungDiagram.IsRimHook.exists_rimHookRows_eq_Icc: a rim hook meets a contiguous block of rows.
• YoungDiagram.IsRimHook.card_add_rowLen: the number of cells of a rim hook is μ.rowLen a - ν.rowLen b plus its height, stated without truncated subtraction.
• YoungDiagram.IsRimHook.card_add_betaNumber: removing a rim hook lowers one beta-number by the number of cells removed, with YoungDiagram.betaNumber_eq_of_notMem_rimHookRows and YoungDiagram.IsRimHook.betaNumber_eq_betaNumber_succ describing the other beta-numbers.
• YoungDiagram.IsRimHook.card_filter_betaNumber: the height of a rim hook is the number of beta-numbers of μ that the moved bead jumps over.
• YoungDiagram.IsRimHook.update_betaNumber_eq_comp_cycleIcc: the beta-numbers of ν with the bead of the bottom row raised are those of μ, rearranged by the cycle of the rows the hook meets, whose sign is (-1) to the height.
• YoungDiagram.exists_isRimHook_rimHookRows_eq_Icc, YoungDiagram.IsRimHook.betaNumber_ne_betaNumber_add and YoungDiagram.IsRimHook.eq_of_card_eq_of_rimHookRows_eq_Icc: conversely, raising a bead of ν to a free position adds a rim hook with that bottom row, every rim hook arises this way, and it is determined by its bottom row and size. So the rim hooks of size s that can be added to ν correspond to the beads of ν that can move up s places.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 1, Example 8, for border strips and their description by beta-numbers.
• B. E. Sagan, The Symmetric Group, Section 4.10, for rim hooks, their heights and the Murnaghan--Nakayama rule.
• Schur--Weyl roadmap, Layer 6, whose "rim hooks and Murnaghan--Nakayama" item this supplies the combinatorics of.

The definition

structure YoungDiagram.IsRimHook (μ ν : YoungDiagram) : Prop

The skew shape μ / ν is a rim hook (border strip): it is nonempty, edge-connected, and contains no 2 × 2 block. The conditions are recorded on row lengths, which is where the geometry lands for a skew shape; see YoungDiagram.IsRimHook.mem_succ_succ_of_notMem, YoungDiagram.IsRimHook.mem_succ_rowLen and YoungDiagram.isRimHook_of_forall for the equivalence with the geometric conditions. As in YoungDiagram.InterlacedBy, the ambient shape is written first.

• le : ν ≤ μ

  The removed shape is a sub-diagram.

• ne : ν ≠ μ

  The skew shape is nonempty.

• ordConnected : {i : ℕ | ν.rowLen i < μ.rowLen i}.OrdConnected

  The rows met by the skew shape form an interval, so the shape is connected across rows.

• rowLen_succ (i : ℕ) : ν.rowLen i < μ.rowLen i → ν.rowLen (i + 1) < μ.rowLen (i + 1) → μ.rowLen (i + 1) = ν.rowLen i + 1

  Two consecutive rows met by the skew shape overlap in exactly one column.

theorem YoungDiagram.IsRimHook.card_lt {μ ν : YoungDiagram} (h : μ.IsRimHook ν) : ν.card < μ.card

A rim hook has at least one cell.

The geometry: connected, and no 2 × 2 block

theorem YoungDiagram.IsRimHook.mem_succ_succ_of_notMem {μ ν : YoungDiagram} {i j : ℕ} (h : μ.IsRimHook ν) (hμ : (i, j) ∈ μ) (hν : (i, j) ∉ ν) (hμ' : (i + 1, j + 1) ∈ μ) : (i + 1, j + 1) ∈ ν

A rim hook contains no 2 × 2 block: the diagonal neighbour of a cell of μ / ν is never a cell of μ / ν. For a skew shape that is exactly 2 × 2-freeness, because μ and ν are lower sets, so a 2 × 2 block of μ / ν contains such a pair as its top-left and bottom-right cells.

theorem YoungDiagram.IsRimHook.mem_succ_rowLen {μ ν : YoungDiagram} {i : ℕ} (h : μ.IsRimHook ν) (hi : ν.rowLen i < μ.rowLen i) (hi' : ν.rowLen (i + 1) < μ.rowLen (i + 1)) : (i + 1, ν.rowLen i) ∈ μ ∧ (i + 1, ν.rowLen i) ∉ ν

A rim hook is connected across rows: if the rows i and i + 1 both meet μ / ν, then the cell (i + 1, ν.rowLen i) lies in μ / ν, directly below the cell (i, ν.rowLen i) of μ / ν. So consecutive rows met by the shape share a column.

theorem YoungDiagram.isRimHook_of_forall {μ ν : YoungDiagram} (hle : ν ≤ μ) (hne : ν ≠ μ) (hoc : {i : ℕ | ν.rowLen i < μ.rowLen i}.OrdConnected) (hblock : ∀ (i j : ℕ), (i, j) ∈ μ → (i, j) ∉ ν → (i + 1, j + 1) ∈ μ → (i + 1, j + 1) ∈ ν) (hconn : ∀ (i : ℕ), ν.rowLen i < μ.rowLen i → ν.rowLen (i + 1) < μ.rowLen (i + 1) → (i + 1, ν.rowLen i) ∈ μ) : μ.IsRimHook ν

The two geometric conditions characterize rim hooks: a nonempty skew shape μ / ν whose rows form an interval, which contains no 2 × 2 block and whose consecutive rows overlap, is a rim hook. This is the converse of YoungDiagram.IsRimHook.mem_succ_succ_of_notMem and YoungDiagram.IsRimHook.mem_succ_rowLen.

The rows a rim hook meets

def YoungDiagram.rimHookRows (μ ν : YoungDiagram) : Finset ℕ

The rows met by the skew shape μ / ν: the rows in which ν is strictly shorter than μ.

Equations

• μ.rimHookRows ν = {i ∈ Finset.range (μ.colLen 0) | ν.rowLen i < μ.rowLen i}

@[simp]

theorem YoungDiagram.mem_rimHookRows {μ ν : YoungDiagram} {i : ℕ} : i ∈ μ.rimHookRows ν ↔ ν.rowLen i < μ.rowLen i

theorem YoungDiagram.rowLen_eq_of_notMem_rimHookRows {μ ν : YoungDiagram} {i : ℕ} (hle : ν ≤ μ) (hi : i ∉ μ.rimHookRows ν) : ν.rowLen i = μ.rowLen i

Outside the rows it meets, the skew shape μ / ν is empty, so ν and μ agree there.

def YoungDiagram.rimHookHeight (μ ν : YoungDiagram) : ℕ

One less than the number of rows the skew shape μ / ν meets. For a rim hook this is its height, the sign exponent in the Murnaghan--Nakayama rule.

Equations

• μ.rimHookHeight ν = (μ.rimHookRows ν).card - 1

theorem YoungDiagram.rimHookHeight_eq_sub {μ ν : YoungDiagram} {a b : ℕ} (hab : μ.rimHookRows ν = Finset.Icc a b) : μ.rimHookHeight ν = b - a

The height of a rim hook occupying the rows a ≤ i ≤ b is b - a.

theorem YoungDiagram.IsRimHook.rimHookRows_nonempty {μ ν : YoungDiagram} (h : μ.IsRimHook ν) : (μ.rimHookRows ν).Nonempty

A rim hook meets at least one row.

theorem YoungDiagram.IsRimHook.exists_rimHookRows_eq_Icc {μ ν : YoungDiagram} (h : μ.IsRimHook ν) : ∃ (a : ℕ) (b : ℕ), a ≤ b ∧ μ.rimHookRows ν = Finset.Icc a b

A rim hook meets a contiguous block of rows.

theorem YoungDiagram.IsRimHook.le_of_rimHookRows_eq_Icc {μ ν : YoungDiagram} {a b : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) : a ≤ b

The block of rows a rim hook meets is a nonempty interval.

theorem YoungDiagram.rowLen_lt_of_rimHookRows_eq_Icc {μ ν : YoungDiagram} {a b i : ℕ} (hab : μ.rimHookRows ν = Finset.Icc a b) (hai : a ≤ i) (hib : i ≤ b) : ν.rowLen i < μ.rowLen i

Every row of the block a rim hook meets really is met by it.

The number of cells of a rim hook

theorem YoungDiagram.IsRimHook.card_add_rowLen {μ ν : YoungDiagram} {a b : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) : μ.card + ν.rowLen b + a = ν.card + μ.rowLen a + b

The number of cells of a rim hook. A rim hook meeting the rows a ≤ i ≤ b has (μ.rowLen a - ν.rowLen b) + (b - a) cells: the rows contribute the drop in row length from the top row of the hook to its bottom row, plus one extra cell for each step down. The statement is additive, so that no truncated subtraction appears.

theorem YoungDiagram.IsRimHook.card_add_rimHookHeight_lt {μ ν : YoungDiagram} (h : μ.IsRimHook ν) : ν.card + μ.rimHookHeight ν < μ.card

The height of a rim hook is smaller than its number of cells: a rim hook with s cells meets at most s rows.

Rim hooks with one cell are the erasures of corners

theorem YoungDiagram.IsCorner.isRimHook_erase {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) : μ.IsRimHook (μ.erase c)

Erasing a corner of μ leaves a rim hook. This is the nontrivial witness that YoungDiagram.IsRimHook is satisfiable, and the size-one case of the Murnaghan--Nakayama recursion.

theorem YoungDiagram.IsRimHook.exists_isCorner_of_card_succ {μ ν : YoungDiagram} (h : μ.IsRimHook ν) (hcard : ν.card + 1 = μ.card) : ∃ (c : ℕ × ℕ), μ.IsCorner c ∧ ν = μ.erase c

Conversely, a rim hook with a single cell is the erasure of a corner.

Removing a rim hook moves one beta-number

theorem YoungDiagram.betaNumber_eq_of_notMem_rimHookRows {μ ν : YoungDiagram} {i r : ℕ} (hle : ν ≤ μ) (hi : i ∉ μ.rimHookRows ν) : ν.betaNumber r i = μ.betaNumber r i

Outside the rows the skew shape μ / ν meets, the beta-numbers are unchanged.

theorem YoungDiagram.IsRimHook.betaNumber_eq_betaNumber_succ {μ ν : YoungDiagram} {a b i r : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) (hai : a ≤ i) (hib : i < b) (hbr : b < r) : ν.betaNumber r i = μ.betaNumber r (i + 1)

Inside the block of rows a rim hook meets, and above its bottom row, the beta-numbers of ν are those of μ shifted up by one index: the moving bead has vacated position a, and the beads it passes keep their values.

theorem YoungDiagram.IsRimHook.card_add_betaNumber {μ ν : YoungDiagram} {a b r : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) (hbr : b < r) : ν.card + μ.betaNumber r a = μ.card + ν.betaNumber r b

Removing a rim hook lowers one beta-number by the number of cells removed. The bead at position a moves down μ.card - ν.card places, landing at position b. The statement is additive, so that no truncated subtraction appears.

theorem YoungDiagram.IsRimHook.card_filter_betaNumber {μ ν : YoungDiagram} {a b r : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) (hbr : b < r) : {i ∈ Finset.range r | ν.betaNumber r b < μ.betaNumber r i ∧ μ.betaNumber r i < μ.betaNumber r a}.card = μ.rimHookHeight ν

The height of a rim hook counts the beads the moving bead jumps over. The beta-numbers of μ lying strictly between the new value ν.betaNumber r b and the old value μ.betaNumber r a are exactly those of the rows a < i ≤ b, so there are μ.rimHookHeight ν of them.

Adding a rim hook moves one bead up

theorem YoungDiagram.IsRimHook.update_betaNumber_eq_comp_cycleIcc {μ ν : YoungDiagram} {a b r : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) (hbr : b < r) : Function.update (fun (i : Fin r) => ν.betaNumber r ↑i) ⟨b, hbr⟩ (ν.betaNumber r b + (μ.card - ν.card)) = (fun (i : Fin r) => μ.betaNumber r ↑i) ∘ ⇑(⟨a, ⋯⟩.cycleIcc ⟨b, hbr⟩)

Adding a rim hook, read on all the beta-numbers at once. Let μ / ν be a rim hook meeting the rows a ≤ i ≤ b. Raising the beta-number of ν at the bottom row b by the number of cells of the hook gives the beta-numbers of μ, rearranged by the cycle a ↦ a + 1 ↦ ⋯ ↦ b ↦ a of the rows the hook meets. That cycle has sign (-1) ^ (b - a), the sign of the height of the hook (Fin.sign_cycleIcc_of_le).

theorem YoungDiagram.IsRimHook.lt_colLen_of_rimHookRows_eq_Icc {μ ν : YoungDiagram} {a b : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) : b < μ.colLen 0

The bottom row of a rim hook lies above the first empty row of the larger diagram.

theorem YoungDiagram.IsRimHook.eq_of_card_eq_of_rimHookRows_eq_Icc {ν : YoungDiagram} {b : ℕ} {μ₁ μ₂ : YoungDiagram} {a₁ a₂ : ℕ} (h₁ : μ₁.IsRimHook ν) (h₂ : μ₂.IsRimHook ν) (hcard : μ₁.card = μ₂.card) (hab₁ : μ₁.rimHookRows ν = Finset.Icc a₁ b) (hab₂ : μ₂.rimHookRows ν = Finset.Icc a₂ b) : μ₁ = μ₂

A rim hook is determined by its size and its bottom row. Two rim hooks μ₁ / ν and μ₂ / ν with the same number of cells and the same bottom row have the same larger diagram: by YoungDiagram.IsRimHook.update_betaNumber_eq_comp_cycleIcc the beta-numbers of μ₁ and of μ₂ are rearrangements of the same family, and a strictly decreasing family is determined by its set of values.

theorem YoungDiagram.IsRimHook.betaNumber_ne_betaNumber_add {μ ν : YoungDiagram} {a b i r : ℕ} (h : μ.IsRimHook ν) (hab : μ.rimHookRows ν = Finset.Icc a b) (hir : i < r) (hbr : b < r) : ν.betaNumber r i ≠ ν.betaNumber r b + (μ.card - ν.card)

The bead moved by a rim hook lands on a free position: raising the beta-number of ν at the bottom row of a rim hook μ / ν by the number of cells of the hook gives a value that is not a beta-number of ν. This is the converse of YoungDiagram.exists_isRimHook_rimHookRows_eq_Icc.

theorem YoungDiagram.exists_isRimHook_rimHookRows_eq_Icc {ν : YoungDiagram} {j r s : ℕ} (hν : ν.colLen 0 ≤ r) (hjr : j < r) (hfree : ∀ i < r, ν.betaNumber r i ≠ ν.betaNumber r j + s) : ∃ (μ : YoungDiagram), μ.IsRimHook ν ∧ μ.colLen 0 ≤ r ∧ μ.card = ν.card + s ∧ ∃ (a : ℕ), μ.rimHookRows ν = Finset.Icc a j

Adding a rim hook moves one bead up. Let ν have at most r rows, and suppose that raising its beta-number at the row j < r by s produces a value that is not already a beta-number of ν (which forces s > 0). Then there is a rim hook μ / ν with s cells whose bottom row is j, and μ still has at most r rows. This is the converse of YoungDiagram.IsRimHook.card_add_betaNumber: the moved bead lands at the first row a whose beta-number falls below the new value, and the rows a < i ≤ j are the beads it jumps over.