Library Combi.SymGroup.cycletype: The Cycle Type of a Permutation
Cycle type and conjugacy classes in the symmetric groups
- canporbit s x == a chosen canonical element in the s-cycle of x
- indporbit s x == the position of x in its cycle wrt canporbit s x
- porbits_map s t == if s and t are respectively two permutations of two fintype U and V, then porbits_map s t is a record for maps {set U} -> {set V}, sending cycles of s of a given size to cycles of t of the same size.
- cymap P == if P : porbits_map s t then cymap P is a map U -> V
which commute with s and t:
Lemma cymapP x : cymap (s x) = t (cymap x).moreover, cymap P sends canonical to canonical canporbit_cymap.
- cycle_type s == the cycle typle of s as a 'P_#|T|.
- conjbij s t pf == if pf : cycle_type s = cycle_type t, a bijection U -> V which commute with s and t
- perm_of_porbit C == a cyclic permutation with support C
- perm_of_setpart P == a permutation whose cycle supports are the part of the set partition P
- permCT p == a permutation of cycle type p : P_#|T|.
- classCT p == the set of permutations of cycle type p : P_#|T|.
- '1_[p] == the class function associated to p : P_#|T|.
- partnCT p == cast a p : 'P_#|'I_n| to a 'P_n.
- cycle_typeSn s == the cycle type in 'P_n of a permutations in 'S_n.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import tuple finfun finset path bigop.
From mathcomp Require Import fingroup perm action.
From mathcomp Require Import ssralg matrix mxalgebra algC classfun.
Require Import partition tools sorted.
Require Import permcomp fibered_set cycles.
Set Implicit Arguments.
Import LeqGeqOrder.
#[local] Hint Resolve porbit_id : core.
Reserved Notation "''1_[' G ]"
(at level 8, G at level 2, format "''1_[' G ]").
Section CanPorbit.
Variable T : finType.
Variable s : {perm T}.
Definition canporbit x := odflt x [pick y in porbit s x].
Lemma canporbitP x : x \in porbit s (canporbit x).
Lemma canporbitE x y :
(porbit s x == porbit s y) = (canporbit x == canporbit y).
Lemma porbitPb x y :
y \in porbit s x -> exists i, y == (s ^+ i)%g x.
Definition indporbit (x : T) : nat := ex_minn (porbitPb (canporbitP x)).
Lemma indporbitP x : ((s ^+ (indporbit x)) (canporbit x))%g = x.
End CanPorbit.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import tuple finfun finset path bigop.
From mathcomp Require Import fingroup perm action.
From mathcomp Require Import ssralg matrix mxalgebra algC classfun.
Require Import partition tools sorted.
Require Import permcomp fibered_set cycles.
Set Implicit Arguments.
Import LeqGeqOrder.
#[local] Hint Resolve porbit_id : core.
Reserved Notation "''1_[' G ]"
(at level 8, G at level 2, format "''1_[' G ]").
Section CanPorbit.
Variable T : finType.
Variable s : {perm T}.
Definition canporbit x := odflt x [pick y in porbit s x].
Lemma canporbitP x : x \in porbit s (canporbit x).
Lemma canporbitE x y :
(porbit s x == porbit s y) = (canporbit x == canporbit y).
Lemma porbitPb x y :
y \in porbit s x -> exists i, y == (s ^+ i)%g x.
Definition indporbit (x : T) : nat := ex_minn (porbitPb (canporbitP x)).
Lemma indporbitP x : ((s ^+ (indporbit x)) (canporbit x))%g = x.
End CanPorbit.
Section PorbitBijection.
Variables (U V : finType).
Variables (s : {perm U}) (t : {perm V}).
Record porbits_map := PorbitMap {
fs :> {set U} -> {set V};
fs_stab : fs @: porbits s \subset porbits t;
fs_homog : {in porbits s, forall C, #|fs C| = #|C| }
}.
Variable CM : porbits_map.
Fact cymapcan_aux (x : U) : V.
#[local] Definition cymapcan x :=
odflt (cymapcan_aux x) [pick y in CM (porbit s x)].
Definition cymap x := ((t ^+ (indporbit s x)) (cymapcan x))%g.
Lemma fs_porbitP x : CM (porbit s x) \in porbits t.
Lemma porbit_cymapcan x : porbit t (cymapcan x) = CM (porbit s x).
Lemma porbit_cymap x : porbit t (cymap x) = CM (porbit s x).
Lemma cymapcan_perm i x : cymapcan ((s ^+ i)%g x) = cymapcan x.
Lemma cymapP x : cymap (s x) = t (cymap x).
Lemma canporbit_cymap x : canporbit t (cymap x) = cymapcan x.
Lemma indporbit_cymap x : indporbit t (cymap x) = indporbit s x.
End PorbitBijection.
Lemma cymapE (U V : finType) (s : {perm U}) (t : {perm V})
(CM1 CM2 : porbits_map s t) :
{in porbits s, CM1 =1 CM2} -> cymap CM1 =1 cymap CM2.
Lemma cymap_id (U : finType) (s : {perm U}) (CM : porbits_map s s) :
{in porbits s, CM =1 id} -> cymap CM =1 id.
Lemma cymap_comp (U V W: finType)
(u : {perm U}) (v : {perm V}) (w : {perm W})
(CMuv : porbits_map u v) (CMvw : porbits_map v w) (CMuw : porbits_map u w) :
{in porbits u, CMvw \o CMuv =1 CMuw} ->
(cymap CMvw) \o (cymap CMuv) =1 (cymap CMuw).
Lemma cymapK (U V : finType)
(u : {perm U}) (v : {perm V})
(CM : porbits_map u v) (CMi : porbits_map v u) :
{in porbits u, cancel CM CMi} -> cancel (cymap CM) (cymap CMi).
Variables (U V : finType).
Variables (s : {perm U}) (t : {perm V}).
Record porbits_map := PorbitMap {
fs :> {set U} -> {set V};
fs_stab : fs @: porbits s \subset porbits t;
fs_homog : {in porbits s, forall C, #|fs C| = #|C| }
}.
Variable CM : porbits_map.
Fact cymapcan_aux (x : U) : V.
#[local] Definition cymapcan x :=
odflt (cymapcan_aux x) [pick y in CM (porbit s x)].
Definition cymap x := ((t ^+ (indporbit s x)) (cymapcan x))%g.
Lemma fs_porbitP x : CM (porbit s x) \in porbits t.
Lemma porbit_cymapcan x : porbit t (cymapcan x) = CM (porbit s x).
Lemma porbit_cymap x : porbit t (cymap x) = CM (porbit s x).
Lemma cymapcan_perm i x : cymapcan ((s ^+ i)%g x) = cymapcan x.
Lemma cymapP x : cymap (s x) = t (cymap x).
Lemma canporbit_cymap x : canporbit t (cymap x) = cymapcan x.
Lemma indporbit_cymap x : indporbit t (cymap x) = indporbit s x.
End PorbitBijection.
Lemma cymapE (U V : finType) (s : {perm U}) (t : {perm V})
(CM1 CM2 : porbits_map s t) :
{in porbits s, CM1 =1 CM2} -> cymap CM1 =1 cymap CM2.
Lemma cymap_id (U : finType) (s : {perm U}) (CM : porbits_map s s) :
{in porbits s, CM =1 id} -> cymap CM =1 id.
Lemma cymap_comp (U V W: finType)
(u : {perm U}) (v : {perm V}) (w : {perm W})
(CMuv : porbits_map u v) (CMvw : porbits_map v w) (CMuw : porbits_map u w) :
{in porbits u, CMvw \o CMuv =1 CMuw} ->
(cymap CMvw) \o (cymap CMuv) =1 (cymap CMuw).
Lemma cymapK (U V : finType)
(u : {perm U}) (v : {perm V})
(CM : porbits_map u v) (CMi : porbits_map v u) :
{in porbits u, cancel CM CMi} -> cancel (cymap CM) (cymap CMi).
Section CycleTypeConj.
Variable T : finType.
Implicit Types (a b s t : {perm T}) (n : nat).
Fact cycle_type_subproof s : is_part_of_n #|T| (setpart_shape (porbits s)).
Definition cycle_type s := IntPartN (cycle_type_subproof s).
Lemma size_cycle_type s : size (cycle_type s) = #|porbits s|.
Lemma odd_cycle_type s :
odd_perm s = odd (sumn (cycle_type s) - size (cycle_type s)).
Lemma cycle_type1 : cycle_type 1%g = colpartn #|T|.
Lemma cycle_typeV s : cycle_type s^-1 = cycle_type s.
Lemma conjg_cycle s a : (<[s]> :^ a = <[s ^ a]>)%g.
Lemma porbit_conjg s a x :
porbit ((s ^ a)%g) (a x) = [set a y | y in porbit s x].
Lemma porbits_conjg s a :
porbits (s ^ a)%g = [set [set a y | y in (X : {set T})] | X in porbits s].
Lemma cycle_type_conjg s a : cycle_type (s ^ a)%g = cycle_type s.
Lemma card_pred_card_porbits s (P : pred nat) :
#|[set x in porbits s | P #|x| ]| = count P (cycle_type s).
Lemma cycle_type_cyclic s :
(s \is cyclic) = (count (fun x => x != 1) (cycle_type s) == 1).
Lemma cyclic_conjg s a : s \is cyclic -> (s ^ a)%g \is cyclic.
Lemma psupport_conjg s a : psupport (s ^ a) = [set a x | x in psupport s].
Lemma card_psupport_conjg s a : #|psupport s| = #|psupport (s ^ a)%g|.
Lemma disjoint_psupports_conjg (A : {set {perm T}}) a :
disjoint_psupports A -> disjoint_psupports [set (s ^ a)%g | s in A].
Import finmodule.FiniteModule morphism.
Lemma cycle_dec_conjg s a:
[set (c ^ a)%g | c in cycle_dec s] = cycle_dec (s ^ a)%g.
End CycleTypeConj.
#[local] Definition slporbits (T : finType) (s : {perm T}) :=
FiberedSet set0 (porbits s) (fun x => #{x}).
Lemma fiber_slporbitE (T : finType) (s : {perm T}) i :
#|fiber (slporbits s) i| = count_mem i (cycle_type s).
Section DefsFiber.
Variables (U V : finType).
Variables (s : {perm U}) (t : {perm V}).
Hypothesis eqct : cycle_type s = cycle_type t :> seq nat.
Lemma cycle_type_eq :
forall i, #|fiber (slporbits s) i| = #|fiber (slporbits t) i|.
Fact conjg_porbits_stab :
[set fbbij (slporbits t) x | x in (slporbits s)] \subset slporbits t.
Fact conjg_porbits_homog :
{in porbits s, forall C, #|fbbij (U := slporbits s) (slporbits t) C| = #|C| }.
#[local] Definition CMbij := PorbitMap conjg_porbits_stab conjg_porbits_homog.
Definition conjbij := cymap CMbij.
Lemma conjbijP x : conjbij (s x) = t (conjbij x).
End DefsFiber.
Lemma conjbijK
(U V : finType) (s : {perm U}) (t : {perm V})
(eqct : cycle_type s = cycle_type t :> seq nat) :
cancel (conjbij eqct) (conjbij (esym eqct)).
Section CycleType.
Variable T : finType.
Implicit Types (s t : {perm T}) (C : {set T}) (P : {set {set T}}).
Theorem conj_permP s t :
reflect (exists c, t = (s ^ c)%g) (cycle_type s == cycle_type t).
Lemma classes_of_permP s t :
(t \in (s ^: [set: {perm T}])%g) = (cycle_type s == cycle_type t).
Section Permofcycletype.
Implicit Types (l : nat) (ct : 'P_#|T|).
Fact perm_of_porbit_subproof C : injective (next (enum C)).
Definition perm_of_porbit C := perm (@perm_of_porbit_subproof C).
Lemma psupport_perm_of_porbit C :
#|C| > 1 -> psupport (perm_of_porbit C) = C.
Lemma perm_of_porbitE C x :
x \in C -> C = porbit (perm_of_porbit C) (head x (enum C)).
Lemma porbits_of_set C : #|C| > 1 -> C \in porbits (perm_of_porbit C).
Lemma porbit_set_of_set C : #|C| > 1 -> porbit_set (perm_of_porbit C) = [set C].
Lemma isperm_of_porbit C : #|C| > 1 -> perm_of_porbit C \is cyclic.
Definition perm_of_setpart P : {perm T} :=
(\prod_(C in [set perm_of_porbit s | s in [set X in P |#|X|>1]]) C)%g.
Lemma psupports_perm_of_porbit P :
[set psupport (perm_of_porbit s) | s in [set X in P | 1 < #|X| ]] =
[set X in P | 1 < #|X|].
Lemma disj_perm_of_setpart P :
partition P [set: T] ->
disjoint_psupports [set perm_of_porbit s| s in [set X0 in P | 1 < #|X0|]].
Lemma porbits_perm_of_setpart P :
partition P [set: T] -> porbits (perm_of_setpart P) = P.
Lemma perm_of_setpartE P :
partition P [set: T] ->
cycle_type (perm_of_setpart P) = setpart_shape P :> seq nat.
End Permofcycletype.
Section TPerm.
Implicit Types (x y z : T).
Lemma porbit_tpermD x y z :
x != z -> y != z -> porbit (tperm x y) z = [set z].
Lemma porbit_tpermL x y : porbit (tperm x y) x = [set x; y].
Lemma porbit_tpermR x y : porbit (tperm x y) y = [set x; y].
Lemma porbits_tperm x y :
porbits (tperm x y) =
[set x; y] |: [set [set z] | z : T & (x != z) && (y != z)].
Lemma cycle_type_tperm x y :
x != y -> cycle_type (tperm x y) = hookpartn #|T| 1.
Lemma tperm_conj x1 y1 x2 y2 :
x1 != y1 -> x2 != y2 -> exists t, tperm x2 y2 = ((tperm x1 y1) ^ t)%g.
Lemma cycle_type_tpermP (s : {perm T}) :
#|T| > 1 ->
cycle_type s = hookpartn #|T| 1 ->
exists x y, x != y /\ s = tperm x y.
End TPerm.
Section Classes.
Variable ct : 'P_#|T|.
Lemma permCT_exists : {s | cycle_type s == ct}.
Definition permCT := val permCT_exists.
Lemma permCTP : cycle_type permCT = ct.
Definition classCT : {set {perm T}} := class permCT [set: {perm T}].
Lemma classCTP s :
(cycle_type s == ct) = (s \in classCT).
Lemma card_classCT_neq0 : #|classCT| != 0%N.
End Classes.
Lemma permCT_colpartn_card : permCT (colpartn #|T|) = 1%g.
Lemma classCT_inj : injective classCT.
Lemma imset_classCT :
[set classCT p | p in setT] = classes [set: {perm T}].
Lemma card_classes_perm :
#|classes [set: {perm T}]| = #|{: 'P_#|T| }|.
Import GroupScope GRing.Theory.
#[local] Open Scope ring_scope.
Variable T : finType.
Implicit Types (a b s t : {perm T}) (n : nat).
Fact cycle_type_subproof s : is_part_of_n #|T| (setpart_shape (porbits s)).
Definition cycle_type s := IntPartN (cycle_type_subproof s).
Lemma size_cycle_type s : size (cycle_type s) = #|porbits s|.
Lemma odd_cycle_type s :
odd_perm s = odd (sumn (cycle_type s) - size (cycle_type s)).
Lemma cycle_type1 : cycle_type 1%g = colpartn #|T|.
Lemma cycle_typeV s : cycle_type s^-1 = cycle_type s.
Lemma conjg_cycle s a : (<[s]> :^ a = <[s ^ a]>)%g.
Lemma porbit_conjg s a x :
porbit ((s ^ a)%g) (a x) = [set a y | y in porbit s x].
Lemma porbits_conjg s a :
porbits (s ^ a)%g = [set [set a y | y in (X : {set T})] | X in porbits s].
Lemma cycle_type_conjg s a : cycle_type (s ^ a)%g = cycle_type s.
Lemma card_pred_card_porbits s (P : pred nat) :
#|[set x in porbits s | P #|x| ]| = count P (cycle_type s).
Lemma cycle_type_cyclic s :
(s \is cyclic) = (count (fun x => x != 1) (cycle_type s) == 1).
Lemma cyclic_conjg s a : s \is cyclic -> (s ^ a)%g \is cyclic.
Lemma psupport_conjg s a : psupport (s ^ a) = [set a x | x in psupport s].
Lemma card_psupport_conjg s a : #|psupport s| = #|psupport (s ^ a)%g|.
Lemma disjoint_psupports_conjg (A : {set {perm T}}) a :
disjoint_psupports A -> disjoint_psupports [set (s ^ a)%g | s in A].
Import finmodule.FiniteModule morphism.
Lemma cycle_dec_conjg s a:
[set (c ^ a)%g | c in cycle_dec s] = cycle_dec (s ^ a)%g.
End CycleTypeConj.
#[local] Definition slporbits (T : finType) (s : {perm T}) :=
FiberedSet set0 (porbits s) (fun x => #{x}).
Lemma fiber_slporbitE (T : finType) (s : {perm T}) i :
#|fiber (slporbits s) i| = count_mem i (cycle_type s).
Section DefsFiber.
Variables (U V : finType).
Variables (s : {perm U}) (t : {perm V}).
Hypothesis eqct : cycle_type s = cycle_type t :> seq nat.
Lemma cycle_type_eq :
forall i, #|fiber (slporbits s) i| = #|fiber (slporbits t) i|.
Fact conjg_porbits_stab :
[set fbbij (slporbits t) x | x in (slporbits s)] \subset slporbits t.
Fact conjg_porbits_homog :
{in porbits s, forall C, #|fbbij (U := slporbits s) (slporbits t) C| = #|C| }.
#[local] Definition CMbij := PorbitMap conjg_porbits_stab conjg_porbits_homog.
Definition conjbij := cymap CMbij.
Lemma conjbijP x : conjbij (s x) = t (conjbij x).
End DefsFiber.
Lemma conjbijK
(U V : finType) (s : {perm U}) (t : {perm V})
(eqct : cycle_type s = cycle_type t :> seq nat) :
cancel (conjbij eqct) (conjbij (esym eqct)).
Section CycleType.
Variable T : finType.
Implicit Types (s t : {perm T}) (C : {set T}) (P : {set {set T}}).
Theorem conj_permP s t :
reflect (exists c, t = (s ^ c)%g) (cycle_type s == cycle_type t).
Lemma classes_of_permP s t :
(t \in (s ^: [set: {perm T}])%g) = (cycle_type s == cycle_type t).
Section Permofcycletype.
Implicit Types (l : nat) (ct : 'P_#|T|).
Fact perm_of_porbit_subproof C : injective (next (enum C)).
Definition perm_of_porbit C := perm (@perm_of_porbit_subproof C).
Lemma psupport_perm_of_porbit C :
#|C| > 1 -> psupport (perm_of_porbit C) = C.
Lemma perm_of_porbitE C x :
x \in C -> C = porbit (perm_of_porbit C) (head x (enum C)).
Lemma porbits_of_set C : #|C| > 1 -> C \in porbits (perm_of_porbit C).
Lemma porbit_set_of_set C : #|C| > 1 -> porbit_set (perm_of_porbit C) = [set C].
Lemma isperm_of_porbit C : #|C| > 1 -> perm_of_porbit C \is cyclic.
Definition perm_of_setpart P : {perm T} :=
(\prod_(C in [set perm_of_porbit s | s in [set X in P |#|X|>1]]) C)%g.
Lemma psupports_perm_of_porbit P :
[set psupport (perm_of_porbit s) | s in [set X in P | 1 < #|X| ]] =
[set X in P | 1 < #|X|].
Lemma disj_perm_of_setpart P :
partition P [set: T] ->
disjoint_psupports [set perm_of_porbit s| s in [set X0 in P | 1 < #|X0|]].
Lemma porbits_perm_of_setpart P :
partition P [set: T] -> porbits (perm_of_setpart P) = P.
Lemma perm_of_setpartE P :
partition P [set: T] ->
cycle_type (perm_of_setpart P) = setpart_shape P :> seq nat.
End Permofcycletype.
Section TPerm.
Implicit Types (x y z : T).
Lemma porbit_tpermD x y z :
x != z -> y != z -> porbit (tperm x y) z = [set z].
Lemma porbit_tpermL x y : porbit (tperm x y) x = [set x; y].
Lemma porbit_tpermR x y : porbit (tperm x y) y = [set x; y].
Lemma porbits_tperm x y :
porbits (tperm x y) =
[set x; y] |: [set [set z] | z : T & (x != z) && (y != z)].
Lemma cycle_type_tperm x y :
x != y -> cycle_type (tperm x y) = hookpartn #|T| 1.
Lemma tperm_conj x1 y1 x2 y2 :
x1 != y1 -> x2 != y2 -> exists t, tperm x2 y2 = ((tperm x1 y1) ^ t)%g.
Lemma cycle_type_tpermP (s : {perm T}) :
#|T| > 1 ->
cycle_type s = hookpartn #|T| 1 ->
exists x y, x != y /\ s = tperm x y.
End TPerm.
Section Classes.
Variable ct : 'P_#|T|.
Lemma permCT_exists : {s | cycle_type s == ct}.
Definition permCT := val permCT_exists.
Lemma permCTP : cycle_type permCT = ct.
Definition classCT : {set {perm T}} := class permCT [set: {perm T}].
Lemma classCTP s :
(cycle_type s == ct) = (s \in classCT).
Lemma card_classCT_neq0 : #|classCT| != 0%N.
End Classes.
Lemma permCT_colpartn_card : permCT (colpartn #|T|) = 1%g.
Lemma classCT_inj : injective classCT.
Lemma imset_classCT :
[set classCT p | p in setT] = classes [set: {perm T}].
Lemma card_classes_perm :
#|classes [set: {perm T}]| = #|{: 'P_#|T| }|.
Import GroupScope GRing.Theory.
#[local] Open Scope ring_scope.
Section CFunIndicator.
Variable ct : 'P_#|T|.
Definition cfuniCT :=
cfun_indicator [set: {perm T}] (classCT ct).
#[local] Notation "''1_[' p ]" := (cfuniCT p) : ring_scope.
Lemma cfuniCTE s :
('1_[s]) = (cycle_type s == ct)%:R.
End CFunIndicator.
End CycleType.
Notation "''1_[' p ]" := (cfuniCT p) : ring_scope.
Coercion CTpartn n := cast_intpartn (esym (card_ord n)).
Import GroupScope GRing.Theory.
#[local] Open Scope ring_scope.
Variable ct : 'P_#|T|.
Definition cfuniCT :=
cfun_indicator [set: {perm T}] (classCT ct).
#[local] Notation "''1_[' p ]" := (cfuniCT p) : ring_scope.
Lemma cfuniCTE s :
('1_[s]) = (cycle_type s == ct)%:R.
End CFunIndicator.
End CycleType.
Notation "''1_[' p ]" := (cfuniCT p) : ring_scope.
Coercion CTpartn n := cast_intpartn (esym (card_ord n)).
Import GroupScope GRing.Theory.
#[local] Open Scope ring_scope.
Section Sn.
Variable n : nat.
Definition partnCT : 'P_#|'I_n| -> 'P_n := cast_intpartn (card_ord n).
Definition cycle_typeSn (s : 'S_n) : 'P_n := partnCT (cycle_type s).
Lemma CTpartnK (p : 'P_n) : partnCT p = p.
Lemma partnCTE p1 p2 : (p1 == p2) = (partnCT p1 == partnCT p2).
Lemma partnCTK (p : 'P_#|'I_n|) : p = partnCT p.
Lemma partnCT_congr p1 (p2 : 'P_n) : (partnCT p1 == p2) = (p1 == p2).
Lemma CTpartn_colpartn : CTpartn (colpartn n) = colpartn #|'I_n|.
Lemma cycle_typeSn1 : cycle_typeSn 1%g = colpartn n.
Lemma permCT_colpartn : permCT (colpartn n) = 1%g.
Lemma cfuniCTnE (ct : 'P_n) (s : 'S_n) :
'1_[ct] s = (cycle_typeSn s == ct)%:R.
Lemma cycle_typeSn_permCT (ct : 'P_n) : cycle_typeSn (permCT ct) = ct.
End Sn.
Lemma cast_cycle_typeSN m n (s : 'S_m) (eq_mn : m = n) :
cycle_typeSn (cast_perm eq_mn s) = cast_intpartn eq_mn (cycle_typeSn s).
Variable n : nat.
Definition partnCT : 'P_#|'I_n| -> 'P_n := cast_intpartn (card_ord n).
Definition cycle_typeSn (s : 'S_n) : 'P_n := partnCT (cycle_type s).
Lemma CTpartnK (p : 'P_n) : partnCT p = p.
Lemma partnCTE p1 p2 : (p1 == p2) = (partnCT p1 == partnCT p2).
Lemma partnCTK (p : 'P_#|'I_n|) : p = partnCT p.
Lemma partnCT_congr p1 (p2 : 'P_n) : (partnCT p1 == p2) = (p1 == p2).
Lemma CTpartn_colpartn : CTpartn (colpartn n) = colpartn #|'I_n|.
Lemma cycle_typeSn1 : cycle_typeSn 1%g = colpartn n.
Lemma permCT_colpartn : permCT (colpartn n) = 1%g.
Lemma cfuniCTnE (ct : 'P_n) (s : 'S_n) :
'1_[ct] s = (cycle_typeSn s == ct)%:R.
Lemma cycle_typeSn_permCT (ct : 'P_n) : cycle_typeSn (permCT ct) = ct.
End Sn.
Lemma cast_cycle_typeSN m n (s : 'S_m) (eq_mn : m = n) :
cycle_typeSn (cast_perm eq_mn s) = cast_intpartn eq_mn (cycle_typeSn s).