The Weyl dimension formula for SO (2n + 1)

The irreducible representations of the odd special orthogonal group SO (2n + 1) are indexed by the partitions λ₁ ≥ ⋯ ≥ λₙ ≥ 0 with at most n parts. The positive roots of type Bₙ are eᵢ ± eⱼ for i < j and eᵢ, and the half-sum of the positive roots is ρ = (n - 1/2, n - 3/2, …, 1/2), so with lᵢ = λᵢ + n - i - 1/2 the entries of λ + ρ and rᵢ = n - i - 1/2 those of ρ (indexing from 0), the Weyl dimension formula reads

dim V_λ = ∏_{i < n} lᵢ / rᵢ · ∏_{i < j < n} (lᵢ² - lⱼ²) / (rᵢ² - rⱼ²).

This file builds the right-hand side as a natural number. As for Sp 2n (TauCeti.symplecticWeylDimension), that is a step in its own right: the factors are rational, and neither the integrality nor the positivity of the product is visible from the formula.

The entries of λ + ρ are half-integers, so the file works with the integers xᵢ = λᵢ + n - 1 - i = lᵢ - 1/2, the sequence TauCeti.orthogonalRhoShift it shares with SO (2n). In these, 2lᵢ = 2xᵢ + 1 and lᵢ² - lⱼ² = (xᵢ - xⱼ)(xᵢ + xⱼ + 1), so the numerator TauCeti.oddOrthogonalWeylDimensionNumerator is ∏ᵢ (2xᵢ + 1) · ∏_{i < j} (xᵢ - xⱼ)(xᵢ + xⱼ + 1), the product of the pairings of λ + ρ with the positive roots, each pairing with a short root eᵢ doubled. The denominator is its value at λ = 0, which is 1! · 3! ⋯ (2n - 1)! (TauCeti.oddOrthogonalWeylDimensionNumerator_bot), the same as for Sp 2n. Integrality is TauCeti.prod_factorial_dvd_prod_two_mul_add_one_mul_prod_sub_mul_add_add_one: the factors (xᵢ - xⱼ)(xᵢ + xⱼ + 1) are the differences of the values xᵢ (xᵢ + 1), and in their Vandermonde determinant, weighted by the 2xᵢ + 1, the column of (x (x + 1))^k may be replaced by the column of (2x + 1) ∏_{c < k} (x - c)(x + c + 1), a sum of two products of 2k + 1 consecutive integers. The same polynomial evaluates each row of the numerator once the rows below it are those of ρ - 1/2, which computes the denominator and the one-row weights.

A Young diagram μ is read through its first n rows (TauCeti.oddOrthogonalWeylDimension_congr). When μ has at most n rows it is a dominant weight of SO (2n + 1), and the value is the dimension of the corresponding irreducible representation; the identification with that dimension is downstream of the highest-weight classification. The spin representations of Spin (2n + 1), whose highest weights have half-integral entries, are not indexed by Young diagrams and are not covered here.

Main definitions

• TauCeti.oddOrthogonalWeylDimensionNumerator: the product ∏ᵢ (2xᵢ + 1) · ∏_{i < j} (xᵢ - xⱼ)(xᵢ + xⱼ + 1).
• TauCeti.oddOrthogonalWeylDimension: the dimension predicted by the Weyl dimension formula.

Main results

• TauCeti.oddOrthogonalWeylDimension_mul_prod_factorial: the defining identity, division-free.
• TauCeti.oddOrthogonalWeylDimension_eq_prod_prod_div: the product form of the formula, over ℚ.
• TauCeti.oddOrthogonalWeylDimension_pos: the dimension is positive.
• TauCeti.oddOrthogonalWeylDimension_congr: the dimension reads only the first n rows.
• TauCeti.oddOrthogonalWeylDimension_eq_choose_add_choose_of_colLen_le_one: for SO (2n + 3), a one-row weight (d, 0, …, 0) has dimension (d + 2n + 1).choose (2n + 1) + (d + 2n).choose (2n + 1), that of the space of harmonic polynomials of degree d in 2n + 3 variables; in particular TauCeti.oddOrthogonalWeylDimension_bot, the trivial representation has dimension 1.
• TauCeti.oddOrthogonalWeylDimension_one_eq_two_mul_rowLen_add_one: for SO 3 the formula reads 2d + 1.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §24.2.

def TauCeti.oddOrthogonalWeylDimensionNumerator (n : ℕ) (μ : YoungDiagram) : ℤ

The numerator of the odd orthogonal Weyl dimension formula: with xᵢ = μᵢ + n - 1 - i, the product ∏_{i < n} (2xᵢ + 1) · ∏_{i < j < n} (xᵢ - xⱼ)(xᵢ + xⱼ + 1) of the pairings of μ + ρ with the positive roots eᵢ ± eⱼ and eᵢ of type Bₙ, each pairing with a short root eᵢ doubled to clear the half.

theorem TauCeti.oddOrthogonalWeylDimensionNumerator_eq_prod_prod (n : ℕ) (μ : YoungDiagram) : oddOrthogonalWeylDimensionNumerator n μ = ∏ i ∈ Finset.range n, (2 * orthogonalRhoShift n μ i + 1) * ∏ j ∈ Finset.Ico (i + 1) n, (orthogonalRhoShift n μ i - orthogonalRhoShift n μ j) * (orthogonalRhoShift n μ i + orthogonalRhoShift n μ j + 1)

The numerator as a double product: the defining equation of TauCeti.oddOrthogonalWeylDimensionNumerator, the form every computation with it starts from.

theorem TauCeti.oddOrthogonalWeylDimensionNumerator_pos (n : ℕ) (μ : YoungDiagram) : 0 < oddOrthogonalWeylDimensionNumerator n μ

Every factor of the numerator is positive.

theorem TauCeti.prod_factorial_dvd_oddOrthogonalWeylDimensionNumerator (n : ℕ) (μ : YoungDiagram) : ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial ∣ oddOrthogonalWeylDimensionNumerator n μ

Integrality of the odd orthogonal Weyl dimension formula: 1! · 3! ⋯ (2n - 1)! divides the numerator.

@[simp]

theorem TauCeti.oddOrthogonalWeylDimensionNumerator_bot (n : ℕ) : oddOrthogonalWeylDimensionNumerator n ⊥ = ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial

The value of the numerator at μ = 0, the denominator of the Weyl dimension formula: at ρ - 1/2 = (n - 1, …, 0) the row i is (2k + 1)! with k = n - 1 - i, so the numerator is 1! · 3! ⋯ (2n - 1)!.

def TauCeti.oddOrthogonalWeylDimension (n : ℕ) (μ : YoungDiagram) : ℕ

The odd orthogonal Weyl dimension of a Young diagram μ, read through its first n rows: the value

∏_{i < n} lᵢ / rᵢ · ∏_{i < j < n} (lᵢ² - lⱼ²) / (rᵢ² - rⱼ²), lᵢ = μᵢ + n - i - 1/2, rᵢ = n - i - 1/2,

of the Weyl dimension formula for SO (2n + 1). For μ with at most n rows it is the dimension of the irreducible representation of SO (2n + 1) with highest weight μ. The quotient is taken once, of TauCeti.oddOrthogonalWeylDimensionNumerator by 1! · 3! ⋯ (2n - 1)!; TauCeti.oddOrthogonalWeylDimension_eq_prod_prod_div recovers the term-by-term form over ℚ.

theorem TauCeti.oddOrthogonalWeylDimension_mul_prod_factorial (n : ℕ) (μ : YoungDiagram) : ↑(oddOrthogonalWeylDimension n μ) * ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial = oddOrthogonalWeylDimensionNumerator n μ

The defining identity of TauCeti.oddOrthogonalWeylDimension, in division-free form: the dimension times 1! · 3! ⋯ (2n - 1)! is the numerator.

theorem TauCeti.oddOrthogonalWeylDimension_pos (n : ℕ) (μ : YoungDiagram) : 0 < oddOrthogonalWeylDimension n μ

The odd orthogonal Weyl dimension is positive.

theorem TauCeti.oddOrthogonalWeylDimension_eq_prod_prod_div (n : ℕ) (μ : YoungDiagram) : ↑(oddOrthogonalWeylDimension n μ) = ∏ i ∈ Finset.range n, (↑(μ.rowLen i) + ↑n - ↑i - 1 / 2) / (↑n - ↑i - 1 / 2) * ∏ j ∈ Finset.Ico (i + 1) n, ((↑(μ.rowLen i) + ↑n - ↑i - 1 / 2) ^ 2 - (↑(μ.rowLen j) + ↑n - ↑j - 1 / 2) ^ 2) / ((↑n - ↑i - 1 / 2) ^ 2 - (↑n - ↑j - 1 / 2) ^ 2)

The Weyl dimension formula for SO (2n + 1) in its product form: over ℚ, with lᵢ = μᵢ + n - i - 1/2 and rᵢ = n - i - 1/2 the entries of μ + ρ and of ρ, the dimension is

∏_{i < n} lᵢ / rᵢ · ∏_{i < j < n} (lᵢ² - lⱼ²) / (rᵢ² - rⱼ²).

theorem TauCeti.oddOrthogonalWeylDimensionNumerator_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : oddOrthogonalWeylDimensionNumerator n μ = oddOrthogonalWeylDimensionNumerator n ν

The numerator reads only the first n rows: two diagrams whose rows 0, …, n - 1 have the same lengths have the same numerator.

theorem TauCeti.oddOrthogonalWeylDimension_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : oddOrthogonalWeylDimension n μ = oddOrthogonalWeylDimension n ν

The odd orthogonal Weyl dimension reads only the first n rows: two diagrams whose rows 0, …, n - 1 have the same lengths have the same dimension.

theorem TauCeti.oddOrthogonalWeylDimension_eq_choose_add_choose_of_colLen_le_one (n : ℕ) (μ : YoungDiagram) (h : μ.colLen 0 ≤ 1) : oddOrthogonalWeylDimension (n + 1) μ = (μ.rowLen 0 + 2 * n + 1).choose (2 * n + 1) + (μ.rowLen 0 + 2 * n).choose (2 * n + 1)

One-row weights: if μ has at most one row, of length d, then the odd orthogonal Weyl dimension for SO (2n + 3) is (d + 2n + 1).choose (2n + 1) + (d + 2n).choose (2n + 1), the dimension of the space of harmonic polynomials of degree d in 2n + 3 variables, on which SO (2n + 3) acts irreducibly.

@[simp]

theorem TauCeti.oddOrthogonalWeylDimension_zero (μ : YoungDiagram) : oddOrthogonalWeylDimension 0 μ = 1

The group SO 1 is trivial, and so is the formula: an empty product.

@[simp]

theorem TauCeti.oddOrthogonalWeylDimension_bot (n : ℕ) : oddOrthogonalWeylDimension n ⊥ = 1

The trivial representation: the empty diagram has odd orthogonal Weyl dimension 1.

@[simp]

theorem TauCeti.oddOrthogonalWeylDimension_one_eq_two_mul_rowLen_add_one (μ : YoungDiagram) : oddOrthogonalWeylDimension 1 μ = 2 * μ.rowLen 0 + 1

The SO 3 case: the irreducible representation with highest weight (d) has dimension 2d + 1. The formula reads only the first row.