Absolute irreducibility of rational Specht modules

Every endomorphism of a rational Specht module that commutes with the symmetric-group action is scalar. Equivalently, the endomorphism algebra of S^mu is ℚ. This is the Schur-index-one statement needed to pass from the rational Specht classification to irreducible complex representations.

The proof uses the same column-antisymmetrizer calculation as James's submodule theorem. For a tableau t, the antisymmetrizer b_t maps the whole permutation module onto the line spanned by the polytabloid e_t. Moreover, e_t = b_t v for some v already in the Specht module. An equivariant endomorphism therefore maps e_t to a scalar multiple of itself. Since the orbit of e_t spans the Specht module, the endomorphism is that scalar everywhere.

Main results

• TauCeti.algebraMap_intertwiningMap_spechtSubrepresentation_bijective: the scalar map onto the equivariant endomorphisms of the diagram-indexed Specht representation is bijective.
• TauCeti.algebraMap_intertwiningMap_spechtModule_bijective: the partition-indexed version for spechtModule.
• TauCeti.spechtModuleEndAlgEquiv: the ℚ[S_n]-linear endomorphism algebra of S^mu is isomorphic to ℚ.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 2.4.
• Schur--Weyl roadmap, Layer 4, "Absolute irreducibility".

theorem TauCeti.algebraMap_intertwiningMap_spechtSubrepresentation_bijective (mu : YoungDiagram) : Function.Bijective ⇑(algebraMap ℚ ((spechtSubrepresentation mu).toRepresentation.IntertwiningMap (spechtSubrepresentation mu).toRepresentation))

Every equivariant endomorphism of the diagram-indexed rational Specht representation is a scalar. In the canonical algebra structure on intertwining endomorphisms, this says that the algebra map from ℚ is bijective.

theorem TauCeti.algebraMap_intertwiningMap_spechtModule_bijective {n : ℕ} (mu : n.Partition) : Function.Bijective ⇑(algebraMap ℚ (Representation.IntertwiningMap (spechtModule mu).ρ (spechtModule mu).ρ))

Every equivariant endomorphism of the partition-indexed rational Specht module is scalar.

noncomputable def TauCeti.spechtModuleIntertwiningEndAlgEquiv {n : ℕ} (mu : n.Partition) : Representation.IntertwiningMap (spechtModule mu).ρ (spechtModule mu).ρ ≃ₐ[ℚ] ℚ

The algebra of intertwining endomorphisms of a rational Specht module is ℚ.

Equations

• TauCeti.spechtModuleIntertwiningEndAlgEquiv mu = (TauCeti.spechtModuleScalarAlgEquiv✝ mu).symm

noncomputable def TauCeti.spechtModuleEndAlgEquiv {n : ℕ} (mu : n.Partition) : Module.End (MonoidAlgebra ℚ (Equiv.Perm (Fin n))) (Representation.asModule (spechtModule mu).ρ) ≃ₐ[ℚ] ℚ

The algebra of ℚ[S_n]-linear endomorphisms of a rational Specht module is ℚ.

Equations

• TauCeti.spechtModuleEndAlgEquiv mu = (Representation.IntertwiningMap.equivAlgEnd (TauCeti.spechtModule mu).ρ).symm.trans (TauCeti.spechtModuleIntertwiningEndAlgEquiv mu)