The Weyl dimension formula for Sp 2n

The irreducible representations of the symplectic group Sp 2n are indexed by the partitions λ₁ ≥ ⋯ ≥ λₙ ≥ 0 with at most n parts. The positive roots of type Cₙ are eᵢ ± eⱼ for i < j and 2eᵢ, and the half-sum of the positive roots is ρ = (n, n - 1, …, 1), so with xᵢ = λᵢ + n - i the entries of λ + ρ (indexing from 0), the Weyl dimension formula reads

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

This file builds the right-hand side as a natural number. As for GL n (TauCeti.weylDimension), 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 numerator TauCeti.symplecticWeylDimensionNumerator is the odd Vandermonde product ∏ᵢ xᵢ · ∏_{i < j} (xᵢ² - xⱼ²), and the denominator is its value at λ = 0, which is 1! · 3! ⋯ (2n - 1)! (TauCeti.symplecticWeylDimensionNumerator_bot). Integrality is TauCeti.prod_factorial_dvd_prod_mul_prod_sq_sub_sq: in the Vandermonde determinant of the squares xᵢ², weighted by the xᵢ, the column of x^{2k+1} may be replaced by the column of the odd polynomial x (x² - 1²) ⋯ (x² - k²), a product of 2k + 1 consecutive integers. 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.symplecticWeylDimension_congr). When μ has at most n rows it is a dominant weight of Sp 2n, and the value is the dimension of the corresponding irreducible representation; the identification with that dimension is downstream of the highest-weight classification.

Main definitions

• TauCeti.symplecticRhoShift: the entries μᵢ + n - i of μ + ρ.
• TauCeti.symplecticWeylDimensionNumerator: the product ∏ᵢ xᵢ · ∏_{i < j} (xᵢ² - xⱼ²).
• TauCeti.symplecticWeylDimension: the dimension predicted by the Weyl dimension formula.

Main results

• TauCeti.symplecticWeylDimension_mul_prod_factorial: the defining identity, division-free.
• TauCeti.symplecticWeylDimension_eq_prod_prod_div: the product form of the formula, over ℚ.
• TauCeti.symplecticWeylDimension_pos: the dimension is positive.
• TauCeti.symplecticWeylDimension_congr: the dimension reads only the first n rows.
• TauCeti.symplecticWeylDimension_eq_choose_of_colLen_le_one: for Sp (2n + 2), a one-row weight (d, 0, …, 0) has dimension (d + 2n + 1).choose (2n + 1), that of the symmetric power Symᵈ of the standard representation; in particular TauCeti.symplecticWeylDimension_bot, the trivial representation has dimension 1.
• TauCeti.symplecticWeylDimension_one_eq_rowLen_add_one: for Sp 2 = SL 2 the formula reads d + 1.

References

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

def TauCeti.symplecticRhoShift (n : ℕ) (μ : YoungDiagram) (i : ℕ) : ℤ

The entries μᵢ + n - i of μ + ρ for Sp 2n, where ρ = (n, n - 1, …, 1) is the half-sum of the positive roots of type Cₙ. Only the indices i < n are used.

@[simp]

theorem TauCeti.symplecticRhoShift_apply (n : ℕ) (μ : YoungDiagram) (i : ℕ) : symplecticRhoShift n μ i = ↑(μ.rowLen i) + ↑n - ↑i

The defining equation of TauCeti.symplecticRhoShift.

theorem TauCeti.symplecticRhoShift_pos {n : ℕ} {μ : YoungDiagram} {i : ℕ} (hi : i < n) : 0 < symplecticRhoShift n μ i

The entries of μ + ρ are positive below n.

theorem TauCeti.symplecticRhoShift_strictAnti (n : ℕ) (μ : YoungDiagram) : StrictAnti (symplecticRhoShift n μ)

Adding the strictly decreasing ρ to the weakly decreasing row lengths gives a strictly decreasing sequence, which makes every factor of TauCeti.symplecticWeylDimensionNumerator positive.

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

The numerator of the symplectic Weyl dimension formula: with xᵢ = μᵢ + n - i, the product ∏_{i < n} xᵢ · ∏_{i < j < n} (xᵢ² - xⱼ²) of the pairings of μ + ρ with the positive roots 2eᵢ and eᵢ ± eⱼ of type Cₙ, the factors 2 of the long roots being dropped since they cancel against the denominator.

theorem TauCeti.symplecticWeylDimensionNumerator_eq_prod_prod (n : ℕ) (μ : YoungDiagram) : symplecticWeylDimensionNumerator n μ = ∏ i ∈ Finset.range n, symplecticRhoShift n μ i * ∏ j ∈ Finset.Ico (i + 1) n, (symplecticRhoShift n μ i ^ 2 - symplecticRhoShift n μ j ^ 2)

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

theorem TauCeti.symplecticWeylDimensionNumerator_pos (n : ℕ) (μ : YoungDiagram) : 0 < symplecticWeylDimensionNumerator n μ

Every factor of the numerator is positive.

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

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

@[simp]

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

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

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

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

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

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

theorem TauCeti.symplecticWeylDimension_mul_prod_factorial (n : ℕ) (μ : YoungDiagram) : ↑(symplecticWeylDimension n μ) * ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial = symplecticWeylDimensionNumerator n μ

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

theorem TauCeti.symplecticWeylDimension_pos (n : ℕ) (μ : YoungDiagram) : 0 < symplecticWeylDimension n μ

The symplectic Weyl dimension is positive.

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

The Weyl dimension formula for Sp 2n in its product form: over ℚ, with xᵢ = μᵢ + n - i, the dimension is

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

theorem TauCeti.symplecticWeylDimensionNumerator_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : symplecticWeylDimensionNumerator n μ = symplecticWeylDimensionNumerator 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.symplecticWeylDimension_congr {n : ℕ} {μ ν : YoungDiagram} (h : ∀ i < n, μ.rowLen i = ν.rowLen i) : symplecticWeylDimension n μ = symplecticWeylDimension n ν

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

One-row weights: if μ has at most one row, of length d, then the symplectic Weyl dimension for Sp (2n + 2) is (d + 2n + 1).choose (2n + 1), the dimension of the symmetric power Symᵈ of the standard representation, which is irreducible for the symplectic group.

@[simp]

theorem TauCeti.symplecticWeylDimension_zero (μ : YoungDiagram) : symplecticWeylDimension 0 μ = 1

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

@[simp]

theorem TauCeti.symplecticWeylDimension_bot (n : ℕ) : symplecticWeylDimension n ⊥ = 1

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

@[simp]

theorem TauCeti.symplecticWeylDimension_one_eq_rowLen_add_one (μ : YoungDiagram) : symplecticWeylDimension 1 μ = μ.rowLen 0 + 1

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