The Specht ideals of the one-row and the one-column shape

The two extreme shapes of a partition of n are the single row (n) and the single column (1ⁿ), and their Specht modules are the two representations of Sₙ that are visible without any representation theory: the trivial one and the sign one. This file proves that for the left-ideal presentation ℚ[Sₙ] c_t of the Specht module. Both are lines, so both are irreducible, but that is a special case of TauCeti.YoungTableau.isIrreducible_spechtIdealRep in TauCeti.RepresentationTheory.Symmetric.Specht.Ideal.Irreducible, which holds for every shape, and is not restated here.

The shape hypotheses are stated on the row and column groups rather than on the diagram, because that is the form the symmetrizer identities consume: rowSubgroup t = ⊤ says that all the labels share a row, and colSubgroup t = ⊤ says that all of them share a column. Each is supplied by a diagram-level criterion, YoungTableau.rowSubgroup_eq_top_iff and YoungTableau.colSubgroup_eq_top_iff in TauCeti.RepresentationTheory.Symmetric.RowColumnSubgroup, which say that the two hypotheses hold exactly for the shapes intended: a diagram has at most one row exactly when its zeroth column has length at most one, and dually. The two hypotheses are compatible rather than exclusive -- the empty diagram satisfies both, and there Sₙ is trivial and so are the sign and the trivial representation.

The two eigenvector identities YoungTableau.single_mul_youngSymmetrizer_of_rowSubgroup_eq_top and ..._of_colSubgroup_eq_top are in TauCeti.RepresentationTheory.Symmetric.Symmetrizer: for a shape with at most one row the column antisymmetrizer is 1, so c_t is the sum of the whole group and every group element fixes it; for a shape with at most one column the row symmetrizer is 1, so c_t is the signed sum of the whole group and every group element scales it by its sign. What is left for this file is that either way c_t spans a ℚ-line inside ℚ[Sₙ], which is therefore the whole left ideal it generates, and that the action on that line is the character in question.

Only the ideal presentation ℚ[Sₙ] c_t of the Specht module is available here, so that is what these results are about; the identification of S^λ with the span of the polytabloids inside the Young permutation module is a separate milestone and is not used or claimed. The corresponding statements one level down, that the permutation module M^{(n)} is the trivial representation and M^{(1ⁿ)} the regular one, are in TauCeti.RepresentationTheory.Symmetric.PermutationModule.Extremes.

Main results

• YoungTableau.spechtIdealRep_ρ_eq_trivial: the one-row Specht ideal is the trivial representation.
• YoungTableau.spechtIdealRep_ρ_apply_of_colSubgroup_eq_top: the one-column Specht ideal is the sign representation.
• YoungTableau.finrank_spechtIdeal_of_rowSubgroup_eq_top and YoungTableau.finrank_spechtIdeal_of_colSubgroup_eq_top: both are lines.
• YoungTableau.youngSymmetrizer_sq_of_rowSubgroup_eq_top and YoungTableau.youngSymmetrizer_sq_of_colSubgroup_eq_top: because both are lines, the scalar in the essential idempotence of c_t is the full n!.

References

• W. Fulton, Young Tableaux, Section 7.2.
• Schur--Weyl roadmap, Layer 4, "the named small irreducibles".

The left ideal generated by an eigenvector of the group

The one-row shape gives the trivial representation

theorem TauCeti.YoungTableau.finrank_spechtIdeal_of_rowSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) : Module.finrank ℚ ↥t.spechtIdeal = 1

The Specht ideal of a shape with at most one row is a line.

theorem TauCeti.YoungTableau.spechtIdealRep_ρ_apply_of_rowSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) (g : Equiv.Perm (Fin μ.card)) (x : ↥t.spechtIdeal) : (t.spechtIdealRep.ρ g) x = x

The symmetric group fixes the Specht ideal of a shape with at most one row pointwise.

theorem TauCeti.YoungTableau.spechtIdealRep_ρ_eq_trivial {μ : YoungDiagram} (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) : t.spechtIdealRep.ρ = Representation.trivial ℚ (Equiv.Perm (Fin μ.card)) ↥t.spechtIdeal

S^{(n)} is the trivial representation: on a shape with at most one row the Specht ideal ℚ[Sₙ] c_t carries the trivial action of Sₙ. Together with YoungTableau.finrank_spechtIdeal_of_rowSubgroup_eq_top this identifies it as the one-dimensional trivial representation.

The one-column shape gives the sign representation

theorem TauCeti.YoungTableau.finrank_spechtIdeal_of_colSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.colSubgroup = ⊤) : Module.finrank ℚ ↥t.spechtIdeal = 1

The Specht ideal of a shape with at most one column is a line.

theorem TauCeti.YoungTableau.spechtIdealRep_ρ_apply_of_colSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.colSubgroup = ⊤) (g : Equiv.Perm (Fin μ.card)) (x : ↥t.spechtIdeal) : (t.spechtIdealRep.ρ g) x = ↑↑(Equiv.Perm.sign g) • x

S^{(1ⁿ)} is the sign representation: on a shape with at most one column the symmetric group acts on the Specht ideal ℚ[Sₙ] c_t through the sign character. Together with YoungTableau.finrank_spechtIdeal_of_colSubgroup_eq_top this identifies it as the one-dimensional sign representation.

The essential idempotence on the extreme shapes

On both extreme shapes the left ideal is a line, so the scalar in TauCeti.YoungTableau.youngSymmetrizer_sq is the full n!. These are the two cases in which it can be read off directly, and they check the normalisation.

theorem TauCeti.YoungTableau.youngSymmetrizer_sq_of_rowSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) : t.youngSymmetrizer * t.youngSymmetrizer = ↑μ.card.factorial • t.youngSymmetrizer

On a shape with at most one row the square of the Young symmetrizer is n! times itself.

theorem TauCeti.YoungTableau.youngSymmetrizer_sq_of_colSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.colSubgroup = ⊤) : t.youngSymmetrizer * t.youngSymmetrizer = ↑μ.card.factorial • t.youngSymmetrizer

On a shape with at most one column the square of the Young symmetrizer is n! times itself.