Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Branching.Rationality

Rational representations under the block inclusion #

The block inclusion TauCeti.glBlockSucc : GL (Fin n) ℂ →* GL (Fin (n + 1)) ℂ replaces a matrix g by diag(g, 1). Polynomial and rational functions pull back along it (TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_polynomialFunctions and TauCeti.Matrix.GeneralLinearGroup.comp_glBlockSucc_mem_rationalFunctions), so polynomial and rational representations remain so after restriction.

Applying this to the rational Weyl representations gives the coordinate-regularity statement needed by the GL (n + 1) ↓ GL n branching problem. This file does not construct the multiplicity-free decomposition of that restriction; the decomposition additionally needs the highest-weight classification and complete reducibility.

Main results #

Restriction of representations #

source
theorem TauCeti.IsPolynomialRep.comp_glBlockSucc {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin (n + 1)) ℂ) W} (h : IsPolynomialRep ρ) :
IsPolynomialRep (MonoidHom.comp ρ (glBlockSucc ℂ n))

A polynomial representation remains polynomial after restriction along the block inclusion.

source
theorem TauCeti.IsRationalRep.comp_glBlockSucc {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin (n + 1)) ℂ) W} (h : IsRationalRep ρ) :
IsRationalRep (MonoidHom.comp ρ (glBlockSucc ℂ n))

A rational representation remains rational after restriction along the block inclusion.

Restricted rational Weyl representations #

source
@[simp]
theorem TauCeti.isRationalRep_rationalWeylRep_comp_glBlockSucc (n : ℕ) (l : DominantWeight (n + 1)) :
IsRationalRep (MonoidHom.comp (rationalWeylRep ℂ (n + 1) l) (glBlockSucc ℂ n))

The restriction of a rational Weyl representation from GL (n + 1) to GL n is rational. This is the rationality input for its multiplicity-free branching decomposition.