Centralizer of a permutation and cardinality of conjugacy classes in the symmetric groups

Let α : Type with Fintype α (and DecidableEq α). The main goal of this file is to compute the cardinality of conjugacy classes in Equiv.Perm α. Every g : Equiv.Perm α has a g.cycleType : Multiset ℕ. By Equiv.Perm.isConj_iff_cycleType_eq, two permutations are conjugate in Equiv.Perm α iff their cycle types are equal. To compute the cardinality of the conjugacy classes, we could use a purely combinatorial approach and compute the number of permutations with given cycle type but we resorted to a more algebraic approach based on the study of the centralizer of a permutation g.

Given g : Equiv.Perm α, the conjugacy class of g is the orbit of g under the action ConjAct (Equiv.Perm α), and we use the orbit-stabilizer theorem (MulAction.card_orbit_mul_card_stabilizer_eq_card_group) to reduce the computation to the computation of the centralizer of g, the subgroup of Equiv.Perm α consisting of all permutations which commute with g. It is accessed here as MulAction.stabilizer (ConjAct (Equiv.Perm α)) g and Subgroup.centralizer_eq_comap_stabilizer.

We compute this subgroup as follows.

• If h : Subgroup.centralizer {g}, then the action of ConjAct.toConjAct h by conjugation on Equiv.Perm α stabilizes g.cycleFactorsFinset. That induces an action of Subgroup.centralizer {g} on g.cycleFactorsFinset which is defined as an instance.

• This action defines a group morphism Equiv.Perm.OnCycleFactors.toPermHom g from Subgroup.centralizer {g} to Equiv.Perm g.cycleFactorsFinset.

• Equiv.Perm.OnCycleFactors.range_toPermHom' is the subgroup of Equiv.Perm g.cycleFactorsFinset consisting of permutations that preserve the cardinality of the support.

• Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom' shows that the range of Equiv.Perm.OnCycleFactors.toPermHom g is the subgroup Equiv.Perm.OnCycleFactors.toPermHom_range' g of Equiv.Perm g.cycleFactorsFinset.

This is shown by constructing a right inverse Equiv.Perm.Basis.toCentralizer, as established by Equiv.Perm.Basis.toPermHom_apply_toCentralizer.

• Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom computes the cardinality of (Equiv.Perm.OnCycleFactors.toPermHom g).range as a product of factorials.

• Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff proves that k : Subgroup.centralizer {g} belongs to the kernel of Equiv.Perm.OnCycleFactors.toPermHom g if and only if it commutes with each cycle of g. This is equivalent to the conjunction of two properties:

  • k preserves the set of fixed points of g;
  • on each cycle c, k acts as a power of that cycle.

This allows to give a description of the kernel of Equiv.Perm.OnCycleFactors.toPermHom g as the product of a symmetric group and of a product of cyclic groups. This analysis starts with the morphism Equiv.Perm.OnCycleFactors.kerParam, its injectivity Equiv.Perm.OnCycleFactors.kerParam_injective, its range Equiv.Perm.OnCycleFactors.kerParam_range_eq, and its cardinality Equiv.Perm.OnCycleFactors.kerParam_range_card.

• Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply computes the signature of the permutation induced given by Equiv.Perm.OnCycleFactors.kerParam.

• Equiv.Perm.nat_card_centralizer g computes the cardinality of the centralizer of g.

• Equiv.Perm.card_isConj_mul_eq gcomputes the cardinality of the conjugacy class of g.

• We now can compute the cardinality of the set of permutations with given cycle type. The condition for this cardinality to be zero is given by Equiv.Perm.card_of_cycleType_eq_zero_iff which is itself derived from Equiv.Perm.exists_with_cycleType_iff.

• Equiv.Perm.card_of_cycleType_mul_eq m and Equiv.Perm.card_of_cycleType m compute this cardinality.

theorem Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset {α : Type u_1} [DecidableEq α] [Fintype α] {g k c : Perm α} (k_mem : k ∈ Subgroup.centralizer {g}) (c_mem : c ∈ g.cycleFactorsFinset) : ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset

def Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.cycleFactorsFinset_mulAction {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : MulAction ↥(Subgroup.centralizer {g}) { x : Perm α // x ∈ g.cycleFactorsFinset }

The action by conjugation of Subgroup.centralizer {g} on the cycles of a given permutation

def Equiv.Perm.OnCycleFactors.instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : MulAction ↥(Subgroup.centralizer {g}) { x : Perm α // x ∈ g.cycleFactorsFinset }

The conjugation action of Subgroup.centralizer {g} on g.cycleFactorsFinset

def Equiv.Perm.OnCycleFactors.toPermHom {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : ↥(Subgroup.centralizer {g}) →* Perm { x : Perm α // x ∈ g.cycleFactorsFinset }

The canonical morphism from Subgroup.centralizer {g} to the group of permutations of g.cycleFactorsFinset

theorem Equiv.Perm.OnCycleFactors.centralizer_smul_def {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : ↥(Subgroup.centralizer {g})) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : k • c = ⟨↑k * ↑c * ↑k⁻¹, ⋯⟩

@[simp]

theorem Equiv.Perm.OnCycleFactors.val_centralizer_smul {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : ↥(Subgroup.centralizer {g})) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : ↑(k • c) = ↑k * ↑c * ↑k⁻¹

theorem Equiv.Perm.OnCycleFactors.toPermHom_apply {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : ↥(Subgroup.centralizer {g})) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : ((toPermHom g) k) c = k • c

theorem Equiv.Perm.OnCycleFactors.coe_toPermHom {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : ↥(Subgroup.centralizer {g})) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : ↑(((toPermHom g) k) c) = ↑k * ↑c * (↑k)⁻¹

def Equiv.Perm.OnCycleFactors.range_toPermHom' {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Subgroup (Perm { x : Perm α // x ∈ g.cycleFactorsFinset })

The range of Equiv.Perm.OnCycleFactors.toPermHom.

The equality is proved by Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom'.

theorem Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} {τ : Perm { x : Perm α // x ∈ g.cycleFactorsFinset }} : τ ∈ range_toPermHom' g ↔ ∀ (c : { x : Perm α // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card

theorem Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : ↥(Subgroup.centralizer {g})) : k ∈ (toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

k : Subgroup.centralizer {g} belongs to the kernel of toPermHom g iff it commutes with each cycle of g

structure Equiv.Perm.Basis {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Type u_1

A Basis of a permutation is a choice of an element in each of its cycles

• toFun : { x : Perm α // x ∈ g.cycleFactorsFinset } → α

  A choice of elements in each cycle

• mem_support_self' (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : self.toFun c ∈ (↑c).support

  For each cycle, the chosen element belongs to the cycle

instance Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : FunLike g.Basis { x : Perm α // x ∈ g.cycleFactorsFinset } α

theorem Equiv.Perm.Basis.nonempty {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Nonempty g.Basis

theorem Equiv.Perm.Basis.mem_support_self {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : a c ∈ (↑c).support

theorem Equiv.Perm.Basis.injective {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) : Function.Injective ⇑a

theorem Equiv.Perm.Basis.cycleOf_eq {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) : g.cycleOf (a c) = ↑c

theorem Equiv.Perm.Basis.sameCycle {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) {x : α} (hx : g.cycleOf x ∈ g.cycleFactorsFinset) : g.SameCycle (a ⟨g.cycleOf x, hx⟩) x

def Equiv.Perm.Basis.ofPermHomFun {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) (x : α) : α

The function that will provide a right inverse toCentralizer to toPermHom

theorem Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (x : α) : x ∈ Function.fixedPoints ⇑g ∨ ∃ (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) (_ : x ∈ (↑c).support) (m : ℤ), (g ^ m) (a c) = x

theorem Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) {x : α} {c : { x : Perm α // x ∈ g.cycleFactorsFinset }} (hx : x ∈ (↑c).support) {m : ℤ} (hm : (g ^ m) (a c) = x) : a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

theorem Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) {x : α} (hx : x ∈ Function.fixedPoints ⇑g) : a.ofPermHomFun τ x = x

theorem Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) {x : α} {c : { x : Perm α // x ∈ g.cycleFactorsFinset }} : a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

theorem Equiv.Perm.Basis.ofPermHomFun_commute_zpow_apply {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) (x : α) (j : ℤ) : a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

theorem Equiv.Perm.Basis.ofPermHomFun_mul {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (σ τ : ↥(OnCycleFactors.range_toPermHom' g)) (x : α) : a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)

theorem Equiv.Perm.Basis.ofPermHomFun_one {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (x : α) : a.ofPermHomFun 1 x = x

noncomputable def Equiv.Perm.Basis.ofPermHom {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) : ↥(OnCycleFactors.range_toPermHom' g) →* Perm α

Given a : g.Basis and a permutation of g.cycleFactorsFinset that preserve the lengths of the cycles, a permutation of α that moves the Basis and commutes with g

theorem Equiv.Perm.Basis.ofPermHom_apply {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) (x : α) : (a.ofPermHom τ) x = a.ofPermHomFun τ x

theorem Equiv.Perm.Basis.ofPermHom_support {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) : (a.ofPermHom τ).support = (↑τ).support.biUnion fun (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) => (↑c).support

theorem Equiv.Perm.Basis.card_ofPermHom_support {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) : (a.ofPermHom τ).support.card = ∑ c ∈ (↑τ).support, (↑c).support.card

theorem Equiv.Perm.Basis.ofPermHom_mem_centralizer {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) : a.ofPermHom τ ∈ Subgroup.centralizer {g}

noncomputable def Equiv.Perm.Basis.toCentralizer {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) : ↥(OnCycleFactors.range_toPermHom' g) →* ↥(Subgroup.centralizer {g})

Given a : Equiv.Perm.Basis g, we define a right inverse of Equiv.Perm.OnCycleFactors.toPermHom, on range_toPermHom' g

theorem Equiv.Perm.Basis.toCentralizer_apply {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) (x : α) : ↑(a.toCentralizer τ) x = a.ofPermHomFun τ x

theorem Equiv.Perm.Basis.toCentralizer_equivariant {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) (τ : ↥(OnCycleFactors.range_toPermHom' g)) : a.toCentralizer τ • c = ↑τ c

theorem Equiv.Perm.Basis.toPermHom_apply_toCentralizer {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} (a : g.Basis) (τ : ↥(OnCycleFactors.range_toPermHom' g)) : (OnCycleFactors.toPermHom g) (a.toCentralizer τ) = ↑τ

theorem Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} {τ : Perm { x : Perm α // x ∈ g.cycleFactorsFinset }} : τ ∈ (toPermHom g).range ↔ ∀ (c : { x : Perm α // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card

theorem Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff' {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} {τ : Perm { x : Perm α // x ∈ g.cycleFactorsFinset }} : τ ∈ (toPermHom g).range ↔ (fun (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) => (↑c).support.card) ∘ ⇑τ = fun (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) => (↑c).support.card

Unapplied variant of Equiv.Perm.mem_range_toPermHom_iff

theorem Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom' {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} : (toPermHom g).range = range_toPermHom' g

Computes the range of Equiv.Perm.toPermHom g

theorem Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} : Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial

def Equiv.Perm.OnCycleFactors.kerParam {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Perm ↑(Function.fixedPoints ⇑g) × ((c : { x : Perm α // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)) →* Perm α

The parametrization of the kernel of toPermHom

theorem Equiv.Perm.OnCycleFactors.kerParam_apply {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} {u : Perm ↑(Function.fixedPoints ⇑g)} {v : (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)} {x : α} : ((kerParam g) (u, v)) x = if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x

theorem Equiv.Perm.OnCycleFactors.kerParam_injective {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Function.Injective ⇑(kerParam g)

theorem Equiv.Perm.OnCycleFactors.kerParam_range_eq {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} : (kerParam g).range = Subgroup.map (Subgroup.centralizer {g}).subtype (toPermHom g).ker

theorem Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer {α : Type u_1} [DecidableEq α] [Fintype α] {g : Perm α} : (kerParam g).range ≤ Subgroup.centralizer {g}

theorem Equiv.Perm.OnCycleFactors.kerParam_range_card {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Fintype.card ↥(kerParam g).range = (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod

theorem Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : Perm ↑(Function.fixedPoints ⇑g)) (v : (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)) : sign ((kerParam g) (k, v)) = sign k * ∏ c : { x : Perm α // x ∈ g.cycleFactorsFinset }, sign ↑(v c)

theorem Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) (k : Perm ↑(Function.fixedPoints ⇑g)) (v : (c : { x : Perm α // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)) : ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x : Perm α // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

theorem Equiv.Perm.nat_card_centralizer {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Nat.card ↥(Subgroup.centralizer {g}) = (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial

Cardinality of the centralizer in Equiv.Perm α of a permutation given cycleType

theorem Equiv.Perm.card_isConj_mul_eq {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Nat.card ↑{h : Perm α | IsConj g h} * ((Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial) = (Fintype.card α).factorial

theorem Equiv.Perm.card_isConj_eq {α : Type u_1} [DecidableEq α] [Fintype α] (g : Perm α) : Nat.card ↑{h : Perm α | IsConj g h} = (Fintype.card α).factorial / ((Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial)

Cardinality of a conjugacy class in Equiv.Perm α of a given cycleType

theorem Equiv.Perm.card_of_cycleType_eq_zero_iff (α : Type u_1) [DecidableEq α] [Fintype α] {m : Multiset ℕ} : {g : Perm α | g.cycleType = m}.card = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

theorem Equiv.Perm.card_of_cycleType_mul_eq (α : Type u_1) [DecidableEq α] [Fintype α] (m : Multiset ℕ) : {g : Perm α | 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 then (Fintype.card α).factorial else 0

theorem Equiv.Perm.card_of_cycleType (α : Type u_1) [DecidableEq α] [Fintype α] (m : Multiset ℕ) : {g : Perm α | g.cycleType = m}.card = if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α).factorial / ((Fintype.card α - m.sum).factorial * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial) else 0

Cardinality of the Finset of Equiv.Perm α of given cycleType

theorem Equiv.Perm.card_of_cycleType_singleton {α : Type u_1} [DecidableEq α] [Fintype α] {n : ℕ} (hn' : 2 ≤ n) (hα : n ≤ Fintype.card α) : {g : Perm α | g.cycleType = {n}}.card = (n - 1).factorial * (Fintype.card α).choose n

The number of cycles of given length