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 and AlternatingGroup.card_of_cycleType m compute the number of even permutations of given cycle type.

• Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup : if Subgroup.centralizer {g} ≤ alternatingGroup α, then all members of the g.cycleType are odd.

• Equiv.Perm.card_le_of_centralizer_le_alternating : if Subgroup.centralizer {g} ≤ alternatingGroup α, then the cardinality of α is at most g.cycleType.sum plus one.

• Equiv.Perm.count_le_one_of_centralizer_le_alternating : if Subgroup.centralizer {g} ≤ alternatingGroup α, then g.cycleType has no repetitions.

• Equiv.Perm.centralizer_le_alternating_iff : the previous three conditions are necessary and sufficient for having Subgroup.centralizer {g} ≤ alternatingGroup α.

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

theorem Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] {g : Perm α} (h : Subgroup.centralizer {g} ≤ alternatingGroup α) (i : ℕ) (hi : i ∈ g.cycleType) : Odd i

theorem AlternatingGroup.map_subtype_of_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (m : Multiset ℕ) : Finset.map (Function.Embedding.subtype fun (x : Equiv.Perm α) => x ∈ alternatingGroup α) {g : ↥(alternatingGroup α) | (↑g).cycleType = m} = if Even (m.sum + m.card) then {g : Equiv.Perm α | g.cycleType = m} else ∅

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 * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial) = if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 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 α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α).factorial / ((Fintype.card α - m.sum).factorial * (m.prod * ∏ n ∈ m.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) (hα : 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

theorem Equiv.Perm.card_le_of_centralizer_le_alternating {α : Type u_1} [Fintype α] [DecidableEq α] {g : Perm α} (h : Subgroup.centralizer {g} ≤ alternatingGroup α) : Fintype.card α ≤ g.cycleType.sum + 1

theorem Equiv.Perm.count_le_one_of_centralizer_le_alternating {α : Type u_1} [Fintype α] [DecidableEq α] {g : Perm α} (h : Subgroup.centralizer {g} ≤ alternatingGroup α) (i : ℕ) : Multiset.count i g.cycleType ≤ 1

theorem Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one {α : Type u_1} [Fintype α] [DecidableEq α] {g : Perm α} (h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) : (kerParam g).range = Subgroup.centralizer {g}

theorem Equiv.Perm.centralizer_le_alternating_iff {α : Type u_1} [Fintype α] [DecidableEq α] {g : Perm α} : Subgroup.centralizer {g} ≤ alternatingGroup α ↔ (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

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.

theorem Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) {g : ↥(alternatingGroup α)} (hg : (↑g).IsThreeCycle) : g ∈ commutatorSet ↥(alternatingGroup α)

theorem Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) {g : ↥(alternatingGroup α)} (hg : (↑g).IsThreeCycle) : g ∈ commutator ↥(alternatingGroup α)

theorem alternatingGroup.commutator_perm_le {α : Type u_1} [Fintype α] [DecidableEq α] : commutator (Equiv.Perm α) ≤ alternatingGroup α

theorem commutator_alternatingGroup_eq_top {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) : commutator ↥(alternatingGroup α) = ⊤

If n ≥ 5, then the alternating group on n letters is perfect

theorem commutator_alternatingGroup_eq_self {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) : ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α

If n ≥ 5, then the alternating group on n letters is perfect (subgroup version)

theorem alternatingGroup.commutator_perm_eq {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) : commutator (Equiv.Perm α) = alternatingGroup α

The commutator subgroup of the permutation group is the alternating group