The Weyl modules of the two extreme shapes: symmetric and exterior powers

The Weyl construction TauCeti.YoungTableau.weylModule cuts a subrepresentation of (kⁿ)^{⊗d} out of a Young symmetrizer c_t. This file evaluates it at the two extreme shapes, where the symmetrizer degenerates and the answer is a power of the standard representation:

• a shape with at most one row has the whole symmetric group as its row group and a trivial column group, so c_t is the symmetrization ∑_σ σ and the Weyl module is Symᵈ(kⁿ);
• a shape with at most one column has the whole symmetric group as its column group and a trivial row group, so c_t is the antisymmetrization ∑_σ sgn(σ) σ and the Weyl module is ⋀ᵈ(kⁿ).

Both are proved the same way, and the two halves of the argument are already in place. On the linear-algebra side, SymmetricPower.toTensorPower and Mathlib's exteriorPower.toTensorPower map the symmetric and the exterior power into the tensor power, with image exactly the image of the symmetrization, respectively antisymmetrization, operator, and are injective because composing back is multiplication by d!, invertible over a ℚ-algebra. On the symmetric-group side, the extreme-shape lemmas of TauCeti/RepresentationTheory/Symmetric/Symmetrizer.lean collapse c_t to a single factor and evaluate it in the group algebra, which is read here as an operator on the tensor power. Both maps are equivariant for GL n k, because GL n k acts diagonally and the two operators only permute tensor factors; so the identification of subspaces is an isomorphism of representations, by Representation.IntertwiningMap.equivOfRange.

The hypotheses are stated on the shape, as μ.colLen 0 ≤ 1 and μ.rowLen 0 ≤ 1, which is how TauCeti.YoungTableau.rowSubgroup_eq_top_iff and TauCeti.YoungTableau.colSubgroup_eq_top_iff read the two degeneracies off the diagram. No condition relating μ.card to n is needed: for a one-column shape with μ.card > n both sides are zero, the exterior power because it is above the rank and the Weyl module by TauCeti.YoungTableau.weylModule_eq_bot, and the isomorphism holds vacuously.

Main results

• TauCeti.YoungTableau.weylRepEquivSymPowerRep: 𝕊^{(d)}(kⁿ) ≅ Symᵈ(kⁿ), the Weyl module of a shape with at most one row is the symmetric power, with TauCeti.weylRepOfShapeEquivSymPowerRep its shape-indexed form.
• TauCeti.YoungTableau.weylRepEquivExtPowerRep: 𝕊^{(1ᵈ)}(kⁿ) ≅ ⋀ᵈ(kⁿ), the Weyl module of a shape with at most one column is the exterior power, with TauCeti.weylRepOfShapeEquivExtPowerRep its shape-indexed form.
• TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_of_rowSubgroup_eq_top and TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_of_colSubgroup_eq_top: the operators on the tensor power that c_t becomes at the two extreme shapes.

Implementation notes

The symmetric statements are over a base ring in Type, not in Type u: Mathlib's SymmetricPower R ι M requires R and the index type ι to lie in the same universe, and the index type here is Fin μ.card. The exterior statements carry no such restriction. This matches TauCeti.symPowerRep, which is already monomorphic for the same reason.

The results are stated for an arbitrary tableau of the shape, not only for the row-superstandard one, since the Weyl module of any tableau of a given shape is the image of an operator that the extreme-shape hypothesis pins down completely. The shape-indexed forms are then the special case of the row-superstandard tableau, which is what TauCeti.weylModuleOfShape is defined from.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6, "Weyl's construction", where 𝕊^{(d)}V = Sym^d V and 𝕊^{(1^d)}V = ⋀^d V are the two extreme cases of the construction.

The Young symmetrizer of an extreme shape

theorem TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_of_rowSubgroup_eq_top (k : Type u) [CommSemiring k] [Algebra ℚ k] {μ : YoungDiagram} (n : ℕ) (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) : (permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t) = ∑ σ : Equiv.Perm (Fin μ.card), ↑(PiTensorProduct.reindex k (fun (x : Fin μ.card) => Fin n → k) σ)

On a shape with at most one row the Young symmetrizer acts on the tensor power by the symmetrization operator ∑_σ σ.

theorem TauCeti.YoungTableau.permTensorActionAlgHom_youngSymmetrizerOver_of_colSubgroup_eq_top (k : Type u) [CommRing k] [Algebra ℚ k] {μ : YoungDiagram} (n : ℕ) (t : YoungTableau μ) (h : t.colSubgroup = ⊤) : (permTensorActionAlgHom k n μ.card) (youngSymmetrizerOver k t) = ∑ σ : Equiv.Perm (Fin μ.card), ↑(Equiv.Perm.sign σ) • ↑(PiTensorProduct.reindex k (fun (x : Fin μ.card) => Fin n → k) σ)

On a shape with at most one column the Young symmetrizer acts on the tensor power by the antisymmetrization operator ∑_σ sgn(σ) σ.

A shape with at most one row: the symmetric power

noncomputable def TauCeti.symPowerToTensorPower (k : Type) [CommRing k] (n d : ℕ) : (symPowerRep k n d).IntertwiningMap (tensorPowerRep k n d)

The symmetrization, as an intertwining map of the symmetric power of the standard representation with its tensor power.

Equations

• TauCeti.symPowerToTensorPower k n d = { toLinearMap := SymmetricPower.toTensorPower k (Fin d) (Fin n → k), isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.symPowerToTensorPower_toLinearMap (k : Type) [CommRing k] (n d : ℕ) : (symPowerToTensorPower k n d).toLinearMap = SymmetricPower.toTensorPower k (Fin d) (Fin n → k)

noncomputable def TauCeti.YoungTableau.weylRepEquivSymPowerRep (k : Type) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.colLen 0 ≤ 1) : (weylRep k n t).Equiv (symPowerRep k n μ.card)

𝕊^{(d)}(kⁿ) ≅ Symᵈ(kⁿ): the Weyl module of a shape with at most one row is the symmetric power of the standard representation.

Equations

• TauCeti.YoungTableau.weylRepEquivSymPowerRep k n t h = (TauCeti.symPowerRepEquivWeylRep✝ k n t h).symm

@[simp]

theorem TauCeti.YoungTableau.toTensorPower_weylRepEquivSymPowerRep (k : Type) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.colLen 0 ≤ 1) (x : ↥(weylModule k n t).toSubmodule) : (SymmetricPower.toTensorPower k (Fin μ.card) (Fin n → k)) ((weylRepEquivSymPowerRep k n t h) x) = ↑x

The isomorphism TauCeti.YoungTableau.weylRepEquivSymPowerRep is inverse to the symmetrization: symmetrizing its value returns the element of the tensor power it was applied to.

noncomputable def TauCeti.weylRepOfShapeEquivSymPowerRep (k : Type) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) (h : μ.colLen 0 ≤ 1) : (weylRepOfShape k n μ).Equiv (symPowerRep k n μ.card)

The shape-indexed form of TauCeti.YoungTableau.weylRepEquivSymPowerRep.

Equations

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

@[simp]

theorem TauCeti.weylRepOfShapeEquivSymPowerRep_apply (k : Type) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) (h : μ.colLen 0 ≤ 1) (x : ↥(weylModuleOfShape k n μ).toSubmodule) : (weylRepOfShapeEquivSymPowerRep k n μ h) x = (YoungTableau.weylRepEquivSymPowerRep k n (StandardYoungTableau.rowSuperstandard μ).toTableau h) ((YoungTableau.weylRepEquivOfShape k n (StandardYoungTableau.rowSuperstandard μ).toTableau).symm x)

The shape-indexed isomorphism is the tableau-indexed one at the row-superstandard tableau, after moving the argument along TauCeti.YoungTableau.weylRepEquivOfShape.

A shape with at most one column: the exterior power

noncomputable def TauCeti.extPowerToTensorPower (k : Type u) [CommRing k] (n d : ℕ) : (extPowerRep k n d).IntertwiningMap (tensorPowerRep k n d)

The antisymmetrization, as an intertwining map of the exterior power of the standard representation with its tensor power.

Equations

• TauCeti.extPowerToTensorPower k n d = { toLinearMap := exteriorPower.toTensorPower k (Fin n → k) d, isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.extPowerToTensorPower_toLinearMap (k : Type u) [CommRing k] (n d : ℕ) : (extPowerToTensorPower k n d).toLinearMap = exteriorPower.toTensorPower k (Fin n → k) d

noncomputable def TauCeti.YoungTableau.weylRepEquivExtPowerRep (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.rowLen 0 ≤ 1) : (weylRep k n t).Equiv (extPowerRep k n μ.card)

𝕊^{(1ᵈ)}(kⁿ) ≅ ⋀ᵈ(kⁿ): the Weyl module of a shape with at most one column is the exterior power of the standard representation.

Equations

• TauCeti.YoungTableau.weylRepEquivExtPowerRep k n t h = (TauCeti.extPowerRepEquivWeylRep✝ k n t h).symm

@[simp]

theorem TauCeti.YoungTableau.toTensorPower_weylRepEquivExtPowerRep (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.rowLen 0 ≤ 1) (x : ↥(weylModule k n t).toSubmodule) : (exteriorPower.toTensorPower k (Fin n → k) μ.card) ((weylRepEquivExtPowerRep k n t h) x) = ↑x

The isomorphism TauCeti.YoungTableau.weylRepEquivExtPowerRep is inverse to the antisymmetrization: antisymmetrizing its value returns the element of the tensor power it was applied to.

noncomputable def TauCeti.weylRepOfShapeEquivExtPowerRep (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) (h : μ.rowLen 0 ≤ 1) : (weylRepOfShape k n μ).Equiv (extPowerRep k n μ.card)

The shape-indexed form of TauCeti.YoungTableau.weylRepEquivExtPowerRep.

Equations

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

@[simp]

theorem TauCeti.weylRepOfShapeEquivExtPowerRep_apply (k : Type u) [CommRing k] [Algebra ℚ k] (n : ℕ) (μ : YoungDiagram) (h : μ.rowLen 0 ≤ 1) (x : ↥(weylModuleOfShape k n μ).toSubmodule) : (weylRepOfShapeEquivExtPowerRep k n μ h) x = (YoungTableau.weylRepEquivExtPowerRep k n (StandardYoungTableau.rowSuperstandard μ).toTableau h) ((YoungTableau.weylRepEquivOfShape k n (StandardYoungTableau.rowSuperstandard μ).toTableau).symm x)

The shape-indexed isomorphism is the tableau-indexed one at the row-superstandard tableau, after moving the argument along TauCeti.YoungTableau.weylRepEquivOfShape.