Counting Gelfand-Tsetlin patterns, from the branching side

Deleting the top row of a Gelfand-Tsetlin pattern with n + 1 rows and top row l leaves a pattern with n rows whose own top row interlaces l (TauCeti.GTPattern.truncateEquiv). Sorting those by the row they expose turns that bijection into a count: the patterns over l are as many as the patterns over each interlacing m, summed over m. That recursion,

#{P : GTPattern (n + 1) | top row l} = ∑_{m ≺ l} #{Q : GTPattern n | top row m},

is TauCeti.GTPattern.card_topRow_succ, and it is the combinatorial shadow of the multiplicity-free branching GL (n + 1) ↓ GL n: a basis vector of V_l is a constituent of the restriction together with a basis vector of it. Iterating it down the chain GL 1 ⊂ ⋯ ⊂ GL n is how the Gelfand-Tsetlin dimension formula is meant to be proved — from the branching, by induction on n, and independently of the Weyl dimension formula.

The sum is indexed by TauCeti.interlacingFinset, the sequences interlacing l collected into a Finset. Interlacing is a two-sided bound at each index, so this is nothing but the interval Finset.Icc of the pointwise order on Fin n → ℤ, and no new finiteness argument is needed.

Two further readings of the recursion are recorded. Which top rows occur at all is settled by TauCeti.GTPattern.nonempty_topRow_eq_iff: a sequence is the top row of some pattern exactly when it is weakly decreasing, that is, exactly when it is a dominant weight. Both directions are one-line consequences of the machinery — reading a top row produces a weakly decreasing sequence, and prepending a dominant l on top of the pattern built inductively over l ∘ Fin.castSucc produces a pattern over l. And unwinding the recursion twice gives the GL 3 count TauCeti.GTPattern.card_topRow_three as an explicit double sum over the two free entries of the middle and bottom rows, which settles two worked examples: the polynomial top row (2, 1, 0) and its determinant twist (1, 0, -1) both carry exactly 8 patterns.

Main definitions

• TauCeti.interlacingFinset: the sequences interlacing a given one, as a Finset.
• TauCeti.interlacingWeights: the dominant weights interlacing a given one, as a Finset.

Main results

• TauCeti.card_interlacingFinset: how many sequences interlace a given one.
• TauCeti.GTPattern.truncateSigmaEquiv: the patterns over l sorted by the row below the top.
• TauCeti.GTPattern.card_topRow_succ: the branching recursion for the pattern count.
• TauCeti.GTPattern.truncateTopWeightSigmaEquiv: the patterns with top weight l sorted by the dominant weight of the row below the top.
• TauCeti.GTPattern.nonempty_topRow_eq_iff and TauCeti.GTPattern.card_topRow_pos_iff: a sequence is the top row of a pattern exactly when it is weakly decreasing.
• TauCeti.GTPattern.card_topWeight_eq_card_topRow: counting by top weight is counting by top row.
• TauCeti.GTPattern.card_topRow_three: the GL 3 count as a double sum, and TauCeti.GTPattern.card_topRow_three_two_one_zero, TauCeti.GTPattern.card_topRow_three_one_zero_neg_one: two worked GL 3 examples.

References

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

The interlacing sequences as a finite set

def TauCeti.interlacingFinset {n : ℕ} (l : Fin (n + 1) → ℤ) : Finset (Fin n → ℤ)

The sequences interlacing l, collected into a Finset.

TauCeti.Interlaces l m bounds m i between l i.succ and l i.castSucc and says nothing else, so the interlacing sequences are exactly the points of an interval of the pointwise order on Fin n → ℤ; TauCeti.mem_interlacingFinset is that identification. For a dominant l this is the index set of the constituents of V_l restricted along GL n ↪ GL (n + 1).

@[simp]

theorem TauCeti.mem_interlacingFinset {n : ℕ} {l : Fin (n + 1) → ℤ} {m : Fin n → ℤ} : m ∈ interlacingFinset l ↔ Interlaces l m

The members of TauCeti.interlacingFinset l are exactly the sequences interlacing l: the two bounds defining the interval are the two interlacing inequalities, read at every index at once.

theorem TauCeti.card_interlacingFinset {n : ℕ} (l : Fin (n + 1) → ℤ) : (interlacingFinset l).card = ∏ i : Fin n, (l i.castSucc + 1 - l i.succ).toNat

How many sequences interlace l: the two-sided bounds are independent from index to index, so the count is the product of the lengths of the intervals [lᵢ₊₁, lᵢ]. For a dominant l this is the number of constituents of V_l restricted along GL n ↪ GL (n + 1), each of which is multiplicity-free.

noncomputable def TauCeti.interlacingWeights {n : ℕ} (l : DominantWeight (n + 1)) : Finset (DominantWeight n)

The dominant weights interlacing a dominant weight l, as a Finset.

A sequence interlacing a weakly decreasing sequence is itself weakly decreasing (TauCeti.Interlaces.antitone), so these are the members of TauCeti.interlacingFinset l, each read as a dominant weight. They index the branching rule for the rational representation V_l of GL (n + 1) restricted along GL n ↪ GL (n + 1).

@[simp]

theorem TauCeti.mem_interlacingWeights {n : ℕ} {l : DominantWeight (n + 1)} {m : DominantWeight n} : m ∈ interlacingWeights l ↔ Interlaces ↑l ↑m

The members of TauCeti.interlacingWeights l are exactly the dominant weights interlacing l.

The branching recursion

def TauCeti.GTPattern.truncateSigmaEquiv {n : ℕ} (l : Fin (n + 1) → ℤ) : { P : GTPattern (n + 1) // P.topRow = l } ≃ (m : ↥(interlacingFinset l)) × { Q : GTPattern n // Q.topRow = ↑m }

The patterns over l, sorted by the row below the top. Deleting the top row of a pattern with n + 1 rows and top row l leaves a pattern with n rows whose top row interlaces l (TauCeti.GTPattern.truncateEquiv); recording that row as the index of a Sigma type splits the patterns over l into the fibres of the exposed row. This is the bookkeeping form of the multiplicity-free branching GL (n + 1) ↓ GL n.

theorem TauCeti.GTPattern.card_topRow_succ {n : ℕ} (l : Fin (n + 1) → ℤ) : Nat.card { P : GTPattern (n + 1) // P.topRow = l } = ∑ m ∈ interlacingFinset l, Nat.card { Q : GTPattern n // Q.topRow = m }

The branching recursion for the pattern count. The Gelfand-Tsetlin patterns with n + 1 rows and top row l are counted by the patterns with n rows, summed over the sequences interlacing l.

For a dominant l this is the count of a basis of V_l read off the multiplicity-free restriction GL (n + 1) ↓ GL n: each interlacing m contributes the dimension of V_m. For an arbitrary l it is a bijection between finite sets and nothing more; both sides vanish unless l is weakly decreasing (TauCeti.GTPattern.card_topRow_pos_iff). Iterated, this gives the Gelfand-Tsetlin dimension formula by induction on n from the branching, rather than from the Weyl dimension formula.

The branching recursion, indexed by dominant weights

theorem TauCeti.GTPattern.topWeight_truncate_mem_interlacingWeights {n : ℕ} (P : GTPattern (n + 1)) : P.truncate.topWeight ∈ interlacingWeights P.topWeight

The top weight of the truncation of a pattern interlaces the top weight of the pattern.

def TauCeti.GTPattern.truncateTopWeightSigmaEquiv {n : ℕ} (l : DominantWeight (n + 1)) : { P : GTPattern (n + 1) // P.topWeight = l } ≃ (m : ↥(interlacingWeights l)) × { Q : GTPattern n // Q.topWeight = ↑m }

The patterns with top weight λ, sorted by the dominant weight of their second row. Deleting the top row identifies them with the patterns with one row fewer whose top weight interlaces λ. This is TauCeti.GTPattern.truncateSigmaEquiv indexed by the dominant weights TauCeti.interlacingWeights λ, the index set of the branching GL (n + 1) ↓ GL n.

theorem TauCeti.GTPattern.truncateTopWeightSigmaEquiv_apply {n : ℕ} (l : DominantWeight (n + 1)) (P : { P : GTPattern (n + 1) // P.topWeight = l }) (hm : (↑P).truncate.topWeight ∈ interlacingWeights l) : (truncateTopWeightSigmaEquiv l) P = ⟨⟨(↑P).truncate.topWeight, hm⟩, ⟨(↑P).truncate, ⋯⟩⟩

TauCeti.GTPattern.truncateTopWeightSigmaEquiv sends a pattern to its truncation, indexed by the top weight of the truncation.

@[simp]

theorem TauCeti.GTPattern.truncateTopWeightSigmaEquiv_apply_fst_coe {n : ℕ} (l : DominantWeight (n + 1)) (P : { P : GTPattern (n + 1) // P.topWeight = l }) : ↑((truncateTopWeightSigmaEquiv l) P).fst = (↑P).truncate.topWeight

@[simp]

theorem TauCeti.GTPattern.truncateTopWeightSigmaEquiv_apply_snd_coe {n : ℕ} (l : DominantWeight (n + 1)) (P : { P : GTPattern (n + 1) // P.topWeight = l }) : ↑((truncateTopWeightSigmaEquiv l) P).snd = (↑P).truncate

@[simp]

theorem TauCeti.GTPattern.truncate_truncateTopWeightSigmaEquiv_symm_apply_coe {n : ℕ} (l : DominantWeight (n + 1)) (x : (m : ↥(interlacingWeights l)) × { Q : GTPattern n // Q.topWeight = ↑m }) : (↑((truncateTopWeightSigmaEquiv l).symm x)).truncate = ↑x.snd

Which sequences are top rows

theorem TauCeti.GTPattern.nonempty_topRow_eq_iff {n : ℕ} (l : Fin n → ℤ) : Nonempty { P : GTPattern n // P.topRow = l } ↔ Antitone l

A sequence is the top row of a pattern exactly when it is weakly decreasing, that is, exactly when it is a dominant weight. Reading a top row gives a weakly decreasing sequence (TauCeti.GTPattern.topRow_antitone); conversely a weakly decreasing l interlaces its own truncation l ∘ Fin.castSucc, so a pattern over l is built by prepending l to a pattern supplied inductively.

theorem TauCeti.GTPattern.card_topRow_pos_iff {n : ℕ} (l : Fin n → ℤ) : 0 < Nat.card { P : GTPattern n // P.topRow = l } ↔ Antitone l

A top row is counted at least once exactly when it is weakly decreasing. The Nat.card form of TauCeti.GTPattern.nonempty_topRow_eq_iff, available because only finitely many patterns share a top row.

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

Counting patterns by top weight is counting them by top row. A TauCeti.DominantWeight is a sequence together with a proof, so fixing the top weight and fixing the top row cut out the same patterns. This is what lets the recursion above feed the top-weight-indexed counts of TauCeti.RepresentationTheory.ClassicalGroups.GelfandTsetlin.Shift.

The count for GL 3

theorem TauCeti.GTPattern.card_topRow_three (l : Fin 3 → ℤ) : Nat.card { P : GTPattern 3 // P.topRow = l } = ∑ a ∈ Finset.Icc (l 1) (l 0), ∑ b ∈ Finset.Icc (l 2) (l 1), (a - b + 1).toNat

The count for GL 3. Unwinding the branching recursion once and then the GL 2 count TauCeti.GTPattern.card_topRow_two_eq_toNat_sub_add_one, the patterns with top row (λ₀, λ₁, λ₂) are counted by a double sum over the two entries a ≥ b of the middle row, each contributing the (a - b + 1) choices of bottom entry.

As everywhere in this development the top row is an arbitrary integer sequence: for a top row that is not weakly decreasing one of the two intervals is empty and the count is 0.

theorem TauCeti.GTPattern.card_topRow_three_two_one_zero : Nat.card { P : GTPattern 3 // P.topRow = ![2, 1, 0] } = 8

A worked GL 3 example. The top row (2, 1, 0) carries exactly 8 Gelfand-Tsetlin patterns, one for each choice of an interlacing middle row (a, b) with 2 ≥ a ≥ 1, 1 ≥ b ≥ 0 and a bottom entry between them: the four middle rows (1, 0), (1, 1), (2, 0), (2, 1) admit 2, 1, 3, 2 bottom entries. This is the dimension of the 8-dimensional irreducible representation of GL 3 of highest weight (2, 1, 0), the adjoint representation of SL 3.

theorem TauCeti.GTPattern.card_topRow_three_one_zero_neg_one : Nat.card { P : GTPattern 3 // P.topRow = ![1, 0, -1] } = 8

A worked rational GL 3 example. The top row (1, 0, -1) is the determinant twist of (2, 1, 0) by -1, and it carries the same 8 patterns — now with negative entries in some rows, which the sign-free interlacing of TauCeti.GTPattern admits. A nonnegativity constraint on the row-final entries would wrongly exclude them.