The Specht ideal is irreducible

For a Young tableau t of shape μ, the left ideal ℚ[Sₙ] c_t generated by the Young symmetrizer c_t = a_t b_t carries an irreducible representation of Sₙ (TauCeti.YoungTableau.isIrreducible_spechtIdealRep). This is the Specht module in its ideal presentation, and the theorem is the one all of its representation theory rests on.

Everything the proof needs is already in place. The sandwich calculation of TauCeti.RepresentationTheory.Symmetric.Factorization says that c_t x c_t is always a rational multiple of c_t, and Maschke's theorem says that ℚ[Sₙ] is semisimple. Take a left ideal W ≤ ℚ[Sₙ] c_t and split into the two cases the sandwich calculation allows.

• If c_t w = 0 for every w ∈ W, then W is square-zero: an element of W is a c_t by hypothesis, so a product of two elements of W is a (c_t w) = 0. A square-zero left ideal of a semisimple ring vanishes (TauCeti.Submodule.eq_bot_of_forall_mul_eq_zero), so W = ⊥.
• Otherwise c_t w ≠ 0 for some w = a c_t ∈ W, and c_t w = c_t a c_t is κ • c_t with κ ≠ 0. It lies in W, hence so does c_t, hence so does the whole ideal it generates, and W is everything.

So ℚ[Sₙ] c_t is an atom of the lattice of left ideals, which is exactly simplicity of the module it carries; the transfer to the language of representations is TauCeti.Representation.isIrreducible_ofModule'_iff.

Running the first case on W = ℚ[Sₙ] c_t itself, which is nonzero, shows that the sandwich is not identically zero: some c_t a c_t is a nonzero multiple of c_t (TauCeti.YoungTableau.exists_ne_zero_eq_smul_youngSymmetrizer_mul_mul). Whether the scalar attached to a = 1 is itself nonzero -- that is, whether c_t * c_t = (n! / f^μ) • c_t with the stated nonzero scalar -- does not follow from the sandwich calculation alone (over M₂(ℚ) the element e₁₂ sandwiches to a line and squares to zero), and is not proved here.

The statement is made at the Representation level. Its FDRep mirror is Simple (spechtIdealFDRep t), which follows from FDRep.simple_iff_isIrreducible and the irreducibility theorem below.

On the one-row and the one-column shape the Specht ideal is a line, by the dimension count of TauCeti.RepresentationTheory.Symmetric.Specht.Ideal.Extremes, so on those shapes this theorem is visible without any of the above; there is nothing extra to say about them here. The identification of this representation with the span of the polytabloids inside the Young permutation module, and the classification saying that these exhaust the irreducibles of Sₙ and are pairwise non-isomorphic across shapes, are separate targets and are not claimed here.

Main results

• TauCeti.YoungTableau.exists_ne_zero_eq_smul_youngSymmetrizer_mul_mul: the sandwich c_t x c_t is a nonzero multiple of c_t for some x.
• TauCeti.YoungTableau.isAtom_spechtIdeal: ℚ[Sₙ] c_t is an atom of the lattice of left ideals.
• TauCeti.YoungTableau.isSimpleModule_spechtIdeal: it is a simple ℚ[Sₙ]-module.
• TauCeti.YoungTableau.isIrreducible_spechtIdealRep: it is an irreducible representation of Sₙ.

References

• W. Fulton, Young Tableaux, Section 7.2, Theorem 5.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Theorem 4.3.
• Schur--Weyl roadmap, Layer 4, "irreducibility".

theorem TauCeti.YoungTableau.exists_ne_zero_eq_smul_youngSymmetrizer_mul_mul {μ : YoungDiagram} (t : YoungTableau μ) : ∃ (a : MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))) (κ : ℚ), κ ≠ 0 ∧ t.youngSymmetrizer * a * t.youngSymmetrizer = κ • t.youngSymmetrizer

The sharpened form of TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer_mul_mul: for some element of the group algebra the scalar it sandwiches the Young symmetrizer by is nonzero.

theorem TauCeti.YoungTableau.isAtom_spechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : IsAtom t.spechtIdeal

The Specht ideal is an atom of the lattice of left ideals of ℚ[Sₙ]: it is nonzero, and a left ideal strictly inside it is zero.

theorem TauCeti.YoungTableau.isSimpleModule_spechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : IsSimpleModule (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))) ↥t.spechtIdeal

The Specht ideal is a simple ℚ[Sₙ]-module.

instance TauCeti.YoungTableau.isIrreducible_spechtIdealRep {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdealRep.ρ.IsIrreducible

The Specht module is irreducible, in its presentation as the left ideal ℚ[Sₙ] c_t.