Gelfand-Tsetlin patterns

A Gelfand-Tsetlin pattern for GL n is a triangular array of integers

                    λ₀,ₙ  λ₁,ₙ  …  λₙ₋₁,ₙ
                       λ₀,ₙ₋₁  …  λₙ₋₂,ₙ₋₁
                              ⋱
                            λ₀,₁

whose row j has j entries λ₀,ⱼ ≥ ⋯ ≥ λⱼ₋₁,ⱼ, and in which consecutive rows interlace: λᵢ,ⱼ₊₁ ≥ λᵢ,ⱼ ≥ λᵢ₊₁,ⱼ₊₁. Iterating the multiplicity-free branching GL n ↓ GL (n-1) down the chain GL 1 ⊂ ⋯ ⊂ GL n refines an irreducible representation into lines indexed by exactly these patterns, so they are the combinatorial index of the Gelfand-Tsetlin basis, and their count is the dimension of the representation. Nothing of the kind is in Mathlib (whose Gelfand* files are about C*-algebras), so this file builds the combinatorial object and its recursion.

Entries are integers and no positivity is imposed, so the determinant-twisted (rational) patterns are included alongside the polynomial ones. The polynomial patterns are those all of whose entries are nonnegative; since every entry is at least the last entry of the top row, that is decided by the last entry of the top row alone, and not by the signs of the other entries, which a dominant top row is free to mix. The interlacing inequalities are imposed only on the interior cells i < j < n, where all three entries involved are informative; weak decrease along each row is then a consequence (TauCeti.GTPattern.entry_anti), not an extra hypothesis.

The engine of the file is TauCeti.GTPattern.truncateEquiv: deleting the top row identifies the patterns with n + 1 rows and top row l with the patterns with n rows whose own top row interlaces l. This is the combinatorial shadow of the GL (n+1) ↓ GL n branching rule, and it is what makes the patterns with a prescribed top row finite and countable. Read off at n = 1 it gives a unique pattern for each top row, and at n = 2 the count (λ₀ - λ₁ + 1).toNat, which for a dominant top row λ₁ ≤ λ₀ is λ₀ - λ₁ + 1, the dimension of the irreducible representation of GL 2 of highest weight (λ₀, λ₁).

Main definitions

• TauCeti.GTPattern n: Gelfand-Tsetlin patterns with n rows.
• TauCeti.GTPattern.topRow and TauCeti.GTPattern.topWeight: the longest row, the highest weight the pattern refines, the second packaged as a TauCeti.DominantWeight.
• TauCeti.Interlaces: the betweenness relation lᵢ ≥ mᵢ ≥ lᵢ₊₁ between two integer sequences.
• TauCeti.GTPattern.truncate and TauCeti.GTPattern.extend: deleting and prepending a top row.

Main results

• TauCeti.GTPattern.entry_anti and TauCeti.GTPattern.topRow_antitone: rows are weakly decreasing, so the top row is a dominant weight.
• TauCeti.GTPattern.entry_nonneg: a pattern with a nonnegative top row has nonnegative entries, so the polynomial patterns are cut out by the top row alone.
• TauCeti.Interlaces.antitone: an interlacing sequence is weakly decreasing, so a sequence interlacing a dominant weight is dominant.
• TauCeti.GTPattern.truncateEquiv: patterns with n + 1 rows and top row l correspond to patterns with n rows whose top row interlaces l.
• TauCeti.GTPattern.finite_topRow_eq: only finitely many patterns share a top row.
• TauCeti.GTPattern.card_topRow_one_eq_one and TauCeti.GTPattern.card_topRow_two_eq_toNat_sub_add_one: the counts for n = 1 and n = 2, the latter being (λ₀ - λ₁ + 1).toNat.

References

• Classical groups roadmap, Layer 6, "Gelfand-Tsetlin patterns", which pins the name GTPattern and the convention that the interlacing constraint ranges only over interior cells.
• I. M. Gelfand and M. L. Tsetlin, Finite-dimensional representations of the group of unimodular matrices, Dokl. Akad. Nauk SSSR 71 (1950), 825-828.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §15.3.

structure TauCeti.GTPattern (n : ℕ) : Type

A Gelfand-Tsetlin pattern for GL n: a triangular array of integers whose row j has the j entries λ₀,ⱼ ≥ ⋯ ≥ λⱼ₋₁,ⱼ, subject to the interlacing inequalities λᵢ,ⱼ₊₁ ≥ λᵢ,ⱼ ≥ λᵢ₊₁,ⱼ₊₁.

As with Mathlib's SemistandardYoungTableau, the array is carried by an unrestricted function ℕ → ℕ → ℤ required to vanish off the triangle i < j ≤ n, so that two patterns agreeing on the informative cells are equal. Entries may be negative: the determinant-twisted patterns are included.

• entry : ℕ → ℕ → ℤ

  entry i j is the i-th entry of row j; the informative cells are i < j ≤ n.

• zeros' {i j : ℕ} : n < j ∨ j ≤ i → self.entry i j = 0

  Cells outside the triangle i < j ≤ n carry no data.

• interlacing' {i j : ℕ} : i < j → j < n → self.entry i j ≤ self.entry i (j + 1) ∧ self.entry (i + 1) (j + 1) ≤ self.entry i j

  The interlacing inequalities λᵢ,ⱼ₊₁ ≥ λᵢ,ⱼ ≥ λᵢ₊₁,ⱼ₊₁, imposed on the interior cells i < j < n where all three entries are informative.

@[instance_reducible]

instance TauCeti.GTPattern.instFunLike {n : ℕ} : FunLike (GTPattern n) ℕ (ℕ → ℤ)

Equations

• TauCeti.GTPattern.instFunLike = { coe := TauCeti.GTPattern.entry, coe_injective := ⋯ }

@[simp]

theorem TauCeti.GTPattern.entry_eq_coe {n : ℕ} {P : GTPattern n} : P.entry = ⇑P

theorem TauCeti.GTPattern.ext {n : ℕ} {P P' : GTPattern n} (h : ∀ (i j : ℕ), P i j = P' i j) : P = P'

theorem TauCeti.GTPattern.ext_iff {n : ℕ} {P P' : GTPattern n} : P = P' ↔ ∀ (i j : ℕ), P i j = P' i j

theorem TauCeti.GTPattern.entry_eq_zero {n : ℕ} (P : GTPattern n) {i j : ℕ} (h : n < j ∨ j ≤ i) : P i j = 0

@[simp]

theorem TauCeti.GTPattern.entry_eq_zero_of_lt {n : ℕ} (P : GTPattern n) {i j : ℕ} (h : n < j) : P i j = 0

The i-th entry of row j vanishes once j outruns the number of rows.

@[simp]

theorem TauCeti.GTPattern.entry_eq_zero_of_le {n : ℕ} (P : GTPattern n) {i j : ℕ} (h : j ≤ i) : P i j = 0

The i-th entry of row j vanishes once i outruns the length of the row.

theorem TauCeti.GTPattern.entry_le_entry_succ_row {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i < j) (hj : j < n) : P i j ≤ P i (j + 1)

The first interlacing inequality λᵢ,ⱼ ≤ λᵢ,ⱼ₊₁.

theorem TauCeti.GTPattern.entry_succ_succ_le_entry {n : ℕ} (P : GTPattern n) {i j : ℕ} (hj : j < n) : P (i + 1) (j + 1) ≤ P i j

The second interlacing inequality λᵢ₊₁,ⱼ₊₁ ≤ λᵢ,ⱼ. The interlacing constraint is imposed only on the informative cells i < j, but the inequality needs no such restriction: off them both sides vanish.

theorem TauCeti.GTPattern.entry_succ_le_entry {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i + 1 < j) (hj : j ≤ n) : P (i + 1) j ≤ P i j

Rows decrease weakly, in adjacent form.

theorem TauCeti.GTPattern.entry_anti {n : ℕ} (P : GTPattern n) {i j : ℕ} (hj : j ≤ n) {i' : ℕ} : i ≤ i' → i' < j → P i' j ≤ P i j

Rows decrease weakly: λᵢ,ⱼ ≥ λᵢ',ⱼ for i ≤ i' < j ≤ n. This is a consequence of the interlacing inequalities, not a separate hypothesis on a pattern.

theorem TauCeti.GTPattern.entry_le_entry_of_le {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i < j) {j' : ℕ} : j ≤ j' → j' ≤ n → P i j ≤ P i j'

Entries increase weakly with the row index: λᵢ,ⱼ ≤ λᵢ,ⱼ' for i < j ≤ j' ≤ n.

theorem TauCeti.GTPattern.entry_le_entry_of_nonneg_of_le {n : ℕ} (P : GTPattern n) {i j j' : ℕ} (hnn : 0 ≤ P i j') (hj : j ≤ j') (hj' : j' ≤ n) : P i j ≤ P i j'

Entries increase weakly with the row index across the uninformative cells j ≤ i as well, provided the larger entry is nonnegative: λᵢ,ⱼ ≤ λᵢ,ⱼ' for j ≤ j' ≤ n and 0 ≤ λᵢ,ⱼ'.

theorem TauCeti.GTPattern.entry_add_le {n : ℕ} (P : GTPattern n) {i j d : ℕ} : j + d ≤ n → P (i + d) (j + d) ≤ P i j

Increasing both indices of a cell by the same amount decreases it.

The top row

def TauCeti.GTPattern.topRow {n : ℕ} (P : GTPattern n) : Fin n → ℤ

The top row (λ₀,ₙ, …, λₙ₋₁,ₙ) of a Gelfand-Tsetlin pattern: the highest weight it refines.

Equations

• P.topRow i = P (↑i) n

@[simp]

theorem TauCeti.GTPattern.topRow_apply {n : ℕ} (P : GTPattern n) (i : Fin n) : P.topRow i = P (↑i) n

theorem TauCeti.GTPattern.topRow_antitone {n : ℕ} (P : GTPattern n) : Antitone P.topRow

The top row is weakly decreasing. Rows of a pattern decrease weakly (entry_anti), and the top row is one of them, so it is a dominant weight of GL n; TauCeti.GTPattern.topWeight packages it as one.

def TauCeti.GTPattern.topWeight {n : ℕ} (P : GTPattern n) : DominantWeight n

The top row of a Gelfand-Tsetlin pattern, as a dominant weight of GL n.

Equations

• P.topWeight = ⟨P.topRow, ⋯⟩

@[simp]

theorem TauCeti.GTPattern.topWeight_coe {n : ℕ} (P : GTPattern n) : ↑P.topWeight = P.topRow

theorem TauCeti.GTPattern.entry_le_topRow {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i < j) (hj : j ≤ n) : P i j ≤ P.topRow ⟨i, ⋯⟩

Every entry is at most the top-row entry directly above it.

theorem TauCeti.GTPattern.topRow_le_entry {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i < j) (hj : j ≤ n) : P.topRow ⟨i + (n - j), ⋯⟩ ≤ P i j

Every entry dominates the top-row entry reached from it by increasing both indices equally.

theorem TauCeti.GTPattern.entry_nonneg {n : ℕ} (P : GTPattern n) (h : ∀ (i : Fin n), 0 ≤ P.topRow i) (i j : ℕ) : 0 ≤ P i j

A pattern with a nonnegative top row has nonnegative entries: every informative entry dominates a top-row entry, and the remaining ones vanish. This is what confines a pattern whose top row is a shape to the polynomial regime, where it names a semistandard Young tableau.

theorem TauCeti.GTPattern.entry_mem_Icc {n : ℕ} (P : GTPattern n) {i j : ℕ} (hij : i < j) (hj : j ≤ n) : P i j ∈ Set.Icc (P.topRow ⟨n - 1, ⋯⟩) (P.topRow ⟨0, ⋯⟩)

Every entry of a pattern lies between the last and the first entry of its top row.

@[instance_reducible]

instance TauCeti.GTPattern.instUniqueOfNatNat : Unique (GTPattern 0)

There is exactly one empty pattern.

Equations

• One or more equations did not get rendered due to their size.

Interlacing

def TauCeti.Interlaces {n : ℕ} (l : Fin (n + 1) → ℤ) (m : Fin n → ℤ) : Prop

TauCeti.Interlaces l m says that the integer sequence m : Fin n → ℤ interlaces the longer sequence l : Fin (n + 1) → ℤ: lᵢ ≥ mᵢ ≥ lᵢ₊₁ for every i. This is the betweenness condition relating consecutive rows of a Gelfand-Tsetlin pattern.

No dominance is assumed: l and m are arbitrary integer sequences and the relation is purely combinatorial. When l is dominant it acquires its representation-theoretic reading: every m interlacing l is then dominant too (the two inequalities give mᵢ₊₁ ≤ lᵢ₊₁ ≤ mᵢ), and such m are exactly the highest weights of the constituents of V_l restricted along GL n ↪ GL (n + 1).

Equations

• TauCeti.Interlaces l m = ∀ (i : Fin n), m i ≤ l i.castSucc ∧ l i.succ ≤ m i

@[simp]

theorem TauCeti.interlaces_iff {n : ℕ} {l : Fin (n + 1) → ℤ} {m : Fin n → ℤ} : Interlaces l m ↔ ∀ (i : Fin n), m i ≤ l i.castSucc ∧ l i.succ ≤ m i

Interlacing unfolded: the pair of inequalities at each index. This is the introduction and elimination rule for TauCeti.Interlaces, whose body is not exposed.

theorem TauCeti.Interlaces.le_castSucc {n : ℕ} {l : Fin (n + 1) → ℤ} {m : Fin n → ℤ} (h : Interlaces l m) (i : Fin n) : m i ≤ l i.castSucc

Half of the interlacing condition: mᵢ ≤ lᵢ.

theorem TauCeti.Interlaces.succ_le {n : ℕ} {l : Fin (n + 1) → ℤ} {m : Fin n → ℤ} (h : Interlaces l m) (i : Fin n) : l i.succ ≤ m i

The other half of the interlacing condition: lᵢ₊₁ ≤ mᵢ.

theorem TauCeti.Interlaces.antitone {n : ℕ} {l : Fin (n + 1) → ℤ} {m : Fin n → ℤ} (h : Interlaces l m) : Antitone m

An interlacing sequence is weakly decreasing. The two interlacing inequalities at adjacent indices meet at the same entry of l, giving mᵢ₊₁ ≤ lᵢ₊₁ ≤ mᵢ; no assumption on l is needed. In particular a sequence interlacing a dominant weight is itself dominant, which is what packages the output of TauCeti.GTPattern.truncateEquiv as a TauCeti.DominantWeight.

Deleting and prepending a top row

def TauCeti.GTPattern.truncate {n : ℕ} (P : GTPattern (n + 1)) : GTPattern n

Delete the top row of a pattern with n + 1 rows.

Equations

• P.truncate = { entry := fun (i j : ℕ) => if j ≤ n then P i j else 0, zeros' := ⋯, interlacing' := ⋯ }

@[simp]

theorem TauCeti.GTPattern.truncate_apply {n : ℕ} (P : GTPattern (n + 1)) (i j : ℕ) : P.truncate i j = if j ≤ n then P i j else 0

theorem TauCeti.GTPattern.topRow_truncate {n : ℕ} (P : GTPattern (n + 1)) (i : Fin n) : P.truncate.topRow i = P (↑i) n

The top row of a truncated pattern is the row below the top of the original.

theorem TauCeti.GTPattern.interlaces_topRow_truncate {n : ℕ} (P : GTPattern (n + 1)) : Interlaces P.topRow P.truncate.topRow

The row below the top of a pattern interlaces its top row: the pattern's own witness that TauCeti.GTPattern.truncate lands where TauCeti.GTPattern.extend expects it.

def TauCeti.GTPattern.extend {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) : GTPattern (n + 1)

Prepend the row l on top of a pattern with n rows whose own top row it interlaces.

Equations

• Q.extend l h = { entry := fun (i j : ℕ) => if j = n + 1 then if hi : i < n + 1 then l ⟨i, hi⟩ else 0 else Q i j, zeros' := ⋯, interlacing' := ⋯ }

theorem TauCeti.GTPattern.extend_apply {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) (i j : ℕ) : (Q.extend l h) i j = if j = n + 1 then if hi : i < n + 1 then l ⟨i, hi⟩ else 0 else Q i j

@[simp]

theorem TauCeti.GTPattern.extend_apply_of_ne {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) {i j : ℕ} (hj : j ≠ n + 1) : (Q.extend l h) i j = Q i j

@[simp]

theorem TauCeti.GTPattern.extend_apply_top {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) {i : ℕ} (hi : i < n + 1) : (Q.extend l h) i (n + 1) = l ⟨i, hi⟩

theorem TauCeti.GTPattern.extend_apply_top_of_le {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) {i : ℕ} (hi : n + 1 ≤ i) : (Q.extend l h) i (n + 1) = 0

Prepending a row leaves the cells past the end of the new row empty. This is not @[simp]: entry_eq_zero_of_le already rewrites it, being the general normal form for an out-of-row cell.

@[simp]

theorem TauCeti.GTPattern.topRow_extend {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) : (Q.extend l h).topRow = l

@[simp]

theorem TauCeti.GTPattern.truncate_extend {n : ℕ} (Q : GTPattern n) (l : Fin (n + 1) → ℤ) (h : Interlaces l Q.topRow) : (Q.extend l h).truncate = Q

@[simp]

theorem TauCeti.GTPattern.extend_truncate {n : ℕ} (P : GTPattern (n + 1)) : P.truncate.extend P.topRow ⋯ = P

def TauCeti.GTPattern.truncateEquiv {n : ℕ} (l : Fin (n + 1) → ℤ) : { P : GTPattern (n + 1) // P.topRow = l } ≃ { Q : GTPattern n // Interlaces l Q.topRow }

Deleting the top row is a bijection. The Gelfand-Tsetlin patterns with n + 1 rows and top row l are exactly the patterns with n rows whose own top row interlaces l.

The statement holds for an arbitrary integer sequence l, where it is a bijection between two combinatorial sets and nothing more (for a non-dominant l both sides are empty as soon as n ≥ 1). For a dominant l it is the combinatorial form of the multiplicity-free branching GL (n+1) ↓ GL n: the constituents of the restriction of V_l are indexed by the interlacing weights, which are again dominant, and a basis vector of V_l is a choice of interlacing weight together with a basis vector of the corresponding constituent.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GTPattern.truncateEquiv_apply_coe {n : ℕ} (l : Fin (n + 1) → ℤ) (P : { P : GTPattern (n + 1) // P.topRow = l }) : ↑((truncateEquiv l) P) = (↑P).truncate

@[simp]

theorem TauCeti.GTPattern.truncateEquiv_symm_apply_coe {n : ℕ} (l : Fin (n + 1) → ℤ) (Q : { Q : GTPattern n // Interlaces l Q.topRow }) : ↑((truncateEquiv l).symm Q) = (↑Q).extend l ⋯

Finitely many patterns share a top row

instance TauCeti.GTPattern.finite_topRow_eq {n : ℕ} (l : Fin n → ℤ) : Finite { P : GTPattern n // P.topRow = l }

Only finitely many patterns share a top row. Every entry of a pattern is squeezed between the last and the first entry of its top row (TauCeti.GTPattern.entry_mem_Icc), so the patterns with a prescribed top row form a finite type.

The counts in low rank

@[instance_reducible]

instance TauCeti.GTPattern.uniqueTopRowOne (l : Fin 1 → ℤ) : Unique { P : GTPattern 1 // P.topRow = l }

A one-row pattern is nothing but its top row: for each l there is exactly one pattern with top row l.

Equations

• TauCeti.GTPattern.uniqueTopRowOne l = (TauCeti.GTPattern.truncateEquiv l).unique

theorem TauCeti.GTPattern.card_topRow_one_eq_one (l : Fin 1 → ℤ) : Nat.card { P : GTPattern 1 // P.topRow = l } = 1

A Gelfand-Tsetlin pattern with a single row is its top row: there is exactly one pattern with each prescribed top row. This is the statement that the irreducible representations of GL 1 are one-dimensional.

def TauCeti.GTPattern.equivOne : GTPattern 1 ≃ (Fin 1 → ℤ)

Reading the top row is a bijection from the patterns with one row onto the integer sequences of length one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GTPattern.equivOne_apply (P : GTPattern 1) : equivOne P = P.topRow

theorem TauCeti.GTPattern.card_topRow_two_eq_toNat_sub_add_one (l : Fin 2 → ℤ) : Nat.card { P : GTPattern 2 // P.topRow = l } = (l 0 - l 1 + 1).toNat

The count for GL 2. A Gelfand-Tsetlin pattern with two rows is its top row together with a single integer λ₀,₁ between λ₁ and λ₀, so the patterns with top row (λ₀, λ₁) are counted by (λ₀ - λ₁ + 1).toNat. The truncation is not decoration: l is an arbitrary integer sequence, and for λ₀ < λ₁ there is no such pattern at all. On a dominant top row, λ₁ ≤ λ₀, the count is λ₀ - λ₁ + 1, the dimension of the irreducible representation of GL 2 of highest weight (λ₀, λ₁).