The standard representation of the symmetric group

The symmetric group on a finite type α acts on k[α] by permuting the standard basis. Inside that permutation representation sit the invariant line spanned by the sum of the basis, carrying the trivial representation, and the standard representation, the subrepresentation of dimension |α| - 1 on which the coefficients sum to zero; when |α| is invertible in k the two are complementary and the permutation representation splits as their direct sum. This file proves that the standard representation is irreducible whenever |α| ≥ 2 and either |α| = 2 or |α| is invertible in k.

The hypothesis 2 ≤ |α| is needed: for |α| ≤ 1 the standard representation is zero, and the zero representation is not irreducible. Given 2 ≤ |α|, the disjunction is sharp. Invertibility of |α| cannot simply be dropped: as soon as 3 ≤ |α| and |α| = 0 in k, the sum of the standard basis itself has vanishing coefficient sum, so the invariant line lies inside the standard subrepresentation, and it is a proper subrepresentation because the standard one has dimension |α| - 1 ≥ 2, so the latter is reducible -- this is the first place the modular theory departs from the ordinary one, and it is excluded here rather than developed. The remaining case is the first disjunct: for |α| = 2 the standard subrepresentation is a line -- in characteristic 2 it is the invariant line -- and hence irreducible whatever the characteristic.

The argument is elementary and uses only transpositions. If v has vanishing coefficient sum and is nonzero, two of its coefficients differ, say at x and y; subtracting the transposition (x y) applied to v from v leaves exactly (v x - v y) • (x - y), so any nonzero invariant subspace contains one difference x - y of basis vectors. Transposing y with an arbitrary z produces all the others, and those differences span.

Main definitions

• TauCeti.standardRepresentation: the standard representation of Equiv.Perm α on the augmentation subrepresentation of k[α], with TauCeti.toRepresentation_augmentationSubrepresentation naming it as the action that subrepresentation carries, which is the form a splitting of k[α] produces.

Main results

• TauCeti.sub_ofMulAction_swap: applying a transposition to v and subtracting leaves a multiple of a difference of two standard basis vectors. This is the whole computational content.
• TauCeti.isAtom_augmentationSubrepresentation: the standard subrepresentation is an atom of the lattice of subrepresentations of k[α], and TauCeti.isIrreducible_standardRepresentation: hence it is irreducible.
• TauCeti.char_standardRepresentation: its character is the character of k[α] less 1, the 1 being the character of the trivial quotient of k[α] by the standard subrepresentation.

The two remaining halves of the picture hold for an arbitrary permutation representation and are proved there, in TauCeti.RepresentationTheory.Augmentation: that k[α] is the direct sum of the invariant line and the standard subrepresentation, again under |α| ≠ 0 in k (or α empty), is TauCeti.isCompl_invariantLine_augmentationSubrepresentation, and that the standard subrepresentation has dimension |α| - 1 is TauCeti.finrank_augmentationSubrepresentation.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, §2.1, where the standard representation of Sₙ is introduced as the complement of the trivial summand in the permutation representation.
• G. D. James, The Representation Theory of the Symmetric Groups, §4, for the same representation as the Specht module of the shape (n-1, 1).
• Schur--Weyl roadmap, Layer 4, "the named small irreducibles", which asks for M^{(n-1,1)} = triv ⊕ standard with the standard summand the (n-1)-dimensional irreducible.

Transpositions and differences of basis vectors

theorem TauCeti.sub_ofMulAction_swap {k : Type u_1} [CommRing k] {α : Type u_2} [DecidableEq α] (x y : α) (v : MonoidAlgebra k α) : v - ((Representation.ofMulAction k (Equiv.Perm α) α) (Equiv.swap x y)) v = (v.coeff x - v.coeff y) • (MonoidAlgebra.single x 1 - MonoidAlgebra.single y 1)

Subtracting from v the effect of the transposition (x y) leaves the difference of the two coefficients times the difference of the two standard basis vectors: a transposition changes only the two coefficients it swaps. This is the step that produces a difference of basis vectors from an arbitrary vector, and it needs no hypothesis relating x and y.

The standard representation

noncomputable def TauCeti.standardRepresentation (k : Type u_1) [CommSemiring k] (α : Type u_2) : Representation k (Equiv.Perm α) ↥(augmentationSubrepresentation k (Equiv.Perm α) α).toSubmodule

The standard representation of the symmetric group on α: the action of Equiv.Perm α on the vectors of k[α] whose coefficients sum to zero. No hypothesis on k or on α is imposed here; when α is finite and (Fintype.card α : k) ≠ 0 it is a complement of the invariant line in the permutation representation k[α], by isCompl_invariantLine_augmentationSubrepresentation, whereas when (Fintype.card α : k) = 0 the invariant line lies inside it instead. Over ℚ and on the labels α = Fin μ.card of a Young diagram μ whose second row is a single cell and which has no third row -- a shape (m, 1) -- it is the Specht module S^μ, by TauCeti.standardRepresentationEquivSpechtSubrepresentation of TauCeti.RepresentationTheory.Symmetric.Specht.SingletonSecondRow; for the partition (n+1, 1) of n+2 that reads, on α = Fin (n+2), as S^{(n+1,1)} = standard.

Equations

• TauCeti.standardRepresentation k α = (TauCeti.augmentationSubrepresentation k (Equiv.Perm α) α).toRepresentation

@[simp]

theorem TauCeti.toRepresentation_augmentationSubrepresentation (k : Type u_1) [CommSemiring k] (α : Type u_2) : (augmentationSubrepresentation k (Equiv.Perm α) α).toRepresentation = standardRepresentation k α

The standard representation is the action carried by the augmentation subrepresentation, which is how a splitting of k[α] into subrepresentations names it.

@[simp]

theorem TauCeti.coe_standardRepresentation_apply {k : Type u_1} [CommSemiring k] {α : Type u_2} (g : Equiv.Perm α) (v : ↥(augmentationSubrepresentation k (Equiv.Perm α) α).toSubmodule) : ↑(((standardRepresentation k α) g) v) = ((Representation.ofMulAction k (Equiv.Perm α) α) g) ↑v

The standard representation acts by permuting the standard basis: on underlying elements of k[α] it is the permutation representation.

@[simp]

theorem TauCeti.char_standardRepresentation {k : Type u_1} [Field k] {α : Type u_2} [Finite α] [Nonempty α] (g : Equiv.Perm α) : (standardRepresentation k α).character g = (Representation.ofMulAction k (Equiv.Perm α) α).character g - 1

The character of the standard representation is the character of the permutation representation k[α] less 1. The subtracted 1 is the character of the one-dimensional quotient of k[α] by the standard subrepresentation, which is trivial in every characteristic -- the quotient map is the augmentation k[α] → k -- so no hypothesis on |α| in k is needed. Only when (Fintype.card α : k) ≠ 0 is that quotient realised inside k[α], as the invariant line complementing the standard subrepresentation and splitting a trivial constituent off it; when (Fintype.card α : k) = 0 and 3 ≤ |α| the invariant line lies inside the standard subrepresentation instead.

theorem TauCeti.isAtom_augmentationSubrepresentation {k : Type u_1} [Field k] {α : Type u_2} [Fintype α] (h2 : 2 ≤ Fintype.card α) (hchar : Fintype.card α = 2 ∨ ↑(Fintype.card α) ≠ 0) : IsAtom (augmentationSubrepresentation k (Equiv.Perm α) α)

The standard subrepresentation is minimal. A nonzero subrepresentation of the permutation representation contained in the standard one is the whole of it: from a nonzero vector with vanishing coefficient sum one produces, by transpositions, every difference of standard basis vectors, and those span. For a two-element α the standard subrepresentation is a line, so it is minimal whatever the characteristic.

theorem TauCeti.isIrreducible_standardRepresentation {k : Type u_1} [Field k] {α : Type u_2} [Fintype α] (h2 : 2 ≤ Fintype.card α) (hchar : Fintype.card α = 2 ∨ ↑(Fintype.card α) ≠ 0) : (standardRepresentation k α).IsIrreducible

The standard representation is irreducible. Given 2 ≤ |α|, the hypothesis is sharp: for |α| = 2 the standard representation is a line, hence irreducible whatever the characteristic, and for 3 ≤ |α| with |α| = 0 in k the invariant line is a proper nonzero subrepresentation of it.