Centralizer of an element in the alternating group #
Given a finite type α
, our goal is to compute the cardinality of conjugacy classes
in alternatingGroup α
.
AlternatingGroup.card_of_cycleType_mul_eq m
andAlternatingGroup.card_of_cycleType m
compute the number of even permutations of given cycle type.Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup
: ifSubgroup.centralizer {g} ≤ alternatingGroup α
, then all members of theg.cycleType
are odd.Equiv.Perm.card_le_of_centralizer_le_alternating
: ifSubgroup.centralizer {g} ≤ alternatingGroup α
, then the cardinality of α is at mostg.cycleType.sum
plus one.Equiv.Perm.count_le_one_of_centralizer_le_alternating
: ifSubgroup.centralizer {g} ≤ alternatingGroup α
, theng.cycleType
has no repetitions.Equiv.Perm.centralizer_le_alternating_iff
: the previous three conditions are necessary and sufficient for havingSubgroup.centralizer {g} ≤ alternatingGroup α
.
TODO :
Deduce the formula for the cardinality of the centralizers
and conjugacy classes in alternatingGroup α
.
The cardinality of even permutations of given cycleType
The cardinality of even permutations of given cycleType
The number of cycles of given length
The centralizer of a permutation is contained in the alternating group if and only if its cycles have odd length, with at most one of each, and there is at most one fixed point.
If n ≥ 5
, then the alternating group on n
letters is perfect
If n ≥ 5
, then the alternating group on n
letters is perfect (subgroup version)
The commutator subgroup of the permutation group is the alternating group