Documentation

TauCeti.Combinatorics.Young.HookLength.BetaNumbers

Beta-numbers and the hook-length product #

Fix a Young diagram μ and a bound r on its number of rows, and write βᵢ for the beta-number YoungDiagram.betaNumber μ r i = μ.rowLen i + (r - 1 - i) of row i, defined in TauCeti/Combinatorics/Young/BetaNumbers.lean. For the exact row count r = μ.colLen 0, and only for it, the beta-numbers of the nonempty rows are the hook lengths of the first column: for i < μ.colLen 0 the number βᵢ is the hook length of the cell (i, 0) at the head of row i (YoungDiagram.betaNumber_eq_hookLength). A larger bound r does not merely append entries to that list; it raises every beta-number of a nonempty row by the excess r - μ.colLen 0, and contributes the beta-numbers r - 1 - i of the empty rows i.

The theorem of this file is the identity

(∏_{c ∈ μ} hookLength μ c) * ∏_{i < j < r} (βᵢ - βⱼ) = ∏_{i < r} βᵢ !,

YoungDiagram.prod_hookLength_mul_prod_betaNumber_sub_eq_prod_factorial. It is the combinatorial half of the Frame-Robinson-Thrall route to the hook-length formula: the other half is the Frobenius determinant formula f^μ · ∏_{i < r} βᵢ ! = μ.card ! · ∏_{i < j < r} (βᵢ - βⱼ) for the number of standard Young tableaux, and multiplying the two gives the multiplicative hook-length formula f^μ · ∏_{c ∈ μ} hookLength μ c = μ.card !.

The file also records the one interaction between beta-numbers and corners, which the induction proving the Frobenius formula runs on: erasing a corner lowers the beta-number of its row by one and leaves the other beta-numbers alone.

The row-by-row mechanism #

Everything reduces to one statement about a single row i, proved in YoungDiagram.image_betaNumber_sub_hookLength_union_image_betaNumber: inside {0, …, βᵢ - 1} the numbers βᵢ - hookLength μ (i, c), for the cells (i, c) of row i, are exactly the numbers that are not a later beta-number βⱼ, i < j < r. Equivalently the hook lengths of row i are {1, …, βᵢ} with the differences βᵢ - βⱼ removed, which is the classical description of a row of hook lengths.

Two computations drive it. The first, YoungDiagram.hookLength_add_eq_betaNumber, is that

hookLength μ (i, c) + (c + r - μ.colLen c) = βᵢ,

so the complement βᵢ - hookLength μ (i, c) of a hook length in row i is c + r - μ.colLen c, a quantity that does not depend on the row at all. The second is that this quantity is never a beta-number βⱼ of an index j within the bound (YoungDiagram.betaNumber_sub_hookLength_ne_betaNumber, for j < r; beyond the bound βⱼ is the unshifted μ.rowLen j and the two can agree): the equation c + r - μ.colLen c = βⱼ says c + j + 1 = μ.colLen c + μ.rowLen j, which is too large by one when (j, c) ∈ μ and too small when (j, c) ∉ μ. Disjointness plus a count of both sides then forces the union to exhaust {0, …, βᵢ - 1}, with no separate surjectivity argument.

Main results #

References #

The complement of a hook length in its beta-number #

source
theorem YoungDiagram.hookLength_add_eq_betaNumber {μ : YoungDiagram} {r i c : ℕ} (hr : μ.colLen c ≤ r) (hc : c < μ.rowLen i) :
μ.hookLength (i, c) + (c + r - μ.colLen c) = μ.betaNumber r i

The complement of a hook length inside its beta-number. For a cell (i, c) of μ whose column is no longer than r, the hook length of (i, c) and the quantity c + r - μ.colLen c add up to the beta-number of row i. The second summand depends only on the column c, which is what makes the beta-number description of a row of hook lengths uniform in the row.

source
theorem YoungDiagram.hookLength_le_betaNumber {μ : YoungDiagram} {r i c : ℕ} (hr : μ.colLen c ≤ r) (hc : c < μ.rowLen i) :
μ.hookLength (i, c) ≤ μ.betaNumber r i

A hook length of row i is at most the beta-number of row i.

source
@[simp]
theorem YoungDiagram.betaNumber_sub_hookLength {μ : YoungDiagram} {r i c : ℕ} (hi : i < r) (hc : c < μ.rowLen i) :
μ.betaNumber r i - μ.hookLength (i, c) = c + r - μ.colLen c

The complement of a hook length of row i inside its beta-number, in the closed form supplied by YoungDiagram.hookLength_add_eq_betaNumber.

source
theorem YoungDiagram.betaNumber_sub_hookLength_ne_betaNumber {μ : YoungDiagram} {r i j c : ℕ} (hi : i < r) (hc : c < μ.rowLen i) (hj : j < r) :
μ.betaNumber r i - μ.hookLength (i, c) ≠ μ.betaNumber r j

The complements of the hook lengths of a row avoid the beta-numbers inside the bound. By YoungDiagram.betaNumber_sub_hookLength the claim is that c + r - μ.colLen c is never a beta-number βⱼ with j < r, that is, that c + j + 1 = μ.colLen c + μ.rowLen j is impossible: the right-hand side is at least c + j + 2 when the cell (j, c) lies in μ and at most c + j when it does not.

Beta-numbers as hook lengths #

source
@[simp]
theorem YoungDiagram.betaNumber_eq_hookLength {μ : YoungDiagram} {i : ℕ} (hi : i < μ.colLen 0) :
μ.betaNumber (μ.colLen 0) i = μ.hookLength (i, 0)

Relative to the exact number of rows, the beta-numbers of the nonempty rows of a Young diagram are the hook lengths of its first column: the c = 0, r = μ.colLen 0 case of YoungDiagram.hookLength_add_eq_betaNumber, where the complement c + r - μ.colLen c vanishes.

A row of hook lengths #

source
theorem YoungDiagram.image_betaNumber_sub_hookLength_union_image_betaNumber {μ : YoungDiagram} {r i : ℕ} (hr : μ.colLen 0 ≤ r) :
Finset.image (fun (c : ℕ) => μ.betaNumber r i - μ.hookLength (i, c)) (Finset.range (μ.rowLen i)) ∪ Finset.image (μ.betaNumber r) (Finset.Ico (i + 1) r) = Finset.range (μ.betaNumber r i)

The hook lengths of a single row, through beta-numbers. The complements βᵢ - hookLength μ (i, c) of the hook lengths of row i, together with the later beta-numbers βⱼ for i < j < r, partition {0, …, βᵢ - 1}.

Both families lie in {0, …, βᵢ - 1} and are disjoint, and they have μ.rowLen i and r - 1 - i members respectively, which is exactly βᵢ in total; so the inclusion is an equality.

source
theorem YoungDiagram.prod_hookLength_row_mul_prod_betaNumber_sub_eq_factorial {μ : YoungDiagram} {r i : ℕ} (hr : μ.colLen 0 ≤ r) :
(∏ c ∈ Finset.range (μ.rowLen i), μ.hookLength (i, c)) * ∏ j ∈ Finset.Ico (i + 1) r, (μ.betaNumber r i - μ.betaNumber r j) = (μ.betaNumber r i).factorial

The hook-length product identity for a single row. The hook lengths of row i, multiplied by the differences βᵢ - βⱼ between its beta-number and the later ones, give βᵢ !.

The hook-length product #

source
theorem YoungDiagram.prod_hookLength_mul_prod_betaNumber_sub_eq_prod_factorial {r : ℕ} (μ : YoungDiagram) (hr : μ.colLen 0 ≤ r) :
(∏ c ∈ μ.cells, μ.hookLength c) * ∏ i ∈ Finset.range r, ∏ j ∈ Finset.Ico (i + 1) r, (μ.betaNumber r i - μ.betaNumber r j) = ∏ i ∈ Finset.range r, (μ.betaNumber r i).factorial

The hook-length product identity. For a Young diagram μ with at most r rows, the product of all its hook lengths, multiplied by the Vandermonde-style product of the differences of its beta-numbers, is the product of the factorials of its beta-numbers.

Combined with the Frobenius determinant formula f^μ · ∏_{i < r} βᵢ ! = μ.card ! · ∏_{i < j < r} (βᵢ - βⱼ) for the number of standard Young tableaux, this gives the multiplicative hook-length formula.

Erasing a corner #

source
@[simp]
theorem YoungDiagram.IsCorner.betaNumber_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) (r i : ℕ) :
(μ.erase c).betaNumber r i = if c.1 = i then μ.betaNumber r i - 1 else μ.betaNumber r i

Erasing a corner lowers the beta-number of its row by one and leaves the other beta-numbers unchanged.