The hook-content formula

TauCeti.weylDimension is the value ∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i) of the Weyl dimension formula for GL n, a product over the pairs of rows. For a polynomial weight — a Young diagram μ with at most n rows, read as a weight by TauCeti.weightOfShape — the same number is a product over the cells of μ,

weylDimension (weightOfShape n μ) = ∏_{(i, j) ∈ μ} (n + j - i) / hookLength μ (i, j),

the hook-content formula: each cell contributes the quotient of n plus its content j - i by its hook length. This file proves it, in the division-free form TauCeti.weylDimension_weightOfShape_mul_prod_hookLength and in the quotient form TauCeti.weylDimension_weightOfShape_eq_prod_div, and extends it to an arbitrary dominant weight through the determinant twist (TauCeti.weylDimension_eq_prod_detShiftShape_div_hookLength).

The route

Both sides are compared against the beta-numbers βᵢ = μ.rowLen i + (n - 1 - i) of TauCeti/Combinatorics/Young/BetaNumbers.lean, which are the row lengths of μ shifted so as to be strictly decreasing. Three identities meet.

• The hook lengths, by YoungDiagram.prod_hookLength_mul_prod_betaNumber_sub_eq_prod_factorial: (∏_{c ∈ μ} hookLength c) · ∏_{i < j < n} (βᵢ - βⱼ) = ∏_{i < n} βᵢ !.
• The contents, proved here: row i contributes the cells (i, 0), …, (i, μ.rowLen i - 1), whose contents n + j - i are the μ.rowLen i consecutive integers starting at n - i, so that row contributes βᵢ ! / (n - 1 - i)! — and the missing factorials multiply to the superfactorial sf (n - 1). This is ∏_{c ∈ μ} (n + c₂ - c₁) · sf (n - 1) = ∏_{i < n} βᵢ !.
• The Weyl dimension, by TauCeti.weylDimension_mul_superFactorial: weylDimension · sf (n - 1) = ∏_{i < j < n} (βᵢ - βⱼ), once the numerator of the Weyl dimension formula is recognized as the Vandermonde-style product of the beta-numbers. That recognition is the identity βᵢ - βⱼ = (λᵢ - i) - (λⱼ - j): the two shifts differ by the constant n - 1.

Cancelling the (positive) superfactorial from (∏ contents) · sf = ∏ βᵢ ! = (∏ hooks) · ∏ (βᵢ - βⱼ) = (∏ hooks) · weylDimension · sf leaves the formula.

Main results

• TauCeti.weylDimension_weightOfShape_mul_prod_hookLength: the hook-content formula, in division-free form over ℕ.
• TauCeti.weylDimension_weightOfShape_eq_prod_div: its quotient form over ℚ.
• TauCeti.weylDimension_eq_prod_detShiftShape_div_hookLength: the quotient form for an arbitrary dominant weight, whose cells are those of its polynomial part TauCeti.DominantWeight.detShiftShape. The Weyl dimension is unchanged by a determinant twist, and so is each factor, the content and the hook length being read off the same diagram.

References

• Classical groups roadmap, Layer 5, "The Weyl dimension formula", which asks for the hook-content form of TauCeti.weylDimension and for the proof that the two agree.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Theorem 6.3 and Exercise 6.4, where the hook-content formula is stated for GL n.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 3, Example 4.

The product of the contents

The numerator of the Weyl dimension formula

The hook-content formula

theorem TauCeti.weylDimension_weightOfShape_mul_prod_hookLength {n : ℕ} {μ : YoungDiagram} (hμ : μ.colLen 0 ≤ n) : weylDimension (weightOfShape n μ) * ∏ c ∈ μ.cells, μ.hookLength c = ∏ c ∈ μ.cells, (n + c.2 - c.1)

The hook-content formula, in division-free form: for a Young diagram μ with at most n rows, the Weyl dimension of the weight it determines, times the product of the hook lengths of μ, is the product over the cells of μ of n plus the content j - i.

theorem TauCeti.weylDimension_weightOfShape_eq_prod_div {n : ℕ} {μ : YoungDiagram} (hμ : μ.colLen 0 ≤ n) : ↑(weylDimension (weightOfShape n μ)) = ∏ c ∈ μ.cells, (↑n + ↑c.2 - ↑c.1) / ↑(μ.hookLength c)

The hook-content formula, in its quotient form over ℚ: for a Young diagram μ with at most n rows, the Weyl dimension of the weight it determines is the product over the cells of μ of (n + j - i) / hookLength μ (i, j).

theorem TauCeti.weylDimension_eq_prod_detShiftShape_div_hookLength {n : ℕ} (l : DominantWeight n) : ↑(weylDimension l) = ∏ c ∈ l.detShiftShape.cells, (↑n + ↑c.2 - ↑c.1) / ↑(l.detShiftShape.hookLength c)

The hook-content formula for an arbitrary dominant weight. Every dominant weight of GL n is a determinant twist of a polynomial one, whose Young diagram is TauCeti.DominantWeight.detShiftShape; the twist changes neither the Weyl dimension nor the diagram, so the hook-content formula holds for every weight, read on that diagram.