Library Combi.SymGroup.permcent: The Centralizer of a Permutation

The Centralizer of a Permutation

The main goal is to understand the structure of the centralizer group of a given permutation s, compute its cardinality and deduce the cardinality of the conjugacy class of s.

Here are the notion defined is this file, where s is a fixed permutation on a finite type T:

'CC(s) == the group of permutations of T which commute with s and stabilize each cycle of s.
stab_iporbits s == the group of permutations of T which only move the cycles of s and sends any cycle to a cycle of the same length.
inporbits s t == the permutation induced by t on the set of the cycles of s. inporbits s is a morphism from {perm T} to stab_iporbits s.
permcycles s P == a right inverse morphism from stab_iporbits s to {perm T}. If P belongs to stab_iporbits s then permcycles s P si a compatible lifting of P in {perm T}, otherwise the identity.
zcard l == where is the number of occurrence of in l.

Here are the main results:

'CC(s)' is the direct product of the group generated by the cycles of s. Lemma porbitgrpE:

'CC(s) = \big[dprod/1]_(c in cycle_dec s) <[c]>.
stab_iporbits s is the direct product over i of the group permuting the set of the cycles of size i. Theorem stab_iporbitsE:

stab_iporbits s = \big[dprod/1]_(i < #|T|.+1) Sym (porbits s :&: 'SC_i).
The centralizer 'C[s] is the semidirect product of 'CC(s)' and the lifting of stab_iporbits s. Theorem cent1_permE:

'C[s] = 'CC(s) ><| (permcycles s) @* (stab_iporbits s).
The cardinality of the centralizer of s given by zcard. Corollary card_cent1_perm:

#|'C[s]| = zcard (cycle_type s).
The cardinality of the conjugacy class associated to the partition l of an integer n is given by Theorem card_class_of_part:

#|classCT l| = n`! %/ zcard l.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype.
From mathcomp Require Import tuple path bigop finset div.
From mathcomp Require Import fingroup perm action gproduct morphism.

Require Import tools partition permcomp cycles cycletype.

Import GroupScope.

Set Implicit Arguments.

#[local] Hint Resolve porbit_id : core.

#[local] Notation "''SC_' i " := (finset (fun x => #{x } == i))
(at level 0).

Support and cycle in the centralizer

Section PermCycles.

Variable T : finType.
Implicit Type (s t c : {perm T}).

Lemma disjoint_psupport_dprodE (S : {set {perm T}}) :
  disjoint_psupports S ->
  (\big[dprod/1]_(s in S) <[s]>) = (\prod_(s in S) <[s]>)%G.

Lemma cent1_act_porbit s t x :
  t \in 'C[s] -> ('P)^* (porbit s x) t = porbit s (t x).

Lemma cent1_act_on_porbits s : [acts 'C[s], on porbits s | ('P)^*].

Lemma cent1_act_on_iporbits s i :
  [acts 'C[s], on porbits s :&: 'SC_i | ('P)^*].

Lemma commute_cyclic c t :
  c \is cyclic -> t \in 'C[c] -> perm_on (psupport c) t -> exists i , t = c ^+ i.

The cyclic centralizer

Notation "''CC' ( s )" :=
  'C_('C[s])(porbits s | ('P)^* ) (format "''CC' ( s )") : group_scope.

Lemma restr_perm_genC C s t :
  C \in porbit_set s -> t \in 'CC (s ) -> restr_perm C t \in <[restr_perm C s]>%G.

Lemma stab_porbit S s :
  s \in 'N(S | 'P) -> forall x, (x \in S ) = (porbit s x \subset S ).

Lemma restr_perm_porbits S s :
  restr_perm S s \in 'C(porbits s | ('P)^* ).

Lemma porbitgrpE s : 'CC (s ) = \big[dprod/1]_(c in cycle_dec s) <[c]>.

Lemma card_porbitgrpE s : #|'CC (s )| = (\prod_(i <- cycle_type s) i)%N.

Permuting the cycles among themselves

Definition stab_iporbits s : {set {perm {set T}}} :=
  Sym (porbits s) :&:
    \bigcap_(i : 'I_#|T|.+1) 'N(porbits s :&: 'SC_i | 'P).

Definition inporbits s : {perm T} -> {perm {set T}} :=
  restr_perm (porbits s) \o actperm 'P^*.

Section CM.

Variable s : {perm T}.
Implicit Type P : {perm {set T}}.

Lemma stab_iporbits_stab P :
  (if P \in stab_iporbits s then P else 1) @: porbits s \subset porbits s.

Lemma stab_iporbits_homog P :
  {in porbits s , forall C : {set T},
       #|(if P \in stab_iporbits s then P else 1) C| = #|C| }.

#[local] Definition stab_iporbits_porbitmap P :=
  PorbitMap (stab_iporbits_stab P) (stab_iporbits_homog P).
#[local] Definition stab_iporbits_map P := cymap (stab_iporbits_porbitmap P).

Lemma stab_iporbits_map_inj P : injective (stab_iporbits_map P).
Definition permcycles P := perm (@stab_iporbits_map_inj P).

Lemma permcyclesC P : commute (permcycles P) s.

Lemma permcyclesP P : (permcycles P ) \in 'C[s].

Lemma porbit_permcycles P x :
  P \in stab_iporbits s -> porbit s (permcycles P x) = P (porbit s x).

End CM.

Lemma permcyclesM s :
  {in stab_iporbits s &, {morph permcycles s : P Q / P * Q }}.
Canonical permcycles_morphism s := Morphism (permcyclesM (s := s)).

Lemma permcyclesK s :
  {in stab_iporbits s , cancel (permcycles s) (inporbits s)}.

Lemma permcycles_inj s : 'injm (permcycles s).

Lemma inporbits_im s : inporbits s @: 'C[s] = stab_iporbits s.

Lemma trivIset_iporbits s : trivIset [set porbits s :&: 'SC_i | i : 'I_#|T|.+1].

Lemma cover_iporbits s :
  cover [set porbits s :&: 'SC_i | i : 'I_#|T|.+1] = porbits s.

Lemma stab_iporbitsE_prod s :
  stab_iporbits s =
  (\prod_(i < #|T|.+1) Sym_group (porbits s :&: 'SC_i))%G.

Theorem stab_iporbitsE s :
  stab_iporbits s = \big[dprod/1]_(i < #|T|.+1) Sym (porbits s :&: 'SC_i).

Lemma card_stab_iporbits s :
  #|stab_iporbits s| =
    (\prod_(i < #|T|.+1) (count_mem (nat_of_ord i) (cycle_type s))`!)%N.

Lemma conj_porbitgrp s y z :
  y \in 'C[s] -> z \in 'CC (s ) -> z ^ y \in 'CC (s ).

Lemma inporbits1 s t : t \in 'C(porbits s | ('P)^* ) -> inporbits s t = 1.

Lemma cent1_stab_iporbit_porbitgrpS s :
  'C[s] \subset permcycles s @* stab_iporbits s * 'CC (s ).

Main theorem

Theorem cent1_permE s :
'C[s] = 'CC (s ) ><| (permcycles s) @* (stab_iporbits s).

#[local] Open Scope nat_scope.

Conjucacy class cardinality

Definition zcard l :=
  \prod_(i <- l) i * \prod_(i < (sumn l).+1) (count_mem (i : nat) l)`!.

Lemma zcard_nil : zcard [::] = 1.

Lemma zcard_any l b :
  (sumn l < b ) ->
  \prod_(i <- l) i * \prod_(i < b) (count_mem (i : nat) l)`! = zcard l.

Lemma zcard_rem i l :
  i != 0 -> i \in l -> i * (count_mem i l) * (zcard (rem i l)) = zcard l.

Corollary card_cent1_perm s : #|'C[s]| = zcard (cycle_type s).

Theorem card_class_perm s :
  #|class s [set: {perm T}]| = #|T|`! %/ zcard (cycle_type s).

End PermCycles.

Lemma dvdn_zcard_fact n (l : 'P_n) : zcard l %| n`!.

Lemma neq0zcard n (l : 'P_n) : zcard l != 0.

Theorem card_class_of_part n (l : 'P_n) : #|classCT l| = n`! %/ zcard l.