Documentation

Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Centralizer of an element in the alternating group #

Given a finite type α, our goal is to compute the cardinality of conjugacy classes in alternatingGroup α.

TODO : Deduce the formula for the cardinality of the centralizers and conjugacy classes in alternatingGroup α.

theorem AlternatingGroup.card_of_cycleType_mul_eq (α : Type u_1) [Fintype α] [DecidableEq α] (m : Multiset ) :
{g : (alternatingGroup α) | (↑g).cycleType = m}.card * ((Fintype.card α - m.sum).factorial * m.prod * nm.toFinset, (Multiset.count n m).factorial) = if (m.sum Fintype.card α am, 2 a) Even (m.sum + m.card) then (Fintype.card α).factorial else 0

The cardinality of even permutations of given cycleType

theorem AlternatingGroup.card_of_cycleType (α : Type u_1) [Fintype α] [DecidableEq α] (m : Multiset ) :
{g : (alternatingGroup α) | (↑g).cycleType = m}.card = if (m.sum Fintype.card α am, 2 a) Even (m.sum + m.card) then (Fintype.card α).factorial / ((Fintype.card α - m.sum).factorial * (m.prod * nm.toFinset, (Multiset.count n m).factorial)) else 0

The cardinality of even permutations of given cycleType

theorem AlternatingGroup.card_of_cycleType_singleton {α : Type u_1} [Fintype α] [DecidableEq α] {n : } (hn : 2 n) ( : n Fintype.card α) :
{g : (alternatingGroup α) | (↑g).cycleType = {n}}.card = if Odd n then (n - 1).factorial * (Fintype.card α).choose n else 0

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