Comparing the two Specht-module presentations

The Specht module of a Young diagram has two constructions in this library. It is the span of the polytabloids inside the Young permutation module, and it is the left ideal generated by the Young symmetrizer in the rational group algebra. This file identifies those constructions for the convention fixed throughout the symmetric-group development:

• the permutation module is a left module on left cosets;
• the polytabloid is e_t = b_t · {t};
• the Young symmetrizer is c_t = a_t b_t; and
• the ideal is the left ideal ℚ[Sₙ] c_t.

An element of the ideal acts on the tabloid {t}, giving an intertwining map into the polytabloid Specht module. The map is nonzero: the coefficient of {t} in c_t · {t} is the order of the row group. Both sides are irreducible, so this intertwiner is an equivalence.

Main results

• TauCeti.YoungTableau.spechtIdealToSubrepresentation: the canonical intertwining map from ℚ[Sₙ] c_t to the polytabloid Specht module.
• TauCeti.YoungTableau.spechtIdealEquivSpechtSubrepresentation: the resulting equivalence of representations.
• TauCeti.YoungTableau.spechtIdealIsoSpechtSubrepresentation: the categorical isomorphism of Rep ℚ (Equiv.Perm (Fin μ.card)) objects.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapters 3--4.
• Schur--Weyl roadmap, Layer 3, “Polytabloids and the Specht module”.

noncomputable def TauCeti.YoungTableau.spechtIdealToSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealRep.ρ.IntertwiningMap (spechtSubrepresentation μ).toRepresentation

Acting on {t} gives the canonical intertwining map from the Young-symmetrizer ideal to the polytabloid Specht module.

Equations

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

@[simp]

theorem TauCeti.YoungTableau.coe_spechtIdealToSubrepresentation_apply {μ : YoungDiagram} (t : YoungTableau μ) (x : ↥t.spechtIdeal) : ↑(t.spechtIdealToSubrepresentation x) = ((permutationModule (shapePartition μ)).ρ.asAlgebraHom ↑x) (MonoidAlgebra.single t.tabloid 1)

The canonical comparison map is evaluation of an ideal element on the tabloid {t}.

@[simp]

theorem TauCeti.YoungTableau.youngSymmetrizer_smul_tabloid_coeff_tabloid {μ : YoungDiagram} (t : YoungTableau μ) : (((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.youngSymmetrizer) (MonoidAlgebra.single t.tabloid 1)).coeff t.tabloid = ↑(Nat.card ↥t.rowSubgroup)

The coefficient of {t} in c_t · {t} is the order of the row group. In particular the canonical comparison map does not annihilate the generator of the Young-symmetrizer ideal.

theorem TauCeti.YoungTableau.spechtIdealToSubrepresentation_ne_zero {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealToSubrepresentation ≠ 0

The canonical comparison map from the Young-symmetrizer ideal to the polytabloid Specht module is nonzero.

noncomputable def TauCeti.YoungTableau.spechtIdealEquivSpechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealRep.ρ.Equiv (spechtSubrepresentation μ).toRepresentation

The Young-symmetrizer ideal and the polytabloid Specht module are equivalent representations.

Equations

• t.spechtIdealEquivSpechtSubrepresentation = t.spechtIdealToSubrepresentation.ofBijective ⋯

@[simp]

theorem TauCeti.YoungTableau.coe_spechtIdealEquivSpechtSubrepresentation_apply {μ : YoungDiagram} (t : YoungTableau μ) (x : ↥t.spechtIdeal) : ↑(t.spechtIdealEquivSpechtSubrepresentation x) = ((permutationModule (shapePartition μ)).ρ.asAlgebraHom ↑x) (MonoidAlgebra.single t.tabloid 1)

The representation equivalence sends an ideal element to its action on the tabloid {t}.

noncomputable def TauCeti.YoungTableau.spechtIdealIsoSpechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealRep ≅ Rep.of (spechtSubrepresentation μ).toRepresentation

The Young-symmetrizer ideal and the polytabloid Specht module are isomorphic as objects of Rep ℚ (Equiv.Perm (Fin μ.card)).

Equations

• t.spechtIdealIsoSpechtSubrepresentation = Rep.mkIso t.spechtIdealEquivSpechtSubrepresentation

@[simp]

theorem TauCeti.YoungTableau.spechtIdealIsoSpechtSubrepresentation_hom_hom_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (x : ↥t.spechtIdeal) : ↑((Rep.Hom.hom t.spechtIdealIsoSpechtSubrepresentation.hom) x) = ((permutationModule (shapePartition μ)).ρ.asAlgebraHom ↑x) (MonoidAlgebra.single t.tabloid 1)

The categorical comparison isomorphism sends an ideal element to its action on the tabloid {t}.

@[simp]

theorem TauCeti.YoungTableau.finrank_spechtIdeal_eq_spechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) : Module.finrank ℚ ↥t.spechtIdeal = Module.finrank ℚ ↥(spechtSubrepresentation μ).toSubmodule

The two presentations of the Specht module have the same dimension.

@[simp]

theorem TauCeti.YoungTableau.character_spechtIdeal_eq_spechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealRep.ρ.character = (spechtSubrepresentation μ).toRepresentation.character

The two presentations of the Specht module have the same character.