Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Branching.Rational

Branching of rational Weyl-module characters #

The rational Weyl module V_λ = TauCeti.rationalWeylRep k (n + 1) λ of a dominant weight λ of GL (n + 1) has, on the diagonal torus (kˣ)ⁿ × kˣ, the character

χ_λ(diag(t, z)) = ∑_{μ ≺ λ} z ^ (|λ| - |μ|) * χ_μ(diag t),

where μ runs over the dominant weights of GL n interlacing λ (λᵢ ≥ μᵢ ≥ λᵢ₊₁, TauCeti.interlacingWeights) and |λ| = ∑ᵢ λᵢ. The exponent is an integer and may be negative: for n = 0 and λ = (-1) the module is det⁻¹ and the identity reads z⁻¹ = z⁻¹. Setting z = 1 gives the character identity for the upper-left block inclusion GL n → GL (n + 1), each interlacing weight occurring once, and evaluating at the identity gives the dimension recursion dim V_λ = ∑_{μ ≺ λ} dim V_μ.

This is the rational, DominantWeight-indexed form of the partition-indexed branching rule TauCeti.char_weylRepOfShape_diagonal_snoc. The interlacing now runs over integer sequences rather than Young diagrams, and the two are matched by the determinant twist: writing λ = ν₀ + c·(1, …, 1) with c = λₙ and ν₀ the polynomial part of λ, the shapes interlacing ν₀ with at most n rows correspond to the weights interlacing λ by ν ↦ ν + c·(1, …, 1), and the twist det ^ c on GL (n + 1) restricts to det ^ c on GL n times z ^ c.

As for the partition form, these are identities of characters on the diagonal torus, not isomorphisms of restricted representations.

Main results #

References #

Interlacing shapes and interlacing weights #

The branching rule #

source
theorem TauCeti.char_rationalWeylRep_diagonal_snoc (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight (n + 1)) (t : Fin n → kˣ) (z : kˣ) :
(rationalWeylRep k (n + 1) l).character (diagGL (Fin.snoc t z)) = ∑ m ∈ interlacingWeights l, ↑(z ^ (∑ i : Fin (n + 1), ↑l i - ∑ i : Fin n, ↑m i)) * (rationalWeylRep k n m).character (diagGL t)

The branching rule for rational Weyl characters. On diagonal matrices diag(t, z) of GL (n + 1), the character of the rational Weyl module of a dominant weight l is the sum, over the dominant weights m of GL n interlacing l, of z ^ (|l| - |m|) times the character of the rational Weyl module of m at diag t. Each interlacing weight occurs once, and the exponent of z is an integer that may be negative.

source
theorem TauCeti.char_rationalWeylFDRep_diagonal_snoc (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight (n + 1)) (t : Fin n → kˣ) (z : kˣ) :
(rationalWeylFDRep k (n + 1) l).character (diagGL (Fin.snoc t z)) = ∑ m ∈ interlacingWeights l, ↑(z ^ (∑ i : Fin (n + 1), ↑l i - ∑ i : Fin n, ↑m i)) * (rationalWeylFDRep k n m).character (diagGL t)

The branching rule for rational Weyl characters, for the bundled rational Weyl module.

source
theorem TauCeti.char_rationalWeylRep_glBlockSucc_diagGL (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight (n + 1)) (t : Fin n → kˣ) :
(rationalWeylRep k (n + 1) l).character ((glBlockSucc k n) (diagGL t)) = ∑ m ∈ interlacingWeights l, (rationalWeylRep k n m).character (diagGL t)

Restriction of a rational Weyl character along the block inclusion. On the diagonal torus of GL n, restricting the character of the rational Weyl module of l along GL n ↪ GL (n + 1) gives the sum of the characters of the rational Weyl modules of the dominant weights interlacing l, each occurring once.

source
theorem TauCeti.char_rationalWeylFDRep_glBlockSucc_diagGL (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight (n + 1)) (t : Fin n → kˣ) :
(rationalWeylFDRep k (n + 1) l).character ((glBlockSucc k n) (diagGL t)) = ∑ m ∈ interlacingWeights l, (rationalWeylFDRep k n m).character (diagGL t)

Restriction of a rational Weyl character along the block inclusion, for the bundled rational Weyl module.

source
theorem TauCeti.finrank_rationalWeylFDRep_succ (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight (n + 1)) :
Module.finrank k ↑(rationalWeylFDRep k (n + 1) l).V = ∑ m ∈ interlacingWeights l, Module.finrank k ↑(rationalWeylFDRep k n m).V

The dimension recursion of branching: the rational Weyl module of a dominant weight l of GL (n + 1) has dimension the sum of the dimensions of the rational Weyl modules of the dominant weights of GL n interlacing l. This is the branching rule evaluated at the identity.