The character of a rational Weyl module is a Laurent symmetric polynomial

A Young diagram has nonnegative row lengths, so Schur polynomials only reach the polynomial representations of GL n. The character of the rational Weyl module TauCeti.rationalWeylRep k n λ of a general dominant weight λ is instead a Laurent symmetric polynomial on the diagonal torus: with m = λₙ the determinant-twist exponent (TauCeti.DominantWeight.detShift) and μ the polynomial part of λ (TauCeti.DominantWeight.detShiftShape),

χ_{V_λ}(diag t) = (∏ᵢ tᵢ)^m · s_μ(t),

the determinant character to a possibly negative power times a genuine Schur polynomial. That is TauCeti.char_rationalWeylRep_diagonal_eq_eval_diagramSchurPoly.

The presentation of λ as a shifted diagram is not unique unless the diagram is required to have at most n - 1 rows, and the formula does not care which presentation is used: TauCeti.char_rationalWeylRep_shift_weightOfShape_diagonal evaluates the character of V_{ν + m·(1, …, 1)} as (∏ᵢ tᵢ)^m · s_ν(t) for every Young diagram ν with at most n rows, not only for the polynomial part. Two facts combine to give it. Shifting a weight multiplies the torus character by a power of the determinant (TauCeti.char_rationalWeylRep_shift_diagonal), the twist being invisible to the polynomial part. And a weight that is already the weight of a diagram ν needs no twist at all: the rational Weyl module of TauCeti.weightOfShape n ν has the same character as the Weyl module 𝕊^ν(kⁿ) (TauCeti.char_rationalWeylRep_weightOfShape_diagonal), even when ν has a nonzero n-th row and the canonical presentation therefore carries a nontrivial determinant twist. That last identity is the representation-theoretic reading of TauCeti.diagramSchurPoly_eq_prod_X_pow_mul_of_rowLen_eq_add: the full column block that the canonical presentation strips off the diagram is exactly the determinant character it puts back.

Identifying TauCeti.rationalWeylRep k n λ as the irreducible of highest weight λ belongs to the highest-weight classification and is not claimed here, so these are statements about the construction, not yet about a classified irreducible.

Main results

• TauCeti.char_rationalWeylRep_diagonal_eq_eval_diagramSchurPoly and its bundled form TauCeti.char_rationalWeylFDRep_diagonal_eq_eval_diagramSchurPoly: the torus character of a rational Weyl module is a determinant twist of a Schur polynomial.
• TauCeti.char_rationalWeylRep_shift_diagonal and its bundled form TauCeti.char_rationalWeylFDRep_shift_diagonal: shifting the weight by m multiplies the torus character by the m-th power of the determinant.
• TauCeti.char_rationalWeylRep_weightOfShape_diagonal and its bundled form TauCeti.char_rationalWeylFDRep_weightOfShape_diagonal: on the weight of a Young diagram the rational Weyl module has the character of the Weyl module of that diagram.
• TauCeti.char_rationalWeylRep_shift_weightOfShape_diagonal and its bundled form TauCeti.char_rationalWeylFDRep_shift_weightOfShape_diagonal: the Laurent character read off an arbitrary presentation λ = ν + m·(1, …, 1) of the weight.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15, where the rational representations of GL n are the determinant twists of the polynomial ones and their characters are the corresponding Laurent symmetric functions.

theorem TauCeti.char_rationalWeylRep_diagonal_eq_eval_diagramSchurPoly (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight n) (t : Fin n → kˣ) : (rationalWeylRep k n l).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ l.detShift) * (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k l.detShiftShape)

The torus character of a rational Weyl module is a Laurent symmetric polynomial: it is the determinant character to the power λₙ times the Schur polynomial of the polynomial part of λ. Both factors are needed, the power being negative exactly when λₙ is.

theorem TauCeti.char_rationalWeylFDRep_diagonal_eq_eval_diagramSchurPoly (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight n) (t : Fin n → kˣ) : (rationalWeylFDRep k n l).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ l.detShift) * (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k l.detShiftShape)

The Laurent character of the bundled rational Weyl module, the same identity read in FDRep.

theorem TauCeti.char_rationalWeylRep_shift_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight n) (m : ℤ) (t : Fin n → kˣ) : (rationalWeylRep k n (l.shift m)).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ m) * (rationalWeylRep k n l).character (diagGL t)

Shifting a dominant weight by m twists the torus character by det ^ m. The polynomial part of a weight is unchanged by the shift, so the two characters differ by the determinant factor alone.

theorem TauCeti.char_rationalWeylFDRep_shift_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) (l : DominantWeight n) (m : ℤ) (t : Fin n → kˣ) : (rationalWeylFDRep k n (l.shift m)).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ m) * (rationalWeylFDRep k n l).character (diagGL t)

The determinant twist along a shift of the weight, for the bundled rational Weyl module.

theorem TauCeti.char_rationalWeylRep_weightOfShape_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {ν : YoungDiagram} (hν : ν.colLen 0 ≤ n) (t : Fin n → kˣ) : (rationalWeylRep k n (weightOfShape n ν)).character (diagGL t) = (weylRepOfShape k n ν).character (diagGL t)

On the weight of a Young diagram the determinant twist is invisible: the rational Weyl module of TauCeti.weightOfShape n ν has the torus character of the Weyl module 𝕊^ν(kⁿ). The canonical presentation of that weight strips the full column block of height n off ν and records it as a power of the determinant, and TauCeti.diagramSchurPoly_eq_prod_X_pow_mul_of_rowLen_eq_add says that the two cancel.

theorem TauCeti.char_rationalWeylFDRep_weightOfShape_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {ν : YoungDiagram} (hν : ν.colLen 0 ≤ n) (t : Fin n → kˣ) : (rationalWeylFDRep k n (weightOfShape n ν)).character (diagGL t) = (weylFDRepOfShape k n ν).character (diagGL t)

The absence of a determinant twist on the weight of a Young diagram, for the bundled rational Weyl module.

theorem TauCeti.char_rationalWeylRep_shift_weightOfShape_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {ν : YoungDiagram} (hν : ν.colLen 0 ≤ n) (m : ℤ) (t : Fin n → kˣ) : (rationalWeylRep k n ((weightOfShape n ν).shift m)).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ m) * (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k ν)

The Laurent character of a rational Weyl module, read off an arbitrary presentation of its weight: for every Young diagram ν with at most n rows and every m, the torus character of V_{ν + m·(1, …, 1)} is (∏ᵢ tᵢ)^m · s_ν(t). The canonical presentation TauCeti.char_rationalWeylRep_diagonal_eq_eval_diagramSchurPoly is the case where ν has at most n - 1 rows; here the number of rows is only bounded by n, so the shift m need not be the last entry of the weight.

theorem TauCeti.char_rationalWeylFDRep_shift_weightOfShape_diagonal (k : Type u) [Field k] [CharZero k] (n : ℕ) {ν : YoungDiagram} (hν : ν.colLen 0 ≤ n) (m : ℤ) (t : Fin n → kˣ) : (rationalWeylFDRep k n ((weightOfShape n ν).shift m)).character (diagGL t) = ↑((∏ i : Fin n, t i) ^ m) * (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (diagramSchurPoly n k ν)

The Laurent character read off an arbitrary presentation, for the bundled rational Weyl module.