The Gelfand–Tsetlin lines of a rational Weyl module

Restricting the rational Weyl module V_λ of GL (n + 1) ℂ along the block inclusion GL n ℂ ↪ GL (n + 1) ℂ decomposes it, without multiplicity, into copies of the V_μ with μ interlacing λ, and the copy of each V_μ is a canonical subspace of V_λ (TauCeti.existsUnique_subrepresentation_rationalWeylRep_comp_glBlockSucc). Iterating down the chain GL 0 ⊂ GL 1 ⊂ ⋯ ⊂ GL n splits V_λ into subspaces indexed by the successive choices of interlacing weights, that is, by the Gelfand–Tsetlin patterns P with top weight λ. At the bottom of the chain the module is a line, so every piece is a line: the Gelfand–Tsetlin line TauCeti.gtLine λ P.

The line of a pattern with n + 1 rows is the image of the line of its truncation under an embedding of V_μ in the restriction of V_λ, where μ is the second row. Such an embedding is unique up to a nonzero scalar, because V_μ occurs once, so the line does not depend on the embedding: TauCeti.gtLine_succ holds for every nonzero intertwiner. The lines are canonical; a basis of V_λ indexed by the patterns further requires a normalized vector in each line.

The decomposition into lines is an internal direct sum, TauCeti.isInternal_gtLine, so the lines of the patterns with top weight λ are independent and span V_λ. This is the decomposition underlying the Gelfand–Tsetlin basis, whose vectors are normalized generators of these lines.

Main definitions

• TauCeti.gtLine: the Gelfand–Tsetlin line of a pattern in the rational Weyl module of its top weight.

Main results

• TauCeti.exists_intertwiningMap_ne_zero_of_mem_interlacingWeights: an interlacing weight μ has a nonzero intertwiner from V_μ to the restriction of V_λ.
• TauCeti.gtLine_succ: the line of a pattern is the image of the line of its truncation under any nonzero intertwiner from the Weyl module of the second row.
• TauCeti.finrank_gtLine: each Gelfand–Tsetlin line is one-dimensional.
• TauCeti.span_singleton_eq_gtLine: a nonzero vector of a line spans it.
• TauCeti.isInternal_gtLine: the rational Weyl module is the internal direct sum of the Gelfand–Tsetlin lines of the patterns with its top weight.
• TauCeti.finrank_rationalWeylFDRep_eq_card_gtPattern: the rational Weyl module V_λ has dimension the number of Gelfand–Tsetlin patterns with top weight λ.

References

• I. M. Gelfand and M. L. Tsetlin, Finite-dimensional representations of the group of unimodular matrices, Doklady Akad. Nauk SSSR 71 (1950), 825–828.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §15.3.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants (2009), Section 8.1.

noncomputable def TauCeti.gtLine {n : ℕ} (l : DominantWeight n) : { P : GTPattern n // P.topWeight = l } → Submodule ℂ ↥(weylModuleOfShape ℂ n l.detShiftShape).toSubmodule

The Gelfand–Tsetlin line of a pattern P with top weight λ, a subspace of the rational Weyl module V_λ of GL n ℂ.

For n = 0 it is the whole module, which is a line. For n + 1 rows it is the image of the line of the truncation of P, inside the Weyl module V_μ of the second row μ, under a nonzero intertwiner from V_μ to the restriction of V_λ to GL n ℂ. The choice of intertwiner does not matter (TauCeti.gtLine_succ).

@[simp]

theorem TauCeti.gtLine_zero (l : DominantWeight 0) (P : { P : GTPattern 0 // P.topWeight = l }) : gtLine l P = ⊤

For GL 0 ℂ the Gelfand–Tsetlin line of the unique pattern is the whole Weyl module.

theorem TauCeti.exists_intertwiningMap_ne_zero_of_mem_interlacingWeights {n : ℕ} {l : DominantWeight (n + 1)} {m : DominantWeight n} (hm : m ∈ interlacingWeights l) : ∃ (f : (rationalWeylRep ℂ n m).IntertwiningMap (MonoidHom.comp (rationalWeylRep ℂ (n + 1) l) (glBlockSucc ℂ n))), f ≠ 0

An interlacing weight μ has a nonzero intertwiner from V_μ to the restriction of V_λ.

theorem TauCeti.gtLine_succ {n : ℕ} (l : DominantWeight (n + 1)) (P : { P : GTPattern (n + 1) // P.topWeight = l }) (f : (rationalWeylRep ℂ n (↑P).truncate.topWeight).IntertwiningMap (MonoidHom.comp (rationalWeylRep ℂ (n + 1) l) (glBlockSucc ℂ n))) (hf : f ≠ 0) : gtLine l P = Submodule.map f.toLinearMap (gtLine (↑P).truncate.topWeight ⟨(↑P).truncate, ⋯⟩)

The Gelfand–Tsetlin line does not depend on the embedding. The line of a pattern P with n + 1 rows is the image of the line of its truncation under every nonzero intertwiner from the Weyl module of the second row of P to the restriction of V_λ to GL n ℂ.

@[simp]

theorem TauCeti.finrank_gtLine {n : ℕ} (l : DominantWeight n) (P : { P : GTPattern n // P.topWeight = l }) : Module.finrank ℂ ↥(gtLine l P) = 1

Each Gelfand–Tsetlin line is a line.

theorem TauCeti.span_singleton_eq_gtLine {n : ℕ} (l : DominantWeight n) {P : { P : GTPattern n // P.topWeight = l }} {v : ↥(weylModuleOfShape ℂ n l.detShiftShape).toSubmodule} (hv : v ∈ gtLine l P) (hv0 : v ≠ 0) : ℂ ∙ v = gtLine l P

A nonzero vector of a Gelfand–Tsetlin line spans it.

theorem TauCeti.isInternal_gtLine {n : ℕ} (l : DominantWeight n) : DirectSum.IsInternal (gtLine l)

The Gelfand–Tsetlin decomposition. The rational Weyl module V_λ of GL n ℂ is the internal direct sum of the Gelfand–Tsetlin lines of the patterns with top weight λ.

theorem TauCeti.finrank_rationalWeylFDRep_eq_card_gtPattern {n : ℕ} (l : DominantWeight n) : Module.finrank ℂ ↑(rationalWeylFDRep ℂ n l).V = Nat.card { P : GTPattern n // P.topWeight = l }

The Gelfand–Tsetlin dimension count. The rational Weyl module V_λ of GL n ℂ has dimension the number of Gelfand–Tsetlin patterns with top weight λ: by TauCeti.isInternal_gtLine it is the internal direct sum of the lines of these patterns, each of dimension one (TauCeti.finrank_gtLine).