From 73698b6b4c2c38f0485c24685f79eefcaa74d3d8 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 26 Aug 2018 16:36:58 +0200 Subject: [PATCH] Some more lemmas on permutations --- mathcomp/fingroup/action.v | 30 +++++++++++++ mathcomp/fingroup/perm.v | 87 +++++++++++++++++++++++++++++++++++++- 2 files changed, 116 insertions(+), 1 deletion(-) diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 5c5dcdc7a3..a34af39dac 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -1688,8 +1688,38 @@ Proof. by rewrite ker_actperm astab_actby setIT (setIidPr (astab_sub _ _)). Qed. Lemma im_restr_perm p : restr_perm p @: S = S. Proof. exact: im_perm_on (restr_perm_on p). Qed. +Definition perm_ong : {set {perm T}} := [set s | perm_on S s]. +Lemma group_set_perm_ong : group_set perm_ong. +Proof using. +apply/group_setP; split => [| s t]; rewrite !inE; + [exact: perm_on1 | exact: perm_onM]. +Qed. +Canonical perm_ong_group : {group {perm T}} := Group group_set_perm_ong. +Lemma card_perm_ong : #|perm_ong| = #|S|`!. +Proof using. by rewrite cardsE /= card_perm. Qed. + +Lemma perm_ongE : perm_ong = 'C(~:S | 'P). +Proof using. +apply/setP => s; rewrite inE; apply/idP/astabP => [Hperm x | Hstab]. +- by rewrite inE /= apermE => /out_perm; apply. +- apply/subsetP => x; rewrite unfold_in; apply contraR => H. + by move/(_ x): Hstab; rewrite inE /= apermE => ->. +Qed. + +Lemma restr_perm_commute s : commute (restr_perm s) s. +Proof using. +case: (boolP (s \in 'N(S | 'P))) => + [HC | /triv_restr_perm ->]; last exact: (commute_sym (commute1 _)). +apply/permP => x; case: (boolP (x \in S)) => Hx; rewrite !permM. +- by rewrite !restr_permE //; move: HC => /astabsP/(_ x)/= ->. +- have:= restr_perm_on s => /out_perm Hout. + rewrite (Hout _ Hx) {}Hout //. + by move: Hx; apply contra; move: HC => /astabsP/(_ x)/= ->. +Qed. + End RestrictPerm. + Section AutIn. Variable gT : finGroupType. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 3edcfedcf9..514902751f 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype. From mathcomp -Require Import tuple finfun bigop finset binomial fingroup. +Require Import tuple finfun bigop finset binomial fingroup morphism. (******************************************************************************) (* This file contains the definition and properties associated to the group *) @@ -165,6 +165,9 @@ Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ]. Lemma perm1 x : (1 : {perm T}) x = x. Proof. by rewrite permE. Qed. +Lemma imset_perm1 (S : {set T}) : [set fun_of_perm 1 x | x in S] = S. +Proof. by rewrite -[RHS]imset_id; apply eq_imset => x; rewrite perm1. Qed. + Lemma permM s t x : (s * t) x = t (s x). Proof. by rewrite permE. Qed. @@ -180,6 +183,12 @@ Proof. by rewrite !permM permK. Qed. Lemma permX s x n : (s ^+ n) x = iter n s x. Proof. by elim: n => [|n /= <-]; rewrite ?perm1 // -permM expgSr. Qed. +Lemma permX_fix s x n : s x = x -> (s ^+ n) x = x. +Proof using. +move=> Hs; elim: n => [|n IHn]; first by rewrite expg0 perm1. +by rewrite expgS permM Hs. +Qed. + Lemma im_permV s S : s^-1 @: S = s @^-1: S. Proof. exact: can2_imset_pre (permKV s) (permK s). Qed. @@ -342,6 +351,11 @@ Proof. by rewrite (mem_imset (aperm x)) ?mem_cycle. Qed. Lemma pcycle_id s x : x \in pcycle s x. Proof. by rewrite -{1}[x]perm1 (mem_pcycle s 0). Qed. +Lemma card_pcycle_neq0 s x : #|pcycle s x| != 0. +Proof using. +by rewrite -lt0n card_gt0; apply/set0Pn; exists x; exact: pcycle_id. +Qed. + Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|). Proof. case def_n: #|_| => // [n]; rewrite looping_uniq. @@ -382,6 +396,17 @@ Proof. by rewrite -!eq_pcycle_mem eq_sym. Qed. Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x. Proof. by apply/eqP; rewrite eq_pcycle_mem mem_pcycle. Qed. +Lemma pcyclePmin s x y : + y \in pcycle s x -> exists2 i, i < #[s] & y = (s ^+ i) x. +Proof using. by move=> /imsetP [z /cyclePmin[ i Hi ->{z}] ->{y}]; exists i. Qed. + +Lemma pcycleP s x y : + reflect (exists i, y = (s ^+ i) x) (y \in pcycle s x). +Proof using. +apply (iffP idP) => [/pcyclePmin [i _ ->]| [i ->]]; last exact: mem_pcycle. +by exists i. +Qed. + Lemma ncycles_mul_tperm s x y : let t := tperm x y in #|pcycles (t * s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y). Proof. @@ -513,6 +538,14 @@ Variable n : nat. Implicit Types i j : 'I_n.+1. Implicit Types s t : 'S_n. +Lemma card_Sn : #|'S_(n)| = n`!. +Proof. +rewrite (eq_card (B := perm_on [set : 'I_n])). + by rewrite card_perm /= cardsE /= card_ord. +move=> p; rewrite inE unfold_in /perm_on /=. +by apply/esym/subsetP => i _; rewrite in_set. +Qed. + Definition lift_perm_fun i j s k := if unlift i k is Some k' then lift j (s k') else j. @@ -576,5 +609,57 @@ Qed. End LiftPerm. +Lemma permS0 (g : 'S_0) : g = 1%g. +Proof. by apply permP => x; case x. Qed. +Lemma permS1 (g : 'S_1) : g = 1%g. +Proof. +apply/permP => i; rewrite perm1. +case: (g i) => a Ha; case: i => b Hb. +by apply val_inj => /=; case: a b Ha Hb => [|a] [|b]. +Qed. + +Section CastSn. + +Definition cast_perm m n (eq_mn : m = n) (s : 'S_m) := + let: erefl in _ = n := eq_mn return 'S_n in s. + +Lemma cast_perm_id n eq_n s : cast_perm eq_n s = s :> 'S_n. +Proof using. by apply/permP => i; rewrite /cast_perm /= eq_axiomK. Qed. + +Lemma cast_ord_permE m n eq_m_n (s : 'S_m) i : + @cast_ord m n eq_m_n (s i) = (cast_perm eq_m_n s) (cast_ord eq_m_n i). +Proof using. by subst m; rewrite cast_perm_id !cast_ord_id. Qed. + +Lemma cast_permE m n (eq_m_n : m = n) (s : 'S_m) (i : 'I_n) : + cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)) = cast_perm eq_m_n s i. +Proof. by rewrite cast_ord_permE cast_ordKV. Qed. + +Lemma cast_permK m n eq_m_n : + cancel (@cast_perm m n eq_m_n) (cast_perm (esym eq_m_n)). +Proof using. by subst m. Qed. + +Lemma cast_permKV m n eq_m_n : + cancel (cast_perm (esym eq_m_n)) (@cast_perm m n eq_m_n). +Proof using. by subst m. Qed. + +Lemma cast_perm_inj m n eq_m_n : injective (@cast_perm m n eq_m_n). +Proof using. exact: can_inj (cast_permK eq_m_n). Qed. + +Lemma cast_perm_morphM m n eq_m_n : + {morph @cast_perm m n eq_m_n : x y / x * y >-> x * y}. +Proof using. by subst m. Qed. +Canonical morph_of_cast_perm m n eq_m_n := + Morphism (D := setT) (in2W (@cast_perm_morphM m n eq_m_n)). + +Lemma isom_cast_perm m n eq_m_n : isom setT setT (@cast_perm m n eq_m_n). +Proof using. +subst m. +apply/isomP; split. +- apply/injmP=> i j _ _; exact: cast_perm_inj. +- apply/setP => /= s; rewrite !inE. + by apply/imsetP; exists s; rewrite ?inE. +Qed. + +End CastSn.