The Weyl construction: a Young symmetrizer cuts out a GL n k-subrepresentation

Weyl's construction produces representations of GL n k from representations of the symmetric group: a Young symmetrizer c_t ∈ ℚ[S_d] acts on the tensor power (kⁿ)^{⊗d} by permuting tensor factors, and, because that action commutes with the diagonal action of GL n k, its image is a GL n k-subrepresentation. This file builds that image, the Weyl module of t.

The two inputs are already available: the image of a group-algebra element on a tensor power, as a subrepresentation (TauCeti.tensorPowerRange, built from the commuting actions), and the Young symmetrizer transported into the base ring (TauCeti.YoungTableau.youngSymmetrizerOver). Specializing the first to the standard representation of GL n k and the second to a Young symmetrizer gives TauCeti.YoungTableau.weylModule.

Two facts make the construction usable. Relabeling the tableau moves the Weyl module by the corresponding factor permutation, which is itself GL n k-equivariant, so the Weyl modules of two tableaux of the same shape are isomorphic representations (TauCeti.YoungTableau.weylRepEquiv): up to isomorphism the Weyl module depends only on the shape. That is what makes the shape-indexed form TauCeti.weylModuleOfShape, the Weyl module of the row-superstandard tableau of μ, a legitimate representative of them all. And the Weyl module is nonzero exactly when the shape has at most n rows (TauCeti.YoungTableau.weylModule_eq_bot_iff). Nonvanishing (TauCeti.YoungTableau.weylModule_ne_bot) is proved by evaluating a coordinate functional on c_t · (e_{r(1)} ⊗ ⋯ ⊗ e_{r(d)}), where r records the row of each label: the surviving terms are exactly the row group, each contributing 1, so the value is the order of the row group, nonzero in characteristic zero. Vanishing (TauCeti.YoungTableau.weylModule_eq_bot) is the transposition trick: if the first column is longer than n then, on each basis pure tensor, two of its labels carry the same basis index, so their transposition lies in the column group and fixes that pure tensor while negating c_t; the value is its own negative, hence zero because 2 is invertible.

The Young symmetrizer available here is the one built over ℚ in TauCeti.YoungTableau.youngSymmetrizer, so its coefficients reach the base ring along algebraMap ℚ k; the base ring is therefore a ℚ-algebra throughout. That is a consequence of how c_t is currently defined, not of c_t itself, whose coefficients are integral: an integral Young symmetrizer would let the construction run over any commutative ring, and building one is a separate topic. What the two halves of the criterion actually use of the hypothesis is much less. Vanishing needs only that 2 is invertible, which a ℚ-algebra gives. Nonvanishing needs characteristic zero, and a ℚ-algebra has characteristic zero as soon as it is nontrivial, so the nonvanishing statements carry a Nontrivial hypothesis instead. This is the characteristic-zero setting the roadmap works in.

Main definitions

• TauCeti.YoungTableau.weylModule: the Weyl module of a tableau, a subrepresentation of (kⁿ)^{⊗|μ|}, with weylRep the action of GL n k on it.
• TauCeti.weylModuleOfShape: the Weyl module of a shape, namely that of its row-superstandard tableau, with weylRepOfShape the action of GL n k on it and weylFDRepOfShape its bundled form in FDRep, over a Noetherian base ring.
• TauCeti.schurFunctor: the roadmap-pinned name, weylFDRepOfShape at k = ℂ.

Main results

• TauCeti.YoungTableau.weylRepEquiv: the Weyl modules of two tableaux of the same shape are isomorphic representations of GL n k, and TauCeti.YoungTableau.weylRepEquivOfShape identifies each of them with the shape-indexed one.
• TauCeti.YoungTableau.weylModule_ne_bot: the Weyl module is nonzero when the shape has at most n rows.
• TauCeti.YoungTableau.weylModule_eq_bot: the Weyl module vanishes when the shape has more than n rows.
• TauCeti.YoungTableau.weylModule_eq_bot_iff: the two directions combined, the vanishing criterion, with TauCeti.weylModuleOfShape_eq_bot_iff its shape-indexed form.
• TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_tensorPowerBasis_eq_zero: the symmetrizer kills a monomial basis vector that repeats a basis index on a column, and ...tensorPowerBasis_rowFilling_ne_zero: it does not kill the one indexed by the row filling. These are the two halves of the vanishing criterion at the level of a single basis vector.
• TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_tensorPowerBasis_mem_weylModule states that the image of any monomial basis vector under the symmetrizer belongs to the Weyl module.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6, "Weyl's construction".

• Classical groups roadmap, Layer 2, "Young symmetrizers and the Schur functor", where this object is pinned as schurFunctor. The construction itself is named weylModule here because what is constructed is the module, not a functor: the Schur functor of μ is a functor in the underlying module, and only its value at kⁿ is built. The pinned name is supplied as TauCeti.schurFunctor, the definitional re-export at k = ℂ of the bundled form, so that later roadmap layers can consume it under the name they are written against.

  Of that bullet, the GLₙ-subrepresentation, the fixed choice of tableau, the canonical isomorphism between the images for different tableaux, and the vanishing criterion are built here. The bullet's two remaining deliverables, the extreme cases S^{(d)} V ≅ Symᵈ V and S^{(1ᵈ)} V ≅ ⋀ᵈ V, are proved in TauCeti/RepresentationTheory/ClassicalGroups/ExtremeShape.lean, against TauCeti.YoungTableau.weylModule_toSubmodule and TauCeti.weylRepOfShape and without unfolding anything built here.

The Weyl module of a Young tableau

noncomputable def TauCeti.YoungTableau.weylModule (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) : Subrepresentation (tensorPowerRep k n μ.card)

The Weyl module of a μ-tableau t: the image of the Young symmetrizer c_t acting on the |μ|-fold tensor power of the standard representation of GL n k, a subrepresentation because the symmetric-group and general-linear actions commute.

Fulton and Harris write this as 𝕊^μ(kⁿ), the value at kⁿ of the Schur functor of μ; only the value is built here, and no functoriality in the underlying module is claimed.

Equations

• TauCeti.YoungTableau.weylModule k n t = TauCeti.tensorPowerRange (TauCeti.stdRep k n) μ.card (TauCeti.YoungTableau.youngSymmetrizerOver k t)

theorem TauCeti.YoungTableau.weylModule_def (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) : weylModule k n t = tensorPowerRange (stdRep k n) μ.card (youngSymmetrizerOver k t)

The Weyl module is the image of the Young symmetrizer of t acting on the tensor power, so the general lemmas about TauCeti.tensorPowerRange apply to it.

@[simp]

theorem TauCeti.YoungTableau.weylModule_toSubmodule (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) : (weylModule k n t).toSubmodule = LinearMap.range ((permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t))

The submodule underlying the Weyl module is the range of the Young symmetrizer acting on the tensor power.

@[reducible, inline]

noncomputable abbrev TauCeti.YoungTableau.weylRep (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) : Representation k (GL (Fin n) k) ↥(weylModule k n t).toSubmodule

The action of GL n k on the Weyl module.

Equations

• TauCeti.YoungTableau.weylRep k n t = (TauCeti.YoungTableau.weylModule k n t).toRepresentation

@[simp]

theorem TauCeti.YoungTableau.weylRep_apply_coe (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) (g : GL (Fin n) k) (x : ↥(weylModule k n t).toSubmodule) : ↑(((weylRep k n t) g) x) = ((tensorPowerRep k n μ.card) g) ↑x

The action on the Weyl module is the restriction of the action on the tensor power.

Independence of the tableau

theorem TauCeti.YoungTableau.weylModule_relabel {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (weylModule k n (relabel σ t)).toSubmodule = Submodule.map ((permTensorAction k n μ.card) σ) (weylModule k n t).toSubmodule

Relabeling the tableau by σ moves the Weyl module by the permutation of the tensor factors that σ induces.

noncomputable def TauCeti.YoungTableau.weylRelabelEquiv {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : ↥(weylModule k n t).toSubmodule ≃ₗ[k] ↥(weylModule k n (relabel σ t)).toSubmodule

Permuting the tensor factors by σ as a linear equivalence from the Weyl module of t to the Weyl module of the relabeled tableau σt.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.YoungTableau.weylRelabelEquiv_apply_coe {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (x : ↥(weylModule k n t).toSubmodule) : ↑((weylRelabelEquiv σ t) x) = ((permTensorAction k n μ.card) σ) ↑x

The relabeling equivalence is induced by permuting the tensor factors.

noncomputable def TauCeti.YoungTableau.weylRelabelRepEquiv {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (weylRep k n t).Equiv (weylRep k n (relabel σ t))

Permuting the tensor factors is GL n k-equivariant, so it is an isomorphism of representations from the Weyl module of t to the Weyl module of σt.

Equations

• TauCeti.YoungTableau.weylRelabelRepEquiv σ t = Representation.Equiv.mk (TauCeti.YoungTableau.weylRelabelEquiv σ t) ⋯

noncomputable def TauCeti.YoungTableau.weylRepEquiv {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t t' : YoungTableau μ) : (weylRep k n t).Equiv (weylRep k n t')

The Weyl modules of two tableaux of the same shape are isomorphic representations of GL n k: up to isomorphism the Weyl module depends only on the shape.

Equations

• t.weylRepEquiv t' = ⋯ ▸ TauCeti.YoungTableau.weylRelabelRepEquiv (t.relabelPerm t') t

The vanishing criterion

theorem TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_tensorPowerBasis_rowFilling_ne_zero {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} [Nontrivial k] (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) : ((permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t)) ((tensorPowerBasis k n μ.card) (t.rowFilling hn)) ≠ 0

The symmetrizer does not annihilate the monomial basis vector of the row filling: the coordinate of c_t • e_r at r = TauCeti.YoungTableau.rowFilling t hn is the order of the row group of t, which is nonzero in characteristic zero.

This nonzero image witnesses TauCeti.YoungTableau.weylModule_ne_bot.

theorem TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_tensorPowerBasis_mem_weylModule {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (p : Fin μ.card → Fin n) : ((permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t)) ((tensorPowerBasis k n μ.card) p) ∈ (weylModule k n t).toSubmodule

The image under the Young symmetrizer of any monomial basis vector belongs to the Weyl module.

theorem TauCeti.YoungTableau.weylModule_ne_bot {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} [Nontrivial k] (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) : weylModule k n t ≠ ⊥

The Weyl module of a μ-tableau is nonzero as soon as μ has at most n rows.

The image of the standard pure tensor e_{r(1)} ⊗ ⋯ ⊗ e_{r(d)} under the symmetrizer, where r ℓ is the row of the label ℓ, is detected by the dual coordinate functional, so it is not zero and the module it generates is not ⊥.

theorem TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_tensorPowerBasis_eq_zero {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) {p : Fin μ.card → Fin n} {a b : Fin μ.card} (hcol : t.colIndex a = t.colIndex b) (hab : a ≠ b) (hpab : p a = p b) : ((permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t)) ((tensorPowerBasis k n μ.card) p) = 0

The symmetrizer annihilates a monomial basis vector that repeats a basis index on a column. Transposing the two labels fixes the vector while negating c_t, so the value is its own negative, hence zero because 2 is invertible in a ℚ-algebra.

theorem TauCeti.YoungTableau.weylModule_eq_bot {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t : YoungTableau μ) (hn : n < μ.colLen 0) : weylModule k n t = ⊥

The Weyl module of a μ-tableau vanishes as soon as μ has more than n rows.

The |μ|-fold tensor power is spanned by the monomial basis vectors e_{p(1)} ⊗ ⋯ ⊗ e_{p(d)}. The first column of μ is longer than n, so on each of them two labels of that column share a basis index; their transposition lies in the column group, fixing the vector while negating c_t. The value of c_t is therefore its own negative, hence zero because 2 is invertible in a ℚ-algebra.

theorem TauCeti.YoungTableau.weylModule_eq_bot_iff {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} [Nontrivial k] (t : YoungTableau μ) : weylModule k n t = ⊥ ↔ n < μ.colLen 0

The vanishing criterion for the Weyl module: it vanishes exactly when the shape has more rows than the dimension of the standard representation.

Invariants of the Weyl module

theorem TauCeti.YoungTableau.finrank_weylModule_eq {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} (t t' : YoungTableau μ) : Module.finrank k ↥(weylModule k n t).toSubmodule = Module.finrank k ↥(weylModule k n t').toSubmodule

The Weyl modules of two tableaux of the same shape are isomorphic k-modules, so their Module.finrank values agree; over a field this is the equality of their dimensions.

theorem TauCeti.YoungTableau.nontrivial_weylModule {k : Type u} [CommRing k] [Algebra ℚ k] {n : ℕ} {μ : YoungDiagram} [Nontrivial k] (t : YoungTableau μ) (hn : μ.colLen 0 ≤ n) : Nontrivial ↥(weylModule k n t).toSubmodule

The Weyl module of a shape with at most n rows is nontrivial.

The Weyl module of a shape

noncomputable def TauCeti.weylModuleOfShape (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) : Subrepresentation (tensorPowerRep k n μ.card)

The Weyl module of a shape μ: the Weyl module of the row-superstandard tableau of μ, the canonical μ-tableau. Since the Weyl modules of two μ-tableaux are isomorphic representations, this is a legitimate shape-indexed representative of them all; the identification is TauCeti.YoungTableau.weylRepEquivOfShape.

This is the object the classical-groups roadmap pins as schurFunctor n μ.

Equations

• TauCeti.weylModuleOfShape k n μ = TauCeti.YoungTableau.weylModule k n (TauCeti.StandardYoungTableau.rowSuperstandard μ).toTableau

theorem TauCeti.weylModuleOfShape_def (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) : weylModuleOfShape k n μ = YoungTableau.weylModule k n (StandardYoungTableau.rowSuperstandard μ).toTableau

The Weyl module of a shape is the Weyl module of its row-superstandard tableau, so the tableau-indexed lemmas apply to it.

@[reducible, inline]

noncomputable abbrev TauCeti.weylRepOfShape (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) : Representation k (GL (Fin n) k) ↥(weylModuleOfShape k n μ).toSubmodule

The action of GL n k on the Weyl module of a shape.

Equations

• TauCeti.weylRepOfShape k n μ = (TauCeti.weylModuleOfShape k n μ).toRepresentation

@[simp]

theorem TauCeti.weylModuleOfShape_toSubmodule (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) : (weylModuleOfShape k n μ).toSubmodule = LinearMap.range ((permTensorActionAlgHom k n μ.card) (YoungTableau.youngSymmetrizerOver k (StandardYoungTableau.rowSuperstandard μ).toTableau))

The submodule underlying the Weyl module of a shape is the range of the Young symmetrizer of its row-superstandard tableau acting on the tensor power.

@[simp]

theorem TauCeti.weylRepOfShape_apply_coe (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) (g : GL (Fin n) k) (x : ↥(weylModuleOfShape k n μ).toSubmodule) : ↑(((weylRepOfShape k n μ) g) x) = ((tensorPowerRep k n μ.card) g) ↑x

The action on the Weyl module of a shape is the restriction of the action on the tensor power.

noncomputable def TauCeti.YoungTableau.weylRepEquivOfShape (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) : (weylRep k n t).Equiv (weylRepOfShape k n μ)

The Weyl module of any μ-tableau is isomorphic, as a representation of GL n k, to the Weyl module of the shape μ.

Equations

• TauCeti.YoungTableau.weylRepEquivOfShape k n t = t.weylRepEquiv (TauCeti.StandardYoungTableau.rowSuperstandard μ).toTableau

theorem TauCeti.weylModuleOfShape_eq_bot_iff (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) [Nontrivial k] (μ : YoungDiagram) : weylModuleOfShape k n μ = ⊥ ↔ n < μ.colLen 0

The vanishing criterion for the Weyl module of a shape: it vanishes exactly when the shape has more rows than the dimension of the standard representation.

theorem TauCeti.nontrivial_weylModuleOfShape (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) [Nontrivial k] (μ : YoungDiagram) (hn : μ.colLen 0 ≤ n) : Nontrivial ↥(weylModuleOfShape k n μ).toSubmodule

The Weyl module of a shape with at most n rows is nontrivial.

@[reducible, inline]

noncomputable abbrev TauCeti.weylFDRepOfShape (k : Type u) [CommRing k] [Algebra ℚ k] [IsNoetherianRing k] (n : ℕ) (μ : YoungDiagram) : FDRep k (GL (Fin n) k)

The Weyl module of a shape, bundled as an object of FDRep.

FDRep is the category of finitely generated representations over any ring, and a submodule of the tensor power is finitely generated as soon as the base ring is Noetherian, which is all this bundled form asks; a field is the case of interest, and is Noetherian.

Equations

• TauCeti.weylFDRepOfShape k n μ = FDRep.of (TauCeti.weylRepOfShape k n μ)

@[reducible, inline]

noncomputable abbrev TauCeti.schurFunctor (n : ℕ) (μ : YoungDiagram) : FDRep ℂ (GL (Fin n) ℂ)

The Schur functor 𝕊^μ(ℂⁿ) in the roadmap's pinned form: the Weyl module of the shape μ over ℂ, bundled as an object of FDRep ℂ (GL (Fin n) ℂ).

This is a definitional re-export of TauCeti.weylFDRepOfShape at k = ℂ, under the name later roadmap layers are written against; the general form, over any Noetherian commutative ring that is a ℚ-algebra, is TauCeti.weylFDRepOfShape, and the unbundled construction is TauCeti.weylModuleOfShape.

Equations

• TauCeti.schurFunctor n μ = TauCeti.weylFDRepOfShape ℂ n μ