Hooks and hook lengths of a Young diagram

The hook of a cell c of a Young diagram μ consists of c itself, the cells of μ strictly to the right of c in its row (its arm), and the cells of μ strictly below c in its column (its leg). Its cardinality is the hook length hookLength μ c, the quantity appearing in the hook-length formula f^μ · ∏_{c ∈ μ} hookLength μ c = μ.card !.

This file defines YoungDiagram.arm, YoungDiagram.leg and YoungDiagram.hook as finite sets of cells, together with the numerical armLength, legLength and hookLength, and proves that the cardinalities agree. The basic theory is then developed: transposition exchanges arms and legs, hook lengths strictly decrease along a row and down a column, a cell has hook length 1 exactly when it is a corner of the diagram, and the product of the hook lengths of a diagram with a single row (or a single column) is μ.card !.

The arm, the leg and the hook of a cell c are cut out of μ, so all three are empty apart from c itself when c ∉ μ; in that case hookLength μ c = 1. The lemmas below that would be false for such a junk value carry the hypothesis c ∈ μ explicitly.

Main definitions

• YoungDiagram.hook: the hook of a cell, as a Finset (ℕ × ℕ).
• YoungDiagram.hookLength: the hook length of a cell, armLength + legLength + 1.

Main results

• YoungDiagram.card_hook: the hook of a cell has hookLength many elements.
• YoungDiagram.hookLength_transpose: transposition preserves hook lengths.
• YoungDiagram.hookLength_eq_one_iff: a cell has hook length 1 exactly when neither the cell to its right nor the cell below it lies in the diagram; for a cell of the diagram this says that it is a corner, which is YoungDiagram.isCorner_iff_hookLength_eq_one.
• YoungDiagram.prod_hookLength_eq_factorial_of_colLen_le_one: the hook lengths of a one-row diagram multiply to μ.card !.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 1, Example 1, where the arm, leg and hook lengths of a cell are introduced.
• B. E. Sagan, The Symmetric Group, Section 3.10, for the hook-length formula.
• Schur--Weyl roadmap, Layer 5, where hookLength is a pinned, individually claimable target. Its milestone standardCount μ * ∏ c ∈ μ.cells, hookLength μ c = μ.card ! is stated in terms of Layer 0's standardCount, so nothing here depends on the Specht modules of Layer 3; the Specht-module dimension form is a derived corollary of Layer 5's separate standard-basis target.

Arms, legs and hooks

def YoungDiagram.arm (μ : YoungDiagram) (c : ℕ × ℕ) : Finset (ℕ × ℕ)

The arm of the cell c in the Young diagram μ: the cells of μ lying strictly to the right of c in the same row.

Equations

• μ.arm c = Finset.map { toFun := fun (j : ℕ) => (c.1, j), inj' := ⋯ } (Finset.Ico (c.2 + 1) (μ.rowLen c.1))

def YoungDiagram.leg (μ : YoungDiagram) (c : ℕ × ℕ) : Finset (ℕ × ℕ)

The leg of the cell c in the Young diagram μ: the cells of μ lying strictly below c in the same column.

Equations

• μ.leg c = Finset.map { toFun := fun (i : ℕ) => (i, c.2), inj' := ⋯ } (Finset.Ico (c.1 + 1) (μ.colLen c.2))

def YoungDiagram.hook (μ : YoungDiagram) (c : ℕ × ℕ) : Finset (ℕ × ℕ)

The hook of the cell c in the Young diagram μ: the cell itself together with its arm and its leg.

Equations

• μ.hook c = insert c (μ.arm c ∪ μ.leg c)

@[simp]

theorem YoungDiagram.mem_arm {μ : YoungDiagram} {c d : ℕ × ℕ} : d ∈ μ.arm c ↔ d ∈ μ ∧ d.1 = c.1 ∧ c.2 < d.2

@[simp]

theorem YoungDiagram.mem_leg {μ : YoungDiagram} {c d : ℕ × ℕ} : d ∈ μ.leg c ↔ d ∈ μ ∧ d.2 = c.2 ∧ c.1 < d.1

@[simp]

theorem YoungDiagram.mem_hook {μ : YoungDiagram} {c d : ℕ × ℕ} : d ∈ μ.hook c ↔ d = c ∨ d ∈ μ ∧ d.1 = c.1 ∧ c.2 < d.2 ∨ d ∈ μ ∧ d.2 = c.2 ∧ c.1 < d.1

theorem YoungDiagram.mem_hook_self {μ : YoungDiagram} {c : ℕ × ℕ} : c ∈ μ.hook c

theorem YoungDiagram.arm_subset_cells {μ : YoungDiagram} {c : ℕ × ℕ} : μ.arm c ⊆ μ.cells

theorem YoungDiagram.leg_subset_cells {μ : YoungDiagram} {c : ℕ × ℕ} : μ.leg c ⊆ μ.cells

theorem YoungDiagram.hook_subset_cells {μ : YoungDiagram} {c : ℕ × ℕ} (h : c ∈ μ) : μ.hook c ⊆ μ.cells

theorem YoungDiagram.notMem_arm_self {μ : YoungDiagram} {c : ℕ × ℕ} : c ∉ μ.arm c

theorem YoungDiagram.notMem_leg_self {μ : YoungDiagram} {c : ℕ × ℕ} : c ∉ μ.leg c

theorem YoungDiagram.disjoint_arm_leg {μ : YoungDiagram} {c : ℕ × ℕ} : Disjoint (μ.arm c) (μ.leg c)

Arm, leg and hook lengths

def YoungDiagram.armLength (μ : YoungDiagram) (c : ℕ × ℕ) : ℕ

The arm length of the cell c in the Young diagram μ: the number of cells of μ strictly to the right of c in the same row.

Equations

• μ.armLength c = μ.rowLen c.1 - c.2 - 1

def YoungDiagram.legLength (μ : YoungDiagram) (c : ℕ × ℕ) : ℕ

The leg length of the cell c in the Young diagram μ: the number of cells of μ strictly below c in the same column.

Equations

• μ.legLength c = μ.colLen c.2 - c.1 - 1

def YoungDiagram.hookLength (μ : YoungDiagram) (c : ℕ × ℕ) : ℕ

The hook length of the cell c in the Young diagram μ: the number of cells in its hook.

Equations

• μ.hookLength c = μ.armLength c + μ.legLength c + 1

theorem YoungDiagram.armLength_def (μ : YoungDiagram) (c : ℕ × ℕ) : μ.armLength c = μ.rowLen c.1 - c.2 - 1

The arm length of a cell counts the columns of its row beyond it.

theorem YoungDiagram.legLength_def (μ : YoungDiagram) (c : ℕ × ℕ) : μ.legLength c = μ.colLen c.2 - c.1 - 1

The leg length of a cell counts the rows of its column beyond it.

theorem YoungDiagram.hookLength_def (μ : YoungDiagram) (c : ℕ × ℕ) : μ.hookLength c = μ.armLength c + μ.legLength c + 1

The hook length of a cell is its arm length plus its leg length plus one, the cell itself.

@[simp]

theorem YoungDiagram.card_arm (μ : YoungDiagram) (c : ℕ × ℕ) : (μ.arm c).card = μ.armLength c

The arm of a cell has armLength many elements.

@[simp]

theorem YoungDiagram.card_leg (μ : YoungDiagram) (c : ℕ × ℕ) : (μ.leg c).card = μ.legLength c

The leg of a cell has legLength many elements.

@[simp]

theorem YoungDiagram.card_hook (μ : YoungDiagram) (c : ℕ × ℕ) : (μ.hook c).card = μ.hookLength c

The hook of a cell has hookLength many elements: the numerical definition of hookLength really does count the cells of the hook.

theorem YoungDiagram.hookLength_pos (μ : YoungDiagram) (c : ℕ × ℕ) : 0 < μ.hookLength c

theorem YoungDiagram.prod_hookLength_pos (μ : YoungDiagram) : 0 < ∏ d ∈ μ.cells, μ.hookLength d

Every hook length is positive, so the product of the hook lengths of a diagram is positive. This is what makes the quotient form of the hook-length formula meaningful.

theorem YoungDiagram.hookLength_le_card {μ : YoungDiagram} {c : ℕ × ℕ} (h : c ∈ μ) : μ.hookLength c ≤ μ.card

A cell of the diagram has hook length at most the size of the diagram.

Transposition

@[simp]

theorem YoungDiagram.arm_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.arm c = Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding (μ.leg c.swap)

Transposition exchanges arms with legs: the arm of c in μ.transpose is the reflection of the leg of c.swap in μ.

@[simp]

theorem YoungDiagram.leg_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.leg c = Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding (μ.arm c.swap)

Transposition exchanges legs with arms: the leg of c in μ.transpose is the reflection of the arm of c.swap in μ.

@[simp]

theorem YoungDiagram.hook_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.hook c = Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding (μ.hook c.swap)

Transposition reflects hooks: the hook of c in μ.transpose is the reflection of the hook of c.swap in μ.

@[simp]

theorem YoungDiagram.armLength_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.armLength c = μ.legLength c.swap

Transposition exchanges arm lengths with leg lengths.

@[simp]

theorem YoungDiagram.legLength_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.legLength c = μ.armLength c.swap

Transposition exchanges leg lengths with arm lengths.

@[simp]

theorem YoungDiagram.hookLength_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.hookLength c = μ.hookLength c.swap

Transposition preserves hook lengths: the hook length of c in μ.transpose is that of c.swap in μ.

theorem YoungDiagram.prod_hookLength_transpose (μ : YoungDiagram) : ∏ c ∈ μ.transpose.cells, μ.transpose.hookLength c = ∏ c ∈ μ.cells, μ.hookLength c

Transposing a Young diagram permutes its cells, and hence its hook lengths; in particular the product of all hook lengths is a transposition invariant.

Monotonicity along rows and columns

@[simp]

theorem YoungDiagram.armLength_eq_zero_iff {μ : YoungDiagram} {c : ℕ × ℕ} : μ.armLength c = 0 ↔ (c.1, c.2 + 1) ∉ μ

@[simp]

theorem YoungDiagram.legLength_eq_zero_iff {μ : YoungDiagram} {c : ℕ × ℕ} : μ.legLength c = 0 ↔ (c.1 + 1, c.2) ∉ μ

@[simp]

theorem YoungDiagram.hookLength_eq_one_iff {μ : YoungDiagram} {c : ℕ × ℕ} : μ.hookLength c = 1 ↔ (c.1, c.2 + 1) ∉ μ ∧ (c.1 + 1, c.2) ∉ μ

A cell has hook length 1 exactly when the cell to its right and the cell below it are both absent from the diagram; for a cell of μ this says that it is a corner.

theorem YoungDiagram.isCorner_iff_hookLength_eq_one {μ : YoungDiagram} {c : ℕ × ℕ} : μ.IsCorner c ↔ c ∈ μ ∧ μ.hookLength c = 1

The corners of μ are its cells of hook length 1.

theorem YoungDiagram.hookLength_lt_hookLength_of_col_lt (μ : YoungDiagram) {i j₁ j₂ : ℕ} (h : (i, j₂) ∈ μ) (hj : j₁ < j₂) : μ.hookLength (i, j₂) < μ.hookLength (i, j₁)

Hook lengths strictly decrease from left to right along a row.

theorem YoungDiagram.hookLength_lt_hookLength_of_row_lt (μ : YoungDiagram) {i₁ i₂ j : ℕ} (h : (i₂, j) ∈ μ) (hi : i₁ < i₂) : μ.hookLength (i₂, j) < μ.hookLength (i₁, j)

Hook lengths strictly decrease from top to bottom down a column.

Diagrams with a single row or a single column

A Young diagram μ has at most one row exactly when μ.colLen 0 ≤ 1. Its hook lengths are then μ.card, μ.card - 1, …, 1, so they multiply to μ.card !; the one-column case follows by transposition. These are the two instances of the multiplicative hook-length formula standardCount μ * ∏ c ∈ μ.cells, hookLength μ c = μ.card ! in which the number of standard Young tableaux is 1; that count is not computed here. The shapes themselves are described in TauCeti/Combinatorics/Young/Diagram.lean, by YoungDiagram.cells_eq_of_colLen_le_one and YoungDiagram.card_eq_rowLen_of_colLen_le_one.

theorem YoungDiagram.hookLength_eq_rowLen_sub_of_colLen_le_one {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) {j : ℕ} (hj : j < μ.rowLen 0) : μ.hookLength (0, j) = μ.rowLen 0 - j

theorem YoungDiagram.prod_hookLength_eq_factorial_of_colLen_le_one {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) : ∏ c ∈ μ.cells, μ.hookLength c = μ.card.factorial

The hook-length formula for a Young diagram with at most one row: the hook lengths multiply to μ.card !.

theorem YoungDiagram.prod_hookLength_eq_factorial_of_rowLen_le_one {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) : ∏ c ∈ μ.cells, μ.hookLength c = μ.card.factorial

The hook-length formula for a Young diagram with at most one column: the hook lengths multiply to μ.card !.