James's submodule theorem, and the irreducibility of the Specht module

Every subrepresentation U of the Young permutation module M^μ is comparable with the Specht module S^μ in a very strong sense: either S^μ ≤ U, or U is orthogonal to S^μ for the tabloid form. This dichotomy is James's submodule theorem, and it is proved here (TauCeti.spechtSubrepresentation_le_or_le_orthogonal). Since the tabloid form is positive definite, the two alternatives overlap only on the zero subrepresentation, so the theorem immediately makes S^μ an atom of the lattice of subrepresentations of M^μ, hence irreducible.

The engine is the behaviour of the column antisymmetrizer b_t on a single tabloid, which is James's Lemma 4.6: b_t · {s} is either 0 or ± e_t (TauCeti.YoungTableau.exists_eq_smul_polytabloid_single). Writing {s} = σ · {t}, the two cases are exactly the two cases of the row/column criterion of TauCeti.RepresentationTheory.Symmetric.Vanishing, read with the roles of the two tableaux exchanged.

• If a row of relabel σ t meets a column of t in two distinct labels x ≠ y, then the transposition of x and y lies in the column group of t while fixing the tabloid {s}, so pushing it across turns b_t · {s} into its own negative and kills it.
• Otherwise the row-column factorization of TauCeti.RepresentationTheory.Symmetric.Factorization writes σ⁻¹ = p q with p in the row group and q in the column group of t. The row group is the stabilizer of {t}, so {s} = q⁻¹ · {t}, and b_t absorbs q⁻¹ through its sign: b_t · {s} = sign q • e_t.

By linearity the same holds for an arbitrary vector of M^μ (TauCeti.YoungTableau.exists_eq_smul_polytabloid), and that is the dichotomy. Given a subrepresentation U, either some b_t fails to annihilate some vector of U -- and then e_t itself lies in U, and with it the span of its orbit, which is all of S^μ -- or every b_t annihilates every vector of U, and then U is orthogonal to every polytabloid, because b_t is self-adjoint for the tabloid form (TauCeti.YoungTableau.tabloidForm_asAlgebraHom_columnAntisymmetrizer) and e_t = b_t · {t}.

The dimension of S^μ, the standard basis of polytabloids indexing it, and the statement that the S^μ exhaust the irreducibles of Sₙ and are pairwise non-isomorphic are not proved here. Neither is the comparison of S^μ with the left ideal ℚ[Sₙ] c_t, which is irreducible by TauCeti.YoungTableau.isIrreducible_spechtIdealRep through an argument that shares the row-column factorization but not the tabloid form.

Main results

• TauCeti.YoungTableau.exists_eq_smul_polytabloid_single: the column antisymmetrizer sends a tabloid to a multiple of the polytabloid (James's Lemma 4.6), and TauCeti.YoungTableau.exists_eq_smul_polytabloid extends this to all of M^μ.
• TauCeti.YoungTableau.tabloidForm_asAlgebraHom_columnAntisymmetrizer: the column antisymmetrizer is self-adjoint for the tabloid form.
• TauCeti.spechtSubrepresentation_le_or_le_orthogonal: James's submodule theorem.
• TauCeti.isAtom_spechtSubrepresentation and TauCeti.isIrreducible_spechtSubrepresentation: the Specht module is a minimal subrepresentation of M^μ, hence irreducible, with TauCeti.isIrreducible_spechtModule the partition-indexed form.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4: Lemma 4.6, the submodule theorem 4.8, and Corollary 4.9.
• B. E. Sagan, The Symmetric Group, 2nd ed. (2001), Section 2.4.

James's lemma: the column antisymmetrizer of a tabloid

theorem TauCeti.YoungTableau.exists_eq_smul_polytabloid_single {μ : YoungDiagram} (t : YoungTableau μ) (T : Equiv.Perm (Fin μ.card) ⧸ youngSubgroup (shapePartition μ)) : ∃ (κ : ℚ), (κ = 0 ∨ κ = 1 ∨ κ = -1) ∧ ((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.columnAntisymmetrizer) (MonoidAlgebra.single T 1) = κ • t.polytabloid

James's Lemma 4.6. The column antisymmetrizer of t sends a μ-tabloid to a rational multiple of the polytabloid e_t; the multiple is 0 or a sign.

The tabloid is σ · {t} for some σ, and the two cases are the two cases of the row/column criterion: if a row of relabel σ t meets a column of t twice the transposition of the two shared labels fixes the tabloid while b_t sees its sign, and otherwise σ⁻¹ factors through the row and column groups of t, of which the row part fixes {t}.

theorem TauCeti.YoungTableau.exists_eq_smul_polytabloid {μ : YoungDiagram} (t : YoungTableau μ) (v : ↑(permutationModule (shapePartition μ))) : ∃ (κ : ℚ), ((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.columnAntisymmetrizer) v = κ • t.polytabloid

The column antisymmetrizer collapses M^μ onto the line spanned by the polytabloid. This is the linear extension of TauCeti.YoungTableau.exists_eq_smul_polytabloid_single from the tabloid basis to the whole Young permutation module.

Self-adjointness of the column antisymmetrizer

theorem TauCeti.YoungTableau.tabloidForm_asAlgebraHom_columnAntisymmetrizer {μ : YoungDiagram} (t : YoungTableau μ) (v w : ↑(permutationModule (shapePartition μ))) : ((tabloidForm (shapePartition μ)) (((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.columnAntisymmetrizer) v)) w = ((tabloidForm (shapePartition μ)) v) (((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.columnAntisymmetrizer) w)

The column antisymmetrizer is self-adjoint for the tabloid form. The symmetric group acts on M^μ by isometries, so moving a permutation across the form inverts it, and inversion is a sign-preserving involution of the column group.

The submodule theorem

theorem TauCeti.spechtSubrepresentation_le_or_le_orthogonal (μ : YoungDiagram) (U : Subrepresentation (permutationModule (shapePartition μ)).ρ) : spechtSubrepresentation μ ≤ U ∨ U ≤ orthogonalSubrepresentation (spechtSubrepresentation μ)

James's submodule theorem. A subrepresentation U of the Young permutation module M^μ either contains the Specht module S^μ or is orthogonal to it for the tabloid form.

The dichotomy is whether some column antisymmetrizer b_t fails to annihilate some vector of U. If it does fail, the value is a nonzero multiple of the polytabloid e_t and lies in U, so U contains the orbit of e_t, which spans S^μ. If every b_t annihilates every vector of U, then self-adjointness of b_t moves it off each polytabloid e_t = b_t · {t} and onto the vector of U, where it vanishes.

Irreducibility

theorem TauCeti.isAtom_spechtSubrepresentation (μ : YoungDiagram) : IsAtom (spechtSubrepresentation μ)

The Specht module is a minimal subrepresentation of M^μ. A nonzero subrepresentation strictly inside S^μ would, by the submodule theorem, be orthogonal to S^μ while lying in it, and the tabloid form is positive definite.

theorem TauCeti.isIrreducible_spechtSubrepresentation (μ : YoungDiagram) : (spechtSubrepresentation μ).toRepresentation.IsIrreducible

The Specht module is irreducible. This is James's Corollary 4.9 over a field of characteristic zero, in the concrete presentation of S^μ as the span of the polytabloids inside the Young permutation module.

instance TauCeti.isIrreducible_spechtModule {n : ℕ} (μ : n.Partition) : Representation.IsIrreducible (spechtModule μ).ρ

The Specht module of a partition is irreducible, in the partition-indexed packaging TauCeti.spechtModule. Transporting along the relabelling Fin n ≃ Fin (diagramOf μ).card is an isomorphism of groups, and restriction along an isomorphism preserves irreducibility.