Branching of Weyl-module characters on the diagonal torus

The character of the Weyl module of a shape μ on GL (n + 1) restricts to the diagonal torus (kˣ)ⁿ × kˣ as

χ_μ(diag(t, z)) = ∑_ν z ^ (|μ| - |ν|) * χ_ν(diag t),

where ν ranges over the shapes interlacing μ with at most n rows. Setting z = 1 gives the character identity for the upper-left block inclusion GL n → GL (n + 1). Each interlacing shape occurs once. The formula includes the empty rank and shapes with more than n + 1 rows, whose Weyl modules vanish.

These are identities of group characters evaluated on the diagonal torus, not isomorphisms of restricted representations. They provide the character calculation for multiplicity-free branching; identifying the representation summands is a separate step.

The proofs combine TauCeti.char_weylRepOfShape_diagonal_eq_eval_diagramSchurPoly, the Weyl-module character formula, with TauCeti.eval_snoc_diagramSchurPoly, the Schur-polynomial branching identity. The FDRep forms also apply to TauCeti.schurFunctor over ℂ.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15 and Appendix A: Schur characters and branching of general linear representations.

theorem TauCeti.char_weylRepOfShape_diagonal_snoc (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) (z : kˣ) : (weylRepOfShape k (n + 1) μ).character (diagGL (Fin.snoc t z)) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, ↑z ^ (μ.card - ν.card) * (weylRepOfShape k n ν).character (diagGL t)

On diagonal matrices diag(t, z) of GL (n + 1), the Weyl character branches over interlacing shapes. The last coordinate records the number of boxes removed from the shape.

theorem TauCeti.char_weylFDRepOfShape_diagonal_snoc (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) (z : kˣ) : (weylFDRepOfShape k (n + 1) μ).character (diagGL (Fin.snoc t z)) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, ↑z ^ (μ.card - ν.card) * (weylFDRepOfShape k n ν).character (diagGL t)

The diagonal-torus branching identity for the bundled Weyl module.

theorem TauCeti.char_weylRepOfShape_glBlockSucc_diagGL (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) : (weylRepOfShape k (n + 1) μ).character ((glBlockSucc k n) (diagGL t)) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, (weylRepOfShape k n ν).character (diagGL t)

On the diagonal torus, restriction along the upper-left block inclusion branches the Weyl character as a sum over interlacing shapes, each occurring once.

theorem TauCeti.char_weylFDRepOfShape_glBlockSucc_diagGL (k : Type u) [Field k] [CharZero k] (n : ℕ) (μ : YoungDiagram) (t : Fin n → kˣ) : (weylFDRepOfShape k (n + 1) μ).character ((glBlockSucc k n) (diagGL t)) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, (weylFDRepOfShape k n ν).character (diagGL t)

The block-restriction character identity on the diagonal torus for the bundled Weyl module, equivalently the Schur functor over ℂ.