An odd permutation inverts every linear character of the alternating group #
Let α be a finite type and let χ be a homomorphism from alternatingGroup α to a commutative
monoid. Conjugation by an even permutation cannot move χ, the target being commutative. This
file proves that conjugation by an odd permutation inverts it, once the target has inverses:
χ (s x s⁻¹) = (χ x)⁻¹ for every s ∉ alternatingGroup α and every x.
The consequence the file exists for is that a nontrivial linear character χ satisfies
χ ∘ conj s ≠ χ for every odd s: otherwise χ would be fixed by conjugation by s and the same
lemma would make it trivial. So the odd permutations move χ, and {χ, χ⁻¹} is a single orbit of
two characters under the conjugation action of Equiv.Perm α. That is exactly the hypothesis of the
Mackey irreducibility criterion for an induced linear character, applied to A₄ ◁ S₄ in
TauCeti.RepresentationTheory.Induction.Clifford.Alternating.Basic.
For that application to be about something, alternatingGroup α must have a nontrivial linear
character, and for Nat.card α = 4 this file lists the characters exactly. Mathlib's
alternatingGroup.kleinFour_eq_commutator identifies the commutator subgroup of A₄ with the
Klein four subgroup, of order 4 inside a group of order 12, so the abelianization A₄ / V₄ has
order 3. Two consequences are drawn, and they need different hypotheses.
Unconditionally on the coefficients, every linear character of A₄ is cube-root-of-unity valued:
it factors through A₄ / V₄, in which every element cubes to 1. Under the hypothesis that the
coefficients have enough roots of unity for that quotient, the character group of a finite group is
the dual of its abelianization (TauCeti.card_monoidHom_eq_card_abelianization), so A₄ has
exactly three linear characters. Three is prime, so any nontrivial one generates: the characters
are 1, χ and χ⁻¹. Combined with the inversion lemma above this closes the orbit picture at
A₄ ◁ S₄ -- the two nontrivial characters are χ and χ⁻¹, and an odd permutation carries one to
the other, so they form a single orbit of the conjugation action of Equiv.Perm α, not merely a
pair of distinct characters inside one.
The roots-of-unity hypothesis on the last three statements is not merely a device to rule out too
few characters: the character group can also be too large. Over M = ℂ × ℂ the characters of
A₄ are the pairs of cube roots of unity, nine of them, and a nontrivial one such as (ω, 1) has
neither (1, ω) nor its inverse among its powers, so the classification genuinely fails there.
HasEnoughRootsOfUnity M (Monoid.exponent (Abelianization (alternatingGroup α))) rules that out by
asking for a primitive cube root of unity in M and for the cube roots of unity in M to form a
cyclic group. It is a sufficient condition, not one shown here to be necessary.
For 4 < Nat.card α the alternating group is perfect instead, and the statements above are then all
vacuously about the trivial character.
Main statements #
MonoidHom.eq_one_of_map_conjNormal_eq_alternatingGroup: a linear character of the alternating group fixed by conjugation by an odd permutation is trivial.MonoidHom.alternatingGroup_le_ker: every homomorphism fromEquiv.Perm αto a commutative monoid kills the alternating group.MonoidHom.map_conjNormal_alternatingGroup_eq_inv: an odd permutation inverts every linear character of the alternating group, withMonoidHom.comp_conjNormal_alternatingGroup_eq_invits form as an equality of homomorphisms.MonoidHom.exists_map_conjNormal_alternatingGroup_ne: an odd permutation moves every nontrivial linear character -- the hypothesis of the Mackey irreducibility criterion.MonoidHom.comp_conjNormal_alternatingGroup_ne: the same as an inequality of homomorphisms, so that a nontrivial linear character and its conjugate by an odd permutation are two distinct members of one orbit.TauCeti.card_abelianization_alternatingGroup: the abelianization ofA₄has order three.TauCeti.monoidHom_alternatingGroup_apply_pow_threeandTauCeti.monoidHom_alternatingGroup_pow_three: the linear characters ofA₄are cube-root-of-unity valued, over arbitrary commutative coefficients.TauCeti.card_monoidHom_alternatingGroup:A₄has exactly three linear characters, withTauCeti.exists_monoidHom_alternatingGroup_ne_onethe corollary that one of them is nontrivial.TauCeti.monoidHom_alternatingGroup_eq_one_or_eq_or_eq_inv: the linear characters ofA₄are1,χandχ⁻¹for any nontrivialχ.TauCeti.exists_comp_conjNormal_alternatingGroup_eq: the two nontrivial linear characters ofA₄form a single orbit of the conjugation action ofEquiv.Perm α.
Implementation notes #
The inversion lemma is proved uniformly in α. The product of χ with its conjugate by s is
fixed by conjugation by s, because s * s is even; and a character fixed by conjugation by one
odd permutation is fixed by conjugation by every permutation, since the odd permutations form a
single coset of the even ones. Such a character kills every three-cycle c, because c is
conjugate in Equiv.Perm α to its own inverse, so the value at c squares to 1 while also
cubing to 1. Three-cycles generate the alternating group, so the character is trivial, which is
the claim.
References #
- J.-P. Serre, Linear Representations of Finite Groups, Chapter 5.
A linear character of the alternating group fixed by conjugation by an odd permutation is
trivial. Equivalently, the conjugation action of Equiv.Perm α on the linear characters of
alternatingGroup α has only the trivial character as a fixed point.
Every homomorphism from a permutation group to a commutative monoid kills the alternating group.
An odd permutation inverts every linear character of the alternating group.
An odd permutation inverts every linear character of the alternating group, as an equality of homomorphisms.
An odd permutation moves every nontrivial linear character of the alternating group. This
is the hypothesis of the Mackey irreducibility criterion for an induced linear character, checked
at A₄ ◁ S₄.
A nontrivial linear character of the alternating group and its conjugate by an odd
permutation are distinct, so the two of them make up a single orbit of the conjugation action of
Equiv.Perm α on the characters.
The abelianization of A₄ has order three.
The linear characters of A₄ are cube-root-of-unity valued, over arbitrary commutative
coefficients.
A linear character of A₄ is a cube root of unity in the character group, the form of
TauCeti.monoidHom_alternatingGroup_apply_pow_three as an equation between homomorphisms.
The linear characters of A₄ form a group of order three, when M has enough roots of
unity for the exponent of the abelianization A₄ / V₄.
A₄ has a nontrivial linear character valued in any commutative monoid with enough roots
of unity for the exponent of the abelianization A₄ / V₄, such as an algebraically closed field of
characteristic zero.
A₄ has exactly three linear characters, and once a nontrivial one χ is fixed they are
1, χ and χ⁻¹. Some hypothesis on M is needed on both counts: without roots of unity there
are too few characters, while over M = ℂ × ℂ there are nine of them and the conclusion fails.
The two nontrivial linear characters of A₄ make up a single S₄-orbit: the conjugation
action of Equiv.Perm α is transitive on them.