Beta-numbers of a Young diagram

Fix a Young diagram μ and a bound r on its number of rows. The i-th beta-number YoungDiagram.betaNumber μ r i = μ.rowLen i + (r - 1 - i) is the length of row i plus the number r - 1 - i of rows of the bounding r-row strip that lie below it. Adding that shift to the weakly decreasing row lengths makes the beta-numbers strictly decrease across the indices i < j < r inside the bound, so those r numbers are pairwise distinct; that is the whole point of the construction. This file also records that the natural-number product of their differences casts to the corresponding integer product.

Beta-numbers are the bookkeeping device behind the Frobenius determinant formula and the Frame-Robinson-Thrall route to the hook-length formula. Their relation to hook lengths --- for the exact row count r = μ.colLen 0 the beta-numbers of the nonempty rows i < μ.colLen 0 are the hook lengths of the first column, and in general they describe a row of hook lengths --- needs the hook-length API and is developed in TauCeti/Combinatorics/Young/HookLength/BetaNumbers.lean.

Main definitions

• YoungDiagram.betaNumber: the beta-numbers of μ relative to a bound r on its number of rows.

Main results

• YoungDiagram.betaNumber_lt_betaNumber: the beta-numbers strictly decrease across the indices i < j < r inside the bound.
• YoungDiagram.injOn_betaNumber: the beta-numbers of the indices i < r are pairwise distinct.
• YoungDiagram.strictAnti_betaNumber: the beta-numbers relative to r are strictly antitone on Fin r, and YoungDiagram.exists_eq_betaNumber_of_strictAnti: conversely every strictly antitone Fin r → ℕ is the sequence of beta-numbers of a diagram with at most r rows.
• YoungDiagram.eq_of_betaNumber_eq: a Young diagram with at most r rows is determined by its beta-numbers of the indices i < r.
• YoungDiagram.sum_betaNumber: the beta-numbers of a diagram with at most r rows total its number of cells plus the staircase ∑_j (r - 1 - j).
• YoungDiagram.cast_prod_betaNumber_sub: casts the product of beta-number differences from ℕ to ℤ.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 1, Example 1, for beta-numbers and the description of a row of hook lengths by them.

def YoungDiagram.betaNumber (μ : YoungDiagram) (r i : ℕ) : ℕ

The i-th beta-number of a Young diagram μ, relative to a bound r on its number of rows: the length of row i plus the number r - 1 - i of rows of the bounding r-row strip that lie below it. For r = μ.colLen 0 and a nonempty row i < μ.colLen 0 this is the hook length of the first cell of row i; see YoungDiagram.betaNumber_eq_hookLength.

Equations

• μ.betaNumber r i = μ.rowLen i + (r - 1 - i)

theorem YoungDiagram.betaNumber_def (μ : YoungDiagram) (r i : ℕ) : μ.betaNumber r i = μ.rowLen i + (r - 1 - i)

theorem YoungDiagram.betaNumber_lt_betaNumber {r i j : ℕ} (μ : YoungDiagram) (hij : i < j) (hj : j < r) : μ.betaNumber r j < μ.betaNumber r i

The beta-numbers strictly decrease along the rows, because the row lengths are weakly decreasing while the shifts r - 1 - i strictly decrease.

theorem YoungDiagram.strictAntiOn_betaNumber (μ : YoungDiagram) (r : ℕ) : StrictAntiOn (μ.betaNumber r) (Set.Iio r)

The beta-numbers of the rows inside the bound strictly decrease.

theorem YoungDiagram.injOn_betaNumber (μ : YoungDiagram) (r : ℕ) : Set.InjOn (μ.betaNumber r) (Set.Iio r)

The beta-numbers of the rows inside the bound are pairwise distinct.

theorem YoungDiagram.eq_of_betaNumber_eq {μ : YoungDiagram} {r : ℕ} {ν : YoungDiagram} (hμ : μ.colLen 0 ≤ r) (hν : ν.colLen 0 ≤ r) (h : ∀ i < r, μ.betaNumber r i = ν.betaNumber r i) : μ = ν

A Young diagram is determined by its beta-numbers: two diagrams with at most r rows whose beta-numbers relative to r agree at every index i < r are equal. Inside the bound the row lengths are recovered by subtracting the common shift r - 1 - i, and outside it both diagrams have empty rows.

theorem YoungDiagram.strictAnti_betaNumber (μ : YoungDiagram) (r : ℕ) : StrictAnti fun (j : Fin r) => μ.betaNumber r ↑j

The beta-numbers relative to a bound r strictly decrease along the indices Fin r.

theorem YoungDiagram.exists_eq_betaNumber_of_strictAnti {r : ℕ} {η : Fin r → ℕ} (hη : StrictAnti η) : ∃ (μ : YoungDiagram), μ.colLen 0 ≤ r ∧ ∀ (j : Fin r), μ.betaNumber r ↑j = η j

A strictly decreasing sequence of naturals is a sequence of beta-numbers. Every strictly antitone η : Fin r → ℕ is the sequence of beta-numbers relative to r of a Young diagram with at most r rows, unique by YoungDiagram.eq_of_betaNumber_eq. Strict decrease is exactly what makes the differences η j - (r - 1 - j) weakly decreasing and nonnegative, hence row lengths.

theorem YoungDiagram.sum_betaNumber (μ : YoungDiagram) {r : ℕ} (hμ : μ.colLen 0 ≤ r) : ∑ j : Fin r, μ.betaNumber r ↑j = μ.card + ∑ j : Fin r, (r - 1 - ↑j)

The beta-numbers of a diagram total its size plus the staircase. For a diagram with at most r rows the row lengths add up to the number of cells, and the shifts add up separately.

theorem YoungDiagram.cast_prod_betaNumber_sub (μ : YoungDiagram) (r : ℕ) : ↑(∏ k ∈ Finset.range r, ∏ l ∈ Finset.Ico (k + 1) r, (μ.betaNumber r k - μ.betaNumber r l)) = ∏ k ∈ Finset.range r, ∏ l ∈ Finset.Ico (k + 1) r, (↑(μ.betaNumber r k) - ↑(μ.betaNumber r l))

The Vandermonde-style product of the differences of the beta-numbers is computed by the same formula over ℤ, the differences being nonnegative.