The Specht modules of the one-row and the one-column shape #
The two extreme partitions 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 polytabloid
presentation S^μ, the span of the polytabloids inside the Young permutation module M^μ, and
then for the partition-indexed packaging TauCeti.spechtModule that the classification of the
irreducibles is stated in. It also reads off the two rows χ^{(n)} = 1 and χ^{(1ⁿ)} = sgn of
the integer character table of Sₙ.
The mechanism is the same on both shapes: the orbit of a single polytabloid e_t consists of
scalar multiples of e_t, so the Specht module is the line ℚ ∙ e_t and the symmetric group acts
on it through those scalars. What differs is where the scalars come from.
- On a shape with at most one row the column group of
tis trivial, soe_tis the bare tabloid{t}(TauCeti.YoungTableau.polytabloid_eq_single_of_colSubgroup_eq_bot); and the row group oftis everything, so every permutation fixes{t}, the row group being the stabilizer of a tabloid. The scalars are all1. - On a shape with at most one column the column group of
tis everything, so every permutation is a column permutation oftand rescalese_tby its sign (TauCeti.YoungTableau.polytabloid_relabel_of_mem_colSubgroup). The scalars are the signs.
The two shape hypotheses come in the two equivalent forms that
TauCeti.YoungTableau.rowSubgroup_eq_top_iff and TauCeti.YoungTableau.colSubgroup_eq_top_iff
relate. A statement whose conclusion mentions a tableau t — the polytabloid identities, and the
description of the Specht module as the line through e_t — is stated on the row resp. column
group of that t, as in TauCeti.RepresentationTheory.Symmetric.Specht.Ideal.Extremes, which
proves the same two identifications for the left-ideal presentation ℚ[Sₙ] c_t. A statement
about spechtSubrepresentation μ alone is stated on the diagram, as μ.colLen 0 ≤ 1 resp.
μ.rowLen 0 ≤ 1, so that no tableau has to be produced to use it; the partition-level results
below feed those hypotheses with TauCeti.colLen_diagramOf_indiscrete_le_one and
TauCeti.rowLen_diagramOf_ones_le_one. The two hypotheses are compatible rather than exclusive:
on the empty diagram both hold, and there Sₙ is trivial and so are both characters.
"Is the trivial representation" and "is the sign representation" are stated the way the ideal file
states them, as the action formula together with the dimension: a line on which σ acts by 1
resp. by sgn σ. No isomorphism with a separately constructed model object is built here. The
third named small irreducible, the standard representation S^{(n-1,1)}, is not treated here
either; it is not a line and needs the tabloid combinatorics of the two-row shape, which is
TauCeti.RepresentationTheory.Symmetric.Specht.SingletonSecondRow.
Main results #
TauCeti.spechtSubrepresentation_toRepresentation_eq_trivial:S^{(n)}is the trivial representation, andTauCeti.finrank_spechtSubrepresentation_of_colLen_le_onethat it is a line.TauCeti.spechtSubrepresentation_toRepresentation_apply_of_rowLen_le_one:S^{(1ⁿ)}is the sign representation, andTauCeti.finrank_spechtSubrepresentation_of_rowLen_le_onethat it too is a line.TauCeti.spechtModule_indiscrete_ρ_apply,TauCeti.finrank_spechtModule_indiscrete,TauCeti.spechtModule_ones_ρ_applyandTauCeti.finrank_spechtModule_ones: the same four statements for the partition-indexed Specht modulesS^{(n)}andS^{(1ⁿ)}.TauCeti.spechtChar_indiscreteandTauCeti.spechtChar_ones: the two integer characters,χ^{(n)} = 1andχ^{(1ⁿ)} = sgn.TauCeti.symmetricCharacterTable_indiscreteandTauCeti.symmetricCharacterTable_ones: the two extreme rows of the character table ofSₙ, the all-ones row and the row of signs, the latter read off the number of parts of the cycle type.
References #
- G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4.
- W. Fulton, Young Tableaux, Section 7.2.
- Schur--Weyl roadmap, Layer 4, "the named small irreducibles", and Layer 6, the special values of the Specht character.
The polytabloids of the two extreme shapes #
Every permutation fixes the polytabloid of a tableau all of whose labels share a row: the polytabloid is the bare tabloid, and the row group, which is everything, is its stabilizer.
Every permutation scales the polytabloid of a tableau all of whose labels share a column by its
sign: every permutation is then a column permutation of t.
A Specht module whose generating polytabloid is a group eigenvector #
Both extreme shapes are instances of one situation: the polytabloid e_t is an eigenvector of
every group element, with eigenvalue χ σ. Then the orbit of e_t spans the line through it, so
that line is the whole Specht module and the group acts on it through χ.
The one-row shape gives the trivial representation #
The Specht module of a shape with at most one row is the line through any of its polytabloids.
The Specht module of a shape with at most one row is a line.
The symmetric group fixes the Specht module of a shape with at most one row pointwise.
S^{(n)} is the trivial representation: on a shape with at most one row the symmetric
group acts trivially on the span of the polytabloids. Together with
TauCeti.finrank_spechtSubrepresentation_of_colLen_le_one this identifies it as the
one-dimensional trivial representation.
The one-column shape gives the sign representation #
The Specht module of a shape with at most one column is the line through any of its polytabloids.
The Specht module of a shape with at most one column is a line.
S^{(1ⁿ)} is the sign representation: on a shape with at most one column the symmetric
group acts on the span of the polytabloids through the sign character. Together with
TauCeti.finrank_spechtSubrepresentation_of_rowLen_le_one this identifies it as the
one-dimensional sign representation.
The partition-indexed Specht modules of the two extreme partitions #
S^{(n)} is the trivial representation: the symmetric group fixes it pointwise.
This is not a simp lemma: TauCeti.spechtModule is an abbrev for an FDRep.of, so
FDRep.of_ρ' already rewrites its left-hand side to the action of
TauCeti.spechtSubrepresentation along the relabelling.
S^{(n)} is the trivial representation, in the extensional form its character is read
off.
S^{(1ⁿ)} is the sign representation: the symmetric group acts on it through the sign
character. The sign is unchanged by the relabelling Fin n ≃ Fin (diagramOf (1ⁿ)).card that
TauCeti.spechtModule transports along.
This is not a simp lemma, for the reason given at
TauCeti.spechtModule_indiscrete_ρ_apply.
The two extreme rows of the character table of Sₙ #
χ^{(n)} = 1: the character of the trivial representation, whose value is the dimension of
its carrier.
χ^{(1ⁿ)} = sgn: the character of the sign representation.
The (n) entry of the character table is 1 on every class, the trivial character taking
that value everywhere.
The (1ⁿ) entry of the character table is the sign of the class of cycle type ν, read
off the number of parts of ν by Equiv.Perm.sign_of_parts_partition; the parts of
Equiv.Perm.partition include the fixed points, so the correction is the ambient n.
The row of (n) in the character table of Sₙ is the all-ones row, the trivial character
taking the value 1 on every conjugacy class.
This is not a simp lemma: TauCeti.symmetricCharacterTable_apply already rewrites its left-hand
side to TauCeti.spechtCharValue, where TauCeti.spechtCharValue_indiscrete finishes the
reduction.
The row of (1ⁿ) in the character table of Sₙ is the row of signs, the sign character
evaluated on the class of cycle type ν.
This is not a simp lemma, for the reason given at
TauCeti.symmetricCharacterTable_indiscrete.