diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/fingroup/action.v | 19 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 30 |
3 files changed, 28 insertions, 26 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b6ba306..26f1ed9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -37,8 +37,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added definition `cast_perm` with a group morphism canonical structure, and lemmas `permX_fix`, `imset_perm1`, `permS0`, `permS1`, `cast_perm_id`, `cast_ord_permE`, `cast_permE`, - `cast_permK`, `cast_permKV`, `cast_perm_inj`, `cast_perm_morphM`, - and `isom_cast_perm` in `perm` and `restr_perm_commute` in `action` + `cast_perm_comp`, `cast_permK`, `cast_permKV`, `cast_perm_inj`, + `cast_perm_sym`,`cast_perm_morphM`, and `isom_cast_perm` in `perm` + and `restr_perm_commute` in `action`. - Added `card_porbit_neq0`, `porbitP`, and `porbitPmin` in `perm` diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 9631d28..2d1b6e6 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -1682,13 +1682,11 @@ Proof. exact: im_perm_on (restr_perm_on p). Qed. Lemma restr_perm_commute s : commute (restr_perm s) s. Proof. -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)/= ->. +have [sC|/triv_restr_perm->] := boolP (s \in 'N(S | 'P)); last first. + exact: (commute_sym (commute1 _)). +apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM. +have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS. +by rewrite !(out_perm (restr_perm_on _)) ?xsS. Qed. End RestrictPerm. @@ -1699,10 +1697,9 @@ Variables (T : finType) (S : {set T}). Lemma SymE : Sym S = 'C(~: S | 'P). Proof. -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 => ->. +apply/setP => s; rewrite inE; apply/idP/astabP => [sS x|/= S_id]. + by rewrite inE /= apermE => /out_perm->. +by apply/subsetP => x; move=> /(contra_neqN (S_id _)); rewrite inE negbK. Qed. End Symmetry. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index cb77078..0c02f3b 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -634,14 +634,12 @@ End LiftPerm. Prenex Implicits lift_perm lift_permK. -Lemma permS0 (g : 'S_0) : g = 1%g. -Proof. by apply permP => x; case x. Qed. +Lemma permS0 : all_equal_to (1 : 'S_0). +Proof. by move=> g; apply/permP; case. Qed. -Lemma permS1 (g : 'S_1) : g = 1%g. +Lemma permS1 : all_equal_to (1 : 'S_1). 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]. +by move=> g; apply/permP => i; apply: val_inj; do ![case: (X in val X); case]. Qed. Section CastSn. @@ -657,9 +655,13 @@ Lemma cast_ord_permE m n eq_m_n (s : 'S_m) i : Proof. 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. + cast_perm eq_m_n s i = cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)). Proof. by rewrite cast_ord_permE cast_ordKV. Qed. +Lemma cast_perm_comp m n p (eq_m_n : m = n) (eq_n_p : n = p) s : + cast_perm eq_n_p (cast_perm eq_m_n s) = cast_perm (etrans eq_m_n eq_n_p) s. +Proof. by case: _ / eq_n_p. Qed. + Lemma cast_permK m n eq_m_n : cancel (@cast_perm m n eq_m_n) (cast_perm (esym eq_m_n)). Proof. by subst m. Qed. @@ -668,6 +670,10 @@ Lemma cast_permKV m n eq_m_n : cancel (cast_perm (esym eq_m_n)) (@cast_perm m n eq_m_n). Proof. by subst m. Qed. +Lemma cast_perm_sym m n (eq_m_n : m = n) s t : + s = cast_perm eq_m_n t -> t = cast_perm (esym eq_m_n) s. +Proof. by move/(canLR (cast_permK _)). Qed. + Lemma cast_perm_inj m n eq_m_n : injective (@cast_perm m n eq_m_n). Proof. exact: can_inj (cast_permK eq_m_n). Qed. @@ -675,15 +681,13 @@ Lemma cast_perm_morphM m n eq_m_n : {morph @cast_perm m n eq_m_n : x y / x * y >-> x * y}. Proof. 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)). + @Morphism _ _ setT (cast_perm eq_m_n) (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. -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. +case: {n} _ / eq_m_n; apply/isomP; split. + exact/injmP/(in2W (@cast_perm_inj _ _ _)). +by apply/setP => /= s; rewrite !inE; apply/imsetP; exists s; rewrite ?inE. Qed. End CastSn. |