The Weyl module is an irreducible representation of GL n k

Over a field k of characteristic zero, the Weyl module 𝕊^μ(kⁿ) = c_t · (kⁿ)^{⊗d} of a μ-tableau t, the image of its Young symmetrizer c_t acting on the tensor power, is an irreducible representation of GL n k whenever it is nonzero, that is, whenever μ has at most n rows (TauCeti.YoungTableau.isIrreducible_weylRep). Together with the vanishing criterion TauCeti.YoungTableau.weylModule_eq_bot_iff, irreducibility holds exactly when μ.colLen 0 ≤ n (TauCeti.YoungTableau.isIrreducible_weylRep_iff), and the same holds for the shape-indexed Weyl module and its bundled forms TauCeti.weylFDRepOfShape and TauCeti.schurFunctor.

Main results

• TauCeti.YoungTableau.isAtom_weylModule: the Weyl module of a tableau with at most n rows is a minimal nonzero subrepresentation of (kⁿ)^{⊗d}.
• TauCeti.YoungTableau.isIrreducible_weylRep: it is an irreducible representation of GL n k, and TauCeti.YoungTableau.isIrreducible_weylRep_iff characterizes irreducibility by the number of rows.
• TauCeti.isIrreducible_weylRepOfShape_iff, TauCeti.simple_weylFDRepOfShape_iff and TauCeti.simple_schurFunctor_iff: the same criterion for the Weyl module of a shape, as a representation and as an object of FDRep.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 6, Theorem 6.3, proved there in §6.2 through the commutant of k[S_d]; the same commutant drives the argument here, with an annihilator computation in place of their Lemma 6.22.
• C. Procesi, Lie Groups: An Approach through Invariants and Representations (2007), Chapter 9.

theorem TauCeti.YoungTableau.isAtom_weylModule {k : Type u} [Field k] [CharZero k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) : IsAtom (weylModule k n t)

The Weyl module is a minimal subrepresentation. In characteristic zero, the Weyl module of a μ-tableau with at most n rows is an atom of the lattice of subrepresentations of (kⁿ)^{⊗|μ|}: it is nonzero and has no nonzero proper subrepresentation.

theorem TauCeti.YoungTableau.isIrreducible_weylRep {k : Type u} [Field k] [CharZero k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) : (weylRep k n t).IsIrreducible

The Weyl module is irreducible. In characteristic zero, the Weyl module 𝕊^μ(kⁿ) = c_t · (kⁿ)^{⊗|μ|} of a μ-tableau t with at most n rows is an irreducible representation of GL n k.

@[simp]

theorem TauCeti.YoungTableau.isIrreducible_weylRep_iff {k : Type u} [Field k] [CharZero k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) : (weylRep k n t).IsIrreducible ↔ μ.colLen 0 ≤ n

The irreducibility criterion for the Weyl module. In characteristic zero, the Weyl module of a μ-tableau is an irreducible representation of GL n k exactly when μ has at most n rows; otherwise it is zero.

@[simp]

theorem TauCeti.isIrreducible_weylRepOfShape_iff {k : Type u} [Field k] [CharZero k] {n : ℕ} (μ : YoungDiagram) : (weylRepOfShape k n μ).IsIrreducible ↔ μ.colLen 0 ≤ n

The irreducibility criterion for the Weyl module of a shape. In characteristic zero, the Weyl module of μ is an irreducible representation of GL n k exactly when μ has at most n rows.

@[simp]

theorem TauCeti.simple_weylFDRepOfShape_iff {k : Type u} [Field k] [CharZero k] {n : ℕ} (μ : YoungDiagram) : CategoryTheory.Simple (weylFDRepOfShape k n μ) ↔ μ.colLen 0 ≤ n

The bundled Weyl module of a shape μ is a simple object of FDRep k (GL (Fin n) k) exactly when μ has at most n rows.

theorem TauCeti.simple_schurFunctor_iff (n : ℕ) (μ : YoungDiagram) : CategoryTheory.Simple (schurFunctor n μ) ↔ μ.colLen 0 ≤ n

The Schur functor 𝕊^μ(ℂⁿ) is irreducible exactly when μ has at most n rows.