The Weyl dimension formula for SO (2n)

The positive roots of type Dₙ, the root system of the even special orthogonal group SO (2n), are eᵢ ± eⱼ for i < j, and the half-sum of the positive roots is ρ = (n - 1, n - 2, …, 0). With lᵢ = λᵢ + n - 1 - i the entries of λ + ρ and rᵢ = n - 1 - i those of ρ (indexing from 0), the Weyl dimension formula reads

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

This file builds the right-hand side as a natural number, as TauCeti.symplecticWeylDimension and TauCeti.oddOrthogonalWeylDimension do for Sp 2n and SO (2n + 1): the factors are rational, and neither the integrality nor the positivity of the product is visible from the formula.

The entries of λ + ρ are the integers TauCeti.orthogonalRhoShift n λ i = λᵢ + n - 1 - i, since the half-sum of the positive roots of type Dₙ is that of type Bₙ less 1/2 in every coordinate. The numerator TauCeti.evenOrthogonalWeylDimensionNumerator is the product ∏_{i < j} (lᵢ - lⱼ)(lᵢ + lⱼ) of the pairings of λ + ρ with the positive roots. The denominator is its value at λ = 0, which is 2!/2 · 4!/2 ⋯ (2n - 2)!/2 (TauCeti.evenOrthogonalWeylDimensionNumerator_bot). Integrality is TauCeti.prod_add_one_mul_factorial_dvd_prod_prod_sq_sub_sq: the factors lᵢ² - lⱼ² are the differences of the squares, and in their Vandermonde determinant the column of (l²)^k may be replaced by the column of the degree-2k polynomial ∏_{c < k} (l² - c²), twice which is the sum of the products of the 2k consecutive integers ending at l + k and at l + k - 1 (TauCeti.two_mul_prod_sq_sub_sq_eq, stated for ∏_{c ≤ k} and so with 2k + 2 factors). The same polynomial evaluates each row of the numerator once the rows below it are those of ρ, which computes the denominator and the one-row weights.

A Young diagram μ is read through its first n rows (TauCeti.evenOrthogonalWeylDimension_congr). When μ has at most n rows it is a dominant weight of SO (2n) with nonnegative last entry, and the value is the dimension of the corresponding irreducible representation; the identification with that dimension is downstream of the highest-weight classification. The dominant weights of type Dₙ are the λ₁ ≥ ⋯ ≥ λₙ₋₁ ≥ |λₙ|; the formula reads λₙ only through lₙ₋₁² = λₙ², so the weight with last entry -λₙ has the same value. The half-spin representations of Spin (2n), whose highest weights have half-integral entries, are not indexed by Young diagrams and are not covered here.

Main definitions

• TauCeti.evenOrthogonalWeylDimensionNumerator: the product ∏_{i < j} (lᵢ - lⱼ)(lᵢ + lⱼ).
• TauCeti.evenOrthogonalWeylDimension: the dimension predicted by the Weyl dimension formula.

Main results

• TauCeti.evenOrthogonalWeylDimension_mul_prod_add_one_mul_factorial: the defining identity, division-free.
• TauCeti.evenOrthogonalWeylDimension_eq_prod_prod_div: the product form of the formula, over ℚ.
• TauCeti.evenOrthogonalWeylDimension_pos: the dimension is positive.
• TauCeti.evenOrthogonalWeylDimension_congr: the dimension reads only the first n rows.
• TauCeti.evenOrthogonalWeylDimension_eq_choose_add_choose_of_colLen_le_one: for SO (2n + 4), a one-row weight (d, 0, …, 0) has dimension (d + 2n + 2).choose (2n + 2) + (d + 2n + 1).choose (2n + 2), that of the space of harmonic polynomials of degree d in 2n + 4 variables; and TauCeti.evenOrthogonalWeylDimension_bot, the trivial representation has dimension 1.
• TauCeti.evenOrthogonalWeylDimension_one: the irreducible representations of the circle group SO 2 are one-dimensional.
• TauCeti.evenOrthogonalWeylDimension_two: for SO 4 the formula reads (λ₁ - λ₂ + 1)(λ₁ + λ₂ + 1), the dimension of the exterior tensor product of the irreducible representations of dimensions λ₁ - λ₂ + 1 and λ₁ + λ₂ + 1 of the two factors of Spin 4 ≅ SU 2 × SU 2.

References

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

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

The numerator of the even orthogonal Weyl dimension formula: with lᵢ = μᵢ + n - 1 - i the entries of μ + ρ for the root system of type Dₙ, the product ∏_{i < j < n} (lᵢ - lⱼ)(lᵢ + lⱼ) of the pairings of μ + ρ with the positive roots eᵢ ± eⱼ.

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

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

theorem TauCeti.evenOrthogonalWeylDimensionNumerator_pos (n : ℕ) (μ : YoungDiagram) : 0 < evenOrthogonalWeylDimensionNumerator n μ

Every factor of the numerator is positive: the entries of μ + ρ are strictly decreasing and nonnegative.

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

Integrality of the even orthogonal Weyl dimension formula: 2!/2 · 4!/2 ⋯ (2n - 2)!/2, written ∏_{k < n - 1} (k + 1) (2k + 1)!, divides the numerator.

@[simp]

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

The value of the numerator at μ = 0, the denominator of the Weyl dimension formula: at ρ = (n - 1, …, 0) the row i is ∏_{c < k} (k² - c²) = (2k)! / 2 with k = n - 1 - i (and 1 for k = 0), so the numerator is 2!/2 · 4!/2 ⋯ (2n - 2)!/2.

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

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

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

of the Weyl dimension formula for SO (2n). For μ with at most n rows it is the dimension of the irreducible representation of SO (2n) with highest weight μ. The quotient is taken once, of TauCeti.evenOrthogonalWeylDimensionNumerator by its value 2!/2 · 4!/2 ⋯ (2n - 2)!/2 at μ = 0, written ∏_{k < n - 1} (k + 1) (2k + 1)!; TauCeti.evenOrthogonalWeylDimension_eq_prod_prod_div recovers the term-by-term form over ℚ.

theorem TauCeti.evenOrthogonalWeylDimension_mul_prod_add_one_mul_factorial (n : ℕ) (μ : YoungDiagram) : ↑(evenOrthogonalWeylDimension n μ) * ∏ k ∈ Finset.range (n - 1), (↑k + 1) * ↑(2 * k + 1).factorial = evenOrthogonalWeylDimensionNumerator n μ

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

theorem TauCeti.evenOrthogonalWeylDimension_pos (n : ℕ) (μ : YoungDiagram) : 0 < evenOrthogonalWeylDimension n μ

The even orthogonal Weyl dimension is positive.

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

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

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

theorem TauCeti.evenOrthogonalWeylDimensionNumerator_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : evenOrthogonalWeylDimensionNumerator n μ = evenOrthogonalWeylDimensionNumerator 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.evenOrthogonalWeylDimension_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : evenOrthogonalWeylDimension n μ = evenOrthogonalWeylDimension n ν

The even 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.evenOrthogonalWeylDimension_eq_choose_add_choose_of_colLen_le_one (n : ℕ) (μ : YoungDiagram) (h : μ.colLen 0 ≤ 1) : evenOrthogonalWeylDimension (n + 2) μ = (μ.rowLen 0 + 2 * n + 2).choose (2 * n + 2) + (μ.rowLen 0 + 2 * n + 1).choose (2 * n + 2)

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

@[simp]

theorem TauCeti.evenOrthogonalWeylDimension_zero (μ : YoungDiagram) : evenOrthogonalWeylDimension 0 μ = 1

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

@[simp]

theorem TauCeti.evenOrthogonalWeylDimension_one (μ : YoungDiagram) : evenOrthogonalWeylDimension 1 μ = 1

The SO 2 case: the circle group is abelian, and the formula, an empty product, gives every irreducible representation dimension 1.

@[simp]

theorem TauCeti.evenOrthogonalWeylDimension_bot (n : ℕ) : evenOrthogonalWeylDimension n ⊥ = 1

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

@[simp]

theorem TauCeti.evenOrthogonalWeylDimension_two (μ : YoungDiagram) : evenOrthogonalWeylDimension 2 μ = (μ.rowLen 0 - μ.rowLen 1 + 1) * (μ.rowLen 0 + μ.rowLen 1 + 1)

The SO 4 case: the irreducible representation with highest weight (λ₁, λ₂) has dimension (λ₁ - λ₂ + 1)(λ₁ + λ₂ + 1). Under Spin 4 ≅ SU 2 × SU 2 it is the exterior tensor product of the irreducible representations of the two factors of dimensions λ₁ - λ₂ + 1 and λ₁ + λ₂ + 1. The formula reads only the first two rows.