The branching rule from GL (n + 1) ℂ to GL n ℂ

Restrict an irreducible rational representation V_λ of GL (n + 1) ℂ along the block inclusion TauCeti.glBlockSucc : GL n ℂ →* GL (n + 1) ℂ, g ↦ diag(g, 1). The branching rule says that the restriction is multiplicity free,

V_λ|_{GL n} ≅ ⨁_{μ ≺ λ} V_μ,

the sum running over the dominant weights μ of GL n interlacing λ (λᵢ ≥ μᵢ ≥ λᵢ₊₁, TauCeti.interlacingWeights), each once. This file proves it as an equivalence of representations (TauCeti.nonempty_equiv_rationalWeylRep_comp_glBlockSucc), and in the polynomial form for the Weyl module of a Young diagram (TauCeti.nonempty_equiv_weylRepOfShape_comp_glBlockSucc), where the sum runs over the diagrams interlacing the given one with at most n rows.

Both sides are rational representations of GL n ℂ: the restriction by TauCeti.IsRationalRep.comp_glBlockSucc, the direct sum by TauCeti.IsRationalRep.directSum. Their characters agree on the diagonal torus by the branching rule for characters (TauCeti.char_rationalWeylRep_glBlockSucc_diagGL and TauCeti.char_weylRepOfShape_glBlockSucc_diagGL), and rational representations with equal characters on the diagonal torus are equivalent (TauCeti.IsRationalRep.nonempty_equiv_of_forall_character_diagGL_eq).

Main results

• TauCeti.nonempty_equiv_rationalWeylRep_comp_glBlockSucc: the branching rule for the rational Weyl modules, indexed by dominant weights.
• TauCeti.nonempty_equiv_weylRepOfShape_comp_glBlockSucc: the branching rule for the polynomial Weyl modules, indexed by Young diagrams.

Both are equivalences of representations; TauCeti.nonempty_fdRepIso_iff reads them as isomorphisms of the corresponding objects of FDRep ℂ (GL (Fin n) ℂ).

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants (2009), Section 8.1: the branching law from GL n to GL (n - 1).

theorem TauCeti.nonempty_equiv_rationalWeylRep_comp_glBlockSucc (n : ℕ) (l : DominantWeight (n + 1)) : Nonempty (Representation.Equiv (MonoidHom.comp (rationalWeylRep ℂ (n + 1) l) (glBlockSucc ℂ n)) (Representation.directSum fun (m : ↥(interlacingWeights l)) => rationalWeylRep ℂ n ↑m))

The branching rule from GL (n + 1) ℂ to GL n ℂ. The rational Weyl module V_λ of a dominant weight λ of GL (n + 1), restricted along the block inclusion g ↦ diag(g, 1), is the direct sum of the rational Weyl modules V_μ of the dominant weights μ of GL n interlacing λ, each occurring once.

theorem TauCeti.nonempty_equiv_weylRepOfShape_comp_glBlockSucc (n : ℕ) (μ : YoungDiagram) : Nonempty (Representation.Equiv (MonoidHom.comp (weylRepOfShape ℂ (n + 1) μ) (glBlockSucc ℂ n)) (Representation.directSum fun (ν : ↥(YoungDiagram.interlacingShapes n μ)) => weylRepOfShape ℂ n ↑ν))

The branching rule for polynomial representations. The Weyl module of a Young diagram μ for GL (n + 1) ℂ, restricted along the block inclusion g ↦ diag(g, 1), is the direct sum of the Weyl modules for GL n ℂ of the diagrams with at most n rows interlacing μ, each occurring once.