Mackey on S₃: the point stabilizer against the alternating subgroup #
The roadmap's smallest Mackey example takes G = S₃ and contrasts its two kinds of proper
nontrivial subgroup.
From H = ⟨(1 2)⟩, the two-element subgroup generated by a transposition and hence the stabilizer
of the remaining point, nothing induces irreducibly. Inducing a linear character of H gives a
three-dimensional representation of S₃, which the roadmap records as sgn ⊕ standard for the
sign character, and which the Mackey criterion reports reducible. This file proves that for every
representation of H, not only for a linear character: H is a non-normal subgroup of prime
order, so TauCeti.not_simple_indFDRep_of_prime_card_of_not_normal applies with no information
about the representation at all.
For the sign character of H the two constituents can be named. Over any field, the character of
Ind_H^{S₃} (sgn|_H) is sgn + χ_standard, where sgn is the sign character of S₃ and
χ_standard is the character of TauCeti.standardRepresentation -- the two-dimensional
constituent that the permutation representation of three points splits off. Over an algebraically
closed field of characteristic zero, the remaining results below produce the faithful character
needed for the A₃ example. For the point-stabilizer example, characteristic zero alone ensures
that representations are determined by their characters, so the identity is a decomposition
Ind_H^{S₃} (sgn|_H) ≅ sgn ⊕ standard, exhibiting the reducibility that the Mackey criterion
detects without naming the pieces.
From the normal subgroup A₃, on the other hand, every faithful linear character induces
irreducibly, producing the two-dimensional irreducible of S₃. Here the normal-subgroup Mackey
criterion, read on a linear character by
TauCeti.simple_indFDRep_ofLinearCharacter_iff_centralizer_le, reduces the question to whether
anything outside A₃ centralizes A₃, and nothing does. A faithful linear character exists
because A₃ is cyclic of order three and the coefficient field has enough roots of unity for the
exponent of A₃ -- which an algebraically closed field of characteristic zero does, having a
primitive cube root of unity.
S₃ is realized as Equiv.Perm (Fin 3), the two-element subgroup as the point stabilizer
MulAction.stabilizer (Equiv.Perm (Fin 3)) a -- which
TauCeti.stabilizer_perm_fin_three_eq_zpowers identifies with the subgroup generated by the
transposition of the two points other than a -- and A₃ as Mathlib's
alternatingGroup (Fin 3). Those identifications, the two orders, the non-normality of the
stabilizer and the centralizer of A₃ are group theory and live in
TauCeti.GroupTheory.Perm.FinThree.Basic; all this file adds is the passage to representations,
which is what makes it a worked example rather than a further piece of theory.
Main statements #
TauCeti.not_simple_indFDRep_stabilizer_perm_fin_three: nothing induced from a point stabilizer ofS₃is irreducible, in particular not the roadmap's linear characters.TauCeti.signLinearCharacter_comp_stabilizer_subtype_ne_one: the sign character of the point stabilizer is nontrivial, in characteristic other than two.TauCeti.character_indFDRep_sign_stabilizer_perm_fin_three: the character ofInd_{C₂}^{S₃} (sgn)issgn + χ_standard, over any field.TauCeti.nonempty_equiv_indFDRep_sign_stabilizer_perm_fin_three: henceInd_{C₂}^{S₃} (sgn) ≅ sgn ⊕ standardover a field of characteristic zero.TauCeti.simple_indFDRep_ofLinearCharacter_alternatingGroup_fin_three: a faithful linear character ofA₃induces irreducibly toS₃.TauCeti.finrank_indFDRep_ofLinearCharacter_alternatingGroup_fin_three: what it induces to is two-dimensional, so this is the two-dimensional irreducible ofS₃.TauCeti.exists_monoidHom_alternatingGroup_fin_three_injective: a faithful linear character ofA₃exists, so the previous two statements are not vacuous.
References #
The "Mackey on a small group" worked example of the induction and restriction roadmap, in both its reducible and its irreducible half.
- J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.4.
Nothing induced from a point stabilizer of S₃ is irreducible. This is the roadmap's
Ind_{C₂}^{S₃} example: the subgroup has prime order two and is not normal, so
TauCeti.not_simple_indFDRep_of_prime_card_of_not_normal refutes irreducibility for every
representation A whatsoever -- in particular for the linear characters the roadmap induces.
For a consumer holding the subgroup in the roadmap's generated form ⟨(1 2)⟩,
TauCeti.stabilizer_perm_fin_three_eq_zpowers converts it to the stabilizer form used here.
The decomposition of the induced sign character #
The sign character of a point stabilizer of S₃ is nontrivial, over any field in which
2 ≠ 0. So the representation induced below is not the permutation representation of the trivial
character under another name.
The character of Ind_{C₂}^{S₃}(sign) is sgn + χ_standard, at every σ and over any
field: inducing the sign character of a point stabilizer of S₃ gives a three-dimensional
representation whose character is the sum of the sign character of S₃ and the character of the
two-dimensional standard representation. No hypothesis on the characteristic is needed; in
characteristic two, where the sign character is trivial, this degenerates to the permutation
character of the three points.
Ind_{C₂}^{S₃}(sign) ≅ sgn ⊕ standard, over a field of characteristic zero: the sign
character of a point stabilizer of S₃ induces to the direct sum of
the sign character of S₃ and the two-dimensional standard representation. The two summands are a
line and an irreducible plane, so this names the constituents whose existence
TauCeti.not_simple_indFDRep_stabilizer_perm_fin_three asserts. The hypotheses on k are those
under which characters determine representations; the underlying identity of characters,
TauCeti.character_indFDRep_sign_stabilizer_perm_fin_three, needs neither.
The alternating subgroup #
A faithful linear character of A₃ induces irreducibly to S₃. A₃ is normal, so the
Mackey criterion for an induced linear character asks only that nothing outside A₃ centralize
A₃, which is TauCeti.centralizer_alternatingGroup_fin_three_le.
What a linear character of A₃ induces to is two-dimensional, A₃ having index two in
S₃. Together with TauCeti.simple_indFDRep_ofLinearCharacter_alternatingGroup_fin_three this is
the roadmap's two-dimensional irreducible of S₃.
A₃ has a faithful linear character valued in any commutative monoid with enough roots of
unity for the exponent of A₃: it is cyclic of order three, so a primitive cube root of unity
suffices, and an algebraically closed field of characteristic zero supplies one. A character of a
group of prime order is faithful as soon as it is nontrivial, its kernel being a proper
subgroup.