The highest weight determines a Weyl module

Over a field k that is a ℚ-algebra, the rational Weyl module V_λ = det ^ λₙ ⊗ 𝕊^μ(kⁿ) of a dominant weight λ of GL n k has λ as its highest weight in the dominance order: λ is a weight of V_λ, and every weight a of V_λ satisfies

∑_{j < m} a j ≤ ∑_{j < m} λ j for every bound m.

The weights of a representation are an isomorphism invariant (Representation.Equiv.weightSpace_eq_bot_iff), and the dominance order is antisymmetric, so a representation has at most one weight that occurs and dominates all of its weights. Hence distinct dominant weights give non-isomorphic rational Weyl modules: V_λ ≅ V_λ' exactly when λ = λ'. In the same way, when μ has at most n rows, the Weyl module 𝕊^ν(kⁿ) of a Young diagram ν is isomorphic to 𝕊^μ(kⁿ) exactly when ν = μ; the row bound is needed, since every diagram with more than n rows has the zero Weyl module.

Together with the irreducibility of V_λ (TauCeti.isIrreducible_rationalWeylRep), this says that λ ↦ V_λ is an injective map from the dominant weights of GL n to the isomorphism classes of irreducible representations, TauCeti.SimpleFDRepClasses k (GL n k) (TauCeti.rationalWeylFDRepClass_injective): half of the theorem of the highest weight for GL n. The other half, that every irreducible rational representation is some V_λ, is TauCeti.IsRationalRep.exists_nonempty_equiv_rationalWeylRep in TauCeti.RepresentationTheory.ClassicalGroups.WeylModule.Classification.

Main results

• TauCeti.eq_of_forall_sum_filter_lt_le: the dominance order on integer vectors is antisymmetric.
• Representation.Equiv.eq_of_forall_sum_filter_lt_le: a weight that occurs in a representation and dominates all of its weights is an isomorphism invariant.
• TauCeti.weightSpace_rationalWeylRep_self_ne_bot and TauCeti.sum_le_sum_of_weightSpace_rationalWeylRep_ne_bot: λ is the highest weight of the rational Weyl module of λ.
• TauCeti.rationalWeylRep_apply_transvectionUnit_eq_self: over ℂ, the vectors of weight λ in V_λ are fixed by every transvection xᵢⱼ(c) with i < j, so they are highest weight vectors; TauCeti.weylRepOfShape_apply_transvectionUnit_eq_self is the same for the vectors of weight μ in the Weyl module 𝕊^μ(ℂⁿ) of a Young diagram μ.
• TauCeti.nonempty_equiv_rationalWeylRep_iff and TauCeti.nonempty_iso_rationalWeylFDRep_iff: rational Weyl modules of distinct dominant weights are not isomorphic.
• TauCeti.rationalWeylFDRepClass and TauCeti.rationalWeylFDRepClass_injective: the isomorphism class of V_λ as a simple object, and λ ↦ V_λ is injective on the isomorphism classes of irreducible representations.
• TauCeti.nonempty_equiv_weylRepOfShape_iff and TauCeti.nonempty_iso_weylFDRepOfShape_iff: a Young diagram with at most n rows is recovered from its Weyl module.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15, where the Weyl modules are identified as the irreducible representations of GL n with given highest weight, and their determinant twists as the rational ones.

The highest weight of a rational Weyl module

theorem TauCeti.weightSpace_rationalWeylRep_self_ne_bot {n : ℕ} (k : Type u) [CommRing k] [Algebra ℚ k] [Nontrivial k] (l : DominantWeight n) : weightSpace (rationalWeylRep k n l) ↑l ≠ ⊥

A dominant weight is a weight of its own rational Weyl module: the twist by det ^ λₙ moves the highest weight of the Weyl module of the polynomial part of λ back to λ.

theorem TauCeti.sum_le_sum_of_weightSpace_rationalWeylRep_ne_bot {n : ℕ} {k : Type u} [Field k] [Algebra ℚ k] {l : DominantWeight n} {a : Fin n → ℤ} (ha : weightSpace (rationalWeylRep k n l) a ≠ ⊥) (m : ℕ) : ∑ j : Fin n with ↑j < m, a j ≤ ∑ j : Fin n with ↑j < m, ↑l j

Every weight of the rational Weyl module of λ is dominated by λ: the weights are those of the Weyl module of the polynomial part of λ, which are dominated by its shape, translated by the constant λₙ.

theorem TauCeti.rationalWeylRep_apply_transvectionUnit_eq_self {n : ℕ} (l : DominantWeight n) {i j : Fin n} (hij : i < j) {v : ↥(weylModuleOfShape ℂ n l.detShiftShape).toSubmodule} (hv : v ∈ weightSpace (rationalWeylRep ℂ n l) ↑l) (c : ℂ) : ((rationalWeylRep ℂ n l) (transvectionUnit ⋯ c)) v = v

The vectors of weight λ in the rational Weyl module V_λ are highest weight vectors: every transvection xᵢⱼ(c) with i < j fixes each vector of weight λ.

theorem TauCeti.weylRepOfShape_apply_transvectionUnit_eq_self {n : ℕ} (μ : YoungDiagram) {i j : Fin n} (hij : i < j) {v : ↥(weylModuleOfShape ℂ n μ).toSubmodule} (hv : v ∈ weightSpace (weylRepOfShape ℂ n μ) ↑(weightOfShape n μ)) (c : ℂ) : ((weylRepOfShape ℂ n μ) (transvectionUnit ⋯ c)) v = v

The vectors of weight μ in the Weyl module 𝕊^μ(ℂⁿ) are highest weight vectors: every transvection xᵢⱼ(c) with i < j fixes each vector of the weight of the shape μ.

Distinct highest weights give non-isomorphic Weyl modules

theorem TauCeti.nonempty_equiv_rationalWeylRep_iff {n : ℕ} (k : Type u) [Field k] [Algebra ℚ k] {l l' : DominantWeight n} : Nonempty ((rationalWeylRep k n l).Equiv (rationalWeylRep k n l')) ↔ l = l'

Rational Weyl modules of distinct dominant weights are not isomorphic: the dominant weight is recovered from the representation as its highest weight.

theorem TauCeti.nonempty_iso_rationalWeylFDRep_iff {n : ℕ} (k : Type u) [Field k] [Algebra ℚ k] {l l' : DominantWeight n} : Nonempty (rationalWeylFDRep k n l ≅ rationalWeylFDRep k n l') ↔ l = l'

The rational Weyl modules of distinct dominant weights are non-isomorphic objects of FDRep.

theorem TauCeti.nonempty_equiv_weylRepOfShape_iff {n : ℕ} (k : Type u) [Field k] [Algebra ℚ k] {μ ν : YoungDiagram} (hμ : μ.colLen 0 ≤ n) : Nonempty ((weylRepOfShape k n μ).Equiv (weylRepOfShape k n ν)) ↔ μ = ν

A Young diagram with at most n rows is recovered from its Weyl module: a Weyl module isomorphic to that of μ is the Weyl module of μ itself. The Weyl module of μ is nonzero, so the other diagram has at most n rows as well, and the shape is then read off as the highest weight. Without the row bound the statement fails, since all diagrams with more than n rows have the zero Weyl module.

theorem TauCeti.nonempty_iso_weylFDRepOfShape_iff {n : ℕ} (k : Type u) [Field k] [Algebra ℚ k] {μ ν : YoungDiagram} (hμ : μ.colLen 0 ≤ n) : Nonempty (weylFDRepOfShape k n μ ≅ weylFDRepOfShape k n ν) ↔ μ = ν

A Young diagram with at most n rows is recovered from its Weyl module as an object of FDRep.

The isomorphism class of a rational Weyl module

noncomputable def TauCeti.rationalWeylFDRepClass {n : ℕ} (k : Type u) [Field k] [CharZero k] (l : DominantWeight n) : SimpleFDRepClasses k (GL (Fin n) k)

The isomorphism class of the rational Weyl module V_λ as a simple object of FDRep k (GL n k), in parallel with TauCeti.spechtModuleFDRepClass. Naming the class needs V_λ to be simple, so the hypotheses are those of TauCeti.isIrreducible_rationalWeylRep: characteristic zero rather than a bare ℚ-algebra structure.

@[simp]

theorem TauCeti.rationalWeylFDRepClass_def {n : ℕ} (k : Type u) [Field k] [CharZero k] (l : DominantWeight n) : rationalWeylFDRepClass k l = SimpleFDRepClasses.mk (rationalWeylFDRep k n l)

theorem TauCeti.rationalWeylFDRepClass_injective {n : ℕ} (k : Type u) [Field k] [CharZero k] : Function.Injective (rationalWeylFDRepClass k)

λ ↦ V_λ is injective on isomorphism classes: distinct dominant weights of GL n name distinct isomorphism classes of irreducible rational representations. This is the injectivity half of the highest-weight classification; that every irreducible rational representation is some V_λ is TauCeti.IsRationalRep.exists_nonempty_equiv_rationalWeylRep.