Documentation

TauCeti.RepresentationTheory.ClassicalGroups.GelfandTsetlin.Dimension

The Gelfand-Tsetlin dimension formula #

The Gelfand-Tsetlin patterns with a given weakly decreasing top row λ are counted by the Weyl dimension formula for GL n:

#{P : GTPattern n | topRow P = λ} = ∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i).

This is TauCeti.GTPattern.card_topRow_eq_weylDimension, and its DominantWeight-indexed form TauCeti.GTPattern.card_topWeight_eq_weylDimension. Both sides are already built: the left by TauCeti.RepresentationTheory.ClassicalGroups.GelfandTsetlin.Count, the right by TauCeti.RepresentationTheory.ClassicalGroups.WeylDimension.Basic. What is proved here is that they agree, so that the two candidate dimensions for the irreducible rational representation of GL n of highest weight λ — the number of Gelfand-Tsetlin patterns, and the Weyl product formula — are the same natural number. That either of them is the dimension of a representation is not proved here and cannot yet be stated: no representation and no Gelfand-Tsetlin basis is constructed, and none is used. This is an identity between a lattice-point count and a product formula.

The proof #

The proof is the branching recursion: deleting the top row of a pattern gives TauCeti.GTPattern.card_topRow_succ, which counts the patterns over λ by the patterns over each sequence interlacing λ. So it suffices to know that the Weyl dimension satisfies the same recursion, ∑_{μ ≺ λ} dim V_μ = dim V_λ.

In the shifted coordinates xₖ = k - λₖ, which turn a weakly decreasing sequence into a weakly increasing one, the Weyl numerator ∏_{i<j} (λᵢ - λⱼ + j - i) is the Vandermonde determinant of x, and the interlacing condition becomes the box xᵢ ≤ yᵢ ≤ xᵢ₊₁ - 1. The recursion is then exactly the box-sum identity TauCeti.factorial_mul_sum_det_vandermonde, the factor n ! being the ratio of the two superfactorial denominators.

Main results #

References #

Two reformulations #

The branching recursion for the Weyl numerator #

The dimension formula #

source
theorem TauCeti.GTPattern.card_topRow_eq_weylDimension {n : ℕ} (l : DominantWeight n) :
Nat.card { P : GTPattern n // P.topRow = ↑l } = weylDimension l

The Gelfand-Tsetlin dimension formula. The Gelfand-Tsetlin patterns with top row a weakly decreasing sequence λ are counted by the Weyl dimension formula ∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i).

Both sides are candidates for the dimension of the irreducible rational representation of GL n with highest weight λ, but that representation and the Gelfand-Tsetlin basis are not built here and do not enter the proof: what is proved is the identity of a lattice-point count with a product formula, obtained by checking that both satisfy the branching recursion of GL (n + 1) ↓ GL n.

This is deliberately not a simp lemma: {P : GTPattern n // P.topRow = l} carries a Fintype instance, so Nat.card_eq_fintype_card rewrites the left-hand side first and the simpNF linter rejects the tag. The DominantWeight-indexed TauCeti.GTPattern.card_topWeight_eq_weylDimension below, whose subtype has no such instance, is the simp form.

source
@[simp]
theorem TauCeti.GTPattern.card_topWeight_eq_weylDimension {n : ℕ} (l : DominantWeight n) :
Nat.card { P : GTPattern n // P.topWeight = l } = weylDimension l

The Gelfand-Tsetlin dimension formula, indexed by a dominant weight. The form the downstream representation theory consumes: fixing the top weight rather than the top row.

source
theorem TauCeti.weylDimension_two_one_zero :
weylDimension ⟨![2, 1, 0], weylDimension_two_one_zero._proof_1⟩ = 8

A worked GL 3 example: the weight (2, 1, 0) has Weyl dimension 8, the dimension of the adjoint representation of SL 3. Read off the eight Gelfand-Tsetlin patterns over that top row (TauCeti.GTPattern.card_topRow_three_two_one_zero) through the dimension formula, rather than by evaluating the product.