The Frobenius determinant formula and the hook-length formula

Let μ be a Young diagram with n = μ.card cells and let f^μ = TauCeti.standardCount μ be its number of standard Young tableaux. This file proves the multiplicative hook-length formula

f^μ * ∏ c ∈ μ.cells, hookLength μ c = n !

(TauCeti.standardCount_mul_prod_hookLength), the milestone of Layer 5 of the Schur--Weyl roadmap. It carries no division obligation. The familiar quotient form f^μ = n ! / ∏ hooks is derived from it at the end of the file, over ℕ in TauCeti.standardCount_eq_factorial_div_prod_hookLength and over a semifield of characteristic zero in TauCeti.cast_standardCount_eq_factorial_div_prod_hookLength; the ℕ-division is exact because the product of the hook lengths divides n ! (YoungDiagram.prod_hookLength_dvd_factorial), with f^μ as cofactor.

The route

Fix a bound r on the number of rows and write βᵢ = μ.rowLen i + (r - 1 - i) for the beta-numbers YoungDiagram.betaNumber μ r i, which strictly decrease across i < j < r. The hook lengths are already related to them by YoungDiagram.prod_hookLength_mul_prod_betaNumber_sub_eq_prod_factorial:

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

What remains, and is the substance of this file, is the Frobenius determinant formula

f^μ * ∏_{i < r} βᵢ ! = n ! * ∏_{i < j < r} (βᵢ - βⱼ)

(TauCeti.standardCount_mul_prod_factorial_betaNumber). Dividing one by the other cancels the Vandermonde-style product, which is positive, and leaves the hook-length formula.

The Frobenius formula is proved by induction on n along the corner recursion TauCeti.standardCount_eq_sum_corners, f^μ = ∑_{c a corner} f^{μ ∖ c}. Erasing a corner lowers the beta-number of its row by one and leaves the others alone (YoungDiagram.IsCorner.betaNumber_erase), and βᵢ ! = βᵢ * (βᵢ - 1) ! converts the induction hypothesis for μ ∖ c into a statement about μ. Summing it over the corners reduces the induction step to an identity between Vandermonde-style products,

∑_{i < r} βᵢ * ∏_{k < l < r} (β^{(i)}_k - β^{(i)}_l) = (∑_{i < r} βᵢ - ∑_{i < r} i) * ∏_{k < l < r} (β_k - β_l)

where β^{(i)} lowers βᵢ by one, which is TauCeti.sum_mul_prod_sub_update_sub_one. Two bookkeeping facts fit the two sides together. First, the rows of the corners inject into {0, …, r - 1}, because a corner is the last cell of its row; and a row i < r carrying no corner contributes nothing to the left-hand sum, since either βᵢ = 0 or βᵢ₊₁ = βᵢ - 1 with i + 1 < r, which puts a zero factor in its product. Second, ∑_{i < r} βᵢ - ∑_{i < r} i = n, because the row lengths sum to n and the shifts r - 1 - i are a reflection of 0, 1, …, r - 1.

Main results

• TauCeti.standardCount_mul_prod_factorial_betaNumber: the Frobenius determinant formula.
• TauCeti.standardCount_mul_prod_hookLength: the multiplicative hook-length formula.
• YoungDiagram.prod_hookLength_dvd_factorial: the product of the hook lengths divides n !.
• TauCeti.standardCount_eq_factorial_div_prod_hookLength and TauCeti.cast_standardCount_eq_factorial_div_prod_hookLength: the hook-length formula in quotient form, over ℕ and over a semifield of characteristic zero.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 1, Example 1, and Section 7, Example 6, for the beta-number route to the hook-length formula.
• B. E. Sagan, The Symmetric Group, Section 3.10.
• Schur--Weyl roadmap, Layer 5, whose hookLengthFormula milestone this closes.

Corners and beta-numbers

The Frobenius determinant formula

theorem TauCeti.standardCount_mul_prod_factorial_betaNumber (μ : YoungDiagram) {r : ℕ} (hr : μ.colLen 0 ≤ r) : standardCount μ * ∏ i ∈ Finset.range r, (μ.betaNumber r i).factorial = μ.card.factorial * ∏ k ∈ Finset.range r, ∏ l ∈ Finset.Ico (k + 1) r, (μ.betaNumber r k - μ.betaNumber r l)

The Frobenius determinant formula for the number f^μ of standard Young tableaux of shape μ: for any bound r on the number of rows, f^μ times the product of the factorials of the beta-numbers is μ.card ! times the product of their differences over the ordered pairs of rows.

The differences are differences of natural numbers, and are truncated at no ordered pair: the beta-numbers strictly decrease across k < l < r.

This is the multiplicative form of f^μ = n ! * ∏_{k < l} (β_k - β_l) / ∏_k β_k !, and carries no division obligation.

The hook-length formula

theorem TauCeti.standardCount_mul_prod_hookLength (μ : YoungDiagram) : standardCount μ * ∏ c ∈ μ.cells, μ.hookLength c = μ.card.factorial

The multiplicative hook-length formula. The number of standard Young tableaux of shape μ, times the product of the hook lengths of the cells of μ, is the factorial of the number of cells.

The quotient form f^μ = μ.card ! / ∏ hooks is derived from it below, in TauCeti.standardCount_eq_factorial_div_prod_hookLength.

The quotient form

theorem TauCeti.standardCount_eq_factorial_div_prod_hookLength (μ : YoungDiagram) : standardCount μ = μ.card.factorial / ∏ c ∈ μ.cells, μ.hookLength c

The hook-length formula in quotient form: the number of standard Young tableaux of shape μ is μ.card ! divided by the product of the hook lengths.

The division is exact: the product of the hook lengths divides μ.card !, by YoungDiagram.prod_hookLength_dvd_factorial.

theorem TauCeti.cast_standardCount_eq_factorial_div_prod_hookLength {K : Type u_1} [Semifield K] [CharZero K] (μ : YoungDiagram) : ↑(standardCount μ) = ↑μ.card.factorial / ∏ c ∈ μ.cells, ↑(μ.hookLength c)

The hook-length formula over a semifield of characteristic zero, in the familiar quotient form f^μ = n ! / ∏ hooks. The denominator is nonzero because every hook length is positive.

theorem YoungDiagram.prod_hookLength_dvd_factorial (μ : YoungDiagram) : ∏ c ∈ μ.cells, μ.hookLength c ∣ μ.card.factorial

The product of the hook lengths divides n !, the cofactor being the number f^μ of standard Young tableaux of the shape. This is the divisibility that makes the quotient form TauCeti.standardCount_eq_factorial_div_prod_hookLength of the hook-length formula an exact identity rather than a truncated one.