Library Combi.SymGroup.cycles: The Cycle Decomposition of a Permutation
The Cycle Decomposition of a Permutation
- psupport s == the set of non fixed points for s
- porbit_set s == the set of the supports of the cycles of s
- s \is cyclic == s is a cyclic permutation
- perm_dec E s == for E : {set {set T}} the set of the restriction of s to the elements of E.
- cycle_dec s == the decomposition of s in cyclic permutations.
- disjoint_supports A == For A : {set {perm T}}, the element of A have pairwise dijoint supports.
- cycle_dec_spec s A == A is a decomposition of s into disjoint cycles.
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 ssralg.
From mathcomp Require finmodule.
Require Import tools permcomp.
Set Implicit Arguments.
Import GroupScope.
#[export] Hint Resolve porbit_id : core.
Section PermCycles.
Variable T : finType.
Implicit Type (s : {perm T}).
Implicit Type (X : {set T}).
Implicit Type (A : {set {perm T}}).
Definition psupport s := ~: 'Fix_('P)([set s]).
Lemma in_psupport s x : (x \in psupport s) = (s x != x).
Lemma psupport_expg s n : psupport (s ^+ n) \subset psupport s.
Lemma psupport_perm_on S s : (perm_on S s) = (psupport s \subset S).
Lemma psupport1 : psupport (perm_one T) = set0.
Lemma psupport_eq0 s : (s == 1) = (psupport s == set0).
Lemma psupport_stable s x : (x \in psupport s) = (s x \in psupport s).
Lemma card_psupport_noteq1 s : #|psupport s| != 1%N.
Lemma psupport_card_porbit s x : (#|porbit s x| != 1%N) = (x \in psupport s).
Lemma in_psupport s x : (x \in psupport s) = (s x != x).
Lemma psupport_expg s n : psupport (s ^+ n) \subset psupport s.
Lemma psupport_perm_on S s : (perm_on S s) = (psupport s \subset S).
Lemma psupport1 : psupport (perm_one T) = set0.
Lemma psupport_eq0 s : (s == 1) = (psupport s == set0).
Lemma psupport_stable s x : (x \in psupport s) = (s x \in psupport s).
Lemma card_psupport_noteq1 s : #|psupport s| != 1%N.
Lemma psupport_card_porbit s x : (#|porbit s x| != 1%N) = (x \in psupport s).
Complement on porbit
Lemma porbit_fix s x : (s x == x) = (porbit s x == [set x]).
Lemma porbit_mod s x i :
(s ^+ i)%g x = (s ^+ (i %% #|porbit s x|))%g x.
Lemma eq_in_porbit s x i j :
((s ^+ i)%g x == (s ^+ j)%g x) = (i == j %[mod #|porbit s x|]).
Lemma porbit_mod s x i :
(s ^+ i)%g x = (s ^+ (i %% #|porbit s x|))%g x.
Lemma eq_in_porbit s x i j :
((s ^+ i)%g x == (s ^+ j)%g x) = (i == j %[mod #|porbit s x|]).
Definition porbit_set s : {set {set T}} := [set x in porbits s | #|x| != 1%N].
Lemma in_porbit_setP s X x:
reflect (exists2 X, X \in porbit_set s & x \in X) (s x != x).
Lemma partition_porbits s : partition (porbits s) setT.
Lemma partition_psupport s : partition (porbit_set s) (psupport s).
Lemma porbit_set_eq0 s : (s == perm_one T) = (porbit_set s == set0).
Lemma porbit_set_astabs s X : X \in porbit_set s -> s \in 'N(X | 'P).
Lemma in_porbit_setP s X x:
reflect (exists2 X, X \in porbit_set s & x \in X) (s x != x).
Lemma partition_porbits s : partition (porbits s) setT.
Lemma partition_psupport s : partition (porbit_set s) (psupport s).
Lemma porbit_set_eq0 s : (s == perm_one T) = (porbit_set s == set0).
Lemma porbit_set_astabs s X : X \in porbit_set s -> s \in 'N(X | 'P).
Definition cyclic := [qualify s | #|porbit_set s| == 1%N].
Lemma cyclicP c :
reflect (exists2 x, x \in psupport c & psupport c = porbit c x)
(c \is cyclic).
Lemma cycle_cyclic t :
t \is cyclic -> cycle t = [set t ^+ i | i : 'I_#|psupport t|].
Lemma order_cyclic t : t \is cyclic -> #[t] = #|psupport t|.
Lemma cyclicP c :
reflect (exists2 x, x \in psupport c & psupport c = porbit c x)
(c \is cyclic).
Lemma cycle_cyclic t :
t \is cyclic -> cycle t = [set t ^+ i | i : 'I_#|psupport t|].
Lemma order_cyclic t : t \is cyclic -> #[t] = #|psupport t|.
Complement about restr_perm
Lemma psupport_restr_perm_incl X s :
psupport (restr_perm X s) \subset X.
Lemma restr_perm_neq X s x :
restr_perm X s x != x -> restr_perm X s x = s x.
Lemma psupport_restr_perm X s :
X \in porbit_set s -> psupport (restr_perm X s) = X.
Lemma restr_perm_psupportE X s :
restr_perm (psupport (restr_perm X s)) s = restr_perm X s.
Lemma porbit_restr_perm s x :
porbit (restr_perm (porbit s x) s) x = porbit s x.
Lemma porbit_set_restr s X :
X \in porbit_set s -> porbit_set (restr_perm X s) = [set X].
psupport (restr_perm X s) \subset X.
Lemma restr_perm_neq X s x :
restr_perm X s x != x -> restr_perm X s x = s x.
Lemma psupport_restr_perm X s :
X \in porbit_set s -> psupport (restr_perm X s) = X.
Lemma restr_perm_psupportE X s :
restr_perm (psupport (restr_perm X s)) s = restr_perm X s.
Lemma porbit_restr_perm s x :
porbit (restr_perm (porbit s x) s) x = porbit s x.
Lemma porbit_set_restr s X :
X \in porbit_set s -> porbit_set (restr_perm X s) = [set X].
Definition perm_dec (S : {set {set T}}) s : {set {perm T}} :=
[set restr_perm X s | X in S].
Definition cycle_dec s : {set {perm T}} := perm_dec (porbit_set s) s.
Lemma cyclic_dec s : {in (cycle_dec s), forall C, C \is cyclic}.
Lemma psupport_cycle_dec s :
[set psupport C | C in cycle_dec s] = porbit_set s.
[set restr_perm X s | X in S].
Definition cycle_dec s : {set {perm T}} := perm_dec (porbit_set s) s.
Lemma cyclic_dec s : {in (cycle_dec s), forall C, C \is cyclic}.
Lemma psupport_cycle_dec s :
[set psupport C | C in cycle_dec s] = porbit_set s.
Definition disjoint_psupports A :=
trivIset [set psupport C| C in A] /\ {in A &, injective psupport}.
Lemma disjoint_psupport_subset (S1 S2 : {set {perm T}}) :
S1 \subset S2 -> disjoint_psupports S2 -> disjoint_psupports S1.
Lemma disjoint_perm_dec S s :
trivIset S -> disjoint_psupports (perm_dec S s).
Lemma disjoint_cycle_dec s :
disjoint_psupports (cycle_dec s).
Lemma psupport_disjointC s t :
[disjoint psupport s & psupport t] -> commute s t.
Lemma abelian_disjoint_psupports A : disjoint_psupports A -> abelian <<A>>.
Lemma abelian_perm_dec S s : trivIset S -> abelian <<perm_dec S s>>.
Lemma abelian_cycle_dec s : abelian <<cycle_dec s>>.
Lemma restr_perm_inj s :
{in porbit_set s &, injective ((restr_perm (T:=T))^~ s)}.
Lemma out_perm_prod A x :
{in A, forall C, x \notin psupport C} -> (\prod_(C in A) C) x = x.
Import finmodule.FiniteModule morphism.
Lemma prod_of_disjoint A C x:
disjoint_psupports A -> C \in A ->
x \in psupport C -> (\prod_(C0 in A) C0) x = C x.
Lemma expg_prod_of_disjoint A C x i:
disjoint_psupports A -> C \in A ->
x \in psupport C -> ((\prod_(C0 in A) C0) ^+ i) x = (C ^+ i) x.
Lemma psupport_of_disjoint A :
disjoint_psupports A ->
psupport (\prod_(C0 in A) C0) = \bigcup_(C0 in A) psupport C0.
Lemma porbit_set_of_disjoint A :
disjoint_psupports A ->
porbit_set (\prod_(C0 in A) C0) = \bigcup_(C0 in A) porbit_set C0.
Lemma perm_decE S s :
trivIset S -> psupport s \subset cover S ->
s \in 'C(S | ('P)^* ) ->
\prod_(C in perm_dec S s) C = s.
Lemma cycle_decE s : \prod_(C in cycle_dec s) C = s.
Lemma disjoint_psupports_of_decomp A B :
disjoint_psupports A -> disjoint_psupports B ->
\prod_(C in A) C = \prod_(C in B) C ->
{in A & B, forall c1 c2, psupport c1 = psupport c2 -> c1 = c2}.
Lemma disjoint_psupports_cycles A :
{in A, forall C, C \is cyclic} ->
disjoint_psupports A ->
{in A, forall C, psupport C \in porbits (\prod_(C in A) C)}.
Lemma disjoint_psupports_porbits A :
{in A, forall C, C \is cyclic} ->
disjoint_psupports A ->
{in porbit_set (\prod_(C in A) C),
forall X, exists2 C, C \in A & psupport C = X}.
trivIset [set psupport C| C in A] /\ {in A &, injective psupport}.
Lemma disjoint_psupport_subset (S1 S2 : {set {perm T}}) :
S1 \subset S2 -> disjoint_psupports S2 -> disjoint_psupports S1.
Lemma disjoint_perm_dec S s :
trivIset S -> disjoint_psupports (perm_dec S s).
Lemma disjoint_cycle_dec s :
disjoint_psupports (cycle_dec s).
Lemma psupport_disjointC s t :
[disjoint psupport s & psupport t] -> commute s t.
Lemma abelian_disjoint_psupports A : disjoint_psupports A -> abelian <<A>>.
Lemma abelian_perm_dec S s : trivIset S -> abelian <<perm_dec S s>>.
Lemma abelian_cycle_dec s : abelian <<cycle_dec s>>.
Lemma restr_perm_inj s :
{in porbit_set s &, injective ((restr_perm (T:=T))^~ s)}.
Lemma out_perm_prod A x :
{in A, forall C, x \notin psupport C} -> (\prod_(C in A) C) x = x.
Import finmodule.FiniteModule morphism.
Lemma prod_of_disjoint A C x:
disjoint_psupports A -> C \in A ->
x \in psupport C -> (\prod_(C0 in A) C0) x = C x.
Lemma expg_prod_of_disjoint A C x i:
disjoint_psupports A -> C \in A ->
x \in psupport C -> ((\prod_(C0 in A) C0) ^+ i) x = (C ^+ i) x.
Lemma psupport_of_disjoint A :
disjoint_psupports A ->
psupport (\prod_(C0 in A) C0) = \bigcup_(C0 in A) psupport C0.
Lemma porbit_set_of_disjoint A :
disjoint_psupports A ->
porbit_set (\prod_(C0 in A) C0) = \bigcup_(C0 in A) porbit_set C0.
Lemma perm_decE S s :
trivIset S -> psupport s \subset cover S ->
s \in 'C(S | ('P)^* ) ->
\prod_(C in perm_dec S s) C = s.
Lemma cycle_decE s : \prod_(C in cycle_dec s) C = s.
Lemma disjoint_psupports_of_decomp A B :
disjoint_psupports A -> disjoint_psupports B ->
\prod_(C in A) C = \prod_(C in B) C ->
{in A & B, forall c1 c2, psupport c1 = psupport c2 -> c1 = c2}.
Lemma disjoint_psupports_cycles A :
{in A, forall C, C \is cyclic} ->
disjoint_psupports A ->
{in A, forall C, psupport C \in porbits (\prod_(C in A) C)}.
Lemma disjoint_psupports_porbits A :
{in A, forall C, C \is cyclic} ->
disjoint_psupports A ->
{in porbit_set (\prod_(C in A) C),
forall X, exists2 C, C \in A & psupport C = X}.
Variant cycle_dec_spec s A : Prop :=
CycleDecSpec of
{in A, forall C, C \is cyclic} &
disjoint_psupports A &
\prod_(C in A) C = s : cycle_dec_spec s A.
Theorem cycle_decP s : unique (cycle_dec_spec s) (cycle_dec s).
End PermCycles.
Arguments cyclic {T}.
CycleDecSpec of
{in A, forall C, C \is cyclic} &
disjoint_psupports A &
\prod_(C in A) C = s : cycle_dec_spec s A.
Theorem cycle_decP s : unique (cycle_dec_spec s) (cycle_dec s).
End PermCycles.
Arguments cyclic {T}.