The Weyl dimension formula for GL n

The irreducible rational representation of GL n with dominant weight λ₁ ≥ ⋯ ≥ λₙ has dimension

∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i),

the Weyl dimension formula specialized to GL n. This file builds the right-hand side as a natural number, before any representation is attached to a weight. That is a step in its own right: the product is a quotient of integers term by term, and neither the integrality nor the positivity of the value is visible from the formula as written.

The route through the file is the Vandermonde determinant. Writing λ + ρ for the strictly decreasing sequence TauCeti.DominantWeight.rhoShift λ, i ↦ λᵢ - i, the numerator TauCeti.weylDimensionNumerator is the product of its differences, hence — after reversing the index, so that the sequence increases — the determinant of a Vandermonde matrix (TauCeti.weylDimensionNumerator_eq_det_vandermonde). Mathlib's Matrix.superFactorial_dvd_vandermonde_det then supplies exactly the divisibility the formula needs, and the denominator ∏_{i < j} (j - i) is the same determinant for the sequence 0, 1, …, n - 1, so it is the superfactorial sf (n - 1) (TauCeti.prod_Ioi_sub_eq_superFactorial). Dividing gives TauCeti.weylDimension, and the division-free identity TauCeti.weylDimension_mul_superFactorial is the form all later results are proved from; the quotient form of the definition is recovered over ℚ in TauCeti.weylDimension_eq_prod_prod_div.

The classical shift is λᵢ + n - i rather than λᵢ - i; the two differ by the constant n, so they have the same differences and hence the same Weyl dimension. Subtracting i avoids truncated subtraction on ℕ and is what makes the reversed sequence literally a Vandermonde node list.

Main definitions

• TauCeti.DominantWeight.rhoShift: the strictly decreasing sequence λᵢ - i.
• TauCeti.weylDimensionNumerator: the product ∏_{i < j} (λᵢ - λⱼ + j - i) of its differences.
• TauCeti.weylDimension: the dimension predicted by the Weyl dimension formula.

Main results

• TauCeti.weylDimension_mul_superFactorial: the defining identity, division-free.
• TauCeti.weylDimension_eq_prod_prod_div: the quotient form of the formula, over ℚ.
• TauCeti.weylDimension_pos: the dimension is positive.
• TauCeti.weylDimension_congr: it depends on the weight only through the differences λᵢ - λⱼ, whence TauCeti.weylDimension_shift: it is unchanged by a determinant twist.
• TauCeti.weylDimension_eq_one_of_forall_eq: a constant weight — a power of the determinant — has dimension one.
• TauCeti.weylDimension_fin_two: for GL 2 the formula reads λ₁ - λ₂ + 1.

References

• Classical groups roadmap, Layer 5, “The Weyl dimension formula”.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Theorem 6.3 and Exercise 15.4.

def TauCeti.DominantWeight.rhoShift {n : ℕ} (l : DominantWeight n) (i : Fin n) : ℤ

The sequence λᵢ - i attached to a dominant weight λ. It is the classical λ + ρ up to the constant n: the traditional normalization is λᵢ + n - i, and only the differences of the sequence are ever used.

Equations

• l.rhoShift i = ↑l i - ↑↑i

@[simp]

theorem TauCeti.DominantWeight.rhoShift_apply {n : ℕ} (l : DominantWeight n) (i : Fin n) : l.rhoShift i = ↑l i - ↑↑i

The defining equation of TauCeti.DominantWeight.rhoShift, its pointwise normal form.

theorem TauCeti.DominantWeight.rhoShift_strictAnti {n : ℕ} (l : DominantWeight n) : StrictAnti l.rhoShift

Subtracting the staircase turns the weak decrease of a dominant weight into strict decrease. This is what makes every factor of TauCeti.weylDimensionNumerator positive.

theorem TauCeti.DominantWeight.rhoShift_sub_rhoShift {n : ℕ} (l : DominantWeight n) (i j : Fin n) : l.rhoShift i - l.rhoShift j = ↑l i - ↑l j + (↑↑j - ↑↑i)

The differences of TauCeti.DominantWeight.rhoShift are the factors of the Weyl dimension formula.

theorem TauCeti.DominantWeight.rhoShift_shift_apply {n : ℕ} (l : DominantWeight n) (m : ℤ) (i : Fin n) : (l.shift m).rhoShift i = l.rhoShift i + m

The determinant twist λ ↦ λ + m·(1, …, 1) shifts TauCeti.DominantWeight.rhoShift by m. Not a simp lemma: TauCeti.DominantWeight.rhoShift_apply already rewrites its left-hand side.

theorem TauCeti.prod_Ioi_sub_eq_superFactorial (R : Type u_1) [CommRing R] (n : ℕ) : ∏ i : Fin n, ∏ j > i, (↑↑j - ↑↑i) = ↑(n - 1).superFactorial

The denominator of the Weyl dimension formula, ∏_{i < j} (j - i), is the superfactorial sf (n - 1) = 0! · 1! ⋯ (n-1)!: it is the Vandermonde determinant of the nodes 0, 1, …, n - 1. Stated over an arbitrary commutative ring, since the formula is used both over ℤ, where the quotient is taken, and over ℚ, where it is displayed.

def TauCeti.weylDimensionNumerator {n : ℕ} (l : DominantWeight n) : ℤ

The numerator of the Weyl dimension formula: the product ∏_{i < j} (λᵢ - λⱼ + j - i) of the differences of TauCeti.DominantWeight.rhoShift.

Equations

• TauCeti.weylDimensionNumerator l = ∏ i : Fin n, ∏ j > i, (l.rhoShift i - l.rhoShift j)

theorem TauCeti.weylDimensionNumerator_eq_prod_prod {n : ℕ} (l : DominantWeight n) : weylDimensionNumerator l = ∏ i : Fin n, ∏ j > i, (↑l i - ↑l j + (↑↑j - ↑↑i))

The numerator in weight coordinates: expanding the differences of TauCeti.DominantWeight.rhoShift rewrites TauCeti.weylDimensionNumerator as the product ∏_{i < j} (λᵢ - λⱼ + j - i) of the factors of the Weyl dimension formula. This is the form every computation with the numerator starts from.

theorem TauCeti.weylDimensionNumerator_pos {n : ℕ} (l : DominantWeight n) : 0 < weylDimensionNumerator l

Every factor of the numerator is positive, because TauCeti.DominantWeight.rhoShift is strictly decreasing.

theorem TauCeti.weylDimensionNumerator_eq_det_vandermonde {n : ℕ} (l : DominantWeight n) : weylDimensionNumerator l = (Matrix.vandermonde fun (i : Fin n) => l.rhoShift i.rev).det

The numerator is a Vandermonde determinant: reversing the index makes TauCeti.DominantWeight.rhoShift increasing, and the product of the differences of an increasing sequence is the determinant of the Vandermonde matrix on those nodes.

theorem TauCeti.superFactorial_dvd_weylDimensionNumerator {n : ℕ} (l : DominantWeight n) : ↑(n - 1).superFactorial ∣ weylDimensionNumerator l

Integrality of the Weyl dimension formula: the denominator sf (n - 1) divides the numerator. This is Mathlib's divisibility for Vandermonde determinants at integer nodes.

def TauCeti.weylDimension {n : ℕ} (l : DominantWeight n) : ℕ

The Weyl dimension of a dominant weight λ of GL n, the value

∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i)

of the Weyl dimension formula. It is the dimension of the irreducible rational representation with highest weight λ; the identification with that dimension is downstream of the highest-weight classification, and what is proved here is that the formula is a well-defined positive natural number. The quotient is taken once, of the numerator by the denominator sf (n - 1), rather than factor by factor; TauCeti.weylDimension_eq_prod_prod_div recovers the term-by-term form over ℚ.

Equations

• TauCeti.weylDimension l = (TauCeti.weylDimensionNumerator l / ↑(n - 1).superFactorial).toNat

theorem TauCeti.weylDimension_mul_superFactorial {n : ℕ} (l : DominantWeight n) : ↑(weylDimension l) * ↑(n - 1).superFactorial = weylDimensionNumerator l

The defining identity of TauCeti.weylDimension, in division-free form: the dimension times the denominator sf (n - 1) is the numerator ∏_{i < j} (λᵢ - λⱼ + j - i).

theorem TauCeti.weylDimension_pos {n : ℕ} (l : DominantWeight n) : 0 < weylDimension l

The Weyl dimension is positive: the numerator is a product of positive factors, so the quotient by sf (n - 1) cannot vanish.

theorem TauCeti.weylDimension_eq_prod_prod_div {n : ℕ} (l : DominantWeight n) : ↑(weylDimension l) = ∏ i : Fin n, ∏ j > i, (↑(↑l i) - ↑(↑l j) + (↑↑j - ↑↑i)) / (↑↑j - ↑↑i)

The Weyl dimension formula in its quotient form: over ℚ, the dimension is the product of the term-by-term quotients (λᵢ - λⱼ + j - i) / (j - i).

theorem TauCeti.weylDimensionNumerator_congr {n : ℕ} {l l' : DominantWeight n} (h : ∀ (i j : Fin n), i < j → ↑l i - ↑l j = ↑l' i - ↑l' j) : weylDimensionNumerator l = weylDimensionNumerator l'

The formula reads only the differences of a weight: two weights with the same differences λᵢ - λⱼ for i < j — the only ones the product ranges over — have the same numerator.

theorem TauCeti.weylDimension_congr {n : ℕ} {l l' : DominantWeight n} (h : ∀ (i j : Fin n), i < j → ↑l i - ↑l j = ↑l' i - ↑l' j) : weylDimension l = weylDimension l'

The Weyl dimension reads only the differences of a weight: two weights with the same differences λᵢ - λⱼ for i < j have the same dimension. Cancelling sf (n - 1) in TauCeti.weylDimension_mul_superFactorial reduces this to the numerator.

@[simp]

theorem TauCeti.weylDimensionNumerator_shift {n : ℕ} (l : DominantWeight n) (m : ℤ) : weylDimensionNumerator (l.shift m) = weylDimensionNumerator l

The numerator is unchanged by the determinant twist λ ↦ λ + m·(1, …, 1), since the twist adds m to every entry and so leaves all differences alone.

@[simp]

theorem TauCeti.weylDimension_shift {n : ℕ} (l : DominantWeight n) (m : ℤ) : weylDimension (l.shift m) = weylDimension l

Since only the differences of a weight matter, the Weyl dimension is unchanged by the determinant twist λ ↦ λ + m·(1, …, 1), which on representations is tensoring with detᵐ.

theorem TauCeti.weylDimensionNumerator_eq_superFactorial_of_forall_eq {n : ℕ} {l : DominantWeight n} {c : ℤ} (h : ∀ (i : Fin n), ↑l i = c) : weylDimensionNumerator l = ↑(n - 1).superFactorial

A constant weight (c, …, c) — the weight of the c-th power of the determinant — has numerator exactly the denominator sf (n - 1).

theorem TauCeti.weylDimension_eq_one_of_forall_eq {n : ℕ} {l : DominantWeight n} {c : ℤ} (h : ∀ (i : Fin n), ↑l i = c) : weylDimension l = 1

A power of the determinant is one-dimensional: a constant dominant weight has Weyl dimension 1.

@[simp]

theorem TauCeti.weylDimension_fin_zero (l : DominantWeight 0) : weylDimension l = 1

GL 0 has a single weight, of dimension 1.

@[simp]

theorem TauCeti.weylDimension_fin_one (l : DominantWeight 1) : weylDimension l = 1

Every weight of GL 1 is a power of the determinant, hence one-dimensional.

theorem TauCeti.weylDimension_fin_two (l : DominantWeight 2) : ↑(weylDimension l) = ↑l 0 - ↑l 1 + 1

The GL 2 case: the irreducible with highest weight (λ₁, λ₂) has dimension λ₁ - λ₂ + 1. For λ = (d, 0) this is the (d+1)-dimensional symmetric power Symᵈ.