Clifford theory along A₄ ◁ S₄: the inertia group of a linear character #
The alternating group is normal in the symmetric group, so Clifford theory applies to the pair
alternatingGroup α ◁ Equiv.Perm α, and the first thing it asks for is the inertia group of a
representation of the normal subgroup. This file computes it for a linear character: for a
nontrivial χ : alternatingGroup α →* kˣ,
inertia (FDRep.ofLinearCharacter χ) = alternatingGroup α,
the smallest value Clifford theory allows, TauCeti.le_inertia giving the other inclusion for
free. The computation is the group theory of TauCeti.GroupTheory.Perm.AlternatingCharacter: an
odd permutation inverts every linear character of the alternating group, so it moves a nontrivial
one, and χ and χ⁻¹ are two distinct characters making up one conjugation orbit.
A minimal inertia group is exactly what the Mackey irreducibility criterion for an induced linear
character wants, so Ind of a nontrivial χ is irreducible; and induction from a subgroup of
index two doubles the dimension, so what it produces is a two-dimensional irreducible
representation of Equiv.Perm α.
That dimension count needs nothing new: TauCeti.finrank_indFDRep_ofLinearCharacter and
alternatingGroup.index_eq_two give it in one step wherever it is wanted.
For Nat.card α = 4 this is the A₄ ◁ S₄ case, and it is not vacuous:
TauCeti.exists_monoidHom_alternatingGroup_ne_one produces a nontrivial linear character of A₄
from the identification of its commutator subgroup with the Klein four subgroup. The example
closing the file records that case: over an algebraically closed field of characteristic zero, S₄
has a two-dimensional irreducible representation induced from A₄.
That the nontrivial linear characters of A₄ are exactly χ and χ⁻¹, and so form a single
S₄-orbit rather than merely a pair inside one, is the character count
TauCeti.card_monoidHom_alternatingGroup and its consequence
TauCeti.exists_comp_conjNormal_alternatingGroup_eq, proved with the rest of the group theory in
TauCeti.GroupTheory.Perm.AlternatingCharacter. One further fact about the pair A₄ ◁ S₄ lies
outside the scope of this file: that the three-dimensional irreducible of A₄ is S₄-fixed, the
case of the Clifford correspondence complementary to the one treated here.
Main statements #
TauCeti.inertia_ofLinearCharacter_alternatingGroup: the inertia group of a nontrivial linear character of the alternating group is the alternating group.TauCeti.simple_indFDRep_ofLinearCharacter_alternatingGroup: a nontrivial linear character of the alternating group induces irreducibly to the symmetric group.
References #
- J.-P. Serre, Linear Representations of Finite Groups, Chapter 8.
The inertia group of a nontrivial linear character of the alternating group is the alternating group itself, the smallest value Clifford theory allows. This is the hypothesis the Mackey irreducibility criterion for an induced linear character asks for.
A nontrivial linear character of the alternating group induces irreducibly to the symmetric
group. What it induces to is two-dimensional, by TauCeti.finrank_indFDRep_ofLinearCharacter and
alternatingGroup.index_eq_two, so this exhibits a two-dimensional irreducible representation of
the symmetric group.