Rationality of Weyl representations

Weyl modules are images of Young symmetrizers acting on tensor powers of the standard representation. The tensor power is polynomial, and the canonical map from it onto the image is a surjective intertwining map. Since polynomiality passes to quotients, this realizes every Weyl representation over ℂ as a polynomial representation.

A rational Weyl representation is a Weyl representation tensored with an integral determinant power. Determinant powers are rational and tensor products of rational representations are rational, so the tensor-product presentation TauCeti.tprodEquivRationalWeylRep proves rationality of every rational Weyl representation.

These facts provide the coordinate-regularity input for restricting rational Weyl representations along inclusions of general linear groups. They do not assert that rational Weyl representations exhaust the rational representations; that requires the highest-weight classification.

Main results

• TauCeti.isPolynomialRep_weylRepOfShape: a Weyl representation is polynomial.
• TauCeti.isRationalRep_rationalWeylRep: a rational Weyl representation is rational.

Polynomial Weyl representations

@[simp]

theorem TauCeti.isPolynomialRep_weylRepOfShape (n : ℕ) (μ : YoungDiagram) : IsPolynomialRep (weylRepOfShape ℂ n μ)

A Weyl representation over ℂ is polynomial. It is the image of its Young symmetrizer on a tensor power of the polynomial standard representation.

Rational Weyl representations

@[simp]

theorem TauCeti.isRationalRep_rationalWeylRep (n : ℕ) (l : DominantWeight n) : IsRationalRep (rationalWeylRep ℂ n l)

A rational Weyl representation over ℂ is rational. Its tensor-product presentation is the product of a rational determinant power with a polynomial Weyl representation.