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.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 α) (Finset.filter (fun (g : ↥(alternatingGroup α)) => (↑g).cycleType = m) Finset.univ) = if Even (m.sum + m.card) then Finset.filter (fun (g : Equiv.Perm α) => g.cycleType = m) Finset.univ else ∅

theorem AlternatingGroup.card_of_cycleType_mul_eq (α : Type u_1) [Fintype α] [DecidableEq α] (m : Multiset ℕ) : (Finset.filter (fun (g : ↥(alternatingGroup α)) => (↑g).cycleType = m) Finset.univ).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 ℕ) : (Finset.filter (fun (g : ↥(alternatingGroup α)) => (↑g).cycleType = m) Finset.univ).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 α) : (Finset.filter (fun (g : ↥(alternatingGroup α)) => (↑g).cycleType = {n}) Finset.univ).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.