diff options
| author | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
| commit | 532de9b68384a114c6534a0736ed024c900447f9 (patch) | |
| tree | e100a6a7839bf7548ab8a9e053033f8eef3c7492 /mathcomp/solvable | |
| parent | f180c539a00fd83d8b3b5fd2d5710eb16e971e2e (diff) | |
Updating files + reorganizing everything
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/Make | 3 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 77 | ||||
| -rw-r--r-- | mathcomp/solvable/all_solvable.v (renamed from mathcomp/solvable/all.v) | 1 | ||||
| -rw-r--r-- | mathcomp/solvable/alt.v | 35 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 31 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 37 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 27 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 869 | ||||
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 50 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 134 | ||||
| -rw-r--r-- | mathcomp/solvable/finmodule.v | 43 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 49 | ||||
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 50 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 32 | ||||
| -rw-r--r-- | mathcomp/solvable/hall.v | 78 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 27 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 170 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 75 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 177 | ||||
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 37 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 71 |
21 files changed, 1444 insertions, 629 deletions
diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make index 41bd3e0..d89d213 100644 --- a/mathcomp/solvable/Make +++ b/mathcomp/solvable/Make @@ -1,9 +1,10 @@ abelian.v -all.v +all_solvable.v alt.v burnside_app.v center.v commutator.v +cyclic.v extraspecial.v extremal.v finmodule.v diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 52f92ec..0d87755 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1,14 +1,13 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div fintype finfun bigop finset prime binomial. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism action quotient gproduct. -From mathcomp.algebra -Require Import cyclic zmodp. -Require Import gfunctor pgroup gseries nilpotent sylow. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype. +From mathcomp +Require Import finfun bigop finset prime binomial fingroup morphism perm. +From mathcomp +Require Import automorphism action quotient gfunctor gproduct zmodp cyclic. +From mathcomp +Require Import pgroup gseries nilpotent sylow. (******************************************************************************) (* Constructions based on abelian groups and their structure, with some *) @@ -245,7 +244,7 @@ Lemma exponent1 : exponent [1 gT] = 1%N. Proof. by apply/eqP; rewrite -dvdn1 -trivg_exponent eqxx. Qed. Lemma exponent_dvdn G : exponent G %| #|G|. -Proof. by apply/dvdn_biglcmP=> x Gx; exact: order_dvdG. Qed. +Proof. by apply/dvdn_biglcmP=> x Gx; apply: order_dvdG. Qed. Lemma exponent_gt0 G : 0 < exponent G. Proof. exact: dvdn_gt0 (exponent_dvdn G). Qed. @@ -257,7 +256,7 @@ congr (_ && _); first by rewrite cardG_gt0 exponent_gt0. apply: eq_all_r => p; rewrite !mem_primes cardG_gt0 exponent_gt0 /=. apply: andb_id2l => p_pr; apply/idP/idP=> pG. exact: dvdn_trans pG (exponent_dvdn G). -by case/Cauchy: pG => // x Gx <-; exact: dvdn_exponent. +by case/Cauchy: pG => // x Gx <-; apply: dvdn_exponent. Qed. Lemma exponentJ A x : exponent (A :^ x) = exponent A. @@ -284,7 +283,7 @@ Lemma exponent_cycle x : exponent <[x]> = #[x]. Proof. by apply/eqP; rewrite eqn_dvd exponent_dvdn dvdn_exponent ?cycle_id. Qed. Lemma exponent_cyclic X : cyclic X -> exponent X = #|X|. -Proof. by case/cyclicP=> x ->; exact: exponent_cycle. Qed. +Proof. by case/cyclicP=> x ->; apply: exponent_cycle. Qed. Lemma primes_exponent G : primes (exponent G) = primes (#|G|). Proof. @@ -320,7 +319,7 @@ Lemma exponent_Hall pi G H : pi.-Hall(G) H -> exponent H = (exponent G)`_pi. Proof. move=> hallH; have [sHG piH _] := and3P hallH. rewrite -(partn_exponentS sHG) -?(card_Hall hallH) ?part_pnat_id //. -by apply: pnat_dvd piH; exact: exponent_dvdn. +by apply: pnat_dvd piH; apply: exponent_dvdn. Qed. Lemma exponent_Zgroup G : Zgroup G -> exponent G = #|G|. @@ -371,7 +370,7 @@ Proof. move=> cGG; apply/group_setP. split=> [|x y]; rewrite !inE ?group1 ?expg1n //=. case/andP=> Gx /eqP xn /andP[Gy /eqP yn]. -rewrite groupM //= expgMn ?xn ?yn ?mulg1 //; exact: (centsP cGG). +by rewrite groupM //= expgMn ?xn ?yn ?mulg1 //; apply: (centsP cGG). Qed. Lemma abelian_exponent_gen A : abelian A -> exponent <<A>> = exponent A. @@ -414,7 +413,7 @@ Qed. Lemma cyclic_abelem_prime p X : p.-abelem X -> cyclic X -> X :!=: 1 -> #|X| = p. Proof. move=> abelX cycX; case/cyclicP: cycX => x -> in abelX *. -by rewrite cycle_eq1; exact: abelem_order_p abelX (cycle_id x). +by rewrite cycle_eq1; apply: abelem_order_p abelX (cycle_id x). Qed. Lemma cycle_abelem p x : p.-elt x || prime p -> p.-abelem <[x]> = (#[x] %| p). @@ -423,7 +422,7 @@ move=> p_xVpr; rewrite /abelem cycle_abelian /=. apply/andP/idP=> [[_ xp1] | x_dvd_p]. by rewrite order_dvdn (exponentP xp1) ?cycle_id. split; last exact: dvdn_trans (exponent_dvdn _) x_dvd_p. -by case/orP: p_xVpr => // /pnat_id; exact: pnat_dvd. +by case/orP: p_xVpr => // /pnat_id; apply: pnat_dvd. Qed. Lemma exponent2_abelem G : exponent G %| 2 -> 2.-abelem G. @@ -494,7 +493,7 @@ by rewrite (is_abelem_pgroup (abelem_pgroup abelG)). Qed. Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)). -Proof. by rewrite inE; exact: andP. Qed. +Proof. by rewrite inE; apply: andP. Qed. Implicit Arguments pElemP [p A E]. Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B). @@ -602,7 +601,7 @@ apply/and3P; split; last 1 first. - apply/imsetP=> [[X /card_p1Elem oX X'0]]. by rewrite -oX (cardsD1 1) -X'0 group1 cards0 in p_pr. - rewrite eqEsubset; apply/andP; split. - by apply/bigcupsP=> _ /imsetP[X /pnElemP[sXE _ _] ->]; exact: setSD. + by apply/bigcupsP=> _ /imsetP[X /pnElemP[sXE _ _] ->]; apply: setSD. apply/subsetP=> x /setD1P[ntx Ex]. apply/bigcupP; exists <[x]>^#; last by rewrite !inE ntx cycle_id. apply/imsetP; exists <[x]>%G; rewrite ?p1ElemE // !inE cycle_subG Ex /=. @@ -680,7 +679,7 @@ Qed. Lemma pmaxElemP p A E : reflect (E \in 'E_p(A) /\ forall H, H \in 'E_p(A) -> E \subset H -> H :=: E) (E \in 'E*_p(A)). -Proof. by rewrite [E \in 'E*_p(A)]inE; exact: (iffP maxgroupP). Qed. +Proof. by rewrite [E \in 'E*_p(A)]inE; apply: (iffP maxgroupP). Qed. Lemma pmaxElem_exists p A D : D \in 'E_p(A) -> {E | E \in 'E*_p(A) & D \subset E}. @@ -716,7 +715,7 @@ Proof. move=> sAB; apply/subsetP=> E; rewrite !inE. case/andP=> /maxgroupP[/pElemP[_ abelE] maxE] sEA. apply/maxgroupP; rewrite inE sEA; split=> // D EpD. -by apply: maxE; apply: subsetP EpD; exact: pElemS. +by apply: maxE; apply: subsetP EpD; apply: pElemS. Qed. Lemma pmaxElemJ p A E x : ((E :^ x)%G \in 'E*_p(A :^ x)) = (E \in 'E*_p(A)). @@ -736,7 +735,7 @@ Qed. Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}. Proof. rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid. -by exists B; first exact/eqP. +by exists B; first apply/eqP. Qed. Lemma p_rank_witness p G : {E | E \in 'E_p^('r_p(G))(G)}. @@ -751,7 +750,7 @@ Proof. apply: (iffP idP) => [|[E]]; last first. by rewrite inE => /andP[Ep_E /eqP <-]; rewrite (bigmax_sup E). have [D /pnElemP[sDG abelD <-]] := p_rank_witness p G. -by case/abelem_pnElem=> // E; exists E; exact: (subsetP (pnElemS _ _ sDG)). +by case/abelem_pnElem=> // E; exists E; apply: (subsetP (pnElemS _ _ sDG)). Qed. Lemma p_rank_gt0 p H : ('r_p(H) > 0) = (p \in \pi(H)). @@ -772,7 +771,7 @@ Proof. by move=> EpA_E; rewrite (bigmax_sup E). Qed. Lemma p_rank_le_logn p G : 'r_p(G) <= logn p #|G|. Proof. have [E EpE] := p_rank_witness p G. -by have [sEG _ <-] := pnElemP EpE; exact: lognSg. +by have [sEG _ <-] := pnElemP EpE; apply: lognSg. Qed. Lemma p_rank_abelem p G : p.-abelem G -> 'r_p(G) = logn p #|G|. @@ -931,7 +930,7 @@ Qed. Lemma morphim_Ldiv n A : f @* 'Ldiv_n(A) \subset 'Ldiv_n(f @* A). Proof. -by apply: subset_trans (morphimI f A _) (setIS _ _); exact: morphim_LdivT. +by apply: subset_trans (morphimI f A _) (setIS _ _); apply: morphim_LdivT. Qed. Lemma morphim_abelem p G : p.-abelem G -> p.-abelem (f @* G). @@ -984,7 +983,7 @@ by rewrite sub_morphim_pre ?morphim_sub // morphpre_invm. Qed. Lemma injm_abelem p : p.-abelem (f @* G) = p.-abelem G. -Proof. by apply/idP/idP; first rewrite -{2}defG; exact: morphim_abelem. Qed. +Proof. by apply/idP/idP; first rewrite -{2}defG; apply: morphim_abelem. Qed. Lemma injm_pElem p (E : {group aT}) : E \subset D -> ((f @* E)%G \in 'E_p(f @* G)) = (E \in 'E_p(G)). @@ -1255,7 +1254,7 @@ move=> pG; apply/eqP; rewrite eqEsubset !gen_subG; apply/andP. do [split; apply/subsetP=> xpn; case/imsetP=> x] => [|Gx ->]; last first. by rewrite Mho_p_elt ?(mem_p_elt pG). case/setIdP=> Gx _ ->; have [-> | ntx] := eqVneq x 1; first by rewrite expg1n. -by rewrite (pdiv_p_elt (mem_p_elt pG Gx) ntx) mem_gen //; exact: mem_imset. +by rewrite (pdiv_p_elt (mem_p_elt pG Gx) ntx) mem_gen //; apply: mem_imset. Qed. Lemma MhoEabelian p G : @@ -1264,7 +1263,7 @@ Proof. move=> pG cGG; rewrite (MhoE pG); rewrite gen_set_id //; apply/group_setP. split=> [|xn yn]; first by apply/imsetP; exists 1; rewrite ?expg1n. case/imsetP=> x Gx ->; case/imsetP=> y Gy ->. -by rewrite -expgMn; [apply: mem_imset; rewrite groupM | exact: (centsP cGG)]. +by rewrite -expgMn; [apply: mem_imset; rewrite groupM | apply: (centsP cGG)]. Qed. Lemma trivg_Mho G : 'Mho^n(G) == 1 -> 'Ohm_n(G) == G. @@ -1274,14 +1273,14 @@ rewrite -{1}(Sylow_gen G) genS //; apply/bigcupsP=> P. case/SylowP=> p p_pr /and3P[sPG pP _]; apply/subsetP=> x Px. have Gx := subsetP sPG x Px; rewrite inE Gx //=. rewrite (sameP eqP set1P) (subsetP Gp1) ?mem_gen //; apply: mem_imset. -by rewrite inE Gx; exact: pgroup_p (mem_p_elt pP Px). +by rewrite inE Gx; apply: pgroup_p (mem_p_elt pP Px). Qed. Lemma Mho_p_cycle p x : p.-elt x -> 'Mho^n(<[x]>) = <[x ^+ (p ^ n)]>. Proof. move=> p_x. apply/eqP; rewrite (MhoE p_x) eqEsubset cycle_subG mem_gen; last first. - by apply: mem_imset; exact: cycle_id. + by apply: mem_imset; apply: cycle_id. rewrite gen_subG andbT; apply/subsetP=> _ /imsetP[_ /cycleP[k ->] ->]. by rewrite -expgM mulnC expgM mem_cycle. Qed. @@ -1332,7 +1331,7 @@ Proof. exact: morphimF. Qed. Lemma injm_Ohm (f : {morphism D >-> rT}) : 'injm f -> G \subset D -> f @* 'Ohm_n(G) = 'Ohm_n(f @* G). -Proof. by move=> injf; exact: injmF. Qed. +Proof. by move=> injf; apply: injmF. Qed. Lemma isog_Ohm (H : {group rT}) : G \isog H -> 'Ohm_n(G) \isog 'Ohm_n(H). Proof. exact: gFisog. Qed. @@ -1425,7 +1424,7 @@ Lemma abelem_Ohm1P p G : abelian G -> p.-group G -> reflect ('Ohm_1(G) = G) (p.-abelem G). Proof. move=> cGG pG. -apply: (iffP idP) => [| <-]; [exact: Ohm1_id | exact: Ohm1_abelem]. +by apply: (iffP idP) => [| <-]; [apply: Ohm1_id | apply: Ohm1_abelem]. Qed. Lemma TI_Ohm1 G H : H :&: 'Ohm_1(G) = 1 -> H :&: G = 1. @@ -1699,7 +1698,7 @@ have{lnOx} lnOy i: lnO i <[x]> = lnO i <[y]>. have co_yx': coprime #[y] #[x.`_p^'] by rewrite !order_constt coprime_partC. have defX: <[y]> \x <[x.`_p^']> = <[x]>. rewrite dprodE ?coprime_TIg //. - by rewrite -cycleM ?consttC //; apply: (centsP cXX); exact: mem_cycle. + by rewrite -cycleM ?consttC //; apply: (centsP cXX); apply: mem_cycle. by apply: (sub_abelian_cent2 cXX); rewrite cycle_subG mem_cycle. rewrite -(lnOx i _ _ _ defX) addnC {1}/lnO lognE. case: and3P => // [[p_pr _ /idPn[]]]; rewrite -p'natE //. @@ -1760,7 +1759,7 @@ apply/eqP; rewrite -def_t size_map eqn_leq andbC; apply/andP; split. case/lastP def_b: b => // [b' x]; pose p := pdiv #[x]. have p_pr: prime p. have:= abelian_type_gt1 G; rewrite -def_t def_b map_rcons -cats1 all_cat. - by rewrite /= andbT => /andP[_]; exact: pdiv_prime. + by rewrite /= andbT => /andP[_]; apply: pdiv_prime. suffices: all [pred y | logn p #[y] > 0] b. rewrite all_count (count_logn_dprod_cycle _ _ defG) -def_b; move/eqP <-. by rewrite Ohm0 indexg1 -p_rank_abelian ?p_rank_le_rank. @@ -1791,9 +1790,9 @@ case p_x: (p_group <[x]>); last first. rewrite -order_gt1 /p_group -orderE; set p := pdiv _ => ntx p'x. have def_x: <[x.`_p]> \x <[x.`_p^']> = <[x]>. have ?: coprime #[x.`_p] #[x.`_p^'] by rewrite !order_constt coprime_partC. - have ?: commute x.`_p x.`_p^' by exact: commuteX2. + have ?: commute x.`_p x.`_p^' by apply: commuteX2. rewrite dprodE ?coprime_TIg -?cycleM ?consttC //. - by rewrite cent_cycle cycle_subG; exact/cent1P. + by rewrite cent_cycle cycle_subG; apply/cent1P. rewrite -(dprod_card (Ohm_dprod n def_x)) -(dprod_card (Mho_dprod n def_x)). rewrite mulnCA -mulnA mulnCA mulnA. rewrite !{}IHm ?(dprod_card def_x) ?(leq_trans _ lexm) {m lexm}//. @@ -1801,7 +1800,7 @@ case p_x: (p_group <[x]>); last first. rewrite p_part -(expn0 p) ltn_exp2l 1?lognE ?prime_gt1 ?pdiv_prime //. by rewrite order_gt0 pdiv_dvd. rewrite proper_card // properEneq cycle_subG mem_cycle andbT. - by apply: contra (negbT p'x); move/eqP <-; exact: p_elt_constt. + by apply: contra (negbT p'x); move/eqP <-; apply: p_elt_constt. case/p_groupP: p_x => p p_pr p_x. rewrite (Ohm_p_cycle n p_x) (Mho_p_cycle n p_x) -!orderE. set k := logn p #[x]; have ox: #[x] = (p ^ k)%N by rewrite -card_pgroup. @@ -1865,7 +1864,7 @@ Lemma homocyclic_Ohm_Mho n p G : p.-group G -> homocyclic G -> 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G). Proof. move=> pG /andP[cGG homoG]; set e := exponent G. -have{pG} p_e: p.-nat e by apply: pnat_dvd pG; exact: exponent_dvdn. +have{pG} p_e: p.-nat e by apply: pnat_dvd pG; apply: exponent_dvdn. have{homoG}: all (pred1 e) (abelian_type G). move: homoG; rewrite /abelian_type -(prednK (cardG_gt0 G)) /=. by case: (_ && _) (tag _); rewrite //= genGid eqxx. @@ -1884,7 +1883,7 @@ Lemma Ohm_Mho_homocyclic (n p : nat) G : Proof. set e := exponent G => cGG pG /andP[n_gt0 n_lte] eq_Ohm_Mho. suffices: all (pred1 e) (abelian_type G). - by rewrite /homocyclic cGG; exact: all_pred1_constant. + by rewrite /homocyclic cGG; apply: all_pred1_constant. case/abelian_structure: cGG (abelian_type_gt1 G) => b defG <-. elim: b {-3}G defG (subxx G) eq_Ohm_Mho => //= x b IHb H. rewrite big_cons => defG; case/dprodP: defG (defG) => [[_ K _ defK]]. @@ -2081,7 +2080,7 @@ case: (ltnP e _) (b_sorted p) => [lt_e_x | le_x_e]. move: ordb; rewrite (take_nth 1 ltib) -/x rev_rcons all_rcons /= lt_e_x. case/andP=> _ /=; move/(order_path_min leq_trans); apply: contraLR. rewrite -!has_predC !has_map; case/hasP=> y b_y /= le_y_e; apply/hasP. - by exists y; rewrite ?mem_rev //=; apply: contra le_y_e; exact: leq_trans. + by exists y; rewrite ?mem_rev //=; apply: contra le_y_e; apply: leq_trans. rewrite -(cat_take_drop i b) -map_rev rev_cat !map_cat cat_path. case/andP=> ordb _; rewrite count_cat -{1}(size_takel (ltnW ltib)) ltnNge. rewrite addnC ((count _ _ =P 0) _) ?count_size //. diff --git a/mathcomp/solvable/all.v b/mathcomp/solvable/all_solvable.v index 8c2ea8f..b05a3c4 100644 --- a/mathcomp/solvable/all.v +++ b/mathcomp/solvable/all_solvable.v @@ -3,6 +3,7 @@ Require Export alt. Require Export burnside_app. Require Export center. Require Export commutator. +Require Export cyclic. Require Export extraspecial. Require Export extremal. Require Export finmodule. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index 3ee2526..18a6588 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype tuple finfun bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action. -From mathcomp.algebra -Require Import cyclic. -Require Import pgroup gseries sylow primitive_action. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div fintype tuple. +From mathcomp +Require Import tuple bigop prime finset fingroup morphism perm automorphism. +From mathcomp +Require Import quotient action cyclic pgroup gseries sylow primitive_action. (******************************************************************************) (* Definitions of the symmetric and alternate groups, and some properties. *) @@ -189,10 +186,10 @@ have FF (H : {group {perm T}}): H <| 'Alt_T -> H :<>: 1 -> 20 %| #|H|. - move=> Hh1 Hh3. have [x _]: exists x, x \in T by apply/existsP/eqP; rewrite oT. have F2 := Alt_trans T; rewrite oT /= in F2. - have F3: [transitive 'Alt_T, on setT | 'P] by exact: ntransitive1 F2. - have F4: [primitive 'Alt_T, on setT | 'P] by exact: ntransitive_primitive F2. + have F3: [transitive 'Alt_T, on setT | 'P] by apply: ntransitive1 F2. + have F4: [primitive 'Alt_T, on setT | 'P] by apply: ntransitive_primitive F2. case: (prim_trans_norm F4 Hh1) => F5. - case: Hh3; apply/trivgP; exact: subset_trans F5 (aperm_faithful _). + by case: Hh3; apply/trivgP; apply: subset_trans F5 (aperm_faithful _). have F6: 5 %| #|H| by rewrite -oT -cardsT (atrans_dvd F5). have F7: 4 %| #|H|. have F7: #|[set~ x]| = 4 by rewrite cardsC1 oT. @@ -206,10 +203,10 @@ have FF (H : {group {perm T}}): H <| 'Alt_T -> H :<>: 1 -> 20 %| #|H|. exact: ntransitive1 F9. have F11: [primitive Gx, on [set~ x] | 'P]. exact: ntransitive_primitive F9. - have F12: K \subset Gx by apply: setSI; exact: normal_sub. + have F12: K \subset Gx by apply: setSI; apply: normal_sub. have F13: K <| Gx by rewrite /(K <| _) F12 normsIG // normal_norm. case: (prim_trans_norm F11 F13) => Ksub; last first. - apply: dvdn_trans (cardSg F8); rewrite -F7; exact: atrans_dvd Ksub. + by apply: dvdn_trans (cardSg F8); rewrite -F7; apply: atrans_dvd Ksub. have F14: [faithful Gx, on [set~ x] | 'P]. apply/subsetP=> g; do 2![case/setIP] => Altg cgx cgx'. apply: (subsetP (aperm_faithful 'Alt_T)). @@ -293,7 +290,7 @@ Lemma rfd_funP (p : {perm T}) (u : T') : let p1 := if p x == x then p else 1 in p1 (val u) != x. Proof. case: (p x =P x) => /= [pxx|_]; last by rewrite perm1 (valP u). -by rewrite -{2}pxx (inj_eq (@perm_inj _ p)); exact: (valP u). +by rewrite -{2}pxx (inj_eq (@perm_inj _ p)); apply: (valP u). Qed. Definition rfd_fun p := [fun u => Sub ((_ : {perm T}) _) (rfd_funP p u) : T']. @@ -366,7 +363,7 @@ have Hcp1: #|[set x | p1 x != x]| <= n. by move: Hp; rewrite (cardD1 x1) inE Hx1. have ->: p = p1 * tperm x1 (p x1) by rewrite -mulgA tperm2 mulg1. rewrite odd_permM odd_tperm eq_sym Hx1 morphM; last 2 first. -- by rewrite 2!inE; exact/astab1P. +- by rewrite 2!inE; apply/astab1P. - by rewrite 2!inE; apply/astab1P; rewrite -{1}Hpx /= /aperm -permM. rewrite odd_permM Hrec //=; congr (_ (+) _). pose x2 : T' := Sub x1 nx1x; pose px2 : T' := Sub (p x1) npx1x. @@ -441,7 +438,7 @@ have F11: [primitive Gx, on [set~ x] | 'P]. have F12: K \subset Gx by rewrite setSI // normal_sub. have F13: K <| Gx by apply/andP; rewrite normsIG. have:= prim_trans_norm F11; case/(_ K) => //= => Ksub; last first. - have F14: Gx * H = 'Alt_T by exact/(subgroup_transitiveP _ _ F3). + have F14: Gx * H = 'Alt_T by apply/(subgroup_transitiveP _ _ F3). have: simple Gx. by rewrite (isog_simple (rfd_iso x)) Hrec //= card_sig cardC1 Hde. case/simpleP=> _ simGx; case/simGx: F13 => /= HH2. @@ -470,7 +467,7 @@ have Hreg g z: g \in H -> g z = z -> g = 1. by rewrite memJ_norm ?(subsetP nH). clear K F8 F12 F13 Ksub F14. have Hcard: 5 < #|H|. - apply: (leq_trans oT); apply dvdn_leq; first by exact: cardG_gt0. + apply: (leq_trans oT); apply dvdn_leq; first by apply: cardG_gt0. by rewrite -cardsT (atrans_dvd F5). case Eh: (pred0b [predD1 H & 1]). by move: Hcard; rewrite /pred0b in Eh; rewrite (cardD1 1) group1 (eqP Eh). @@ -491,7 +488,7 @@ case diff_gx_hx: (g x == h x). by rewrite permM -(eqP diff_gx_hx) -permM mulgV perm1. case diff_hgx_x: ((h * g) x == x). case/negP: diff_h1_g; apply/eqP; apply: (mulgI h); rewrite !gsimp. - by apply: (Hreg _ x); [exact: groupM | apply/eqP]. + by apply: (Hreg _ x); [apply: groupM | apply/eqP]. case diff_hgx_hx: ((h * g) x == h x). case/negP: diff_1_g; apply/eqP. by apply: (Hreg _ (h x)) => //; apply/eqP; rewrite -permM. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 635fd84..e8fe7dc 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype tuple finfun bigop finset. -From mathcomp.fingroup -Require Import fingroup action perm. -Require Import primitive_action. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import tuple finfun bigop finset fingroup action perm primitive_action. (* Application of the Burside formula to count the number of distinct *) (* colorings of the vertices of a square and a cube. *) @@ -120,7 +117,7 @@ Qed. Lemma rot_r1 : forall r, is_rot r -> r = r1 ^+ (r c0). Proof. move=> r hr;apply: rot_eq_c0 => //;apply/eqP. - by symmetry; exact: commuteX. + by symmetry; apply: commuteX. by case: (r c0); do 4?case => //=; rewrite ?permM !permE /=. Qed. @@ -304,12 +301,12 @@ Definition square_coloring_number4 := #|orbit to rotations @: setT|. Definition square_coloring_number8 := #|orbit to isometries @: setT|. Lemma Fid : 'Fix_to(1) = setT. -Proof. apply/setP=> x /=; rewrite in_setT; apply/afix1P; exact: act1. Qed. +Proof. by apply/setP=> x /=; rewrite in_setT; apply/afix1P; apply: act1. Qed. Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N. Proof. rewrite -[4]card_ord -[n]card_ord -card_ffun_on Fid cardsE. -by symmetry; apply: eq_card => f; exact/ffun_onP. +by symmetry; apply: eq_card => f; apply/ffun_onP. Qed. Definition coin0 (sc : col_squares) : colors := sc c0. @@ -691,7 +688,7 @@ Qed. Definition sop (p : {perm cube}) : seq cube := val (val (val p)). Lemma sop_inj : injective sop. -Proof. do 2!apply: (inj_comp val_inj); exact: val_inj. Qed. +Proof. by do 2!apply: (inj_comp val_inj); apply: val_inj. Qed. Definition prod_tuple (t1 t2 : seq cube) := map (fun n : 'I_6 => nth F0 t2 n) t1. @@ -728,7 +725,7 @@ Definition seq_iso_L := [:: Lemma seqs1 : forall f injf, sop (@perm _ f injf) = map f ecubes. Proof. move=> f ?; rewrite ecubes_def /sop /= -codom_ffun pvalE. -apply: eq_codom; exact: permE. +by apply: eq_codom; apply: permE. Qed. Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23; @@ -741,7 +738,7 @@ Proof. by move=> p; rewrite /= !inE /= -!(eq_sym p). Qed. Lemma L_iso : forall p, (p \in dir_iso3) = (sop p \in seq_iso_L). Proof. -move=> p; rewrite (eqP Lcorrect) mem_map ?iso0_1 //; exact: sop_inj. +by move=> p; rewrite (eqP Lcorrect) mem_map ?iso0_1 //; apply: sop_inj. Qed. Lemma stable : forall x y, @@ -831,7 +828,7 @@ Canonical iso_group3 := Group group_set_iso3. Lemma group_set_diso3 : group_set dir_iso3. Proof. apply/group_setP;split;first by rewrite inE eqxx /=. -by exact:stable. +by apply:stable. Qed. Canonical diso_group3 := Group group_set_diso3. @@ -862,8 +859,8 @@ have -> : s3 = r05 * r14 * r05 by iso_tac. have -> : s4 = r05 * r14 * r14 * r14 * r05 by iso_tac. have -> : s5 = r14 * r05 * r05 by iso_tac. have -> : s6 = r05 * r05 * r14 by iso_tac. -do ?case/predU1P=> [<-|]; first exact: group1; last (move/eqP => <-); - by rewrite ?groupMl ?mem_gen // !inE eqxx ?orbT. +by do ?case/predU1P=> [<-|]; first exact: group1; last (move/eqP => <-); + rewrite ?groupMl ?mem_gen // !inE eqxx ?orbT. Qed. Notation col_cubes := {ffun cube -> colors}. @@ -887,7 +884,7 @@ Proof. by apply/setP=> x /=; rewrite (sameP afix1P eqP) !inE act1 eqxx. Qed. Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N. Proof. rewrite -[6]card_ord -[n]card_ord -card_ffun_on Fid3 cardsT. -by symmetry; apply: eq_card => ff; exact/ffun_onP. +by symmetry; apply: eq_card => ff; apply/ffun_onP. Qed. Definition col0 (sc : col_cubes) : colors := sc F0. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 6226861..c0c0451 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div fintype bigop finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import cyclic. -Require Import gfunctor. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop. +From mathcomp +Require Import finset fingroup morphism perm automorphism quotient action. +From mathcomp +Require Import gproduct gfunctor cyclic. (******************************************************************************) (* Definition of the center of a group and of external central products: *) @@ -63,7 +60,7 @@ Notation "''Z' ( A )" := (center A) : group_scope. Notation "''Z' ( H )" := (center_group H) : Group_scope. Lemma morphim_center : GFunctor.pcontinuous center. -Proof. move=> gT rT G D f; exact: morphim_subcent. Qed. +Proof. by move=> gT rT G D f; apply: morphim_subcent. Qed. Canonical center_igFun := [igFun by fun _ _ => subsetIl _ _ & morphim_center]. Canonical center_gFun := [gFun by morphim_center]. @@ -103,8 +100,8 @@ Proof. exact: subcentP. Qed. Lemma center_sub A : 'Z(A) \subset A. Proof. exact: subsetIl. Qed. -Lemma center1 : 'Z(1) = [1 gT]. -Proof. by apply/eqP; rewrite eqEsubset center_sub sub1G. Qed. +Lemma center1 : 'Z(1) = 1 :> {set gT}. +Proof. exact: gF1. Qed. Lemma centerC A : {in A, centralised 'Z(A)}. Proof. by apply/centsP; rewrite centsC subsetIr. Qed. @@ -137,13 +134,13 @@ by apply: (iffP cent1P) => [|[]]. Qed. Lemma subcent1_id x G : x \in G -> x \in 'C_G[x]. -Proof. move=> Gx; rewrite inE Gx; exact/cent1P. Qed. +Proof. by move=> Gx; rewrite inE Gx; apply/cent1P. Qed. Lemma subcent1_sub x G : 'C_G[x] \subset G. Proof. exact: subsetIl. Qed. Lemma subcent1C x y G : x \in G -> y \in 'C_G[x] -> x \in 'C_G[y]. -Proof. by move=> Gx /subcent1P[_ cxy]; exact/subcent1P. Qed. +Proof. by move=> Gx /subcent1P[_ cxy]; apply/subcent1P. Qed. Lemma subcent1_cycle_sub x G : x \in G -> <[x]> \subset 'C_G[x]. Proof. by move=> Gx; rewrite cycle_subG ?subcent1_id. Qed. @@ -171,9 +168,9 @@ Lemma cyclic_factor_abelian H G : H \subset 'Z(G) -> cyclic (G / H) -> abelian G. Proof. move=> sHZ cycGH; apply: cyclic_center_factor_abelian. -have nG: G \subset 'N(_) := normal_norm (sub_center_normal _). -have [f <-]:= homgP (homg_quotientS (nG _ sHZ) (nG _ (subxx _)) sHZ). -exact: morphim_cyclic. +have /andP[_ nHG]: H <| G := sub_center_normal sHZ. +have [f <-]:= homgP (homg_quotientS nHG (gFnorm _ G) sHZ). +exact: morphim_cyclic cycGH. Qed. Section Injm. @@ -293,7 +290,7 @@ Let kerHK := ker_cprod_by isoZ. Let injgz : 'injm gz. Proof. by case/isomP: isoZ. Qed. Let gzZ : gz @* 'Z(H) = 'Z(K). Proof. by case/isomP: isoZ. Qed. -Let gzZchar : gz @* 'Z(H) \char 'Z(K). Proof. by rewrite gzZ char_refl. Qed. +Let gzZchar : gz @* 'Z(H) \char 'Z(K). Proof. by rewrite gzZ. Qed. Let sgzZZ : gz @* 'Z(H) \subset 'Z(K) := char_sub gzZchar. Let sZH := center_sub H. Let sZK := center_sub K. @@ -557,7 +554,7 @@ by split=> //; apply/isomP; rewrite ker_f' injm_invm im_f' -fC im_invm. Qed. Lemma isog_cprod_by : G \isog C. -Proof. by have [f [isoG _ _]] := cprod_by_uniq; exact: isom_isog isoG. Qed. +Proof. by have [f [isoG _ _]] := cprod_by_uniq; apply: isom_isog isoG. Qed. End Isomorphism. @@ -651,7 +648,7 @@ Lemma Aut_ncprod_full n : Proof. move=> AutZinG; elim: n => [|n IHn]. by rewrite center_ncprod0; apply/Aut_sub_fullP=> // g injg gG0; exists g. -by case: ncprodS => gz isoZ; exact: Aut_cprod_by_full. +by case: ncprodS => gz isoZ; apply: Aut_cprod_by_full. Qed. End IterCprod. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 6f6a2b5..7a42a9a 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat. -From mathcomp.discrete -Require Import fintype bigop finset prime binomial. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient. -Require Import gfunctor. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat fintype bigop finset. +From mathcomp +Require Import binomial fingroup morphism automorphism quotient gfunctor. (******************************************************************************) (* This files contains the proofs of several key properties of commutators, *) @@ -17,8 +14,8 @@ Require Import gfunctor. (* G^`(0) == G *) (* G^`(n.+1) == [~: G^`(n), G^`(n)] *) (* as several classical results involve the (first) derived group G^`(1), *) -(* such as the equivalence H <| G /\ G / H abelian <-> G^`(1) \subset H. The *) -(* connection between the derived series and solvable groups will only be *) +(* such as the equivalence H <| G /\ G / H abelian <-> G^`(1) \subset H. *) +(* The connection between the derived series and solvable groups will only be *) (* established in nilpotent.v, however. *) (******************************************************************************) @@ -49,7 +46,7 @@ Lemma derg1 A : A^`(1) = [~: A, A]. Proof. by []. Qed. Lemma dergSn n A : A^`(n.+1) = [~: A^`(n), A^`(n)]. Proof. by []. Qed. Lemma der_group_set G n : group_set G^`(n). -Proof. by case: n => [|n]; exact: groupP. Qed. +Proof. by case: n => [|n]; apply: groupP. Qed. Canonical derived_at_group G n := Group (der_group_set G n). @@ -130,7 +127,7 @@ Variables (i j : nat) (x y : gT). Hypotheses (cxz : commute x [~ x, y]) (cyz : commute y [~ x, y]). Lemma commXXg : [~ x ^+ i, y ^+ j] = [~ x, y] ^+ (i * j). -Proof. rewrite expgM commgX commXg //; exact: commuteX. Qed. +Proof. by rewrite expgM commgX commXg //; apply: commuteX. Qed. Lemma expMg_Rmul : (y * x) ^+ i = y ^+ i * x ^+ i * [~ x, y] ^+ 'C(i, 2). Proof. @@ -176,10 +173,10 @@ Lemma commg_normal G H : [~: G, H] <| G <*> H. Proof. by rewrite /(_ <| _) commg_sub commg_norm. Qed. Lemma normsRl A G B : A \subset G -> A \subset 'N([~: G, B]). -Proof. by move=> sAG; exact: subset_trans (commg_norml G B). Qed. +Proof. by move=> sAG; apply: subset_trans (commg_norml G B). Qed. Lemma normsRr A G B : A \subset G -> A \subset 'N([~: B, G]). -Proof. by move=> sAG; exact: subset_trans (commg_normr G B). Qed. +Proof. by move=> sAG; apply: subset_trans (commg_normr G B). Qed. Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)). Proof. @@ -225,7 +222,7 @@ Lemma sub_der1_normal G H : G^`(1) \subset H -> H \subset G -> H <| G. Proof. by move=> sG'H sHG; rewrite /(H <| G) sHG sub_der1_norm. Qed. Lemma sub_der1_abelian G H : G^`(1) \subset H -> abelian (G / H). -Proof. by move=> sG'H; exact: quotient_cents2r. Qed. +Proof. by move=> sG'H; apply: quotient_cents2r. Qed. Lemma der1_min G H : G \subset 'N(H) -> abelian (G / H) -> G^`(1) \subset H. Proof. by move=> nHG abGH; rewrite -quotient_cents2. Qed. @@ -341,7 +338,7 @@ by rewrite !dergSn -IHn morphimR ?(subset_trans (der_sub n G)). Qed. Lemma dergS n G H : G \subset H -> G^`(n) \subset H^`(n). -Proof. by move=> sGH; elim: n => // n IHn; exact: commgSS. Qed. +Proof. by move=> sGH; elim: n => // n IHn; apply: commgSS. Qed. Lemma quotient_der n G H : G \subset 'N(H) -> G^`(n) / H = (G / H)^`(n). Proof. exact: morphim_der. Qed. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v new file mode 100644 index 0000000..be77dd9 --- /dev/null +++ b/mathcomp/solvable/cyclic.v @@ -0,0 +1,869 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import mathcomp.ssreflect.ssreflect. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop. +From mathcomp +Require Import prime finset fingroup morphism perm automorphism quotient. +From mathcomp +Require Import gproduct ssralg finalg zmodp poly. + +(******************************************************************************) +(* Properties of cyclic groups. *) +(* Definitions: *) +(* Defined in fingroup.v: *) +(* <[x]> == the cycle (cyclic group) generated by x. *) +(* #[x] == the order of x, i.e., the cardinal of <[x]>. *) +(* Defined in prime.v: *) +(* totient n == Euler's totient function *) +(* Definitions in this file: *) +(* cyclic G <=> G is a cyclic group. *) +(* metacyclic G <=> G is a metacyclic group (i.e., a cyclic extension of a *) +(* cyclic group). *) +(* generator G x <=> x is a generator of the (cyclic) group G. *) +(* Zpm x == the isomorphism mapping the additive group of integers *) +(* mod #[x] to the cyclic group <[x]>. *) +(* cyclem x n == the endomorphism y |-> y ^+ n of <[x]>. *) +(* Zp_unitm x == the isomorphism mapping the multiplicative group of the *) +(* units of the ring of integers mod #[x] to the group of *) +(* automorphisms of <[x]> (i.e., Aut <[x]>). *) +(* Zp_unitm x maps u to cyclem x u. *) +(* eltm dvd_y_x == the smallest morphism (with domain <[x]>) mapping x to *) +(* y, given a proof dvd_y_x : #[y] %| #[x]. *) +(* expg_invn G k == if coprime #|G| k, the inverse of exponent k in G. *) +(* Basic results for these notions, plus the classical result that any finite *) +(* group isomorphic to a subgroup of a field is cyclic, hence that Aut G is *) +(* cyclic when G is of prime order. *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import GroupScope GRing.Theory. + +(***********************************************************************) +(* Cyclic groups. *) +(***********************************************************************) + +Section Cyclic. + +Variable gT : finGroupType. +Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}). + +Definition cyclic A := [exists x, A == <[x]>]. + +Lemma cyclicP A : reflect (exists x, A = <[x]>) (cyclic A). +Proof. exact: exists_eqP. Qed. + +Lemma cycle_cyclic x : cyclic <[x]>. +Proof. by apply/cyclicP; exists x. Qed. + +Lemma cyclic1 : cyclic [1 gT]. +Proof. by rewrite -cycle1 cycle_cyclic. Qed. + +(***********************************************************************) +(* Isomorphism with the additive group *) +(***********************************************************************) + +Section Zpm. + +Variable a : gT. + +Definition Zpm (i : 'Z_#[a]) := a ^+ i. + +Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}. +Proof. +rewrite /Zpm; case: (eqVneq a 1) => [-> | nta] i j _ _. + by rewrite !expg1n ?mulg1. +by rewrite /= {3}Zp_cast ?order_gt1 // expg_mod_order expgD. +Qed. + +Canonical Zpm_morphism := Morphism ZpmM. + +Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>. +Proof. +apply/eqP; rewrite eq_sym eqEcard cycle_subG /= andbC morphimEdom. +rewrite (leq_trans (leq_imset_card _ _)) ?card_Zp //= /Zp order_gt1. +case: eqP => /= [a1 | _]; first by rewrite imset_set1 morph1 a1 set11. +by apply/imsetP; exists 1%R; rewrite ?expg1 ?inE. +Qed. + +Lemma injm_Zpm : 'injm Zpm. +Proof. +apply/injmP/dinjectiveP/card_uniqP. +rewrite size_map -cardE card_Zp //= {7}/order -im_Zpm morphimEdom /=. +by apply: eq_card => x; apply/imageP/imsetP=> [] [i Zp_i ->]; exists i. +Qed. + +Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]). +Proof. +have [->|] := eqVneq a 1; first by rewrite order1 !modn1 !expg1n eqxx. +rewrite -order_gt1 => lt1a; have ZpT: Zp #[a] = setT by rewrite /Zp lt1a. +have: injective Zpm by move=> i j; apply (injmP injm_Zpm); rewrite /= ZpT inE. +move/inj_eq=> eqZ; symmetry; rewrite -(Zp_cast lt1a). +by rewrite -[_ == _](eqZ (inZp m) (inZp n)) /Zpm /= Zp_cast ?expg_mod_order. +Qed. + +Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm. +Proof. by apply/isomP; rewrite injm_Zpm im_Zpm. Qed. + +Lemma Zp_isog : isog (Zp #[a]) <[a]>. +Proof. exact: isom_isog Zp_isom. Qed. + +End Zpm. + +(***********************************************************************) +(* Central and direct product of cycles *) +(***********************************************************************) + +Lemma cyclic_abelian A : cyclic A -> abelian A. +Proof. by case/cyclicP=> a ->; apply: cycle_abelian. Qed. + +Lemma cycleMsub a b : + commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>. +Proof. +move=> cab co_ab; apply/subsetP=> _ /cycleP[k ->]. +apply/cycleP; exists (chinese #[a] #[b] k 0); symmetry. +rewrite expgMn // -expg_mod_order chinese_modl // expg_mod_order. +by rewrite /chinese addn0 -mulnA mulnCA expgM expg_order expg1n mulg1. +Qed. + +Lemma cycleM a b : + commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>. +Proof. +move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)). +rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //. +by rewrite -genM_join cycle_subG mem_gen // mem_imset2 ?cycle_id. +Qed. + +Lemma cyclicM A B : + cyclic A -> cyclic B -> B \subset 'C(A) -> coprime #|A| #|B| -> + cyclic (A * B). +Proof. +move=> /cyclicP[a ->] /cyclicP[b ->]; rewrite cent_cycle cycle_subG => cab coab. +by rewrite -cycleM ?cycle_cyclic //; apply/esym/cent1P. +Qed. + +Lemma cyclicY K H : + cyclic K -> cyclic H -> H \subset 'C(K) -> coprime #|K| #|H| -> + cyclic (K <*> H). +Proof. by move=> cycK cycH cKH coKH; rewrite cent_joinEr // cyclicM. Qed. + +(***********************************************************************) +(* Order properties *) +(***********************************************************************) + +Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1). +Proof. by rewrite (eq_expg_mod_order a n 0) mod0n. Qed. + +Lemma order_inf a n : a ^+ n.+1 == 1 -> #[a] <= n.+1. +Proof. by rewrite -order_dvdn; apply: dvdn_leq. Qed. + +Lemma order_dvdG G a : a \in G -> #[a] %| #|G|. +Proof. by move=> Ga; apply: cardSg; rewrite cycle_subG. Qed. + +Lemma expg_cardG G a : a \in G -> a ^+ #|G| = 1. +Proof. by move=> Ga; apply/eqP; rewrite -order_dvdn order_dvdG. Qed. + +Lemma expg_znat G x k : x \in G -> x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k. +Proof. +case: (eqsVneq G 1) => [-> /set1P-> | ntG Gx]; first by rewrite !expg1n. +apply/eqP; rewrite val_Zp_nat ?cardG_gt1 // eq_expg_mod_order. +by rewrite modn_dvdm ?order_dvdG. +Qed. + +Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G -> x ^+ (- k)%R = x ^- k. +Proof. +move=> Gx; apply/eqP; rewrite eq_sym eq_invg_mul -expgD. +by rewrite -(expg_znat _ Gx) natrD natr_Zp natr_negZp subrr. +Qed. + +Lemma nt_gen_prime G x : prime #|G| -> x \in G^# -> G :=: <[x]>. +Proof. +move=> Gpr /setD1P[]; rewrite -cycle_subG -cycle_eq1 => ntX sXG. +apply/eqP; rewrite eqEsubset sXG andbT. +by apply: contraR ntX => /(prime_TIg Gpr); rewrite (setIidPr sXG) => ->. +Qed. + +Lemma nt_prime_order p x : prime p -> x ^+ p = 1 -> x != 1 -> #[x] = p. +Proof. +move=> p_pr xp ntx; apply/prime_nt_dvdP; rewrite ?order_eq1 //. +by rewrite order_dvdn xp. +Qed. + +Lemma orderXdvd a n : #[a ^+ n] %| #[a]. +Proof. by apply: order_dvdG; apply: mem_cycle. Qed. + +Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n. +Proof. +apply/eqP; rewrite eqn_dvd; apply/andP; split. + rewrite order_dvdn -expgM -muln_divCA_gcd //. + by rewrite expgM expg_order expg1n. +have [-> | n_gt0] := posnP n; first by rewrite gcdn0 divnn order_gt0 dvd1n. +rewrite -(dvdn_pmul2r n_gt0) divn_mulAC ?dvdn_gcdl // dvdn_lcm. +by rewrite order_dvdn mulnC expgM expg_order eqxx dvdn_mulr. +Qed. + +Lemma orderXdiv a n : n %| #[a] -> #[a ^+ n] = #[a] %/ n. +Proof. by case/dvdnP=> q defq; rewrite orderXgcd {2}defq gcdnC gcdnMl. Qed. + +Lemma orderXexp p m n x : #[x] = (p ^ n)%N -> #[x ^+ (p ^ m)] = (p ^ (n - m))%N. +Proof. +move=> ox; have [n_le_m | m_lt_n] := leqP n m. + rewrite -(subnKC n_le_m) subnDA subnn expnD expgM -ox. + by rewrite expg_order expg1n order1. +rewrite orderXdiv ox ?dvdn_exp2l ?expnB ?(ltnW m_lt_n) //. +by have:= order_gt0 x; rewrite ox expn_gt0 orbC -(ltn_predK m_lt_n). +Qed. + +Lemma orderXpfactor p k n x : + #[x ^+ (p ^ k)] = n -> prime p -> p %| n -> #[x] = (p ^ k * n)%N. +Proof. +move=> oxp p_pr dv_p_n. +suffices pk_x: p ^ k %| #[x] by rewrite -oxp orderXdiv // mulnC divnK. +rewrite pfactor_dvdn // leqNgt; apply: contraL dv_p_n => lt_x_k. +rewrite -oxp -p'natE // -(subnKC (ltnW lt_x_k)) expnD expgM. +rewrite (pnat_dvd (orderXdvd _ _)) // -p_part // orderXdiv ?dvdn_part //. +by rewrite -{1}[#[x]](partnC p) // mulKn // part_pnat. +Qed. + +Lemma orderXprime p n x : + #[x ^+ p] = n -> prime p -> p %| n -> #[x] = (p * n)%N. +Proof. exact: (@orderXpfactor p 1). Qed. + +Lemma orderXpnat m n x : #[x ^+ m] = n -> \pi(n).-nat m -> #[x] = (m * n)%N. +Proof. +move=> oxm n_m; have [m_gt0 _] := andP n_m. +suffices m_x: m %| #[x] by rewrite -oxm orderXdiv // mulnC divnK. +apply/dvdn_partP=> // p; rewrite mem_primes => /and3P[p_pr _ p_m]. +have n_p: p \in \pi(n) by apply: (pnatP _ _ n_m). +have p_oxm: p %| #[x ^+ (p ^ logn p m)]. + apply: dvdn_trans (orderXdvd _ m`_p^'); rewrite -expgM -p_part ?partnC //. + by rewrite oxm; rewrite mem_primes in n_p; case/and3P: n_p. +by rewrite (orderXpfactor (erefl _) p_pr p_oxm) p_part // dvdn_mulr. +Qed. + +Lemma orderM a b : + commute a b -> coprime #[a] #[b] -> #[a * b] = (#[a] * #[b])%N. +Proof. by move=> cab co_ab; rewrite -coprime_cardMg -?cycleM. Qed. + +Definition expg_invn A k := (egcdn k #|A|).1. + +Lemma expgK G k : + coprime #|G| k -> {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}. +Proof. +move=> coGk x /order_dvdG Gx; apply/eqP. +rewrite -expgM (eq_expg_mod_order _ _ 1) -(modn_dvdm 1 Gx). +by rewrite -(chinese_modl coGk 1 0) /chinese mul1n addn0 modn_dvdm. +Qed. + +Lemma cyclic_dprod K H G : + K \x H = G -> cyclic K -> cyclic H -> cyclic G = coprime #|K| #|H| . +Proof. +case/dprodP=> _ defKH cKH tiKH cycK cycH; pose m := lcmn #|K| #|H|. +apply/idP/idP=> [/cyclicP[x defG] | coKH]; last by rewrite -defKH cyclicM. +rewrite /coprime -dvdn1 -(@dvdn_pmul2l m) ?lcmn_gt0 ?cardG_gt0 //. +rewrite muln_lcm_gcd muln1 -TI_cardMg // defKH defG order_dvdn. +have /mulsgP[y z Ky Hz ->]: x \in K * H by rewrite defKH defG cycle_id. +rewrite -[1]mulg1 expgMn; last exact/commute_sym/(centsP cKH). +apply/eqP; congr (_ * _); apply/eqP; rewrite -order_dvdn. + exact: dvdn_trans (order_dvdG Ky) (dvdn_lcml _ _). +exact: dvdn_trans (order_dvdG Hz) (dvdn_lcmr _ _). +Qed. + +(***********************************************************************) +(* Generator *) +(***********************************************************************) + +Definition generator (A : {set gT}) a := A == <[a]>. + +Lemma generator_cycle a : generator <[a]> a. +Proof. exact: eqxx. Qed. + +Lemma cycle_generator a x : generator <[a]> x -> x \in <[a]>. +Proof. by move/(<[a]> =P _)->; apply: cycle_id. Qed. + +Lemma generator_order a b : generator <[a]> b -> #[a] = #[b]. +Proof. by rewrite /order => /(<[a]> =P _)->. Qed. + +End Cyclic. + +Arguments Scope cyclic [_ group_scope]. +Arguments Scope generator [_ group_scope group_scope]. +Arguments Scope expg_invn [_ group_scope nat_scope]. +Implicit Arguments cyclicP [gT A]. +Prenex Implicits cyclic Zpm generator expg_invn. + +(* Euler's theorem *) +Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n = 1 %[mod n]. +Proof. +case: n => [|[|n']] //; [by rewrite !modn1 | set n := n'.+2] => co_a_n. +have{co_a_n} Ua: coprime n (inZp a : 'I_n) by rewrite coprime_sym coprime_modl. +have: FinRing.unit 'Z_n Ua ^+ totient n == 1. + by rewrite -card_units_Zp // -order_dvdn order_dvdG ?inE. +by rewrite -2!val_eqE unit_Zp_expg /= -/n modnXm => /eqP. +Qed. + +Section Eltm. + +Variables (aT rT : finGroupType) (x : aT) (y : rT). + +Definition eltm of #[y] %| #[x] := fun x_i => y ^+ invm (injm_Zpm x) x_i. + +Hypothesis dvd_y_x : #[y] %| #[x]. + +Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i. +Proof. +apply/eqP; rewrite eq_expg_mod_order. +have [x_le1 | x_gt1] := leqP #[x] 1. + suffices: #[y] %| 1 by rewrite dvdn1 => /eqP->; rewrite !modn1. + by rewrite (dvdn_trans dvd_y_x) // dvdn1 order_eq1 -cycle_eq1 trivg_card_le1. +rewrite -(expg_znat i (cycle_id x)) invmE /=; last by rewrite /Zp x_gt1 inE. +by rewrite val_Zp_nat // modn_dvdm. +Qed. + +Lemma eltm_id : eltm dvd_y_x x = y. Proof. exact: (eltmE 1). Qed. + +Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i * x_j}}. +Proof. +move=> _ _ /cycleP[i ->] /cycleP[j ->]. +by apply/eqP; rewrite -expgD !eltmE expgD. +Qed. +Canonical eltm_morphism := Morphism eltmM. + +Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>. +Proof. by rewrite morphim_cycle ?cycle_id //= eltm_id. Qed. + +Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>. +Proof. +apply/eqP; rewrite eq_sym eqEcard cycle_subG 3!inE mem_cycle /= eltmE. +rewrite expg_order eqxx (orderE y) -im_eltm card_morphim setIid -orderE. +by rewrite orderXdiv ?dvdn_indexg //= leq_divRL ?indexg_gt0 ?Lagrange ?subsetIl. +Qed. + +Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]). +Proof. by rewrite ker_eltm subG1 cycle_eq1 -order_dvdn. Qed. + +End Eltm. + +Section CycleSubGroup. + +Variable gT : finGroupType. + +(* Gorenstein, 1.3.1 (i) *) +Lemma cycle_sub_group (a : gT) m : + m %| #[a] -> + [set H : {group gT} | H \subset <[a]> & #|H| == m] + = [set <[a ^+ (#[a] %/ m)]>%G]. +Proof. +move=> m_dv_a; have m_gt0: 0 < m by apply: dvdn_gt0 m_dv_a. +have oam: #|<[a ^+ (#[a] %/ m)]>| = m. + apply/eqP; rewrite [#|_|]orderXgcd -(divnMr m_gt0) muln_gcdl divnK //. + by rewrite gcdnC gcdnMr mulKn. +apply/eqP; rewrite eqEsubset sub1set inE /= cycleX oam eqxx !andbT. +apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard oam. +case/andP=> sXa /eqP oX; rewrite oX leqnn andbT. +apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x. +have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set. +rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](Lagrange sXa) -oX mulnC. +rewrite dvdn_pmul2r // mulnK // => /dvdnP[i ->]. +by rewrite mulnC expgM groupX // cycle_id. +Qed. + +Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> -> H \char <[a]>. +Proof. +move=> sHa; apply: lone_subgroup_char => // J sJa isoJH. +have dvHa: #|H| %| #[a] by apply: cardSg. +have{dvHa} /setP Huniq := esym (cycle_sub_group dvHa). +move: (Huniq H) (Huniq J); rewrite !inE /=. +by rewrite sHa sJa (card_isog isoJH) eqxx => /eqP<- /eqP<-. +Qed. + +End CycleSubGroup. + +(***********************************************************************) +(* Reflected boolean property and morphic image, injection, bijection *) +(***********************************************************************) + +Section MorphicImage. + +Variables aT rT : finGroupType. +Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT). +Hypothesis Dx : x \in D. + +Lemma morph_order : #[f x] %| #[x]. +Proof. by rewrite order_dvdn -morphX // expg_order morph1. Qed. + +Lemma morph_generator A : generator A x -> generator (f @* A) (f x). +Proof. by move/(A =P _)->; rewrite /generator morphim_cycle. Qed. + +End MorphicImage. + +Section CyclicProps. + +Variables gT : finGroupType. +Implicit Types (aT rT : finGroupType) (G H K : {group gT}). + +Lemma cyclicS G H : H \subset G -> cyclic G -> cyclic H. +Proof. +move=> sHG /cyclicP[x defG]; apply/cyclicP. +exists (x ^+ (#[x] %/ #|H|)); apply/congr_group/set1P. +by rewrite -cycle_sub_group /order -defG ?cardSg // inE sHG eqxx. +Qed. + +Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G. +Proof. +apply/cyclicP/cyclicP=> [[y /(canRL (conjsgK x))] | [y ->]]. + by rewrite -cycleJ; exists (y ^ x^-1). +by exists (y ^ x); rewrite cycleJ. +Qed. + +Lemma eq_subG_cyclic G H K : + cyclic G -> H \subset G -> K \subset G -> (H :==: K) = (#|H| == #|K|). +Proof. +case/cyclicP=> x -> sHx sKx; apply/eqP/eqP=> [-> //| eqHK]. +have def_GHx := cycle_sub_group (cardSg sHx); set GHx := [set _] in def_GHx. +have []: H \in GHx /\ K \in GHx by rewrite -def_GHx !inE sHx sKx eqHK /=. +by do 2!move/set1P->. +Qed. + +Lemma cardSg_cyclic G H K : + cyclic G -> H \subset G -> K \subset G -> (#|H| %| #|K|) = (H \subset K). +Proof. +move=> cycG sHG sKG; apply/idP/idP; last exact: cardSg. +case/cyclicP: (cyclicS sKG cycG) => x defK; rewrite {K}defK in sKG *. +case/dvdnP=> k ox; suffices ->: H :=: <[x ^+ k]> by apply: cycleX. +apply/eqP; rewrite (eq_subG_cyclic cycG) ?(subset_trans (cycleX _ _)) //. +rewrite -orderE orderXdiv orderE ox ?dvdn_mulr ?mulKn //. +by have:= order_gt0 x; rewrite orderE ox; case k. +Qed. + +Lemma sub_cyclic_char G H : cyclic G -> (H \char G) = (H \subset G). +Proof. +case/cyclicP=> x ->; apply/idP/idP => [/andP[] //|]. +exact: cycle_subgroup_char. +Qed. + +Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) : + cyclic H -> cyclic (f @* H). +Proof. +move=> cycH; wlog sHG: H cycH / H \subset G. + by rewrite -morphimIdom; apply; rewrite (cyclicS _ cycH, subsetIl) ?subsetIr. +case/cyclicP: cycH sHG => x ->; rewrite gen_subG sub1set => Gx. +by apply/cyclicP; exists (f x); rewrite morphim_cycle. +Qed. + +Lemma quotient_cycle x H : x \in 'N(H) -> <[x]> / H = <[coset H x]>. +Proof. exact: morphim_cycle. Qed. + +Lemma quotient_cyclic G H : cyclic G -> cyclic (G / H). +Proof. exact: morphim_cyclic. Qed. + +Lemma quotient_generator x G H : + x \in 'N(H) -> generator G x -> generator (G / H) (coset H x). +Proof. by move=> Nx; apply: morph_generator. Qed. + +Lemma prime_cyclic G : prime #|G| -> cyclic G. +Proof. +case/primeP; rewrite ltnNge -trivg_card_le1. +case/trivgPn=> x Gx ntx /(_ _ (order_dvdG Gx)). +rewrite order_eq1 (negbTE ntx) => /eqnP oxG; apply/cyclicP. +by exists x; apply/eqP; rewrite eq_sym eqEcard -oxG cycle_subG Gx leqnn. +Qed. + +Lemma dvdn_prime_cyclic G p : prime p -> #|G| %| p -> cyclic G. +Proof. +move=> p_pr pG; case: (eqsVneq G 1) => [-> | ntG]; first exact: cyclic1. +by rewrite prime_cyclic // (prime_nt_dvdP p_pr _ pG) -?trivg_card1. +Qed. + +Lemma cyclic_small G : #|G| <= 3 -> cyclic G. +Proof. +rewrite 4!(ltnS, leq_eqVlt) -trivg_card_le1 orbA orbC. +case/predU1P=> [-> | oG]; first exact: cyclic1. +by apply: prime_cyclic; case/pred2P: oG => ->. +Qed. + +End CyclicProps. + +Section IsoCyclic. + +Variables gT rT : finGroupType. +Implicit Types (G H : {group gT}) (M : {group rT}). + +Lemma injm_cyclic G H (f : {morphism G >-> rT}) : + 'injm f -> H \subset G -> cyclic (f @* H) = cyclic H. +Proof. +move=> injf sHG; apply/idP/idP; last exact: morphim_cyclic. +by rewrite -{2}(morphim_invm injf sHG); apply: morphim_cyclic. +Qed. + +Lemma isog_cyclic G M : G \isog M -> cyclic G = cyclic M. +Proof. by case/isogP=> f injf <-; rewrite injm_cyclic. Qed. + +Lemma isog_cyclic_card G M : cyclic G -> isog G M = cyclic M && (#|M| == #|G|). +Proof. +move=> cycG; apply/idP/idP=> [isoGM | ]. + by rewrite (card_isog isoGM) -(isog_cyclic isoGM) cycG /=. +case/cyclicP: cycG => x ->{G} /andP[/cyclicP[y ->] /eqP oy]. +by apply: isog_trans (isog_symr _) (Zp_isog y); rewrite /order oy Zp_isog. +Qed. + +Lemma injm_generator G H (f : {morphism G >-> rT}) x : + 'injm f -> x \in G -> H \subset G -> + generator (f @* H) (f x) = generator H x. +Proof. +move=> injf Gx sHG; apply/idP/idP; last exact: morph_generator. +rewrite -{2}(morphim_invm injf sHG) -{2}(invmE injf Gx). +by apply: morph_generator; apply: mem_morphim. +Qed. + +End IsoCyclic. + +(* Metacyclic groups. *) +Section Metacyclic. + +Variable gT : finGroupType. +Implicit Types (A : {set gT}) (G H : {group gT}). + +Definition metacyclic A := + [exists H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]]. + +Lemma metacyclicP A : + reflect (exists H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)]) + (metacyclic A). +Proof. exact: 'exists_and3P. Qed. + +Lemma metacyclic1 : metacyclic 1. +Proof. +by apply/existsP; exists 1%G; rewrite normal1 trivg_quotient !cyclic1. +Qed. + +Lemma cyclic_metacyclic A : cyclic A -> metacyclic A. +Proof. +case/cyclicP=> x ->; apply/existsP; exists (<[x]>)%G. +by rewrite normal_refl cycle_cyclic trivg_quotient cyclic1. +Qed. + +Lemma metacyclicS G H : H \subset G -> metacyclic G -> metacyclic H. +Proof. +move=> sHG /metacyclicP[K [cycK nsKG cycGq]]; apply/metacyclicP. +exists (H :&: K)%G; rewrite (cyclicS (subsetIr H K)) ?(normalGI sHG) //=. +rewrite setIC (isog_cyclic (second_isog _)) ?(cyclicS _ cycGq) ?quotientS //. +by rewrite (subset_trans sHG) ?normal_norm. +Qed. + +End Metacyclic. + +Arguments Scope metacyclic [_ group_scope]. +Prenex Implicits metacyclic. +Implicit Arguments metacyclicP [gT A]. + +(* Automorphisms of cyclic groups. *) +Section CyclicAutomorphism. + +Variable gT : finGroupType. + +Section CycleAutomorphism. + +Variable a : gT. + +Section CycleMorphism. + +Variable n : nat. + +Definition cyclem of gT := fun x : gT => x ^+ n. + +Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x * y}}. +Proof. +by move=> x y ax ay; apply: expgMn; apply: (centsP (cycle_abelian a)). +Qed. + +Canonical cyclem_morphism := Morphism cyclemM. + +End CycleMorphism. + +Section ZpUnitMorphism. + +Variable u : {unit 'Z_#[a]}. + +Lemma injm_cyclem : 'injm (cyclem (val u) a). +Proof. +apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. +case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax. +rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. +by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG. +Qed. + +Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>. +Proof. +apply/morphim_fixP=> //; first exact: injm_cyclem. +by rewrite morphim_cycle ?cycle_id ?cycleX. +Qed. + +Definition Zp_unitm := aut injm_cyclem im_cyclem. + +End ZpUnitMorphism. + +Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u * v}}. +Proof. +move=> u v _ _; apply: (eq_Aut (Aut_aut _ _)) => [|x a_x]. + by rewrite groupM ?Aut_aut. +rewrite permM !autE ?groupX //= /cyclem -expgM. +rewrite -expg_mod_order modn_dvdm ?expg_mod_order //. +case: (leqP #[a] 1) => [lea1 | lt1a]; last by rewrite Zp_cast ?order_dvdG. +by rewrite card_le1_trivg // in a_x; rewrite (set1P a_x) order1 dvd1n. +Qed. + +Canonical Zp_unit_morphism := Morphism Zp_unitmM. + +Lemma injm_Zp_unitm : 'injm Zp_unitm. +Proof. +case: (eqVneq a 1) => [a1 | nta]. + by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. +apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. +have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. +rewrite !autE ?cycle_id // eq_expg_mod_order. +by rewrite -[n in _ == _ %[mod n]]Zp_cast ?order_gt1 // !modZp inE. +Qed. + +Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m. +Proof. +rewrite /generator eq_sym eqEcard cycleX -/#[a] [#|_|]orderXgcd /=. +apply/idP/idP=> [le_a_am|co_am]; last by rewrite (eqnP co_am) divn1. +have am_gt0: 0 < gcdn #[a] m by rewrite gcdn_gt0 order_gt0. +by rewrite /coprime eqn_leq am_gt0 andbT -(@leq_pmul2l #[a]) ?muln1 -?leq_divRL. +Qed. + +Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>. +Proof. +rewrite morphimEdom; apply/setP=> f; pose n := invm (injm_Zpm a) (f a). +apply/imsetP/idP=> [[u _ ->] | Af]; first exact: Aut_aut. +have [a1 | nta] := eqVneq a 1. + by rewrite a1 cycle1 Aut1 in Af; exists 1; rewrite // morph1 (set1P Af). +have a_fa: <[a]> = <[f a]>. + by rewrite -(autmE Af) -morphim_cycle ?im_autm ?cycle_id. +have def_n: a ^+ n = f a. + by rewrite -/(Zpm n) invmK // im_Zpm a_fa cycle_id. +have co_a_n: coprime #[a].-2.+2 n. + by rewrite {1}Zp_cast ?order_gt1 // -generator_coprime def_n; apply/eqP. +exists (FinRing.unit 'Z_#[a] co_a_n); rewrite ?inE //. +apply: eq_Aut (Af) (Aut_aut _ _) _ => x ax. +rewrite autE //= /cyclem; case/cycleP: ax => k ->{x}. +by rewrite -(autmE Af) morphX ?cycle_id //= autmE -def_n -!expgM mulnC. +Qed. + +Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm. +Proof. by apply/isomP; rewrite ?injm_Zp_unitm ?im_Zp_unitm. Qed. + +Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>). +Proof. exact: isom_isog Zp_unit_isom. Qed. + +Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a]. +Proof. by rewrite -(card_isog Zp_unit_isog) card_units_Zp. Qed. + +Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|. +Proof. +have [lea1 | lt1a] := leqP #[a] 1. + rewrite /order card_le1_trivg // cards1 (@eq_card1 _ 1) // => x. + by rewrite !inE -cycle_eq1 eq_sym. +rewrite -(card_injm (injm_invm (injm_Zpm a))) /= ?im_Zpm; last first. + by apply/subsetP=> x; rewrite inE; apply: cycle_generator. +rewrite -card_units_Zp // cardsE card_sub morphim_invmE; apply: eq_card => /= d. +by rewrite !inE /= qualifE /= /Zp lt1a inE /= generator_coprime {1}Zp_cast. +Qed. + +Lemma Aut_cycle_abelian : abelian (Aut <[a]>). +Proof. by rewrite -im_Zp_unitm morphim_abelian ?units_Zp_abelian. Qed. + +End CycleAutomorphism. + +Variable G : {group gT}. + +Lemma Aut_cyclic_abelian : cyclic G -> abelian (Aut G). +Proof. by case/cyclicP=> x ->; apply: Aut_cycle_abelian. Qed. + +Lemma card_Aut_cyclic : cyclic G -> #|Aut G| = totient #|G|. +Proof. by case/cyclicP=> x ->; apply: card_Aut_cycle. Qed. + +Lemma sum_ncycle_totient : + \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| * totient d = #|G|. +Proof. +pose h (x : gT) : 'I_#|G|.+1 := inord #[x]. +symmetry; rewrite -{1}sum1_card (partition_big h xpredT) //=. +apply: eq_bigr => d _; set Gd := finset _. +rewrite -sum_nat_const sum1dep_card -sum1_card (_ : finset _ = Gd); last first. + apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx. + by rewrite /eq_op /= inordK // ltnS subset_leq_card ?cycle_subG. +rewrite (partition_big_imset cycle) {}/Gd; apply: eq_bigr => C /=. +case/imsetP=> x /setIdP[Gx /eqP <-] -> {C d}. +rewrite sum1dep_card totient_gen; apply: eq_card => y; rewrite !inE /generator. +move: Gx; rewrite andbC eq_sym -!cycle_subG /order. +by case: eqP => // -> ->; rewrite eqxx. +Qed. + +End CyclicAutomorphism. + +Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n. +Proof. +case: n => [|[|n']]; try by rewrite big_mkcond !big_ord_recl big_ord0. +set n := n'.+2; pose x1 : 'Z_n := 1%R. +have ox1: #[x1] = n by rewrite /order -Zp_cycle card_Zp. +rewrite -[rhs in _ = rhs]ox1 -[#[_]]sum_ncycle_totient [#|_|]ox1 big_mkcond /=. +apply: eq_bigr => d _; rewrite -{2}ox1; case: ifP => [|ndv_dG]; last first. + rewrite eq_card0 // => C; apply/imsetP=> [[x /setIdP[Gx oxd] _{C}]]. + by rewrite -(eqP oxd) order_dvdG in ndv_dG. +move/cycle_sub_group; set Gd := [set _] => def_Gd. +rewrite (_ : _ @: _ = @gval _ @: Gd); first by rewrite imset_set1 cards1 mul1n. +apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]]. + case/imsetP=> x /setIdP[_ oxd] ->; exists <[x]>%G => //. + by rewrite -def_Gd inE -Zp_cycle subsetT. +have:= GdC; rewrite -def_Gd => /setIdP[_ /eqP <-]. +by rewrite (set1P GdC) /= mem_imset // inE eqxx (mem_cycle x1). +Qed. + +Section FieldMulCyclic. + +(***********************************************************************) +(* A classic application to finite multiplicative subgroups of fields. *) +(***********************************************************************) + +Import GRing.Theory. + +Variables (gT : finGroupType) (G : {group gT}). + +Lemma order_inj_cyclic : + {in G &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G. +Proof. +move=> ucG; apply: negbNE (contra _ (negbT (ltnn #|G|))) => ncG. +rewrite -{2}[#|G|]sum_totient_dvd big_mkcond (bigD1 ord_max) ?dvdnn //=. +rewrite -{1}[#|G|]sum_ncycle_totient (bigD1 ord_max) //= -addSn leq_add //. + rewrite eq_card0 ?totient_gt0 ?cardG_gt0 // => C. + apply/imsetP=> [[x /setIdP[Gx /eqP oxG]]]; case/cyclicP: ncG. + by exists x; apply/eqP; rewrite eq_sym eqEcard cycle_subG Gx -oxG /=. +elim/big_ind2: _ => // [m1 n1 m2 n2 | d _]; first exact: leq_add. +set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0. +rewrite {}/Gd => /imsetP[x /setIdP[Gx /eqP <-] _ {C d}]. +rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C. +apply/idP/eqP=> [|-> {C}]; last by rewrite mem_imset // inE Gx eqxx. +by case/imsetP=> y /setIdP[Gy /eqP/ucG->]. +Qed. + +Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT -> R) : + f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> + {in G^#, forall x, f x - 1 \in GRing.unit}%R -> + abelian G -> cyclic G. +Proof. +move=> f1 fM f1P abelG. +have fX n: {in G, {morph f : u / u ^+ n >-> (u ^+ n)%R}}. + by case: n => // n x Gx; elim: n => //= n IHn; rewrite expgS fM ?groupX ?IHn. +have fU x: x \in G -> f x \in GRing.unit. + by move=> Gx; apply/unitrP; exists (f x^-1); rewrite -!fM ?groupV ?gsimp. +apply: order_inj_cyclic => x y Gx Gy; set n := #[x] => yn. +apply/eqP; rewrite eq_sym eqEcard -[#|_|]/n yn leqnn andbT cycle_subG /=. +suff{y Gy yn} ->: <[x]> = G :&: [set z | #[z] %| n] by rewrite !inE Gy yn /=. +apply/eqP; rewrite eqEcard subsetI cycle_subG {}Gx /= cardE; set rs := enum _. +apply/andP; split; first by apply/subsetP=> y xy; rewrite inE order_dvdG. +pose P : {poly R} := ('X^n - 1)%R; have n_gt0: n > 0 by apply: order_gt0. +have szP: size P = n.+1 by rewrite size_addl size_polyXn ?size_opp ?size_poly1. +rewrite -ltnS -szP -(size_map f) max_ring_poly_roots -?size_poly_eq0 ?{}szP //. + apply/allP=> fy /mapP[y]; rewrite mem_enum !inE order_dvdn => /andP[Gy]. + move/eqP=> yn1 ->{fy}; apply/eqP. + by rewrite !(hornerE, hornerXn) -fX // yn1 f1 subrr. +have: uniq rs by apply: enum_uniq. +have: all (mem G) rs by apply/allP=> y; rewrite mem_enum; case/setIP. +elim: rs => //= y rs IHrs /andP[Gy Grs] /andP[y_rs]; rewrite andbC. +move/IHrs=> -> {IHrs}//; apply/allP=> _ /mapP[z rs_z ->]. +have{Grs} Gz := allP Grs z rs_z; rewrite /diff_roots -!fM // (centsP abelG) //. +rewrite eqxx -[f y]mul1r -(mulgKV y z) fM ?groupM ?groupV //=. +rewrite -mulNr -mulrDl unitrMl ?fU ?f1P // !inE. +by rewrite groupM ?groupV // andbT -eq_mulgV1; apply: contra y_rs; move/eqP <-. +Qed. + +Lemma field_mul_group_cyclic (F : fieldType) (f : gT -> F) : + {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> + {in G, forall x, f x = 1%R <-> x = 1} -> + cyclic G. +Proof. +move=> fM f1P; have f1 : f 1 = 1%R by apply/f1P. +apply: (div_ring_mul_group_cyclic f1 fM) => [x|]. + case/setD1P=> x1 Gx; rewrite unitfE; apply: contra x1. + by rewrite subr_eq0 => /eqP/f1P->. +apply/centsP=> x Gx y Gy; apply/commgP/eqP. +apply/f1P; rewrite ?fM ?groupM ?groupV //. +by rewrite mulrCA -!fM ?groupM ?groupV // mulKg mulVg. +Qed. + +End FieldMulCyclic. + +Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) : + cyclic G. +Proof. +apply: field_mul_group_cyclic FinRing.uval _ _ => // u _. +by split=> /eqP ?; apply/eqP. +Qed. + +Section PrimitiveRoots. + +Open Scope ring_scope. +Import GRing.Theory. + +Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) : + n > 0 -> all n.-unity_root rs -> uniq rs -> size rs >= n -> + has n.-primitive_root rs. +Proof. +move=> n_gt0 rsn1 Urs; rewrite leq_eqVlt ltnNge max_unity_roots // orbF eq_sym. +move/eqP=> sz_rs; pose r := val (_ : seq_sub rs). +have rn1 x: r x ^+ n = 1. + by apply/eqP; rewrite -unity_rootE (allP rsn1) ?(valP x). +have prim_r z: z ^+ n = 1 -> z \in rs. + by move/eqP; rewrite -unity_rootE -(mem_unity_roots n_gt0). +pose r' := SeqSub (prim_r _ _); pose sG_1 := r' _ (expr1n _ _). +have sG_VP: r _ ^+ n.-1 ^+ n = 1. + by move=> x; rewrite -exprM mulnC exprM rn1 expr1n. +have sG_MP: (r _ * r _) ^+ n = 1 by move=> x y; rewrite exprMn !rn1 mul1r. +pose sG_V := r' _ (sG_VP _); pose sG_M := r' _ (sG_MP _ _). +have sG_Ag: associative sG_M by move=> x y z; apply: val_inj; rewrite /= mulrA. +have sG_1g: left_id sG_1 sG_M by move=> x; apply: val_inj; rewrite /= mul1r. +have sG_Vg: left_inverse sG_1 sG_V sG_M. + by move=> x; apply: val_inj; rewrite /= -exprSr prednK ?rn1. +pose sgT := BaseFinGroupType _ (FinGroup.Mixin sG_Ag sG_1g sG_Vg). +pose gT := @FinGroupType sgT sG_Vg. +have /cyclicP[x gen_x]: @cyclic gT setT. + apply: (@field_mul_group_cyclic gT [set: _] F r) => // x _. + by split=> [ri1 | ->]; first apply: val_inj. +apply/hasP; exists (r x); first exact: (valP x). +have [m prim_x dvdmn] := prim_order_exists n_gt0 (rn1 x). +rewrite -((m =P n) _) // eqn_dvd {}dvdmn -sz_rs -(card_seq_sub Urs) -cardsT. +rewrite gen_x (@order_dvdn gT) /(_ == _) /= -{prim_x}(prim_expr_order prim_x). +by apply/eqP; elim: m => //= m IHm; rewrite exprS expgS /= -IHm. +Qed. + +End PrimitiveRoots. + +(***********************************************************************) +(* Cycles of prime order *) +(***********************************************************************) + +Section AutPrime. + +Variable gT : finGroupType. + +Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] -> cyclic (Aut <[a]>). +Proof. +move=> pr_a; have inj_um := injm_Zp_unitm a; have eq_a := Fp_Zcast pr_a. +pose fm := cast_ord (esym eq_a) \o val \o invm inj_um. +apply: (@field_mul_group_cyclic _ _ _ fm) => [f g Af Ag | f Af] /=. + by apply: val_inj; rewrite /= morphM ?im_Zp_unitm //= eq_a. +split=> [/= fm1 |->]; last by apply: val_inj; rewrite /= morph1. +apply: (injm1 (injm_invm inj_um)); first by rewrite /= im_Zp_unitm. +by do 2!apply: val_inj; move/(congr1 val): fm1. +Qed. + +Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| -> cyclic (Aut G). +Proof. +move=> pr_G; case/cyclicP: (prime_cyclic pr_G) (pr_G) => x ->. +exact: Aut_prime_cycle_cyclic. +Qed. + +End AutPrime. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 737838b..137518b 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -1,17 +1,15 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype bigop finset prime binomial. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.fingroup -Require Import presentation. -From mathcomp.algebra -Require Import ssralg finalg zmodp matrix cyclic. -Require Import pgroup center gseries commutator gfunctor. -Require Import nilpotent sylow abelian finmodule maximal extremal. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop finset prime binomial fingroup morphism perm automorphism. +From mathcomp +Require Import presentation quotient action commutator gproduct gfunctor. +From mathcomp +Require Import ssralg finalg zmodp cyclic pgroup center gseries. +From mathcomp +Require Import nilpotent sylow abelian finmodule matrix maximal extremal. (******************************************************************************) (* This file contains the fine structure thorems for extraspecial p-groups. *) @@ -332,7 +330,7 @@ Lemma Ohm1_extraspecial_odd (gT : finGroupType) (G : {group gT}) : Proof. move=> pG esG oddG Y; have [spG _] := esG. have [defPhiG defG'] := spG; set Z := 'Z(G) in defPhiG defG'. -have{spG} expG: exponent G %| p ^ 2 by exact: exponent_special. +have{spG} expG: exponent G %| p ^ 2 by apply: exponent_special. have p_pr := extraspecial_prime pG esG. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have oZ: #|Z| = p := card_center_extraspecial pG esG. @@ -341,7 +339,7 @@ have nsYG: Y <| G := Ohm_normal 1 G; have [sYG nYG] := andP nsYG. have ntZ: Z != 1 by rewrite -cardG_gt1 oZ. have sZY: Z \subset Y. by apply: contraR ntZ => ?; rewrite -(setIidPl sZG) TI_Ohm1 ?prime_TIg ?oZ. -have ntY: Y != 1 by apply: contra ntZ; rewrite -!subG1; exact: subset_trans. +have ntY: Y != 1 by apply: subG1_contra ntZ. have p_odd: odd p by rewrite -oZ (oddSg sZG). have expY: exponent Y %| p by rewrite exponent_Ohm1_class2 // nil_class2 defG'. rewrite (prime_nt_dvdP p_pr _ expY) -?dvdn1 -?trivg_exponent //. @@ -372,7 +370,7 @@ have iYG: #|G : Y| = p. have [sVG [u Gu notVu]] := properP (maxgroupp maxV). without loss [v Vv notYv]: / exists2 v, v \in V & v \notin Y. have [->| ] := eqVneq Y V; first by rewrite (p_maximal_index pG). - by rewrite eqEsubset sYV => not_sVY; apply; exact/subsetPn. + by rewrite eqEsubset sYV => not_sVY; apply; apply/subsetPn. pose U := <[u]> <*> <[v]>; have Gv := subsetP sVG v Vv. have sUG: U \subset G by rewrite join_subG !cycle_subG Gu. have Uu: u \in U by rewrite -cycle_subG joing_subl. @@ -418,7 +416,7 @@ have iC1U (U : {group gT}) x: rewrite -(@dvdn_pmul2l (#|U| * #|'C_G[x]|)) ?muln_gt0 ?cardG_gt0 //. have maxCx: maximal 'C_G[x] G. rewrite cent1_extraspecial_maximal //; apply: contra not_cUx. - by rewrite inE Gx; exact: subsetP (centS sUG) _. + by rewrite inE Gx; apply: subsetP (centS sUG) _. rewrite {1}mul_cardG setIA (setIidPl sUG) -(p_maximal_index pG maxCx) -!mulnA. rewrite !Lagrange ?subsetIl // mulnC dvdn_pmul2l //. have [sCxG nCxG] := andP (p_maximal_normal pG maxCx). @@ -432,7 +430,7 @@ have oCG (U : {group gT}): by apply/subsetPn; rewrite eqEsubset sZU subsetI sUG centsC in neZU. pose W := 'C_U[x]; have iWU: #|U : W| = p by rewrite iC1U // inE not_cUx. have maxW: maximal W U by rewrite p_index_maximal ?subsetIl ?iWU. - have ltWU: W \proper U by exact: maxgroupp maxW. + have ltWU: W \proper U by apply: maxgroupp maxW. have [sWU [u Uu notWu]] := properP ltWU. have defU: W * <[u]> = U. have nsWU: W <| U := p_maximal_normal (pgroupS sUG pG) maxW. @@ -548,8 +546,8 @@ have not_cEE: ~~ abelian E. by apply: contra not_le_p3_p => cEE; rewrite -oE -oZ -defZE (center_idP _). have sES: E \subset S by rewrite -defET mulG_subl. have sTS: T \subset S by rewrite -defET mulG_subr. -have expE: exponent E %| p by exact: dvdn_trans (exponentS sES) expG. -have expT: exponent T %| p by exact: dvdn_trans (exponentS sTS) expG. +have expE: exponent E %| p by apply: dvdn_trans (exponentS sES) expG. +have expT: exponent T %| p by apply: dvdn_trans (exponentS sTS) expG. have{expE not_cEE} isoE: E \isog p^{1+2}. apply: isog_pX1p2 => //. by apply: card_p3group_extraspecial p_pr oE _; rewrite defZE. @@ -589,7 +587,7 @@ Qed. Lemma Q8_extraspecial : extraspecial 'Q_8. Proof. -have gt32: 3 > 2 by []; have isoQ: 'Q_8 \isog 'Q_(2 ^ 3) by exact: isog_refl. +have gt32: 3 > 2 by []; have isoQ: 'Q_8 \isog 'Q_(2 ^ 3) by apply: isog_refl. have [[x y] genQ _] := generators_quaternion gt32 isoQ. have [_ [defQ' defPhiQ _ _]] := quaternion_structure gt32 genQ isoQ. case=> defZ oZ _ _ _ _ _; split; last by rewrite oZ. @@ -673,9 +671,9 @@ rewrite subEproper; case/predU1P=> [defG1 | ltZG1]. have [n' n'_gt2 isoG]: exists2 n', n' > 2 & G \isog 'Q_(2 ^ n'). apply/quaternion_classP; apply/eqP. have not_cycG: ~~ cyclic G. - by apply: contra (extraspecial_nonabelian esG); exact: cyclic_abelian. + by apply: contra (extraspecial_nonabelian esG); apply: cyclic_abelian. move: oZ; rewrite defG1; move/prime_Ohm1P; rewrite (negPf not_cycG) /=. - by apply=> //; apply: contra not_cycG; move/eqP->; exact: cyclic1. + by apply=> //; apply: contra not_cycG; move/eqP->; apply: cyclic1. have [n0 n'3]: n = 0%N /\ n' = 3. have [[x y] genG _] := generators_quaternion n'_gt2 isoG. have n'3: n' = 3. @@ -689,7 +687,7 @@ rewrite subEproper; case/predU1P=> [defG1 | ltZG1]. by rewrite center_ncprod0. case/andP: ltZG1 => _; rewrite (OhmE _ pG) gen_subG. case/subsetPn=> x; case/LdivP=> Gx x2 notZx. -have ox: #[x] = 2 by exact: nt_prime_order (group1_contra notZx). +have ox: #[x] = 2 by apply: nt_prime_order (group1_contra notZx). have Z'x: x \in G :\: 'Z(G) by rewrite inE notZx. have [E [R [[oE oR] [defG ziER]]]] := split1_extraspecial pG esG Z'x. case=> defZE defZR [esE Ex] esR. @@ -744,8 +742,8 @@ Qed. Lemma rank_Dn n : 'r_2('D^n) = n.+1. Proof. elim: n => [|n IHn]; first by rewrite p_rank_abelem ?prime_abelem ?card_pX1p2n. -have oDDn: #|'D^n.+1| = (2 ^ n.+1.*2.+1)%N by exact: card_pX1p2n. -have esDDn: extraspecial 'D^n.+1 by exact: pX1p2n_extraspecial. +have oDDn: #|'D^n.+1| = (2 ^ n.+1.*2.+1)%N by apply: card_pX1p2n. +have esDDn: extraspecial 'D^n.+1 by apply: pX1p2n_extraspecial. do [case: pX1p2S => gz isoZ; set DDn := [set: _]] in oDDn esDDn *. have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnat_exp. apply/eqP; rewrite eqn_leq; apply/andP; split. @@ -787,7 +785,7 @@ have esDnQ: extraspecial 'D^n*Q := DnQ_extraspecial n. do [case: DnQ_P => gz isoZ; set DnQ := setT] in pDnQ esDnQ *. suffices [E]: exists2 E, E \in 'E*_2(DnQ) & logn 2 #|E| = n.+1. by rewrite (pmaxElem_extraspecial pDnQ esDnQ); case/pnElemP=> _ _ <-. -have oZ: #|'Z(DnQ)| = 2 by exact: card_center_extraspecial. +have oZ: #|'Z(DnQ)| = 2 by apply: card_center_extraspecial. pose Dn := cpairg1 isoZ @* 'D^n; pose Q := cpair1g isoZ @* 'Q_8. have [injDn injQ] := (injm_cpairg1 isoZ, injm_cpair1g isoZ). have [E EprE]:= p_rank_witness 2 [group of Dn]. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index e233a86..83a9fb8 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -1,17 +1,15 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype bigop finset prime binomial. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.fingroup -Require Import presentation. -From mathcomp.algebra -Require Import ssralg finalg zmodp cyclic matrix. -Require Import pgroup center gseries commutator gfunctor. -Require Import nilpotent sylow abelian finmodule maximal. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop finset prime binomial fingroup morphism perm automorphism. +From mathcomp +Require Import presentation quotient action commutator gproduct gfunctor. +From mathcomp +Require Import ssralg finalg zmodp cyclic pgroup center gseries. +From mathcomp +Require Import nilpotent sylow abelian finmodule matrix maximal. (******************************************************************************) (* This file contains the definition and properties of extremal p-groups; *) @@ -253,10 +251,10 @@ have mV: {in A, {morph m : a / a^-1 >-> (a^-1)%R}}. by rewrite -mM ?groupV ?mulVg. have inv_m (u : 'Z_q) : coprime q u -> {a | a \in A & m a = u}. rewrite -?unitZpE // natr_Zp -im_m => m_u. - by exists (iinv m_u); [exact: mem_iinv | rewrite f_iinv]. + by exists (iinv m_u); [apply: mem_iinv | rewrite f_iinv]. have [cycF ffulF]: cyclic F /\ [faithful F, on 'Ohm_1(G) | [Aut G]]. have Um0 a: ((m a)%:R : 'F_p) \in GRing.unit. - have: m a \in GRing.unit by exact: valP. + have: m a \in GRing.unit by apply: valP. by rewrite -{1}[m a]natr_Zp unitFpE ?unitZpE // {1}/q oG coprime_pexpl. pose fm0 a := FinRing.unit 'F_p (Um0 a). have natZqp u: (u%:R : 'Z_q)%:R = u %:R :> 'F_p. @@ -271,7 +269,7 @@ have [cycF ffulF]: cyclic F /\ [faithful F, on 'Ohm_1(G) | [Aut G]]. by rewrite {1}[q]oG coprime_pexpl // -unitFpE // natZqp natr_Zp. by exists a => //; apply: val_inj; rewrite /= m_a natZqp natr_Zp. have [x1 defG1]: exists x1, 'Ohm_1(G) = <[x1]>. - by apply/cyclicP; exact: cyclicS (Ohm_sub _ _) cycG. + by apply/cyclicP; apply: cyclicS (Ohm_sub _ _) cycG. have ox1: #[x1] = p by rewrite orderE -defG1 (Ohm1_cyclic_pgroup_prime _ pG). have Gx1: x1 \in G by rewrite -cycle_subG -defG1 Ohm_sub. have ker_m0: 'ker m0 = 'C('Ohm_1(G) | [Aut G]). @@ -293,7 +291,7 @@ have [cycF ffulF]: cyclic F /\ [faithful F, on 'Ohm_1(G) | [Aut G]]. have inj_m0: 'ker_F m0 \subset [1] by rewrite setIC ker_m0_P tiPF. split; last by rewrite /faithful -ker_m0. have isogF: F \isog [set: {unit 'F_p}]. - have sFA: F \subset A by exact: pcore_sub. + have sFA: F \subset A by apply: pcore_sub. apply/isogP; exists (restrm_morphism sFA m0); first by rewrite ker_restrm. apply/eqP; rewrite eqEcard subsetT card_injm ?ker_restrm //= oF. by rewrite card_units_Fp. @@ -441,7 +439,7 @@ Lemma Grp_modular_group : 'Mod_(p ^ n) \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ r.+1)). Proof. rewrite /modular_gtype def_p def_q def_r; apply: Extremal.Grp => //. -set B := <[_]>; have Bb: Zp1 \in B by exact: cycle_id. +set B := <[_]>; have Bb: Zp1 \in B by apply: cycle_id. have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast. have cycB: cyclic B by rewrite cycle_cyclic. have pB: p.-group B by rewrite /pgroup oB pnat_exp ?pnat_id. @@ -472,7 +470,7 @@ have [Gx Gy]: x \in G /\ y \in G. have notXy: y \notin <[x]>. apply: contraL ltqm; rewrite -cycle_subG -oG -defG; move/mulGidPl->. by rewrite -leqNgt dvdn_leq ?(ltnW q_gt1) // order_dvdn xq. -have oy: #[y] = p by exact: nt_prime_order (group1_contra notXy). +have oy: #[y] = p by apply: nt_prime_order (group1_contra notXy). exists (x, y) => //=; split; rewrite ?inE ?notXy //. apply/eqP; rewrite -(eqn_pmul2r p_gt0) -expnSr -{1}oy (ltn_predK n_gt2) -/m. by rewrite -TI_cardMg ?defG ?oG // setIC prime_TIg ?cycle_subG // -orderE oy. @@ -528,7 +526,7 @@ have defZ: 'Z(G) = <[x ^+ p]>. rewrite (dvdn_prime_cyclic p_pr) // card_quotient //. rewrite -(dvdn_pmul2l (cardG_gt0 'Z(G))) Lagrange // oG -def_m dvdn_pmul2r //. case/p_natP: (pgroupS sZG pG) gtZr => k ->. - by rewrite ltn_exp2l // def_n1; exact: dvdn_exp2l. + by rewrite ltn_exp2l // def_n1; apply: dvdn_exp2l. have Zxr: x ^+ r \in 'Z(G) by rewrite /r def_n expnS expgM defZ mem_cycle. have rxy: [~ x, y] = x ^+ r by rewrite /commg xy expgS mulKg. have defG': G^`(1) = <[x ^+ r]>. @@ -542,7 +540,7 @@ have nil2_G: nil_class G = 2. have XYp: {in X & <[y]>, forall z t, (z * t) ^+ p \in z ^+ p *: <[x ^+ r ^+ 'C(p, 2)]>}. - move=> z t Xz Yt; have Gz := subsetP sXG z Xz; have Gt := subsetP sYG t Yt. - have Rtz: [~ t, z] \in G^`(1) by exact: mem_commg. + have Rtz: [~ t, z] \in G^`(1) by apply: mem_commg. have cGtz: [~ t, z] \in 'C(G) by case/setIP: (subsetP sG'Z _ Rtz). rewrite expMg_Rmul /commute ?(centP cGtz) //. have ->: t ^+ p = 1 by apply/eqP; rewrite -order_dvdn -oy order_dvdG. @@ -646,7 +644,7 @@ Lemma card_dihedral : #|'D_m| = m. Proof. by rewrite /('D_m)%type def_q card_ext_dihedral ?mul1n. Qed. Lemma Grp_dihedral : 'D_m \isog Grp (x : y : (x ^+ q, y ^+ 2, x ^ y = x^-1)). -Proof. by rewrite /('D_m)%type def_q; exact: Grp_ext_dihedral. Qed. +Proof. by rewrite /('D_m)%type def_q; apply: Grp_ext_dihedral. Qed. Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : (x ^+ 2, y ^+ 2, (x * y) ^+ q)). Proof. @@ -873,7 +871,7 @@ have{defG} defG: <[x]> * <[y]> = G. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. by rewrite dvdn_leq // order_dvdn xq. -have oy: #[y] = 2 by exact: nt_prime_order (group1_contra notXy). +have oy: #[y] = 2 by apply: nt_prime_order (group1_contra notXy). have ox: #[x] = q. apply: double_inj; rewrite -muln2 -oy -mul2n def2q -oG -defG TI_cardMg //. by rewrite setIC prime_TIg ?cycle_subG // -orderE oy. @@ -895,7 +893,7 @@ have{defG} defG: <[x]> * <[y]> = G. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. by rewrite dvdn_leq // order_dvdn xq. -have oy: #[y] = 2 by exact: nt_prime_order (group1_contra notXy). +have oy: #[y] = 2 by apply: nt_prime_order (group1_contra notXy). have ox: #[x] = q. apply: double_inj; rewrite -muln2 -oy -mul2n def2q -oG -defG TI_cardMg //. by rewrite setIC prime_TIg ?cycle_subG // -orderE oy. @@ -1042,7 +1040,7 @@ have maxMt: {in G :\: X, forall t, maximal <<t ^: G>> G}. have X'xy: x * y \in G :\: X by rewrite !inE !groupMl ?cycle_id ?notXy. have ti_yG_xyG: [disjoint yG & xyG]. apply/pred0P=> t; rewrite /= /yG /xyG !def_tG //; apply/andP=> [[yGt]]. - rewrite rcoset_sym (rcoset_transl yGt) mem_rcoset mulgK; move/order_dvdG. + rewrite rcoset_sym (rcoset_eqP yGt) mem_rcoset mulgK; move/order_dvdG. by rewrite -orderE ox2 ox gtnNdvd. have s_tG_X': {in G :\: X, forall t, t ^: G \subset G :\: X}. by move=> t X't /=; rewrite class_sub_norm // normsD ?normG. @@ -1066,7 +1064,7 @@ split. apply/eqP; rewrite eqEsubset Ohm_sub -{1}defXY mulG_subG !cycle_subG. by rewrite -(groupMr _ (sX'G1 y X'y)) !sX'G1. - split=> //= H; apply/idP/idP=> [maxH |]; last first. - by case/or3P; move/eqP->; rewrite ?maxMt. + by case/or3P=> /eqP->; rewrite ?maxMt. have [sHG nHG]:= andP (p_maximal_normal pG maxH). have oH: #|H| = q. apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //. @@ -1075,7 +1073,7 @@ split. case sHX: (H \subset X) => //=; case/subsetPn: sHX => t Ht notXt. have: t \in yG :|: xyG by rewrite defX' inE notXt (subsetP sHG). rewrite !andbT !gen_subG /yG /xyG. - by case/setUP; move/class_transr <-; rewrite !class_sub_norm ?Ht ?orbT. + by case/setUP; move/class_eqP <-; rewrite !class_sub_norm ?Ht ?orbT. rewrite eqn_leq n_gt1; case: leqP n2_abelG => //= n_gt2 _. have ->: 'Z(G) = <[x ^+ r]>. apply/eqP; rewrite eqEcard andbC -orderE oxr -{1}(setIidPr (center_sub G)). @@ -1240,14 +1238,14 @@ have oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}. rewrite quotient_cycle ?(subsetP (nXiG 2)) //= -defPhi. rewrite -orderE (abelem_order_p (Phi_quotient_abelem pG)) ?mem_quotient //. apply: contraNneq notXt; move/coset_idr; move/implyP=> /=. - by rewrite defPhi ?(subsetP (nXiG 2)) //; apply: subsetP; exact: cycleX. + by rewrite defPhi ?(subsetP (nXiG 2)) //; apply: subsetP; apply: cycleX. have maxMt: {in G :\: X, forall t, maximal <<t ^: G>> G}. move=> t X't; rewrite /= p_index_maximal -?divgS ?sMtG ?oMt //. by rewrite oG -def2q mulnK. have X'xy: x * y \in G :\: X by rewrite !inE !groupMl ?cycle_id ?notXy. have ti_yG_xyG: [disjoint yG & xyG]. apply/pred0P=> t; rewrite /= /yG /xyG !def_tG //; apply/andP=> [[yGt]]. - rewrite rcoset_sym (rcoset_transl yGt) mem_rcoset mulgK; move/order_dvdG. + rewrite rcoset_sym (rcoset_eqP yGt) mem_rcoset mulgK; move/order_dvdG. by rewrite -orderE ox2 ox gtnNdvd. have s_tG_X': {in G :\: X, forall t, t ^: G \subset G :\: X}. by move=> t X't /=; rewrite class_sub_norm // normsD ?normG. @@ -1286,7 +1284,7 @@ rewrite pprodE //; split=> // [|||n_gt3]. case sHX: (H \subset X) => //=; case/subsetPn: sHX => z Hz notXz. have: z \in yG :|: xyG by rewrite defX' inE notXz (subsetP sHG). rewrite !andbT !gen_subG /yG /xyG. - by case/setUP=> /class_transr <-; rewrite !class_sub_norm ?Hz ?orbT. + by case/setUP=> /class_eqP <-; rewrite !class_sub_norm ?Hz ?orbT. have isoMt: {in G :\: X, forall z, <<z ^: G>> \isog 'Q_q}. have n1_gt2: n.-1 > 2 by rewrite -(subnKC n_gt3). move=> z X'z /=; rewrite isogEcard card_quaternion ?oMt // leqnn andbT. @@ -1385,7 +1383,7 @@ have defG1: 'Mho^1(G) = <[x ^+ 2]>. by case/cycleP: Xz => i ->; rewrite -expgM mulnC expgM mem_cycle. have{Xz Gz} [xi Xxi ->{z}]: exists2 xi, xi \in X & z = xi * y. have Uvy: y \in <[u]> :* v by rewrite defUv -(defU x). - apply/rcosetP; rewrite /X defU // (rcoset_transl Uvy) defUv. + apply/rcosetP; rewrite /X defU // (rcoset_eqP Uvy) defUv. by rewrite inE -(defU x) ?Xz. rewrite expn1 expgS {2}(conjgC xi) -{2}[y]/(y ^+ 2.-1) -{1}oy -invg_expg. rewrite mulgA mulgK invXX' // -expgS prednK // /r -(subnKC n_gt3) expnS. @@ -1427,14 +1425,14 @@ have oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}. rewrite quotient_cycle ?(subsetP (nXiG 2)) //= -defPhi -orderE. rewrite (abelem_order_p (Phi_quotient_abelem pG)) ?mem_quotient //. apply: contraNneq notXt; move/coset_idr; move/implyP=> /=. - by rewrite /= defPhi (subsetP (nXiG 2)) //; apply: subsetP; exact: cycleX. + by rewrite /= defPhi (subsetP (nXiG 2)) //; apply: subsetP; apply: cycleX. have maxMt: {in G :\: X, forall t, maximal <<t ^: G>> G}. move=> t X't /=; rewrite p_index_maximal -?divgS ?sMtG ?oMt //. by rewrite oG -def2q mulnK. have X'xy: x * y \in G :\: X by rewrite !inE !groupMl ?cycle_id ?notXy. have ti_yG_xyG: [disjoint yG & xyG]. apply/pred0P=> t; rewrite /= /yG /xyG !def_tG //; apply/andP=> [[yGt]]. - rewrite rcoset_sym (rcoset_transl yGt) mem_rcoset mulgK; move/order_dvdG. + rewrite rcoset_sym (rcoset_eqP yGt) mem_rcoset mulgK; move/order_dvdG. by rewrite -orderE ox2 ox gtnNdvd. have s_tG_X': {in G :\: X, forall t, t ^: G \subset G :\: X}. by move=> t X't /=; rewrite class_sub_norm // normsD ?normG. @@ -1481,7 +1479,7 @@ split. case sHX: (H \subset X) => //=; case/subsetPn: sHX => t Ht notXt. have: t \in yG :|: xyG by rewrite defX' inE notXt (subsetP sHG). rewrite !andbT !gen_subG /yG /xyG. - by case/setUP=> /class_transr <-; rewrite !class_sub_norm ?Ht ?orbT. + by case/setUP=> /class_eqP <-; rewrite !class_sub_norm ?Ht ?orbT. have n1_gt2: n.-1 > 2 by [rewrite -(subnKC n_gt3)]; have n1_gt1 := ltnW n1_gt2. rewrite !isogEcard card_2dihedral ?card_quaternion ?oMt // leqnn !andbT. have invX2X': {in G :\: X, forall t, x ^+ 2 ^ t == x ^- 2}. @@ -1686,7 +1684,7 @@ have:= semidihedral_structure n_gt3 genG isoG oy. rewrite -/X -/q -/r -/yG -/xyG -/My -/Mxy. case=> [[defG oxy invXX'] nilG [defZ oZ [-> ->] defMho] [[defX' tiX'] maxG]]. case=> isoMy isoMxy defX; do 2!split=> //. - by apply/dihedral_classP; exists n.-1; first exact: ltnW. + by apply/dihedral_classP; exists n.-1; first apply: ltnW. by apply/quaternion_classP; exists n.-1. Qed. @@ -1724,7 +1722,7 @@ pose Z := <[x ^+ r]>. have defZ: Z = 'Ohm_1(X) by rewrite defX (Ohm_p_cycle _ p_x) ox subn1 pfactorK. have oZ: #|Z| = p by rewrite -orderE orderXdiv ox -def_pr ?dvdn_mull ?mulnK. have cGZ: Z \subset 'C(G). - have nsZG: Z <| G by rewrite defZ (char_normal_trans (Ohm_char 1 _)). + have nsZG: Z <| G by rewrite defZ gFnormal_trans. move/implyP: (meet_center_nil (pgroup_nil pG) nsZG). rewrite -cardG_gt1 oZ p_gt1 setIA (setIidPl (normal_sub nsZG)). by apply: contraR; move/prime_TIg=> -> //; rewrite oZ. @@ -1867,9 +1865,9 @@ Proof. move=> pG /SCN_P[nsUG scUG] not_cGG cycU; have [sUG nUG] := andP nsUG. have [cUU pU] := (cyclic_abelian cycU, pgroupS sUG pG). have ltUG: ~~ (G \subset U). - by apply: contra not_cGG => sGU; exact: abelianS cUU. + by apply: contra not_cGG => sGU; apply: abelianS cUU. have ntU: U :!=: 1. - by apply: contra ltUG; move/eqP=> U1; rewrite -(setIidPl (cents1 G)) -U1 scUG. + by apply: contraNneq ltUG => U1; rewrite -scUG subsetIidl U1 cents1. have [p_pr _ [n oU]] := pgroup_pdiv pU ntU. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have [u defU] := cyclicP cycU; have Uu: u \in U by rewrite defU cycle_id. @@ -1879,7 +1877,7 @@ have modM1 (M : {group gT}): [/\ U \subset M, #|M : U| = p & extremal_class M = ModularGroup] -> M :=: 'C_M('Mho^1(U)) /\ 'Ohm_1(M)%G \in 'E_p^2(M). - case=> sUM iUM /modular_group_classP[q q_pr {n oU}[n n_gt23 isoM]]. - have n_gt2: n > 2 by exact: leq_trans (leq_addl _ _) n_gt23. + have n_gt2: n > 2 by apply: leq_trans (leq_addl _ _) n_gt23. have def_n: n = (n - 3).+3 by rewrite -{1}(subnKC n_gt2). have oM: #|M| = (q ^ n)%N by rewrite (card_isog isoM) card_modular_group. have pM: q.-group M by rewrite /pgroup oM pnat_exp pnat_id. @@ -1905,7 +1903,7 @@ have [_ _ [[|k] oGs]] := pgroup_pdiv pGs ntGs. by right; exists G; case: (modM1 G) => // <- ->; rewrite Ohm_char. by left; case: eqP ext2G => // <-. pose M := 'C_G('Mho^1(U)); right; exists [group of M]. -have sMG: M \subset G by exact: subsetIl. +have sMG: M \subset G by apply: subsetIl. have [pM nUM] := (pgroupS sMG pG, subset_trans sMG nUG). have sUM: U \subset M by rewrite subsetI sUG sub_abelian_cent ?Mho_sub. pose A := Aut U; have cAA: abelian A by rewrite Aut_cyclic_abelian. @@ -1986,9 +1984,9 @@ have not_cMM: ~~ abelian M. by rewrite (setIidPl _) ?indexgg // -scUG subsetI sMG sub_abelian_cent. have modM: extremal_class M = ModularGroup. have sU1Z: 'Mho^1(U) \subset 'Z(M). - by rewrite subsetI (subset_trans (Mho_sub 1 U)) // centsC subsetIr. - case: (predU1P (maximal_cycle_extremal _ _ _ _ iUM)) => //=; rewrite -/M. - case/andP; move/eqP=> p2 ext2M; rewrite p2 add1n in n_gt01. + by rewrite subsetI gFsub_trans // centsC subsetIr. + have /maximal_cycle_extremal/predU1P[] //= := iUM; rewrite -/M. + case/andP=> /eqP-p2 ext2M; rewrite p2 add1n in n_gt01. suffices{sU1Z}: #|'Z(M)| = 2. move/eqP; rewrite eqn_leq leqNgt (leq_trans _ (subset_leq_card sU1Z)) //. by rewrite defU1 -orderE (orderXexp 1 ou) subn1 p2 (ltn_exp2l 1). @@ -2005,9 +2003,9 @@ have modM: extremal_class M = ModularGroup. by case: (m == 2) => [|[]//]; move/abelem_abelian->. split=> //. have [//|_] := modM1 [group of M]; rewrite !inE -andbA /=. - by case/andP; move/subset_trans->. + by case/andP=> /subset_trans->. have{cycGs} [cycGs | [p2 [c fGs_c u_c]]] := cycGs. - suffices ->: 'Ohm_1(M) = 'Ohm_1(G) by exact: Ohm_char. + suffices ->: 'Ohm_1(M) = 'Ohm_1(G) by apply: Ohm_char. suffices sG1M: 'Ohm_1(G) \subset M. by apply/eqP; rewrite eqEsubset -{2}(Ohm_id 1 G) !OhmS. rewrite -(quotientSGK _ sUM) ?(subset_trans (Ohm_sub _ G)) //= defMs. @@ -2017,13 +2015,12 @@ have{cycGs} [cycGs | [p2 [c fGs_c u_c]]] := cycGs. rewrite -(part_pnat_id (pgroupS (Ohm_sub _ _) pGs)) p_part (leq_exp2l _ 1) //. by rewrite -p_rank_abelian -?rank_pgroup -?abelian_rank1_cyclic. suffices charU1: 'Mho^1(U) \char G^`(1). - rewrite (char_trans (Ohm_char _ _)) // subcent_char ?char_refl //. - exact: char_trans (der_char 1 G). + by rewrite gFchar_trans // subcent_char ?(char_trans charU1) ?gFchar. suffices sUiG': 'Mho^1(U) \subset G^`(1). - have cycG': cyclic G^`(1) by rewrite (cyclicS _ cycU) // der1_min. - by case/cyclicP: cycG' sUiG' => zs ->; exact: cycle_subgroup_char. + have /cyclicP[zs cycG']: cyclic G^`(1) by rewrite (cyclicS _ cycU) ?der1_min. + by rewrite cycG' in sUiG' *; apply: cycle_subgroup_char. rewrite defU1 cycle_subG p2 -groupV invMg -{2}u_c. -by case/morphimP: fGs_c => _ _ /morphimP[z _ Gz ->] ->; rewrite fG ?mem_commg. +by have [_ _ /morphimP[z _ Gz ->] ->] := morphimP fGs_c; rewrite fG ?mem_commg. Qed. (* This is Aschbacher, exercise (8.4) *) @@ -2038,7 +2035,7 @@ have [X maxX]: {X | [max X | X <| G & abelian X]}. have cycX: cyclic X by rewrite dn_G_1; case/andP: (maxgroupp maxX). have scX: X \in 'SCN(G) := max_SCN pG maxX. have [[p2 _ cG] | [M [_ _ _]]] := cyclic_SCN pG scX not_cGG cycX; last first. - rewrite 2!inE -andbA; case/and3P=> sEG abelE dimE_2 charE. + rewrite 2!inE -andbA => /and3P[sEG abelE dimE_2] charE. have:= dn_G_1 _ (char_normal charE) (abelem_abelian abelE). by rewrite (abelem_cyclic abelE) (eqP dimE_2). have [n oG] := p_natP pG; right; rewrite p2 cG /= in oG *. @@ -2113,9 +2110,9 @@ move=> pG sympG; have [H [charH]] := Thompson_critical pG. have sHG := char_sub charH; have pH := pgroupS sHG pG. set U := 'Z(H) => sPhiH_U sHG_U defU; set Z := 'Ohm_1(U). have sZU: Z \subset U by rewrite Ohm_sub. -have charU: U \char G := char_trans (center_char H) charH. +have charU: U \char G := gFchar_trans _ charH. have cUU: abelian U := center_abelian H. -have cycU: cyclic U by exact: sympG. +have cycU: cyclic U by apply: sympG. have pU: p.-group U := pgroupS (char_sub charU) pG. have cHU: U \subset 'C(H) by rewrite subsetIr. have cHsHs: abelian (H / Z). @@ -2130,11 +2127,10 @@ have [K /=] := inv_quotientS nsZH (Ohm_sub 1 (H / Z)); fold Z => defKs sZK sKH. have nsZK: Z <| K := normalS sZK sKH nsZH; have [_ nZK] := andP nsZK. have abelKs: p.-abelem (K / Z) by rewrite -defKs Ohm1_abelem ?quotient_pgroup. have charK: K \char G. - have charZ: Z \char H := char_trans (Ohm_char _ _) (center_char H). + have charZ: Z \char H := gFchar_trans _ (center_char H). rewrite (char_trans _ charH) // (char_from_quotient nsZK) //. by rewrite -defKs Ohm_char. -have cycZK: cyclic 'Z(K). - by rewrite sympG ?center_abelian ?(char_trans (center_char _)). +have cycZK: cyclic 'Z(K) by rewrite sympG ?center_abelian ?gFchar_trans. have [cKK | not_cKK] := orP (orbN (abelian K)). have defH: U = H. apply: center_idP; apply: cyclic_factor_abelian (Ohm_sub 1 _) _. @@ -2159,14 +2155,14 @@ have [cKK | not_cKK] := orP (orbN (abelian K)). by apply: (p3group_extraspecial pG); rewrite // p2 oG pfactorK. exists G; [by right | exists ('Z(G))%G; rewrite cprod_center_id setIA setIid]. by split=> //; left; rewrite prime_cyclic; case: esG. -have ntK: K :!=: 1 by apply: contra not_cKK; move/eqP->; exact: abelian1. +have ntK: K :!=: 1 by apply: contra not_cKK => /eqP->; apply: abelian1. have [p_pr _ _] := pgroup_pdiv (pgroupS sKH pH) ntK. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have oZ: #|Z| = p. apply: Ohm1_cyclic_pgroup_prime => //=; apply: contra ntK; move/eqP. by move/(trivg_center_pgroup pH)=> GH; rewrite -subG1 -GH. have sZ_ZK: Z \subset 'Z(K). - by rewrite subsetI sZK (subset_trans (Ohm_sub _ _ )) // subIset ?centS ?orbT. + by rewrite subsetI sZK gFsub_trans // subIset ?centS ?orbT. have sZsKs: 'Z(K) / Z \subset K / Z by rewrite quotientS ?center_sub. have [Es /= splitKs] := abelem_split_dprod abelKs sZsKs. have [_ /= defEsZs cEsZs tiEsZs] := dprodP splitKs. @@ -2187,7 +2183,7 @@ have sEH := subset_trans sEK sKH; have pE := pgroupS sEH pH. have esE: extraspecial E. split; last by rewrite defZE oZ. have sPhiZ: 'Phi(E) \subset Z. - rewrite -quotient_sub1 ?(subset_trans (Phi_sub _)) ?(quotient_Phi pE) //. + rewrite -quotient_sub1 ?gFsub_trans ?(quotient_Phi pE) //. rewrite subG1 (trivg_Phi (quotient_pgroup _ pE)) /= -defEs. by rewrite (abelemS sEsKs) //= -defKs Ohm1_abelem ?quotient_pgroup. have sE'Phi: E^`(1) \subset 'Phi(E) by rewrite (Phi_joing pE) joing_subl. @@ -2207,8 +2203,8 @@ have{defE'} sEG_E': [~: E, G] \subset E^`(1). have Uge: [~ g, e] \in U by rewrite (subsetP sHG_U) ?mem_commg. rewrite inE Uge inE -commgX; last by red; rewrite -(centsP cHU). have sZ_ZG: Z \subset 'Z(G). - have charZ: Z \char G := char_trans (Ohm_char _ _) charU. - move/implyP: (meet_center_nil (pgroup_nil pG) (char_normal charZ)). + have charZ: Z \char G := gFchar_trans _ charU. + have/implyP:= meet_center_nil (pgroup_nil pG) (char_normal charZ). rewrite -cardG_gt1 oZ prime_gt1 //=; apply: contraR => not_sZ_ZG. by rewrite prime_TIg ?oZ. have: e ^+ p \in 'Z(G). @@ -2217,7 +2213,7 @@ have{defE'} sEG_E': [~: E, G] \subset E^`(1). by case/setIP=> _ /centP cGep; apply/commgP; red; rewrite cGep. have sEG: E \subset G := subset_trans sEK (char_sub charK). set R := 'C_G(E). -have{sEG_E'} defG: E \* R = G by exact: (critical_extraspecial pG). +have{sEG_E'} defG: E \* R = G by apply: (critical_extraspecial pG). have [_ defER cRE] := cprodP defG. have defH: E \* 'C_H(E) = H by rewrite -(setIidPr sHG) setIAC (cprod_modl defG). have{defH} [_ defH cRH_E] := cprodP defH. @@ -2232,7 +2228,7 @@ have cRH_RH: abelian 'C_H(E). have:= Ohm_dprod 1 defHs; rewrite /= defKs (Ohm1_id (abelemS sEsKs abelKs)). rewrite dprodC; case/dprodP=> _ defEsRHs1 cRHs1Es tiRHs1Es. have sRHsHs: 'C_H(E) / Z \subset H / Z by rewrite quotientS ?subsetIl. - have cRHsRHs: abelian ('C_H(E) / Z) by exact: abelianS cHsHs. + have cRHsRHs: abelian ('C_H(E) / Z) by apply: abelianS cHsHs. have pHs: p.-group (H / Z) by rewrite quotient_pgroup. rewrite abelian_rank1_cyclic // (rank_pgroup (pgroupS sRHsHs pHs)). rewrite p_rank_abelian // -(leq_add2r (logn p #|Es|)) -lognM ?cardG_gt0 //. @@ -2259,14 +2255,12 @@ have [[p2 _ ext2R] | [M []]] := cyclic_SCN pR scUR not_cRR cycU. exists E; [by right | exists [group of R]; split=> //; right]. by rewrite dvdn_leq ?(@pfactor_dvdn 2 4) ?cardG_gt0 // -{2}p2. rewrite /= -/R => defM iUM modM _ _; pose N := 'C_G('Mho^1(U)). -have charZN2: 'Z('Ohm_2(N)) \char G. - rewrite (char_trans (center_char _)) // (char_trans (Ohm_char _ _)) //. - by rewrite subcent_char ?char_refl // (char_trans (Mho_char _ _)). +have charZN2: 'Z('Ohm_2(N)) \char G by rewrite !(gFchar_trans, subcent_char). have:= sympG _ charZN2 (center_abelian _). rewrite abelian_rank1_cyclic ?center_abelian // leqNgt; case/negP. have defN: E \* M = N. - rewrite defM (cprod_modl defG) // centsC (subset_trans (Mho_sub 1 _)) //. - by rewrite /= -/U -defRH subsetIr. + rewrite defM (cprod_modl defG) // centsC gFsub_trans //= -/U. + by rewrite -defRH subsetIr. case/modular_group_classP: modM => q q_pr [n n_gt23 isoM]. have{n_gt23} n_gt2 := leq_trans (leq_addl _ _) n_gt23. have n_gt1 := ltnW n_gt2; have n_gt0 := ltnW n_gt1. @@ -2276,14 +2270,14 @@ have{q_pr} defq: q = p; last rewrite {q}defq in genM modM isoM. by have [-> _ _ _] := genM; rewrite Euclid_dvdX // dvdn_prime2 //; case: eqP. have [oM Mx ox X'y] := genM; have [My _] := setDP X'y; have [oy _] := modM. have [sUM sMR]: U \subset M /\ M \subset R. - by rewrite defM subsetI sUR subsetIl centsC (subset_trans (Mho_sub _ _)). + by rewrite defM subsetI sUR subsetIl centsC gFsub_trans. have oU1: #|'Mho^1(U)| = (p ^ n.-2)%N. have oU: #|U| = (p ^ n.-1)%N. by rewrite -(divg_indexS sUM) iUM oM -subn1 expnB. case/cyclicP: cycU pU oU => u -> p_u ou. by rewrite (Mho_p_cycle 1 p_u) -orderE (orderXexp 1 ou) subn1. have sZU1: Z \subset 'Mho^1(U). - rewrite -(cardSg_cyclic cycU) ?Ohm_sub ?Mho_sub // oZ oU1. + rewrite -(cardSg_cyclic cycU) ?gFsub // oZ oU1. by rewrite -(subnKC n_gt2) expnS dvdn_mulr. case/modular_group_structure: genM => // _ [defZM _ oZM] _ _. have:= n_gt2; rewrite leq_eqVlt eq_sym !xpair_eqE andbC. @@ -2319,7 +2313,7 @@ have defN2: (E <*> X2) \x <[y]> = 'Ohm_2(N). rewrite /= (OhmE 2 pN) sub_gen /=; last 1 first. by rewrite subsetI -defN mulG_subl sub_LdivT expE. rewrite -cent_joinEl // -genM_join genS // -defN. - apply/subsetP=> ez; case/setIP; case/imset2P=> e z Ee Mz ->{ez}. + apply/subsetP=> _ /setIP[/imset2P[e z Ee Mz ->]]. rewrite inE expgMn; last by red; rewrite -(centsP cME). rewrite (exponentP expE) // mul1g => zp2; rewrite mem_mulg //=. by rewrite (OhmE 2 (pgroupS sMR pR)) mem_gen // !inE Mz. diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v index dd84def..2b2aa5f 100644 --- a/mathcomp/solvable/finmodule.v +++ b/mathcomp/solvable/finmodule.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm action gproduct. -From mathcomp.algebra -Require Import ssralg finalg cyclic. -Require Import commutator. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype bigop ssralg finset fingroup morphism perm. +From mathcomp +Require Import finalg action gproduct commutator cyclic. (******************************************************************************) (* This file regroups constructions and results that are based on the most *) @@ -17,7 +14,7 @@ Require Import commutator. (* splitting and transitivity theorem, from which we will later derive the *) (* Schur-Zassenhaus theorem and the elementary abelian special case of *) (* Maschke's theorem, the coprime abelian centraliser/commutator trivial *) -(* intersection theorem, from which we will derive that p-groups under coprime*) +(* intersection theorem, which is used to show that p-groups under coprime *) (* action factor into special groups, and the construction of the transfer *) (* homomorphism and its expansion relative to a cycle, from which we derive *) (* the Higman Focal Subgroup and the Burnside Normal Complement theorems. *) @@ -26,7 +23,7 @@ Require Import commutator. (* needed much outside this file, which contains all the results that exploit *) (* this construction. *) (* FiniteModule defines the Z[N(A)]-module associated with a finite abelian *) -(* abelian group A, given a proof abelA : abelian A) : *) +(* abelian group A, given a proof (abelA : abelian A) : *) (* fmod_of abelA == the type of elements of the module (similar to but *) (* distinct from [subg A]). *) (* fmod abelA x == the injection of x into fmod_of abelA if x \in A, else 0 *) @@ -95,16 +92,16 @@ Definition fmod_opp u := sub2f u^-1. Definition fmod_add u v := sub2f (u * v). Fact fmod_add0r : left_id (sub2f 1) fmod_add. -Proof. move=> u; apply: val_inj; exact: mul1g. Qed. +Proof. by move=> u; apply: val_inj; apply: mul1g. Qed. Fact fmod_addrA : associative fmod_add. -Proof. move=> u v w; apply: val_inj; exact: mulgA. Qed. +Proof. by move=> u v w; apply: val_inj; apply: mulgA. Qed. Fact fmod_addNr : left_inverse (sub2f 1) fmod_opp fmod_add. -Proof. move=> u; apply: val_inj; exact: mulVg. Qed. +Proof. by move=> u; apply: val_inj; apply: mulVg. Qed. Fact fmod_addrC : commutative fmod_add. -Proof. case=> x Ax [y Ay]; apply: val_inj; exact: (centsP abelA). Qed. +Proof. by case=> x Ax [y Ay]; apply: val_inj; apply: (centsP abelA). Qed. Definition fmod_zmodMixin := ZmodMixin fmod_addrA fmod_addrC fmod_add0r fmod_addNr. @@ -149,7 +146,7 @@ Qed. Lemma injm_fmod : 'injm fmod. Proof. -apply/injmP=> x y Ax Ay []; move/val_inj; exact: (injmP (injm_subg A)). +by apply/injmP=> x y Ax Ay []; move/val_inj; apply: (injmP (injm_subg A)). Qed. Notation "u ^@ x" := (actr u x) : ring_scope. @@ -275,9 +272,9 @@ have PpP x: pP x \in P by rewrite -mem_rcoset rcoset_repr rcoset_refl. have rPmul x y: x \in P -> rP (x * y) = rP y. by move=> Px; rewrite /rP rcosetM rcoset_id. pose pQ x := remgr H Q x; pose rH x := pQ (pP x) * rP x. -have pQhq: {in H & Q, forall h q, pQ (h * q) = q} by exact: remgrMid. +have pQhq: {in H & Q, forall h q, pQ (h * q) = q} by apply: remgrMid. have pQmul: {in P &, {morph pQ : x y / x * y}}. - apply: remgrM; [exact/complP | exact: normalS (nsHG)]. + by apply: remgrM; [apply/complP | apply: normalS (nsHG)]. have HrH x: rH x \in H :* x. by rewrite rcoset_sym mem_rcoset invMg mulgA mem_divgr // eqHQ PpP. have GrH x: x \in G -> rH x \in G. @@ -292,7 +289,7 @@ pose nu y := (\sum_(Px in rcosets P G) mu (repr Px) y)%R. have rHmul: {in G &, forall x y, rH (x * y) = rH x * rH y * val (mu x y)}. move=> x y Gx Gy; rewrite /= fmodK ?mulKVg // -mem_lcoset lcoset_sym. rewrite -norm_rlcoset; last by rewrite nHG ?GrH ?groupM. - by rewrite (rcoset_transl (HrH _)) -rcoset_mul ?nHG ?GrH // mem_mulg. + by rewrite (rcoset_eqP (HrH _)) -rcoset_mul ?nHG ?GrH // mem_mulg. have actrH a x: x \in G -> (a ^@ rH x = a ^@ x)%R. move=> Gx; apply: val_inj; rewrite /= !fmvalJ ?nHG ?GrH //. case/rcosetP: (HrH x) => b /(fmodK abelH) <- ->; rewrite conjgM. @@ -338,7 +335,7 @@ exists (Morphism fM @* G)%G; apply/complP; split. apply/trivgP/subsetP=> x /setIP[Hx /morphimP[y _ Gy eq_x]]. apply/set1P; move: Hx; rewrite {x}eq_x /= groupMr ?subgP //. rewrite -{1}(mulgKV y (rH y)) groupMl -?mem_rcoset // => Hy. - by rewrite -(mulg1 y) /f nu_Hmul // rH_Hmul //; exact: (morph1 (Morphism fM)). + by rewrite -(mulg1 y) /f nu_Hmul // rH_Hmul //; apply: (morph1 (Morphism fM)). apply/setP=> x; apply/mulsgP/idP=> [[h y Hh fy ->{x}] | Gx]. rewrite groupMl; last exact: (subsetP sHG). case/morphimP: fy => z _ Gz ->{h Hh y}. @@ -519,7 +516,7 @@ have HGgHzg: Hzg \in HG :* <[g]>. by rewrite mem_mulg ?set11 // -rcosetE mem_imset. have Hzg_x: x \in Hzg by rewrite (repr_mem_pblock trX). exists x; first by rewrite (repr_mem_transversal trX). -case/mulsgP: Hzg_x => y u /rcoset_transl <- /(orbit_act 'Rs) <- -> /=. +case/mulsgP: Hzg_x => y u /rcoset_eqP <- /(orbit_act 'Rs) <- -> /=. by rewrite rcosetE -rcosetM. Qed. @@ -543,7 +540,7 @@ pose pcyc x := pcycle (actperm 'Rs g) (H :* x). pose traj x := traject (actperm 'Rs g) (H :* x) #|pcyc x|. have Hgr_eq x: H_g_rcosets x = pcyc x. by rewrite /H_g_rcosets -orbitRs -pcycle_actperm ?inE. -have pcyc_eq x: pcyc x =i traj x by exact: pcycle_traject. +have pcyc_eq x: pcyc x =i traj x by apply: pcycle_traject. have uniq_traj x: uniq (traj x) by apply: uniq_traject_pcycle. have n_eq x: n_ x = #|pcyc x| by rewrite -Hgr_eq. have size_traj x: size (traj x) = n_ x by rewrite n_eq size_traject. @@ -572,7 +569,7 @@ have trY: is_transversal Y HG G. by rewrite -[x](mulgK (g ^+ i)) mem_mulg ?rcoset_refl // groupV mem_cycle. apply/set1P; rewrite /y eq_xx'; congr (_ * _ ^+ _) => //; apply/eqP. rewrite -(@nth_uniq _ (H :* x) (traj x)) ?size_traj // ?eq_xx' //. - by rewrite !nth_traj ?(rcoset_transl Hy_x'gj) // -eq_xx'. + by rewrite !nth_traj ?(rcoset_eqP Hy_x'gj) // -eq_xx'. have rYE x i : x \in X -> i < n_ x -> rY (H :* x :* g ^+ i) = x * g ^+ i. move=> Xx lt_i_x; rewrite -rcosetM; apply: (canLR_in (pblockK trY 1)). by apply/bigcupP; exists x => //; apply/imsetP; exists (Ordinal lt_i_x). diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 64fe7e6..cc589a0 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat. -From mathcomp.discrete -Require Import div fintype bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm action quotient gproduct. -From mathcomp.algebra -Require Import cyclic. -Require Import center pgroup nilpotent sylow hall abelian. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat div fintype bigop prime. +From mathcomp +Require Import finset fingroup morphism perm action quotient gproduct. +From mathcomp +Require Import cyclic center pgroup nilpotent sylow hall abelian. (******************************************************************************) (* Definition of Frobenius groups, some basic results, and the Frobenius *) @@ -19,8 +16,7 @@ Require Import center pgroup nilpotent sylow hall abelian. (* condition. *) (* semiprime K H <-> *) (* the internal action of H on K is "prime", i.e., an element of K that *) -(* centralises a nontrivial element of H must actually centralise all *) -(* of H. *) +(* centralises a nontrivial element of H must centralise all of H. *) (* normedTI A G L <=> *) (* A is nonempty, strictly disjoint from its conjugates in G, and has *) (* normaliser L in G. *) @@ -36,8 +32,8 @@ Require Import center pgroup nilpotent sylow hall abelian. (* G is (isomorphic to) a Frobenius group with complement H; same as *) (* above, but without the semi-direct product. The proof that this form *) (* is equivalent to the above (i.e., the existence of Frobenius *) -(* kernels) requires chareacter theory and will only be proved in the *) -(* vcharacter module. *) +(* kernels) requires character theory and will only be proved in the *) +(* vcharacter.v file. *) (* [Frobenius G] <=> G is a Frobenius group. *) (* Frobenius_action G H S to <-> *) (* The action to of G on S defines an isomorphism of G with a *) @@ -306,7 +302,7 @@ Lemma Frobenius_actionP G H : Proof. apply: (iffP andP) => [[neqHG] | [sT S to [ffulG transG regG ntH [u Su defH]]]]. case/normedTI_P=> nzH /subsetIP[sHG _] tiHG. - suffices: Frobenius_action G H (rcosets H G) 'Rs by exact: HasFrobeniusAction. + suffices: Frobenius_action G H (rcosets H G) 'Rs by apply: HasFrobeniusAction. pose Hfix x := 'Fix_(rcosets H G | 'Rs)[x]. have regG: {in G^#, forall x, #|Hfix x| <= 1}. move=> x /setD1P[ntx Gx]. @@ -314,12 +310,12 @@ apply: (iffP andP) => [[neqHG] | [sT S to [ffulG transG regG ntH [u Su defH]]]]. rewrite -(cards1 Hy) => /setIP[/imsetP[y Gy ->{Hy}] cHyx]. apply/subset_leq_card/subsetP=> _ /setIP[/imsetP[z Gz ->] cHzx]. rewrite -!sub_astab1 !astab1_act !sub1set astab1Rs in cHyx cHzx *. - rewrite !rcosetE; apply/set1P/rcoset_transl; rewrite mem_rcoset. + rewrite !rcosetE; apply/set1P/rcoset_eqP; rewrite mem_rcoset. apply: tiHG; [by rewrite !in_group | apply/pred0Pn; exists (x ^ y^-1)]. by rewrite conjD1g !inE conjg_eq1 ntx -mem_conjg cHyx conjsgM memJ_conjg. have ntH: H :!=: 1 by rewrite -subG1 -setD_eq0. split=> //; first 1 last; first exact: transRs_rcosets. - by exists (H : {set gT}); rewrite ?orbit_refl // astab1Rs (setIidPr sHG). + by exists (val H); rewrite ?orbit_refl // astab1Rs (setIidPr sHG). apply/subsetP=> y /setIP[Gy cHy]; apply: contraR neqHG => nt_y. rewrite (index1g sHG) //; apply/eqP; rewrite eqn_leq indexg_gt0 andbT. apply: leq_trans (regG y _); last by rewrite setDE 2!inE Gy nt_y /=. @@ -351,7 +347,7 @@ Lemma FrobeniusWcompl : [Frobenius G with complement H]. Proof. by case/andP: frobG. Qed. Lemma FrobeniusW : [Frobenius G]. -Proof. by apply/existsP; exists H; exact: FrobeniusWcompl. Qed. +Proof. by apply/existsP; exists H; apply: FrobeniusWcompl. Qed. Lemma Frobenius_context : [/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G]. @@ -408,7 +404,7 @@ by rewrite inE (subsetP (Frobenius_cent1_ker K1y)) // inE cent1C (subsetP sHG). Qed. Lemma Frobenius_reg_compl : semiregular H K. -Proof. by apply: semiregular_sym; exact: Frobenius_reg_ker. Qed. +Proof. by apply: semiregular_sym; apply: Frobenius_reg_ker. Qed. Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1. Proof. @@ -490,11 +486,11 @@ Qed. Lemma Frobenius_ker_dvd_ker1 G K : [Frobenius G with kernel K] -> #|G : K| %| #|K|.-1. -Proof. case/existsP=> H; exact: Frobenius_index_dvd_ker1. Qed. +Proof. by case/existsP=> H; apply: Frobenius_index_dvd_ker1. Qed. Lemma Frobenius_ker_coprime G K : [Frobenius G with kernel K] -> coprime #|K| #|G : K|. -Proof. case/existsP=> H; exact: Frobenius_index_coprime. Qed. +Proof. by case/existsP=> H; apply: Frobenius_index_coprime. Qed. Lemma Frobenius_semiregularP G K H : K ><| H = G -> K :!=: 1 -> H :!=: 1 -> @@ -547,7 +543,7 @@ move=> ntH1 sH1H frobG; have [defG ntK _ _ _] := Frobenius_context frobG. apply/Frobenius_semiregularP=> //. have [_ _ /(subset_trans sH1H) nH1K tiHK] := sdprodP defG. by rewrite sdprodEY //; apply/trivgP; rewrite -tiHK setIS. -by apply: sub_in1 (Frobenius_reg_ker frobG); exact/subsetP/setSD. +by apply: sub_in1 (Frobenius_reg_ker frobG); apply/subsetP/setSD. Qed. Lemma Frobenius_kerP G K : @@ -557,7 +553,7 @@ Lemma Frobenius_kerP G K : Proof. apply: (iffP existsP) => [[H frobG] | [ntK ltKG nsKG regK]]. have [/sdprod_context[nsKG _ _ _ _] ntK _ ltKG _] := Frobenius_context frobG. - by split=> //; exact: Frobenius_cent1_ker frobG. + by split=> //; apply: Frobenius_cent1_ker frobG. have /andP[sKG nKG] := nsKG. have hallK: Hall G K. rewrite /Hall sKG //= coprime_sym coprime_pi' //. @@ -568,7 +564,7 @@ have hallK: Hall G K. have /trivgPn[z]: P :&: K :&: 'Z(P) != 1. by rewrite meet_center_nil ?(pgroup_nil pP) ?(normalGI sPG nsKG). rewrite !inE -andbA -sub_cent1=> /and4P[_ Kz _ cPz] ntz. - by apply: subset_trans (regK z _); [exact/subsetIP | exact/setD1P]. + by apply: subset_trans (regK z _); [apply/subsetIP | apply/setD1P]. have /splitsP[H /complP[tiKH defG]] := SchurZassenhaus_split hallK nsKG. have [_ sHG] := mulG_sub defG; have nKH := subset_trans sHG nKG. exists H; apply/Frobenius_semiregularP; rewrite ?sdprodE //. @@ -604,7 +600,7 @@ Proof. move=> defG FrobG. have partG: partition (gval K |: (H^# :^: K)) G. apply: Frobenius_partition; apply/andP; rewrite defG; split=> //. - by apply/Frobenius_actionP; exact: HasFrobeniusAction FrobG. + by apply/Frobenius_actionP; apply: HasFrobeniusAction FrobG. have{FrobG} [ffulG transG regG ntH [u Su defH]]:= FrobG. apply/setP=> x; rewrite !inE; have [-> | ntx] := altP eqP; first exact: group1. rewrite /= -(cover_partition partG) /cover. @@ -677,7 +673,8 @@ Qed. Lemma injm_Frobenius_ker K sGD injf : [Frobenius G with kernel K] -> [Frobenius f @* G with kernel f @* K]. Proof. -case/existsP=> H frobG; apply/existsP; exists (f @* H)%G; exact: injm_Frobenius. +case/existsP=> H frobG; apply/existsP. +by exists (f @* H)%G; apply: injm_Frobenius. Qed. Lemma injm_Frobenius_group sGD injf : [Frobenius G] -> [Frobenius f @* G]. @@ -698,7 +695,7 @@ rewrite ltnS oG mulnK // => leqm. have:= q_gt0; rewrite leq_eqVlt => /predU1P[q1 | lt1q]. rewrite -(mul1n n) q1 -oG (setIidPl _) //. by apply/subsetP=> x Gx; rewrite inE -order_dvdn order_dvdG. -pose p := pdiv q; have pr_p: prime p by exact: pdiv_prime. +pose p := pdiv q; have pr_p: prime p by apply: pdiv_prime. have lt1p: 1 < p := prime_gt1 pr_p; have p_gt0 := ltnW lt1p. have{leqm} lt_qp_mq: q %/ p < mq by apply: leq_trans leqm; rewrite ltn_Pdiv. have: n %| #|'Ldiv_(p * n)(G)|. diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 25295ff..517010f 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -1,10 +1,8 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat. -From mathcomp.discrete -Require Import fintype bigop finset. -From mathcomp.fingroup +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat fintype bigop finset. +From mathcomp Require Import fingroup morphism automorphism quotient gproduct. (******************************************************************************) @@ -121,7 +119,7 @@ Definition iso_continuous := 'injm phi -> phi @* F G \subset F (phi @* G). Lemma continuous_is_iso_continuous : continuous -> iso_continuous. -Proof. by move=> Fcont gT hT G phi inj_phi; exact: Fcont. Qed. +Proof. by move=> Fcont gT hT G phi inj_phi; apply: Fcont. Qed. (* Functoriality on Grp with partial morphisms. *) Definition pcontinuous := @@ -129,7 +127,7 @@ Definition pcontinuous := phi @* F G \subset F (phi @* G). Lemma pcontinuous_is_continuous : pcontinuous -> continuous. -Proof. by move=> Fcont gT hT G; exact: Fcont. Qed. +Proof. by move=> Fcont gT hT G; apply: Fcont. Qed. (* Heredity with respect to inclusion *) Definition hereditary := @@ -269,6 +267,10 @@ Variable F : GFunctor.iso_map. Lemma gFsub gT (G : {group gT}) : F gT G \subset G. Proof. by case: F gT G. Qed. +Lemma gFsub_trans gT (G : {group gT}) (A : pred_class) : + G \subset A -> F gT G \subset A. +Proof. exact/subset_trans/gFsub. Qed. + Lemma gF1 gT : F gT 1 = 1. Proof. exact/trivgP/gFsub. Qed. Lemma gFiso_cont : GFunctor.iso_continuous F. @@ -282,32 +284,44 @@ by rewrite -morphimEsub ?gFsub ?gFiso_cont ?injm_autm. Qed. Lemma gFnorm gT (G : {group gT}) : G \subset 'N(F gT G). -Proof. by rewrite char_norm ?gFchar. Qed. +Proof. exact/char_norm/gFchar. Qed. + +Lemma gFnorms gT (G : {group gT}) : 'N(G) \subset 'N(F gT G). +Proof. exact/char_norms/gFchar. Qed. Lemma gFnormal gT (G : {group gT}) : F gT G <| G. -Proof. by rewrite char_normal ?gFchar. Qed. +Proof. exact/char_normal/gFchar. Qed. + +Lemma gFchar_trans gT (G H : {group gT}) : H \char G -> F gT H \char G. +Proof. exact/char_trans/gFchar. Qed. + +Lemma gFnormal_trans gT (G H : {group gT}) : H <| G -> F gT H <| G. +Proof. exact/char_normal_trans/gFchar. Qed. + +Lemma gFnorm_trans gT (A : pred_class) (G : {group gT}) : + A \subset 'N(G) -> A \subset 'N(F gT G). +Proof. by move/subset_trans/(_ (gFnorms G)). Qed. Lemma injmF_sub gT rT (G D : {group gT}) (f : {morphism D >-> rT}) : 'injm f -> G \subset D -> f @* (F gT G) \subset F rT (f @* G). Proof. -move=> injf sGD; apply/eqP; rewrite -(setIidPr (gFsub G)). -by rewrite-{3}(setIid G) -!(morphim_restrm sGD) gFiso_cont // injm_restrm. +move=> injf sGD; have:= gFiso_cont (injm_restrm sGD injf). +by rewrite im_restrm morphim_restrm (setIidPr _) ?gFsub. Qed. Lemma injmF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) : 'injm f -> G \subset D -> f @* (F gT G) = F rT (f @* G). Proof. -move=> injf sGD; apply/eqP; rewrite eqEsubset injmF_sub //=. -rewrite -{2}(morphim_invm injf sGD) -[f @* F _ _](morphpre_invm injf). -have Fsubs := subset_trans (gFsub _). -by rewrite -sub_morphim_pre (injmF_sub, Fsubs) ?morphimS ?injm_invm. +move=> injf sGD; have [sfGD injf'] := (morphimS f sGD, injm_invm injf). +apply/esym/eqP; rewrite eqEsubset -(injmSK injf') ?gFsub_trans //. +by rewrite !(subset_trans (injmF_sub _ _)) ?morphim_invm // gFsub_trans. Qed. Lemma gFisom gT rT (G D : {group gT}) R (f : {morphism D >-> rT}) : G \subset D -> isom G (gval R) f -> isom (F gT G) (F rT R) f. Proof. -case/(restrmP f)=> g [gf _ _ _]; rewrite -{f}gf. -by case/isomP=> injg <-; rewrite sub_isom ?gFsub ?injmF. +case/(restrmP f)=> g [gf _ _ _]; rewrite -{f}gf => /isomP[injg <-]. +by rewrite sub_isom ?gFsub ?injmF. Qed. Lemma gFisog gT rT (G : {group gT}) (R : {group rT}) : @@ -440,7 +454,7 @@ Section Composition. Variables (F1 : GFunctor.mono_map) (F2 : GFunctor.map). Lemma gFcomp_closed : GFunctor.closed (F1 \o F2). -Proof. by move=> gT G; rewrite (subset_trans (gFsub _ _)) ?gFsub. Qed. +Proof. by move=> gT G; rewrite !gFsub_trans. Qed. Lemma gFcomp_cont : GFunctor.continuous (F1 \o F2). Proof. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 718f074..3878413 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -1,13 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype bigop finset. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient action. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path fintype bigop. +From mathcomp +Require Import finset fingroup morphism automorphism quotient action. +From mathcomp Require Import commutator center. - (******************************************************************************) (* H <|<| G <=> H is subnormal in G, i.e., H <| ... <| G. *) (* invariant_factor A H G <=> A normalises both H and G, and H <| G. *) @@ -173,7 +171,7 @@ Lemma invariant_subnormal A G H : Proof. move=> nGA nHA /andP[]; move: #|G| => m. elim: m => [|m IHm] in G nGA * => sHG. - by rewrite eq_sym; exists [::]; last exact/eqP. + by rewrite eq_sym; exists [::]; last apply/eqP. rewrite iterSr; set K := <<_>>. have nKA: A \subset 'N(K) by rewrite norms_gen ?norms_class_support. have sHK: H \subset K by rewrite sub_gen ?sub_class_support. @@ -297,7 +295,7 @@ apply/maxgroupP/maxgroupP; rewrite morphpre_proper //= => [] [ltMG maxM]. split=> // H ltHG sMH. have dH: H \subset D := subset_trans (proper_sub ltHG) (subsetIl D _). have defH: f @*^-1 (f @* H) = H. - by apply: morphimGK dH; apply: subset_trans sMH; exact: ker_sub_pre. + by apply: morphimGK dH; apply: subset_trans sMH; apply: ker_sub_pre. rewrite -defH morphpre_proper ?morphimS // in ltHG. by rewrite -defH [f @* H]maxM // -(morphpreK dM) morphimS. Qed. @@ -391,12 +389,12 @@ Qed. Lemma maxnormal_proper A B C : maxnormal A B C -> A \proper B. Proof. -by case/maxsetP=> /and3P[gA pAB _] _; exact: (sub_proper_trans (subset_gen A)). +by case/maxsetP=> /and3P[gA pAB _] _; apply: (sub_proper_trans (subset_gen A)). Qed. Lemma maxnormal_sub A B C : maxnormal A B C -> A \subset B. Proof. -by move=> maxA; rewrite proper_sub //; exact: (maxnormal_proper maxA). +by move=> maxA; rewrite proper_sub //; apply: (maxnormal_proper maxA). Qed. Lemma ex_maxnormal_ntrivg G : G :!=: 1-> {N : {group gT} | maxnormal N G G}. @@ -416,7 +414,7 @@ wlog suffices: H K {maxH} maxK nsHG nsKG cHK ltHK_G / H \subset K. by move=> IH; rewrite eqEsubset !IH // -cHK. have{maxK} /maxgroupP[_ maxK] := maxK. apply/joing_idPr/maxK; rewrite ?joing_subr //= comm_joingE //. -by rewrite properEneq ltHK_G; exact: normalM. +by rewrite properEneq ltHK_G; apply: normalM. Qed. Lemma maxnormal_minnormal G L M : @@ -425,7 +423,7 @@ Lemma maxnormal_minnormal G L M : Proof. move=> nMG nGL /maxgroupP[/andP[/andP[sMG ltMG] nML] maxM]; apply/mingroupP. rewrite -subG1 quotient_sub1 ?ltMG ?quotient_norms //. -split=> // Hb /andP[ntHb nHbL]; have nsMG: M <| G by exact/andP. +split=> // Hb /andP[ntHb nHbL]; have nsMG: M <| G by apply/andP. case/inv_quotientS=> // H defHb sMH sHG; rewrite defHb; congr (_ / M). apply/eqP; rewrite eqEproper sHG /=; apply: contra ntHb => ltHG. have nsMH: M <| H := normalS sMH sHG nsMG. @@ -458,14 +456,14 @@ apply: (iffP mingroupP); rewrite normG andbT => [[ntG simG]]. split=> // N /andP[sNG nNG]. by case: (eqsVneq N 1) => [|ntN]; [left | right; apply: simG; rewrite ?ntN]. split=> // N /andP[ntN nNG] sNG. -by case: (simG N) ntN => // [|->]; [exact/andP | case/eqP]. +by case: (simG N) ntN => // [|->]; [apply/andP | case/eqP]. Qed. Lemma quotient_simple gT (G H : {group gT}) : H <| G -> simple (G / H) = maxnormal H G G. Proof. move=> nsHG; have nGH := normal_norm nsHG. -by apply/idP/idP; [exact: minnormal_maxnormal | exact: maxnormal_minnormal]. +by apply/idP/idP; [apply: minnormal_maxnormal | apply: maxnormal_minnormal]. Qed. Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) : @@ -496,7 +494,7 @@ Lemma chief_factor_minnormal G V U : chief_factor G V U -> minnormal (U / V) (G / V). Proof. case/andP=> maxV /andP[sUG nUG]; apply: maxnormal_minnormal => //. -by have /andP[_ nVG] := maxgroupp maxV; exact: subset_trans sUG nVG. +by have /andP[_ nVG] := maxgroupp maxV; apply: subset_trans sUG nVG. Qed. Lemma acts_irrQ G U V : @@ -527,7 +525,7 @@ have /andP[ltVU nVG] := maxgroupp maxV. have [||s ch_s defV] := IHm V; first exact: leq_trans (proper_card ltVU) _. by rewrite /normal (subset_trans (proper_sub ltVU) (normal_sub nsUG)). exists (rcons s U); last by rewrite last_rcons. -by rewrite rcons_path defV /= ch_s /chief_factor; exact/and3P. +by rewrite rcons_path defV /= ch_s /chief_factor; apply/and3P. Qed. End Chiefs. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 90ba407..5e8a41b 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -1,12 +1,12 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype finset bigop prime. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient action gproduct. -Require Import commutator center pgroup finmodule nilpotent sylow. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div fintype finset. +From mathcomp +Require Import prime fingroup morphism automorphism quotient action gproduct. +From mathcomp +Require Import gfunctor commutator center pgroup finmodule nilpotent sylow. +From mathcomp Require Import abelian maximal. (*****************************************************************************) @@ -41,7 +41,7 @@ have [-> | [p pr_p pH]] := trivgVpdiv H. have [P sylP] := Sylow_exists p H. case nPG: (P <| G); last first. pose N := ('N_G(P))%G; have sNG: N \subset G by rewrite subsetIl. - have eqHN_G: H * N = G by exact: Frattini_arg sylP. + have eqHN_G: H * N = G by apply: Frattini_arg sylP. pose H' := (H :&: N)%G. have nsH'N: H' <| N. by rewrite /normal subsetIr normsI ?normG ?(subset_trans sNG). @@ -50,7 +50,7 @@ case nPG: (P <| G); last first. by rewrite -mul_cardG (mulnC #|H'|) divnMl // cardG_gt0. have hallH': Hall N H'. rewrite /Hall -divgS subsetIr //= -eq_iH. - by case/andP: hallH => _; apply: coprimeSg; exact: subsetIl. + by case/andP: hallH => _; apply: coprimeSg; apply: subsetIl. have: [splits N, over H']. apply: IHn hallH' nsH'N; apply: {n}leq_trans Gn. rewrite proper_card // properEneq sNG andbT; apply/eqP=> eqNG. @@ -61,12 +61,12 @@ case nPG: (P <| G); last first. by rewrite /= -(setIidPr sKN) setIA tiKN. by rewrite eqEsubset -eqHN_G mulgS // -eqH'K mulGS mulSg ?subsetIl. pose Z := 'Z(P); pose Gbar := G / Z; pose Hbar := H / Z. -have sZP: Z \subset P by exact: center_sub. -have sZH: Z \subset H by exact: subset_trans (pHall_sub sylP). -have sZG: Z \subset G by exact: subset_trans sHG. -have nZG: Z <| G by apply: char_normal_trans nPG; exact: center_char. -have nZH: Z <| H by exact: normalS nZG. -have nHGbar: Hbar <| Gbar by exact: morphim_normal. +have sZP: Z \subset P by apply: center_sub. +have sZH: Z \subset H by apply: subset_trans (pHall_sub sylP). +have sZG: Z \subset G by apply: subset_trans sHG. +have nZG: Z <| G by apply: gFnormal_trans nPG. +have nZH: Z <| H by apply: normalS nZG. +have nHGbar: Hbar <| Gbar by apply: morphim_normal. have hallHbar: Hall Gbar Hbar by apply: morphim_Hall (normal_norm _) _. have: [splits Gbar, over Hbar]. apply: IHn => //; apply: {n}leq_trans Gn; rewrite ltn_quotient //. @@ -76,7 +76,7 @@ have: [splits Gbar, over Hbar]. case/splitsP=> Kbar /complP[tiHKbar eqHKbar]. have: Kbar \subset Gbar by rewrite -eqHKbar mulG_subr. case/inv_quotientS=> //= ZK quoZK sZZK sZKG. -have nZZK: Z <| ZK by exact: normalS nZG. +have nZZK: Z <| ZK by apply: normalS nZG. have cardZK: #|ZK| = (#|Z| * #|G : H|)%N. rewrite -(Lagrange sZZK); congr (_ * _)%N. rewrite -card_quotient -?quoZK; last by case/andP: nZZK. @@ -86,7 +86,7 @@ have cardZK: #|ZK| = (#|Z| * #|G : H|)%N. have: [splits ZK, over Z]. rewrite (Gaschutz_split nZZK _ sZZK) ?center_abelian //; last first. rewrite -divgS // cardZK mulKn ?cardG_gt0 //. - by case/andP: hallH => _; exact: coprimeSg. + by case/andP: hallH => _; apply: coprimeSg. by apply/splitsP; exists 1%G; rewrite inE -subG1 subsetIr mulg1 eqxx. case/splitsP=> K /complP[tiZK eqZK]. have sKZK: K \subset ZK by rewrite -(mul1g K) -eqZK mulSg ?sub1G. @@ -111,8 +111,8 @@ rewrite ltnS => leHn solH nHK; have [-> | ] := eqsVneq H 1. by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=. pose G := (H <*> K)%G. have defG: G :=: H * K by rewrite -normC // -norm_joinEl // joingC. -have sHG: H \subset G by exact: joing_subl. -have sKG: K \subset G by exact: joing_subr. +have sHG: H \subset G by apply: joing_subl. +have sKG: K \subset G by apply: joing_subr. have nsHG: H <| G by rewrite /(H <| G) sHG join_subG normG. case/(solvable_norm_abelem solH nsHG)=> M [sMH nsMG ntM] /and3P[_ abelM _]. have [sMG nMG] := andP nsMG; rewrite -defG => sK1G coHK oK1K. @@ -134,7 +134,7 @@ case/morphimP=> x nMx Hx ->{xb} eqK1Kx; pose K2 := (K :^ x)%G. have{eqK1Kx} eqK12: K1 / M = K2 / M by rewrite quotientJ. suff [y My ->]: exists2 y, y \in M & K1 :=: K2 :^ y. by exists (x * y); [rewrite groupMl // (subsetP sMH) | rewrite conjsgM]. -have nMK1: K1 \subset 'N(M) by exact: nMsG. +have nMK1: K1 \subset 'N(M) by apply: nMsG. have defMK: M * K1 = M <*> K1 by rewrite -normC // -norm_joinEl // joingC. have sMKM: M \subset M <*> K1 by rewrite joing_subl. have nMKM: M <| M <*> K1 by rewrite normalYl. @@ -243,7 +243,7 @@ have{transHb} transH (K : {group gT}): have: y \in coset M y by rewrite val_coset (subsetP nMK, rcoset_refl). have: coset M y \in (H :^ x) / M. rewrite /quotient morphimJ //=. - rewrite def_x def_H in sKHxb; apply: (subsetP sKHxb); exact: mem_quotient. + by rewrite def_x def_H in sKHxb; apply/(subsetP sKHxb)/mem_quotient. case/morphimP=> z Nz Hxz ->. rewrite val_coset //; case/rcosetP=> t Mt ->; rewrite groupMl //. by rewrite mem_conjg (subsetP sMH) // -mem_conjg (normP Nx). @@ -256,7 +256,7 @@ have [pi_p | pi'p] := boolP (p \in pi). have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|. case: (IHn _ H (leq_trans ltHG leGn)) => [|H1]; first exact: solvableS solG. case/and3P=> sH1H piH1 pi'H1' transH1. - have sH1G: H1 \subset G by exact: subset_trans sHG. + have sH1G: H1 \subset G by apply: subset_trans sHG. exists H1 => [|K sKG piK]. apply/and3P; split => //. rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA. @@ -283,7 +283,7 @@ have nMK: K \subset 'N(M) by apply: subset_trans sKG nMG. have defG1: M * K = G1 by rewrite -normC -?norm_joinEl. have sK1G1: K1 \subset M * K by rewrite defG1 subsetIr. have coMK: coprime #|M| #|K|. - by rewrite coprime_sym (pnat_coprime piK) //; exact: (pHall_pgroup hallM). + by rewrite coprime_sym (pnat_coprime piK) //; apply: (pHall_pgroup hallM). case: (SchurZassenhaus_trans_sol _ nMK sK1G1 coMK) => [||x Mx defK1]. - exact: solvableS solG. - apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 M)) -TI_cardMg //; last first. @@ -389,7 +389,7 @@ pose N := 'N_(A <*> G)(H)%G. have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG. have nGN_N: G :&: N <| N by rewrite /(_ <| N) subsetIr normsI ?normG. have NG_AG: G * N = A <*> G. - by apply: Hall_Frattini_arg hallH => //; exact/andP. + by apply: Hall_Frattini_arg hallH => //; apply/andP. have iGN_A: #|N| %/ #|G :&: N| = #|A|. rewrite setIC divgI -card_quotient // -quotientMidl NG_AG. rewrite card_quotient -?divgS //= norm_joinEl //. @@ -426,14 +426,14 @@ have nGN_N: G :&: N <| N. apply/normalP; rewrite subsetIr; split=> // y Ny. by rewrite conjIg (normP _) // (subsetP nGN, conjGid). have NG_AG : G * N = A <*> G. - by apply: Hall_Frattini_arg hallH => //; exact/andP. + by apply: Hall_Frattini_arg hallH => //; apply/andP. have iGN_A: #|N : G :&: N| = #|A|. rewrite -card_quotient //; last by case/andP: nGN_N. rewrite (card_isog (second_isog nGN)) /= -quotientMidr (normC nGN) NG_AG. rewrite card_quotient // -divgS //= joingC norm_joinEr //. by rewrite coprime_cardMg // mulnC mulnK. -have solGN: solvable (G :&: N) by apply: solvableS solG; exact: subsetIl. -have oAxA: #|A :^ x^-1| = #|A| by exact: cardJg. +have solGN: solvable (G :&: N) by apply: solvableS solG; apply: subsetIl. +have oAxA: #|A :^ x^-1| = #|A| by apply: cardJg. have sAN: A \subset N by rewrite subsetI -{1}genGid genS // subsetUl. have nGNA: A \subset 'N(G :&: N). by apply/normsP=> y ?; rewrite conjIg (normsP nGA) ?(conjGid, subsetP sAN). @@ -471,7 +471,7 @@ apply/eqP; rewrite eqEsubset subsetI morphimS ?subsetIl //=. rewrite (subset_trans _ (morphim_cent _ _)) ?morphimS ?subsetIr //=. apply/subsetP=> _ /setIP[/morphimP[x Nx Gx ->] cAHx]. have{cAHx} cAxR y: y \in A -> [~ x, y] \in R. - move=> Ay; have Ny: y \in 'N(H) by exact: subsetP Ay. + move=> Ay; have Ny: y \in 'N(H) by apply: subsetP Ay. rewrite inE mem_commg // andbT coset_idr ?groupR // morphR //=. by apply/eqP; apply/commgP; apply: (centP cAHx); rewrite mem_quotient. have AxRA: A :^ x \subset R * A. @@ -566,11 +566,11 @@ have defG: G :=: K * H. rewrite -{1}(mulGid G) mulgSS //= (card_Hall hallH) (card_Hall hallK). by rewrite mulnC partnC. have sGA_H: [~: G, A] \subset H. - rewrite gen_subG defG; apply/subsetP=> xya; case/imset2P=> xy a. - case/imset2P=> x y Kx Hy -> Aa -> {xya xy}. + rewrite gen_subG defG. + apply/subsetP=> _ /imset2P[_ a /imset2P[x y Kx Hy ->] Aa ->]. rewrite commMgJ (([~ x, a] =P 1) _) ?(conj1g, mul1g). by rewrite groupMl ?groupV // memJ_norm ?(subsetP nHA). - rewrite subsetI sKG in cKA; apply/commgP; exact: (centsP cKA). + by rewrite subsetI sKG in cKA; apply/commgP/(centsP cKA). apply: pcore_max; last first. by rewrite /(_ <| G) /= commg_norml commGC commg_subr nGA. by case/and3P: hallH => _ piH _; apply: pgroupS piH. @@ -592,11 +592,11 @@ have [G1 | ntG] := eqsVneq G 1. have sG_AG: G \subset A <*> G by rewrite joing_subr. have sA_AG: A \subset A <*> G by rewrite joing_subl. have nG_AG: A <*> G \subset 'N(G) by rewrite join_subG nGA normG. -have nsG_AG: G <| A <*> G by exact/andP. +have nsG_AG: G <| A <*> G by apply/andP. case: (solvable_norm_abelem solG nsG_AG) => // M [sMG nsMAG ntM]. have{nsMAG} [nMA nMG]: A \subset 'N(M) /\ G \subset 'N(M). by apply/andP; rewrite -join_subG normal_norm. -have nMX: X \subset 'N(M) by exact: subset_trans nMG. +have nMX: X \subset 'N(M) by apply: subset_trans nMG. case/is_abelemP=> p pr_p; case/and3P=> pM cMM _. have: #|G / M| < n by rewrite (leq_trans (ltn_quotient _ _)). move/(IHn _ (A / M)%G _ (X / M)%G); rewrite !(quotient_norms, quotientS) //. @@ -609,7 +609,7 @@ have{pi'Hq' sHGq} pi'HM': pi^'.-nat #|G : HM|. move: pi'Hq'; rewrite -!divgS // defHM !card_quotient //. by rewrite -(divnMl (cardG_gt0 M)) !Lagrange. have{nHAq} nHMA: A \subset 'N(HM). - by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; exact/andP. + by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; apply/andP. case/orP: (orbN (p \in pi)) => pi_p. exists HM; split=> //; apply/and3P; split; rewrite /pgroup //. by rewrite -(Lagrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM). @@ -618,7 +618,7 @@ case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}]. - exact: coprimeSg coGA. - exact: solvableS solG. case/and3P: hallH => sHHM piH pi'H'. - have sHG: H \subset G by exact: subset_trans sHMG. + have sHG: H \subset G by apply: subset_trans sHMG. exists H; split=> //; apply/and3P; split=> //. rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //. by rewrite pnat_mul pi'H'. @@ -640,7 +640,7 @@ have hallX: pi.-Hall(XM) X. have sXMG: XM \subset G by rewrite join_subG sXG. have hallY: pi.-Hall(XM) Y. have sYXM: Y \subset XM by rewrite subsetIr. - have piY: pi.-group Y by apply: pgroupS piH; exact: subsetIl. + have piY: pi.-group Y by apply: pgroupS piH; apply: subsetIl. rewrite /pHall sYXM piY -divgS // -(_ : Y * M = XM). by rewrite coprime_cardMg ?co_pi_M // mulKn //. rewrite /= setIC group_modr ?joing_subr //=; apply/setIidPl. @@ -746,7 +746,7 @@ Proof. move=> sHG nHA coHA solH; pose N := 'N_G(H). have nsHN: H <| N by rewrite normal_subnorm. have [sHN nHn] := andP nsHN. -have sNG: N \subset G by exact: subsetIl. +have sNG: N \subset G by apply: subsetIl. have nNA: {acts A, on group N | to}. split; rewrite // actsEsd // injm_subnorm ?injm_sdpair1 //=. by rewrite normsI ?norms_norm ?im_sdpair_norm -?actsEsd. @@ -882,12 +882,12 @@ Lemma sol_coprime_Sylow_subset A G X : Proof. move=> nGA coGA solA sXG pX nXA. pose nAp (Q : {group gT}) := [&& p.-group Q, Q \subset G & A \subset 'N(Q)]. -have: nAp X by exact/and3P. +have: nAp X by apply/and3P. case/maxgroup_exists=> R; case/maxgroupP; case/and3P=> pR sRG nRA maxR sXR. have [P sylP sRP]:= Sylow_superset sRG pR. suffices defP: P :=: R by exists P; rewrite sylP defP. case/and3P: sylP => sPG pP _; apply: (nilpotent_sub_norm (pgroup_nil pP)) => //. -pose N := 'N_G(R); have{sPG} sPN_N: 'N_P(R) \subset N by exact: setSI. +pose N := 'N_G(R); have{sPG} sPN_N: 'N_P(R) \subset N by apply: setSI. apply: norm_sub_max_pgroup (pgroupS (subsetIl _ _) pP) sPN_N (subsetIr _ _). have nNA: A \subset 'N(N) by rewrite normsI ?norms_norm. have coNA: coprime #|N| #|A| by apply: coprimeSg coGA; rewrite subsetIl. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 82d9c8b..f315efa 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -1,11 +1,10 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop finset. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient action. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype. +From mathcomp +Require Import bigop finset fingroup morphism automorphism quotient action. +From mathcomp Require Import gseries. (******************************************************************************) @@ -113,7 +112,7 @@ Qed. Lemma section_repr_isog s1 s2 : s1 \isog s2 -> section_repr s1 = section_repr s2. Proof. -by move=> iso12; congr (odflt _ _); apply: eq_pick => s; exact: isog_transr. +by move=> iso12; congr (odflt _ _); apply: eq_pick => s; apply: isog_transr. Qed. Definition mkfactors (G : {group gT}) (s : seq {group gT}) := @@ -167,7 +166,7 @@ have [-> | ntG] := eqVneq G 1%G; first by exists [::]; rewrite /comps eqxx. have [N maxN] := ex_maxnormal_ntrivg ntG. have [|s /andP[ls cs]] := IHn N. by rewrite -ltnS (leq_trans _ cG) // proper_card // (maxnormal_proper maxN). -by exists (N :: s); exact/and3P. +by exists (N :: s); apply/and3P. Qed. (******************************************************************************) @@ -234,7 +233,7 @@ have i3 : perm_eq fG1 fG2. rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). exact: perm_eq_refl. apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -apply: perm_eq_trans i2; exact: perm_eq_refl. +by apply: perm_eq_trans i2; apply: perm_eq_refl. Qed. End CompositionSeries. @@ -361,7 +360,7 @@ by move/maxgroupp; case/andP; rewrite properE; move/normal_sub->; case/andP. Qed. Lemma maxainv_sub : maxainv K N -> N \subset K. -Proof. move=> h; apply: proper_sub; exact: maxainv_proper. Qed. +Proof. by move=> h; apply: proper_sub; apply: maxainv_proper. Qed. Lemma maxainv_ainvar : maxainv K N -> A \subset 'N(N | to). Proof. by move/maxgroupp; case/and3P. Qed. @@ -557,7 +556,7 @@ have nKQ1 : K <| N2 / N1. have sqA : qact_dom to N1 \subset A. by apply/subsetP=> t; rewrite qact_domE // inE; case/andP. have nNN2 : (N2 :&: N1) <| N2. - rewrite /normal subsetIl; apply: normsI => //; exact: normG. + by rewrite /normal subsetIl; apply: normsI => //; apply: normG. have aKQ1 : [acts qact_dom to N1, on K | to / N1]. pose H':= coset (N2 :&: N1)@*^-1 H. have eHH' : H :=: H' / (N2 :&: N1) by rewrite cosetpreK. @@ -653,7 +652,7 @@ have i1 : perm_eq (mksrepr G N1 :: mkfactors N1 st1) apply: Hi=> //; rewrite /acomps ?lst1 //= lsN csN andbT /=. apply: asimple_quo_maxainv=> //; first by apply: subIset; rewrite sN1D. apply: asimpleI => //. - apply: subset_trans (normal_norm nN2G); exact: normal_sub. + by apply: subset_trans (normal_norm nN2G); apply: normal_sub. rewrite -quotientMidl (maxainvM _ _ maxN_2) //. by apply: maxainv_asimple_quo. by move=> e; apply: neN12. @@ -664,7 +663,7 @@ have i2 : perm_eq (mksrepr G N2 :: mkfactors N2 st2) apply: asimple_quo_maxainv=> //; first by apply: subIset; rewrite sN1D. have e : N1 :&: N2 :=: N2 :&: N1 by rewrite setIC. rewrite (group_inj (setIC N1 N2)); apply: asimpleI => //. - apply: subset_trans (normal_norm nN1G); exact: normal_sub. + by apply: subset_trans (normal_norm nN1G); apply: normal_sub. rewrite -quotientMidl (maxainvM _ _ maxN_1) //. exact: maxainv_asimple_quo. pose fG1 := [:: mksrepr G N1, mksrepr N1 N & mkfactors N sN]. @@ -675,7 +674,7 @@ have i3 : perm_eq fG1 fG2. rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). exact: perm_eq_refl. apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -apply: perm_eq_trans i2; exact: perm_eq_refl. +by apply: perm_eq_trans i2; apply: perm_eq_refl. Qed. End StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index a3cd11c..afca270 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1,14 +1,14 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype finfun bigop finset prime binomial. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg finalg zmodp cyclic. -Require Import pgroup center gseries commutator gfunctor. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype. +From mathcomp +Require Import finfun bigop finset prime binomial fingroup morphism perm. +From mathcomp +Require Import automorphism quotient action commutator gproduct gfunctor. +From mathcomp +Require Import ssralg finalg zmodp cyclic pgroup center gseries. +From mathcomp Require Import nilpotent sylow abelian finmodule. (******************************************************************************) @@ -65,12 +65,12 @@ Definition Fitting A := \big[dprod/1]_(p <- primes #|A|) 'O_p(A). Lemma Fitting_group_set G : group_set (Fitting G). Proof. -suffices [F ->]: exists F : {group gT}, Fitting G = F by exact: groupP. +suffices [F ->]: exists F : {group gT}, Fitting G = F by apply: groupP. rewrite /Fitting; elim: primes (primes_uniq #|G|) => [_|p r IHr] /=. by exists [1 gT]%G; rewrite big_nil. case/andP=> rp /IHr[F defF]; rewrite big_cons defF. suffices{IHr} /and3P[p'F sFG nFG]: p^'.-group F && (F <| G). - have nFGp: 'O_p(G) \subset 'N(F) := subset_trans (pcore_sub p G) nFG. + have nFGp: 'O_p(G) \subset 'N(F) := gFsub_trans _ nFG. have pGp: p.-group('O_p(G)) := pcore_pgroup p G. have{pGp} tiGpF: 'O_p(G) :&: F = 1 by rewrite coprime_TIg ?(pnat_coprime pGp). exists ('O_p(G) <*> F)%G; rewrite dprodEY // (sameP commG1P trivgP) -tiGpF. @@ -78,8 +78,8 @@ suffices{IHr} /and3P[p'F sFG nFG]: p^'.-group F && (F <| G). move/bigdprodWY: defF => <- {F}; elim: r rp => [_|q r IHr] /=. by rewrite big_nil gen0 pgroup1 normal1. rewrite inE eq_sym big_cons -joingE -joing_idr => /norP[qp /IHr {IHr}]. -set F := <<_>> => /andP[p'F nsFG]; rewrite norm_joinEl /= -/F; last first. - exact: subset_trans (pcore_sub q G) (normal_norm nsFG). +set F := <<_>> => /andP[p'F nsFG]. +rewrite norm_joinEl /= -/F; last exact/gFsub_trans/normal_norm. by rewrite pgroupM p'F normalM ?pcore_normal //= (pi_pgroup (pcore_pgroup q G)). Qed. @@ -236,7 +236,7 @@ Lemma Phi_quotient_id G : 'Phi (G / 'Phi(G)) = 1. Proof. apply/trivgP; rewrite -cosetpreSK cosetpre1 /=; apply/bigcapsP=> M maxM. have nPhi := Phi_normal G; have nPhiM: 'Phi(G) <| M. - by apply: normalS nPhi; [exact: bigcap_inf | case/maximal_eqP: maxM]. + by apply: normalS nPhi; [apply: bigcap_inf | case/maximal_eqP: maxM]. by rewrite sub_cosetpre_quo ?bigcap_inf // quotient_maximal_eq. Qed. @@ -265,12 +265,12 @@ apply/eqP/idP=> [trPhi | abP]. apply/set1gP; rewrite -trPhi; apply/bigcapP=> M. case/predU1P=> [-> | maxM]; first exact: groupX. have /andP[_ nMP] := p_maximal_normal pP maxM. - have nMx : x \in 'N(M) by exact: subsetP Px. + have nMx : x \in 'N(M) by apply: subsetP Px. apply: coset_idr; rewrite ?groupX ?morphX //=; apply/eqP. rewrite -(p_maximal_index pP maxM) -card_quotient // -order_dvdn cardSg //=. by rewrite cycle_subG mem_quotient. apply/trivgP/subsetP=> x Phi_x; rewrite -cycle_subG. -have Px: x \in P by exact: (subsetP (Phi_sub P)). +have Px: x \in P by apply: (subsetP (Phi_sub P)). have sxP: <[x]> \subset P by rewrite cycle_subG. case/splitsP: (abelem_splits abP sxP) => K /complP[tiKx defP]. have [-> | nt_x] := eqVneq x 1; first by rewrite cycle1. @@ -301,16 +301,16 @@ have [p_pr _ _] := pgroup_pdiv pP ntP. have [abP x1P] := abelemP p_pr Phi_quotient_abelem. apply/andP; split. have nMP: P \subset 'N(P^`(1) <*> 'Mho^1(P)) by rewrite normsY // !gFnorm. - rewrite -quotient_sub1 ?(subset_trans sPhiP) //=. - suffices <-: 'Phi(P / (P^`(1) <*> 'Mho^1(P))) = 1 by exact: morphimF. + rewrite -quotient_sub1 ?gFsub_trans //=. + suffices <-: 'Phi(P / (P^`(1) <*> 'Mho^1(P))) = 1 by apply: morphimF. apply/eqP; rewrite (trivg_Phi (morphim_pgroup _ pP)) /= -quotientE. apply/abelemP=> //; rewrite [abelian _]quotient_cents2 ?joing_subl //. split=> // _ /morphimP[x Nx Px ->] /=. rewrite -morphX //= coset_id // (MhoE 1 pP) joing_idr expn1. - by rewrite mem_gen //; apply/setUP; right; exact: mem_imset. + by rewrite mem_gen //; apply/setUP; right; apply: mem_imset. rewrite -quotient_cents2 // [_ \subset 'C(_)]abP (MhoE 1 pP) gen_subG /=. apply/subsetP=> _ /imsetP[x Px ->]; rewrite expn1. -have nPhi_x: x \in 'N('Phi(P)) by exact: (subsetP nPhiP). +have nPhi_x: x \in 'N('Phi(P)) by apply: (subsetP nPhiP). by rewrite coset_idr ?groupX ?morphX ?x1P ?mem_morphim. Qed. @@ -334,8 +334,8 @@ Lemma morphim_Phi rT P D (f : {morphism D >-> rT}) : p.-group P -> P \subset D -> f @* 'Phi(P) = 'Phi(f @* P). Proof. move=> pP sPD; rewrite !(@Phi_joing _ p) ?morphim_pgroup //. -rewrite morphim_gen ?(subset_trans _ sPD) ?subUset ?der_subS ?Mho_sub //. -by rewrite morphimU -joingE morphimR ?morphim_Mho. +rewrite morphim_gen ?subUset ?gFsub_trans // morphimU -joingE. +by rewrite morphimR ?morphim_Mho. Qed. Lemma quotient_Phi P H : @@ -347,7 +347,7 @@ Lemma Phi_min G H : p.-group G -> G \subset 'N(H) -> p.-abelem (G / H) -> 'Phi(G) \subset H. Proof. move=> pG nHG; rewrite -trivg_Phi ?quotient_pgroup // -subG1 /=. -by rewrite -(quotient_Phi pG) ?quotient_sub1 // (subset_trans (Phi_sub _)). +by rewrite -(quotient_Phi pG) ?quotient_sub1 // gFsub_trans. Qed. Lemma Phi_cprod G H K : @@ -366,17 +366,17 @@ Lemma Phi_mulg H K : 'Phi(H * K) = 'Phi(H) * 'Phi(K). Proof. move=> pH pK cHK; have defHK := cprodEY cHK. -have [|_ -> _] := cprodP (Phi_cprod _ defHK); rewrite /= cent_joinEr //. -by apply: pnat_dvd (dvdn_cardMg H K) _; rewrite pnat_mul; exact/andP. +have [|_ ->] /= := cprodP (Phi_cprod _ defHK); rewrite cent_joinEr //. +by rewrite pgroupM pH. Qed. Lemma charsimpleP G : reflect (G :!=: 1 /\ forall K, K :!=: 1 -> K \char G -> K :=: G) (charsimple G). Proof. -apply: (iffP mingroupP); rewrite char_refl andbT => [[ntG simG]]. +apply: (iffP mingroupP); rewrite char_refl andbT => -[ntG simG]. by split=> // K ntK chK; apply: simG; rewrite ?ntK // char_sub. -split=> // K /andP[ntK chK] _; exact: simG. +by split=> // K /andP[ntK chK] _; apply: simG. Qed. End Frattini4. @@ -405,26 +405,22 @@ Qed. Lemma Fitting_max G H : H <| G -> nilpotent H -> H \subset 'F(G). Proof. move=> nsHG nilH; rewrite -(Sylow_gen H) gen_subG. -apply/bigcupsP=> P /SylowP[p _ SylP]. +apply/bigcupsP=> P /SylowP[p _ sylP]. case Gp: (p \in \pi(G)); last first. - rewrite card1_trivg ?sub1G // (card_Hall SylP). + rewrite card1_trivg ?sub1G // (card_Hall sylP). rewrite part_p'nat // (pnat_dvd (cardSg (normal_sub nsHG))) //. by rewrite /pnat cardG_gt0 all_predC has_pred1 Gp. -move/nilpotent_Hall_pcore: SylP => ->{P} //. +have{P sylP}[-> //] := nilpotent_Hall_pcore nilH sylP. rewrite -(bigdprodWY (erefl 'F(G))) sub_gen //. rewrite -(filter_pi_of (ltnSn _)) big_filter big_mkord. have le_pG: p < #|G|.+1. by rewrite ltnS dvdn_leq //; move: Gp; rewrite mem_primes => /and3P[]. apply: (bigcup_max (Ordinal le_pG)) => //=. -apply: pcore_max (pcore_pgroup _ _) _. -exact: char_normal_trans (pcore_char p H) nsHG. +by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans. Qed. Lemma pcore_Fitting pi G : 'O_pi('F(G)) \subset 'O_pi(G). -Proof. -rewrite pcore_max ?pcore_pgroup //. -exact: char_normal_trans (pcore_char _ _) (Fitting_normal _). -Qed. +Proof. by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans ?Fitting_normal. Qed. Lemma p_core_Fitting p G : 'O_p('F(G)) = 'O_p(G). Proof. @@ -473,7 +469,7 @@ Qed. Lemma FittingS gT (G H : {group gT}) : H \subset G -> H :&: 'F(G) \subset 'F(H). Proof. move=> sHG; rewrite -{2}(setIidPl sHG). -do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom; exact: morphim_Fitting. +do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom; apply: morphim_Fitting. Qed. Lemma FittingJ gT (G : {group gT}) x : 'F(G :^ x) = 'F(G) :^ x. @@ -655,7 +651,7 @@ Qed. Lemma charsimple_solvable G : charsimple G -> solvable G -> is_abelem G. Proof. case/charsimple_dprod=> H [sHG simH [I Aut_I defG]] solG. -have p_pr: prime #|H| by exact: simple_sol_prime (solvableS sHG solG) simH. +have p_pr: prime #|H| by apply: simple_sol_prime (solvableS sHG solG) simH. set p := #|H| in p_pr; apply/is_abelemP; exists p => //. elim/big_rec: _ (G) defG => [_ <-|f B If IH_B M defM]; first exact: abelem1. have [Af [[_ K _ defB] _ _ _]] := (subsetP Aut_I f If, dprodP defM). @@ -686,8 +682,7 @@ Qed. Lemma trivg_Fitting G : solvable G -> ('F(G) == 1) = (G :==: 1). Proof. -move=> solG; apply/idP/idP=> [F1|]; last first. - by rewrite -!subG1; apply: subset_trans; exact: Fitting_sub. +move=> solG; apply/idP/idP=> [F1 | /eqP->]; last by rewrite gF1. apply/idPn=> /(solvable_norm_abelem solG (normal_refl _))[M [_ nsMG ntM]]. case/is_abelemP=> p _ /and3P[pM _ _]; case/negP: ntM. by rewrite -subG1 -(eqP F1) Fitting_max ?(pgroup_nil pM). @@ -697,11 +692,9 @@ Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)). Proof. apply/eqP; rewrite eqEsubset. rewrite (subset_trans _ (pcoreS _ (Fitting_sub _))); last first. - rewrite subsetI Fitting_sub Fitting_max ?Fitting_nil //. - by rewrite (char_normal_trans (Fitting_char _)) ?pcore_normal. + by rewrite subsetI Fitting_sub Fitting_max ?Fitting_nil ?gFnormal_trans. rewrite (subset_trans _ (FittingS (pcore_sub _ _))) // subsetI pcore_sub. -rewrite pcore_max ?pcore_pgroup //. -by rewrite (char_normal_trans (pcore_char _ _)) ?Fitting_normal. +by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans. Qed. End CharSimple. @@ -722,7 +715,7 @@ Lemma sol_prime_factor_exists : solvable G -> G :!=: 1 -> {H : {group gT} | H <| G & prime #|G : H| }. Proof. move=> solG /ex_maxnormal_ntrivg[H maxH]. -by exists H; [exact: maxnormal_normal | exact: index_maxnormal_sol_prime]. +by exists H; [apply: maxnormal_normal | apply: index_maxnormal_sol_prime]. Qed. End SolvablePrimeFactor. @@ -738,7 +731,7 @@ move=> pG [defPhi defG']. have [-> | ntG] := eqsVneq G 1; first by rewrite center1 abelem1. have [p_pr _ _] := pgroup_pdiv pG ntG. have fM: {in 'Z(G) &, {morph expgn^~ p : x y / x * y}}. - by move=> x y /setIP[_ /centP cxG] /setIP[/cxG cxy _]; exact: expgMn. + by move=> x y /setIP[_ /centP cxG] /setIP[/cxG cxy _]; apply: expgMn. rewrite abelemE //= center_abelian; apply/exponentP=> /= z Zz. apply: (@kerP _ _ _ (Morphism fM)) => //; apply: subsetP z Zz. rewrite -{1}defG' gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]. @@ -786,10 +779,10 @@ have{sZ2G'_Z} sG'Z: G^`(1) \subset 'Z(G). rewrite -quotient_der ?gFnorm // -quotientGI ?ucn_subS ?quotientS1 //=. by rewrite ucn1. have sCG': 'C_G(A) \subset G^`(1). - rewrite -quotient_sub1 //; last by rewrite subIset // char_norm ?der_char. + rewrite -quotient_sub1 //; last by rewrite subIset ?gFnorm. rewrite (subset_trans (quotient_subcent _ G A)) //= -[G in G / _]defG. have nGA: A \subset 'N(G) by rewrite -commg_subl defG. - rewrite quotientR ?(char_norm_trans (der_char _ _)) ?normG //. + rewrite quotientR ?gFnorm_trans ?normG //. rewrite coprime_abel_cent_TI ?quotient_norms ?coprime_morph //. exact: sub_der1_abelian. have defZ: 'Z(G) = G^`(1) by apply/eqP; rewrite eqEsubset (subset_trans cZA). @@ -853,7 +846,7 @@ have pEq: p.-group (E / 'Z(E))%g by rewrite quotient_pgroup. have /andP[sZE nZE] := center_normal E. have oEq: #|E / 'Z(E)|%g = (p ^ 2)%N. by rewrite card_quotient -?divgS // oEp3 oZp expnS mulKn. -have cEEq: abelian (E / 'Z(E))%g by exact: card_p2group_abelian oEq. +have cEEq: abelian (E / 'Z(E))%g by apply: card_p2group_abelian oEq. have not_cEE: ~~ abelian E. have: #|'Z(E)| < #|E| by rewrite oEp3 oZp (ltn_exp2l 1) ?prime_gt1. by apply: contraL => cEE; rewrite -leqNgt subset_leq_card // subsetI subxx. @@ -863,9 +856,9 @@ have defE': E^`(1) = 'Z(E). by rewrite setIC prime_TIg ?oZp. split; [split=> // | by rewrite oZp]; apply/eqP. rewrite eqEsubset andbC -{1}defE' {1}(Phi_joing pE) joing_subl. -rewrite -quotient_sub1 ?(subset_trans (Phi_sub _)) //. -rewrite subG1 /= (quotient_Phi pE) //= (trivg_Phi pEq); apply/abelemP=> //. -split=> // Zx EqZx; apply/eqP; rewrite -order_dvdn /order. +rewrite -quotient_sub1 ?gFsub_trans ?subG1 //=. +rewrite (quotient_Phi pE) //= (trivg_Phi pEq). +apply/abelemP=> //; split=> // Zx EqZx; apply/eqP; rewrite -order_dvdn /order. rewrite (card_pgroup (mem_p_elt pEq EqZx)) (@dvdn_exp2l _ _ 1) //. rewrite leqNgt -pfactor_dvdn // -oEq; apply: contra not_cEE => sEqZx. rewrite cyclic_center_factor_abelian //; apply/cyclicP. @@ -877,7 +870,7 @@ Lemma p3group_extraspecial G : p.-group G -> ~~ abelian G -> logn p #|G| <= 3 -> extraspecial G. Proof. move=> pG not_cGG; have /andP[sZG nZG] := center_normal G. -have ntG: G :!=: 1 by apply: contraNneq not_cGG => ->; exact: abelian1. +have ntG: G :!=: 1 by apply: contraNneq not_cGG => ->; apply: abelian1. have ntZ: 'Z(G) != 1 by rewrite (center_nil_eq1 (pgroup_nil pG)). have [p_pr _ [n oG]] := pgroup_pdiv pG ntG; rewrite oG pfactorK //. have [_ _ [m oZ]] := pgroup_pdiv (pgroupS sZG pG) ntZ. @@ -924,11 +917,11 @@ Qed. Lemma isog_special G (R : {group rT}) : G \isog R -> special G -> special R. -Proof. by case/isogP=> f injf <-; exact: injm_special. Qed. +Proof. by case/isogP=> f injf <-; apply: injm_special. Qed. Lemma isog_extraspecial G (R : {group rT}) : G \isog R -> extraspecial G -> extraspecial R. -Proof. by case/isogP=> f injf <-; exact: injm_extraspecial. Qed. +Proof. by case/isogP=> f injf <-; apply: injm_extraspecial. Qed. Lemma cprod_extraspecial G H K : p.-group G -> H \* K = G -> H :&: K = 'Z(H) -> @@ -972,10 +965,10 @@ have fM: {in G &, {morph f : y z / y * z}}%g. pose fm := Morphism fM. have fmG: fm @* G = 'Z(G). have sfmG: fm @* G \subset 'Z(G). - by apply/subsetP=> _ /morphimP[z _ Gz ->]; exact: fZ. + by apply/subsetP=> _ /morphimP[z _ Gz ->]; apply: fZ. apply/eqP; rewrite eqEsubset sfmG; apply: contraR notZx => /(prime_TIg prZ). rewrite (setIidPr _) // => fmG1; rewrite inE Gx; apply/centP=> y Gy. - by apply/commgP; rewrite -in_set1 -[[set _]]fmG1; exact: mem_morphim. + by apply/commgP; rewrite -in_set1 -[[set _]]fmG1; apply: mem_morphim. have ->: 'C_G[x] = 'ker fm. apply/setP=> z; rewrite inE (sameP cent1P commgP) !inE. by rewrite -invg_comm eq_invg_mul mulg1. @@ -995,7 +988,7 @@ apply/eqP; rewrite eqEsubset sCxH subsetI sHU /= andbT. apply: contraR not_sHU => not_sHCx. have maxCx: maximal 'C_G[x] G. rewrite cent1_extraspecial_maximal //; apply: contra not_cUx. - by rewrite inE Gx; exact: subsetP (centS sUG) _. + by rewrite inE Gx; apply: subsetP (centS sUG) _. have nsCx := p_maximal_normal pG maxCx. rewrite -(setIidPl sUG) -(mulg_normal_maximal nsCx maxCx sHG) ?subsetI ?sHG //. by rewrite -group_modr //= setIA (setIidPl sUG) mul_subG. @@ -1014,7 +1007,7 @@ have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG. pose W := 'C_U[x]; have sCW_G: 'C_G(W) \subset G := subsetIl G _. have maxW: maximal W U by rewrite subcent1_extraspecial_maximal // inE not_cUx. have nsWU: W <| U := p_maximal_normal (pgroupS sUG pG) maxW. -have ltWU: W \proper U by exact: maxgroupp maxW. +have ltWU: W \proper U by apply: maxgroupp maxW. have [sWU [u Uu notWu]] := properP ltWU; have sWG := subset_trans sWU sUG. have defU: W * <[u]> = U by rewrite (mulg_normal_maximal nsWU) ?cycle_subG. have iCW_CU: #|'C_G(W) : 'C_G(U)| = p. @@ -1060,7 +1053,7 @@ have sZE: 'Z(G) \subset E. by rewrite /= -defG' inE !mem_commg. have ziER: E :&: R = 'Z(E) by rewrite setIA (setIidPl sEG). have cER: R \subset 'C(E) by rewrite subsetIr. -have iCxG: #|G : 'C_G[x]| = p by exact: p_maximal_index. +have iCxG: #|G : 'C_G[x]| = p by apply: p_maximal_index. have maxR: maximal R 'C_G[x]. rewrite /R centY !cent_cycle setIA. rewrite subcent1_extraspecial_maximal ?subsetIl // inE Gy andbT -sub_cent1. @@ -1171,7 +1164,7 @@ have defS: <<X>> = S. apply: Phi_nongen; apply/eqP; rewrite eqEsubset join_subG sPS sXS -joing_idr. rewrite -genM_join sub_gen // -quotientSK ?quotient_gen // -defSb genS //. apply/subsetP=> xb Xxb; apply/imsetP; rewrite (setIidPr nPX). - by exists (repr xb); rewrite /= ?coset_reprK //; exact: mem_imset. + by exists (repr xb); rewrite /= ?coset_reprK //; apply: mem_imset. pose f (a : {perm gT}) := [ffun x => if x \in X then x^-1 * a x else 1]. have injf: {in A &, injective f}. move=> _ _ /morphimP[y nSy Ry ->] /morphimP[z nSz Rz ->]. @@ -1235,7 +1228,7 @@ move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. rewrite -(mulnK #|T| (cardG_gt0 (E :&: U))) -defT -mul_cardG /=. have ->: E :&: U = 'Z(S). apply/eqP; rewrite eqEsubset subsetI -{1 2}defZE subsetIl setIS //=. - by case/cprodP: defU => [[V _ -> _]] <- _; exact: mulG_subr. + by case/cprodP: defU => [[V _ -> _]] <- _; apply: mulG_subr. rewrite (IHs U) // oEp3 oZ -expnD addSn expnS mulKn ?prime_gt0 //. by rewrite pfactorK //= uphalf_double. Qed. @@ -1251,7 +1244,7 @@ rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oE; move/eqP=> defZE. move=> es_s; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. have sUT: U \subset T by rewrite -defT mulG_subr. have sZU: 'Z(T) \subset U. - by case/cprodP: defU => [[V _ -> _] <- _]; exact: mulG_subr. + by case/cprodP: defU => [[V _ -> _] <- _]; apply: mulG_subr. have defZU: 'Z(E) = 'Z(U). apply/eqP; rewrite eqEsubset defZE subsetI sZU subIset ?centS ?orbT //=. by rewrite subsetI subIset ?sUT //= -defT centM setSI. @@ -1259,7 +1252,7 @@ apply: (Aut_cprod_full _ defZU); rewrite ?cprodE //; last first. by apply: IHs; rewrite -?defZU ?defZE. have oZE: #|'Z(E)| = p by rewrite defZE. have [p2 | odd_p] := even_prime p_pr. - suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by exact: Aut_in_isog. + suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by apply: Aut_in_isog. apply/eqP; rewrite eqEcard restr_perm_Aut ?center_sub //=. by rewrite card_Aut_cyclic ?prime_cyclic ?oZE // {1}p2 cardG_gt0. have pE: p.-group E by rewrite /pgroup oE pnat_exp pnat_id. @@ -1298,7 +1291,7 @@ have [y Ey not_cxy]: exists2 y, y \in E & y \notin 'C[x]. have notZy: y \notin 'Z(E). apply: contra not_cxy; rewrite inE Ey; apply: subsetP. by rewrite -cent_set1 centS ?sub1set. -pose K := 'C_E[y]; have maxK: maximal K E by exact: cent1_extraspecial_maximal. +pose K := 'C_E[y]; have maxK: maximal K E by apply: cent1_extraspecial_maximal. have nsKE: K <| E := p_maximal_normal pE maxK; have [sKE nKE] := andP nsKE. have oK: #|K| = (p ^ 2)%N. by rewrite -(divg_indexS sKE) oE (p_maximal_index pE) ?mulKn. @@ -1403,7 +1396,7 @@ have{defB} defB : B :=: A * <[x]>. rewrite -quotientK ?cycle_subG ?quotient_cycle // defB quotientGK //. exact: normalS (normal_sub nBG) nsAG. apply/setIidPl; rewrite ?defB -[_ :&: _]center_prod //=. -rewrite /center !(setIidPl _) //; exact: cycle_abelian. +rewrite /center !(setIidPl _) //; apply: cycle_abelian. Qed. (* The two other assertions of Aschbacher 23.15 state properties of the *) @@ -1472,19 +1465,19 @@ have{nil_classY pY sXW sZY sZCA} defW: W = <[x]> * Z. congr (_ * _); apply/eqP; rewrite eqEsubset {1}[Z](OhmE 1 pA). rewrite subsetI setIAC subIset //; first by rewrite sZCA -[Z]Ohm_id OhmS. rewrite sub_gen ?setIS //; apply/subsetP=> w Ww; rewrite inE. - by apply/eqP; apply: exponentP w Ww; exact: exponent_Ohm1_class2. + by apply/eqP; apply: exponentP w Ww; apply: exponent_Ohm1_class2. have{sXG sAG} sXAG: XA \subset G by rewrite join_subG sXG. have{sXAG} nilXA: nilpotent XA := nilpotentS sXAG (pgroup_nil pG). have sYXA: Y \subset XA by rewrite defY defXA mulgS ?subsetIl. rewrite -[Y](nilpotent_sub_norm nilXA) {nilXA sYXA}//= -/Y -/XA. -apply: subset_trans (setIS _ (char_norm_trans (Ohm_char 1 _) (subxx _))) _. +suffices: 'N_XA('Ohm_1(Y)) \subset Y by apply/subset_trans/setIS/gFnorms. rewrite {XA}defXA -group_modl ?normsG /= -/W ?{W}defW ?mulG_subl //. rewrite {Y}defY mulgS // subsetI subsetIl {CA C}sub_astabQ subIset ?nZA //= -/Z. rewrite (subset_trans (quotient_subnorm _ _ _)) //= quotientMidr /= -/Z. rewrite -quotient_sub1 ?subIset ?cent_norm ?orbT //. rewrite (subset_trans (quotientI _ _ _)) ?coprime_TIg //. -rewrite (@pnat_coprime p) // -/(pgroup p _) ?quotient_pgroup {pA}//=. -rewrite -(setIidPr (cent_sub _)) [pnat _ _]p'group_quotient_cent_prime //. +rewrite (@pnat_coprime p) // -/(p.-group _) ?quotient_pgroup {pA}//= -pgroupE. +rewrite -(setIidPr (cent_sub _)) p'group_quotient_cent_prime //. by rewrite (dvdn_trans (dvdn_quotient _ _)) ?order_dvdn. Qed. @@ -1497,10 +1490,8 @@ Proof. move=> p_odd pG; set X := 'Ohm_1('C_G(Z)). case/maxgroupP=> /andP[nsZG abelZ] maxZ. have [sZG nZG] := andP nsZG; have [_ cZZ expZp] := and3P abelZ. -have{nZG} nsXG: X <| G. - apply: (char_normal_trans (Ohm_char 1 'C_G(Z))). - by rewrite /normal subsetIl normsI ?normG ?norms_cent. -have cZX : X \subset 'C(Z) := subset_trans (Ohm_sub _ _) (subsetIr _ _). +have{nZG} nsXG: X <| G by rewrite gFnormal_trans ?norm_normalI ?norms_cent. +have cZX : X \subset 'C(Z) by apply/gFsub_trans/subsetIr. have{sZG expZp} sZX: Z \subset X. rewrite [X](OhmE 1 (pgroupS _ pG)) ?subsetIl ?sub_gen //. apply/subsetP=> x Zx; rewrite !inE ?(subsetP sZG) ?(subsetP cZZ) //=. @@ -1513,23 +1504,23 @@ suffices{sZX} expXp: (exponent X %| p). case/andP=> /sub_center_normal nsZdG. have{nsZdG} [D defD sZD nsDG] := inv_quotientN nsZG nsZdG; rewrite defD. have sDG := normal_sub nsDG; have nsZD := normalS sZD sDG nsZG. - rewrite quotientSGK ?quotient_sub1 ?normal_norm //= -/X => sDX; case/negP. + rewrite quotientSGK ?quotient_sub1 ?normal_norm //= -/X => sDX /negP[]. rewrite (maxZ D) // nsDG andbA (pgroupS sDG) ?(dvdn_trans (exponentS sDX)) //. have sZZD: Z \subset 'Z(D) by rewrite subsetI sZD centsC (subset_trans sDX). by rewrite (cyclic_factor_abelian sZZD) //= -defD cycle_cyclic. pose normal_abelian := [pred A : {group gT} | A <| G & abelian A]. -have{nsZG cZZ} normal_abelian_Z : normal_abelian Z by exact/andP. +have{nsZG cZZ} normal_abelian_Z : normal_abelian Z by apply/andP. have{normal_abelian_Z} [A maxA sZA] := maxgroup_exists normal_abelian_Z. have SCN_A : A \in 'SCN(G) by apply: max_SCN pG maxA. move/maxgroupp: maxA => /andP[nsAG cAA] {normal_abelian}. have pA := pgroupS (normal_sub nsAG) pG. have{abelZ maxZ nsAG cAA sZA} defA1: 'Ohm_1(A) = Z. - apply: maxZ; last by rewrite -(Ohm1_id abelZ) OhmS. - by rewrite Ohm1_abelem ?(char_normal_trans (Ohm_char _ _) nsAG). + have: Z \subset 'Ohm_1(A) by rewrite -(Ohm1_id abelZ) OhmS. + by apply: maxZ; rewrite Ohm1_abelem ?gFnormal_trans. have{SCN_A} sX'A: X^`(1) \subset A. have sX_CWA1 : X \subset 'C('Ohm_1(A)) :&: 'C_G(A / 'Ohm_1(A) | 'Q). - rewrite subsetI /X -defA1 (Ohm1_stab_Ohm1_SCN_series _ p_odd) //= andbT. - exact: subset_trans (Ohm_sub _ _) (subsetIr _ _). + rewrite subsetI /X -defA1 (Ohm1_stab_Ohm1_SCN_series _ p_odd) //=. + by rewrite gFsub_trans ?subsetIr. by apply: subset_trans (der1_stab_Ohm1_SCN_series SCN_A); rewrite commgSS. pose genXp := [pred U : {group gT} | 'Ohm_1(U) == U & ~~ (exponent U %| p)]. apply/idPn=> expXp'; have genXp_X: genXp [group of X] by rewrite /= Ohm_id eqxx. @@ -1582,12 +1573,11 @@ have [|K]:= @maxgroup_exists _ qcr 1 _. case/maxgroupP; rewrite {}/qcr subUset => /and3P[chK sPhiZ sRZ] maxK _. have sKG := char_sub chK; have nKG := char_normal chK. exists K; split=> //; apply/eqP; rewrite eqEsubset andbC setSI //=. -have chZ: 'Z(K) \char G by [exact: subcent_char]; have nZG := char_norm chZ. -have chC: 'C_G(K) \char G by exact: subcent_char (char_refl G) chK. +have chZ: 'Z(K) \char G by [apply: subcent_char]; have nZG := char_norm chZ. +have chC: 'C_G(K) \char G by apply: subcent_char chK. rewrite -quotient_sub1; last by rewrite subIset // char_norm. apply/trivgP; apply: (TI_center_nil (quotient_nil _ (pgroup_nil pG))). - rewrite quotient_normal // /normal subsetIl normsI ?normG ?norms_cent //. - exact: char_norm. + by rewrite quotient_normal ?norm_normalI ?norms_cent ?normal_norm. apply: TI_Ohm1; apply/trivgP; rewrite -trivg_quotient -sub_cosetpre_quo //. rewrite morphpreI quotientGK /=; last first. by apply: normalS (char_normal chZ); rewrite ?subsetIl ?setSI. @@ -1598,16 +1588,16 @@ rewrite subsetI centsC cXK andbT -(mul1g K) -mulSG mul1g -(cent_joinEr cXK). rewrite [_ <*> K]maxK ?joing_subr //= andbC (cent_joinEr cXK). rewrite -center_prod // (subset_trans _ (mulG_subr _ _)). rewrite charM 1?charI ?(char_from_quotient (normal_cosetpre _)) //. - by rewrite cosetpreK (char_trans _ (center_char _)) ?Ohm_char. + by rewrite cosetpreK !gFchar_trans. rewrite (@Phi_mulg p) ?(pgroupS _ pG) // subUset commGC commMG; last first. by rewrite normsR ?(normsG sKG) // cents_norm // centsC. rewrite !mul_subG 1?commGC //. apply: subset_trans (commgS _ (subsetIr _ _)) _. rewrite -quotient_cents2 ?subsetIl // centsC // cosetpreK //. - by rewrite (subset_trans (Ohm_sub _ _)) // subsetIr. -have nZX := subset_trans sXG nZG; have pX : p.-group gX by exact: pgroupS pG. -rewrite -quotient_sub1 ?(subset_trans (Phi_sub _)) //=. -have pXZ: p.-group (gX / 'Z(K)) by exact: morphim_pgroup. + exact/gFsub_trans/subsetIr. +have nZX := subset_trans sXG nZG; have pX : p.-group gX by apply: pgroupS pG. +rewrite -quotient_sub1 ?gFsub_trans //=. +have pXZ: p.-group (gX / 'Z(K)) by apply: morphim_pgroup. rewrite (quotient_Phi pX nZX) subG1 (trivg_Phi pXZ). apply: (abelemS (quotientS _ (subsetIr _ _))); rewrite /= cosetpreK /=. have pZ: p.-group 'Z(G / 'Z(K)). @@ -1644,7 +1634,7 @@ have Hy: y \in H. rewrite -(injmSK inj1) ?cycle_subG // injm_subcent // subsetI. rewrite morphimS ?morphim_cycle ?cycle_subG //=. suffices: sdpair1 [Aut G] y \in [~: G', F']. - by rewrite commGC; apply: subsetP; exact/commG1P. + by rewrite commGC; apply: subsetP; apply/commG1P. rewrite morphM ?groupV ?morphV //= sdpair_act // -commgEl. by rewrite mem_commg ?mem_morphim ?cycle_id. have fy: f y = y := astabP cHFP _ Hy. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index e1baa3f..d9a6f8b 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path fintype div bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient gproduct. -From mathcomp.algebra -Require Import cyclic. -Require Import commutator gfunctor center gseries. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path fintype div. +From mathcomp +Require Import bigop prime finset fingroup morphism automorphism quotient. +From mathcomp +Require Import commutator gproduct gfunctor center gseries cyclic. (******************************************************************************) (* This file defines nilpotent and solvable groups, and give some of their *) @@ -132,29 +129,27 @@ Lemma lcn0 A : 'L_0(A) = A. Proof. by []. Qed. Lemma lcn1 A : 'L_1(A) = A. Proof. by []. Qed. Lemma lcnSn n A : 'L_n.+2(A) = [~: 'L_n.+1(A), A]. Proof. by []. Qed. Lemma lcnSnS n G : [~: 'L_n(G), G] \subset 'L_n.+1(G). -Proof. by case: n => //; exact: der1_subG. Qed. +Proof. by case: n => //; apply: der1_subG. Qed. Lemma lcnE n A : 'L_n.+1(A) = lower_central_at_rec n A. Proof. by []. Qed. Lemma lcn2 A : 'L_2(A) = A^`(1). Proof. by []. Qed. Lemma lcn_group_set n G : group_set 'L_n(G). -Proof. by case: n => [|[|n]]; exact: groupP. Qed. +Proof. by case: n => [|[|n]]; apply: groupP. Qed. Canonical lower_central_at_group n G := Group (lcn_group_set n G). Lemma lcn_char n G : 'L_n(G) \char G. -Proof. -by case: n => [|n]; last elim: n => [|n IHn]; rewrite ?lcnSn ?charR ?char_refl. -Qed. +Proof. by case: n; last elim=> [|n IHn]; rewrite ?char_refl ?lcnSn ?charR. Qed. Lemma lcn_normal n G : 'L_n(G) <| G. -Proof. by apply: char_normal; exact: lcn_char. Qed. +Proof. exact/char_normal/lcn_char. Qed. Lemma lcn_sub n G : 'L_n(G) \subset G. -Proof. by case/andP: (lcn_normal n G). Qed. +Proof. exact/char_sub/lcn_char. Qed. Lemma lcn_norm n G : G \subset 'N('L_n(G)). -Proof. by case/andP: (lcn_normal n G). Qed. +Proof. exact/char_norm/lcn_char. Qed. Lemma lcn_subS n G : 'L_n.+1(G) \subset 'L_n(G). Proof. @@ -173,7 +168,7 @@ Qed. Lemma lcn_sub_leq m n G : n <= m -> 'L_m(G) \subset 'L_n(G). Proof. -by move/subnK <-; elim: {m}(m - n) => // m; exact: subset_trans (lcn_subS _ _). +by move/subnK <-; elim: {m}(m - n) => // m; apply: subset_trans (lcn_subS _ _). Qed. Lemma lcnS n A B : A \subset B -> 'L_n(A) \subset 'L_n(B). @@ -268,13 +263,13 @@ Qed. Lemma lcnP G : reflect (exists n, 'L_n.+1(G) = 1) (nilpotent G). Proof. apply: (iffP idP) => [nilG | [n Ln1]]. - by exists (nil_class G); exact/lcn_nil_classP. + by exists (nil_class G); apply/lcn_nil_classP. apply/forall_inP=> H /subsetIP[sHG sHR]; rewrite -subG1 -{}Ln1. by elim: n => // n IHn; rewrite (subset_trans sHR) ?commSg. Qed. Lemma abelian_nil G : abelian G -> nilpotent G. -Proof. by move=> abG; apply/lcnP; exists 1%N; exact/commG1P. Qed. +Proof. by move=> abG; apply/lcnP; exists 1%N; apply/commG1P. Qed. Lemma nil_class0 G : (nil_class G == 0) = (G :==: 1). Proof. @@ -349,15 +344,15 @@ Qed. (* Now extract all the intermediate facts of the last proof. *) Lemma ucn_group_set gT (G : {group gT}) : group_set 'Z_n(G). -Proof. by have [hZ ->] := ucn_pmap; exact: groupP. Qed. +Proof. by have [hZ ->] := ucn_pmap; apply: groupP. Qed. Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G). Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G. -Proof. by have [hZ ->] := ucn_pmap; exact: gFsub. Qed. +Proof. by have [hZ ->] := ucn_pmap; apply: gFsub. Qed. Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n). -Proof. by have [hZ ->] := ucn_pmap; exact: pmorphimF. Qed. +Proof. by have [hZ ->] := ucn_pmap; apply: pmorphimF. Qed. Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn]. Canonical ucn_gFun := [gFun by morphim_ucn]. @@ -432,7 +427,7 @@ have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z). by rewrite -mulHK quotientMl // center_prod ?quotient_cents. have ZquoZ (B A : {group gT}): B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z. -- move=> cAB {defZ}defZ; have cAZnB := subset_trans (ucn_sub n B) cAB. +- move=> cAB {defZ}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. have /second_isom[/=]: A \subset 'N(Z). by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC. suffices ->: Z :&: A = 'Z_n(A). @@ -442,7 +437,7 @@ have ZquoZ (B A : {group gT}): by apply: subset_trans (ucn_sub_geq A n_gt0); rewrite /= setIC ucn1 setIS. rewrite (ZquoZ H K) 1?centsC 1?(centC cZn) // {ZquoZ}(ZquoZ K H) //. have cZn1: 'Z_n.+1(K) \subset 'C('Z_n.+1(H)) by apply: centSS cHK; apply: gFsub. -rewrite -quotientMl ?quotientK ?mul_subG ?(subset_trans (gFsub _ _)) //=. +rewrite -quotientMl ?quotientK ?mul_subG ?gFsub_trans //=. rewrite cprodE // -cent_joinEr ?mulSGid //= cent_joinEr //= -/Z. by rewrite -defZ mulgSS ?ucn_subS. Qed. @@ -475,25 +470,24 @@ Proof. rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G). elim: {1 3}n 0 (addn0 n) => [j <- //|i IHi j]. rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn. -have nZG := normal_norm (ucn_normal j G). -have nZL := subset_trans (lcn_sub _ _) nZG. -by rewrite -sub_morphim_pre // subsetI morphimS ?lcn_sub // quotient_cents2. +rewrite -sub_morphim_pre ?gFsub_trans ?gFnorm_trans // subsetI. +by rewrite morphimS ?gFsub // quotient_cents2 ?gFsub_trans ?gFnorm_trans. Qed. Lemma ucnP G : reflect (exists n, 'Z_n(G) = G) (nilpotent G). Proof. -apply: (iffP (lcnP G)) => [] [n /eqP clGn]; +apply: (iffP (lcnP G)) => -[n /eqP-clGn]; by exists n; apply/eqP; rewrite ucn_lcnP in clGn *. Qed. Lemma ucn_nil_classP n G : nilpotent G -> reflect ('Z_n(G) = G) (nil_class G <= n). Proof. -move=> nilG; rewrite (sameP (lcn_nil_classP n nilG) eqP) ucn_lcnP; exact: eqP. +move=> nilG; rewrite (sameP (lcn_nil_classP n nilG) eqP) ucn_lcnP; apply: eqP. Qed. Lemma ucn_id n G : 'Z_n('Z_n(G)) = 'Z_n(G). -Proof. by rewrite -{2}['Z_n(G)]gFid. Qed. +Proof. exact: gFid. Qed. Lemma ucn_nilpotent n G : nilpotent 'Z_n(G). Proof. by apply/ucnP; exists n; rewrite ucn_id. Qed. @@ -527,7 +521,7 @@ Lemma injm_nil G : 'injm f -> G \subset D -> nilpotent (f @* G) = nilpotent G. Proof. move=> injf sGD; apply/idP/idP; last exact: morphim_nil. case/ucnP=> n; rewrite -injm_ucn // => /injm_morphim_inj defZ. -by apply/ucnP; exists n; rewrite defZ ?(subset_trans (ucn_sub n G)). +by apply/ucnP; exists n; rewrite defZ ?gFsub_trans. Qed. Lemma nil_class_morphim G : nilpotent G -> nil_class (f @* G) <= nil_class G. @@ -542,7 +536,7 @@ Proof. move=> injf sGD; case nilG: (nilpotent G). apply/eqP; rewrite eqn_leq nil_class_morphim //. rewrite (sameP (lcn_nil_classP _ nilG) eqP) -subG1. - rewrite -(injmSK injf) ?(subset_trans (lcn_sub _ _)) // morphim1. + rewrite -(injmSK injf) ?gFsub_trans // morphim1. by rewrite morphim_lcn // (lcn_nil_classP _ _ (leqnn _)) //= injm_nil. transitivity #|G|; apply/eqP; rewrite eqn_leq. rewrite -(card_injm injf sGD) (leq_trans (index_size _ _)) ?size_mkseq //. @@ -608,21 +602,21 @@ have{nsGH} [i sZH []]: exists2 i, 'Z_i(G) \subset H & ~ 'Z_i.+1(G) \subset H. elim: n => [|i IHi] in nsGH *; first by rewrite sub1G in nsGH. by case sZH: ('Z_i(G) \subset H); [exists i | apply: IHi; rewrite sZH]. apply: subset_trans sNH; rewrite subsetI ucn_sub -commg_subr. -by apply: subset_trans sZH; apply: subset_trans (ucn_comm i G); exact: commgS. +by apply: subset_trans sZH; apply: subset_trans (ucn_comm i G); apply: commgS. Qed. Lemma nilpotent_proper_norm G H : nilpotent G -> H \proper G -> H \proper 'N_G(H). Proof. move=> nilG; rewrite properEneq properE subsetI normG => /andP[neHG sHG]. -by rewrite sHG; apply: contra neHG; move/(nilpotent_sub_norm nilG)->. +by rewrite sHG; apply: contra neHG => /(nilpotent_sub_norm nilG)->. Qed. Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G. Proof. move=> nilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) => // m IHm H. -rewrite ltnS => leGHm sHG; have:= sHG; rewrite subEproper. -case/predU1P=> [->|]; first exact: subnormal_refl. +rewrite ltnS => leGHm sHG. +have [->|] := eqVproper sHG; first exact: subnormal_refl. move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK. have snHK: H <|<| K by rewrite normal_subnormal ?normalSG. have sKG: K \subset G by rewrite subsetIl. @@ -676,7 +670,7 @@ by rewrite (forall_inP nilG) // subsetI sHG (subset_trans sHH') ?commgS. Qed. Lemma abelian_sol G : abelian G -> solvable G. -Proof. by move/abelian_nil; exact: nilpotent_sol. Qed. +Proof. by move/abelian_nil/nilpotent_sol. Qed. Lemma solvable1 : solvable [1 gT]. Proof. exact: abelian_sol (abelian1 gT). Qed. @@ -705,7 +699,7 @@ elim: n => [|n IHn]; first by rewrite subn0 prednK. rewrite dergSn subnS -ltnS. have [-> | ntGn] := eqVneq G^`(n) 1; first by rewrite commG1 cards1. case: (_ - _) IHn => [|n']; first by rewrite leqNgt cardG_gt1 ntGn. -by apply: leq_trans (proper_card _); exact: sol_der1_proper (der_sub _ _) _. +by apply: leq_trans (proper_card _); apply: sol_der1_proper (der_sub _ _) _. Qed. End Solvable. @@ -725,8 +719,7 @@ Lemma injm_sol : 'injm f -> G \subset D -> solvable (f @* G) = solvable G. Proof. move=> injf sGD; apply/idP/idP; last exact: morphim_sol. case/derivedP=> n Gn1; apply/derivedP; exists n; apply/trivgP. -rewrite -(injmSK injf) ?(subset_trans (der_sub _ _)) ?morphim_der //. -by rewrite Gn1 morphim1. +by rewrite -(injmSK injf) ?gFsub_trans ?morphim_der // Gn1 morphim1. Qed. End MorphSol. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index b1d2bf6..3d48a8a 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -1,14 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype bigop finset prime. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient action gproduct. -From mathcomp.algebra -Require Import cyclic. -Require Import gfunctor. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp +Require Import fintype bigop finset prime fingroup morphism. +From mathcomp +Require Import gfunctor automorphism quotient action gproduct cyclic. (******************************************************************************) (* Standard group notions and constructions based on the prime decomposition *) @@ -125,7 +122,7 @@ Implicit Types (x y z : gT) (A B C D : {set gT}) (G H K P Q R : {group gT}). Lemma trivgVpdiv G : G :=: 1 \/ (exists2 p, prime p & p %| #|G|). Proof. -have [leG1|lt1G] := leqP #|G| 1; first by left; exact: card_le1_trivg. +have [leG1|lt1G] := leqP #|G| 1; first by left; apply: card_le1_trivg. by right; exists (pdiv #|G|); rewrite ?pdiv_dvd ?pdiv_prime. Qed. @@ -140,13 +137,13 @@ Qed. Lemma pgroupE pi A : pi.-group A = pi.-nat #|A|. Proof. by []. Qed. Lemma sub_pgroup pi rho A : {subset pi <= rho} -> pi.-group A -> rho.-group A. -Proof. by move=> pi_sub_rho; exact: sub_in_pnat (in1W pi_sub_rho). Qed. +Proof. by move=> pi_sub_rho; apply: sub_in_pnat (in1W pi_sub_rho). Qed. Lemma eq_pgroup pi rho A : pi =i rho -> pi.-group A = rho.-group A. Proof. exact: eq_pnat. Qed. Lemma eq_p'group pi rho A : pi =i rho -> pi^'.-group A = rho^'.-group A. -Proof. by move/eq_negn; exact: eq_pnat. Qed. +Proof. by move/eq_negn; apply: eq_pnat. Qed. Lemma pgroupNK pi A : pi^'^'.-group A = pi.-group A. Proof. exact: pnatNK. Qed. @@ -164,7 +161,7 @@ Lemma p'groupEpi p G : p^'.-group G = (p \notin \pi(G)). Proof. exact: p'natEpi (cardG_gt0 G). Qed. Lemma pgroup_pi G : \pi(G).-group G. -Proof. by rewrite /=; exact: pnat_pi. Qed. +Proof. by rewrite /=; apply: pnat_pi. Qed. Lemma partG_eq1 pi G : (#|G|`_pi == 1%N) = pi^'.-group G. Proof. exact: partn_eq1 (cardG_gt0 G). Qed. @@ -178,10 +175,10 @@ Lemma pgroup1 pi : pi.-group [1 gT]. Proof. by rewrite /pgroup cards1. Qed. Lemma pgroupS pi G H : H \subset G -> pi.-group G -> pi.-group H. -Proof. by move=> sHG; exact: pnat_dvd (cardSg sHG). Qed. +Proof. by move=> sHG; apply: pnat_dvd (cardSg sHG). Qed. Lemma oddSg G H : H \subset G -> odd #|G| -> odd #|H|. -Proof. by rewrite !odd_2'nat; exact: pgroupS. Qed. +Proof. by rewrite !odd_2'nat; apply: pgroupS. Qed. Lemma odd_pgroup_odd p G : odd p -> p.-group G -> odd #|G|. Proof. @@ -212,7 +209,7 @@ Proof. by rewrite /pgroup cardJg. Qed. Lemma pgroup_p p P : p.-group P -> p_group P. Proof. -case: (leqP #|P| 1); first by move=> /card_le1_trivg-> _; exact: pgroup1. +case: (leqP #|P| 1); first by move=> /card_le1_trivg-> _; apply: pgroup1. move/pdiv_prime=> pr_q pgP; have:= pgroupP pgP _ pr_q (pdiv_dvd _). by rewrite /p_group => /eqnP->. Qed. @@ -220,7 +217,7 @@ Qed. Lemma p_groupP P : p_group P -> exists2 p, prime p & p.-group P. Proof. case: (ltnP 1 #|P|); first by move/pdiv_prime; exists (pdiv #|P|). -move/card_le1_trivg=> -> _; exists 2 => //; exact: pgroup1. +by move/card_le1_trivg=> -> _; exists 2 => //; apply: pgroup1. Qed. Lemma pgroup_pdiv p G : @@ -254,7 +251,7 @@ Proof. by case/and3P. Qed. Lemma pHallP pi G H : reflect (H \subset G /\ #|H| = #|G|`_pi) (pi.-Hall(G) H). Proof. apply: (iffP idP) => [piH | [sHG oH]]. - split; [exact: pHall_sub piH | exact: card_Hall]. + by split; [apply: pHall_sub piH | apply: card_Hall]. rewrite /pHall sHG -divgS // /pgroup oH. by rewrite -{2}(@partnC pi #|G|) ?mulKn ?part_pnat. Qed. @@ -268,7 +265,7 @@ Lemma coprime_mulpG_Hall pi G K R : Proof. move=> defG piK pi'R; apply/andP. rewrite /pHall piK -!divgS /= -defG ?mulG_subl ?mulg_subr //= pnatNK. -by rewrite coprime_cardMg ?(pnat_coprime piK) // mulKn ?mulnK //; exact/and3P. +by rewrite coprime_cardMg ?(pnat_coprime piK) // mulKn ?mulnK //; apply/and3P. Qed. Lemma coprime_mulGp_Hall pi G K R : @@ -284,15 +281,15 @@ Lemma eq_in_pHall pi rho G H : Proof. move=> eq_pi_rho; apply: andb_id2l => sHG. congr (_ && _); apply: eq_in_pnat => p piHp. - by apply: eq_pi_rho; exact: (piSg sHG). + by apply: eq_pi_rho; apply: (piSg sHG). by congr (~~ _); apply: eq_pi_rho; apply: (pi_of_dvd (dvdn_indexg G H)). Qed. Lemma eq_pHall pi rho G H : pi =i rho -> pi.-Hall(G) H = rho.-Hall(G) H. -Proof. by move=> eq_pi_rho; exact: eq_in_pHall (in1W eq_pi_rho). Qed. +Proof. by move=> eq_pi_rho; apply: eq_in_pHall (in1W eq_pi_rho). Qed. Lemma eq_p'Hall pi rho G H : pi =i rho -> pi^'.-Hall(G) H = rho^'.-Hall(G) H. -Proof. by move=> eq_pi_rho; exact: eq_pHall (eq_negn _). Qed. +Proof. by move=> eq_pi_rho; apply: eq_pHall (eq_negn _). Qed. Lemma pHallNK pi G H : pi^'^'.-Hall(G) H = pi.-Hall(G) H. Proof. exact: eq_pHall (negnK _). Qed. @@ -322,7 +319,7 @@ by case/andP=> sHG coHG /=; rewrite /pHall sHG /pgroup pnat_pi -?coprime_pi'. Qed. Lemma HallP G H : Hall G H -> exists pi, pi.-Hall(G) H. -Proof. by exists \pi(H); exact: Hall_pi. Qed. +Proof. by exists \pi(H); apply: Hall_pi. Qed. Lemma sdprod_Hall G K H : K ><| H = G -> Hall G K = Hall G H. Proof. @@ -355,7 +352,7 @@ Qed. Lemma compl_p'Hall pi K H G : pi^'.-Hall(G) K -> (H \in [complements to K in G]) = pi.-Hall(G) H. -Proof. by move/compl_pHall->; exact: eq_pHall (negnK pi). Qed. +Proof. by move/compl_pHall->; apply: eq_pHall (negnK pi). Qed. Lemma sdprod_normal_p'HallP pi K H G : K <| G -> pi^'.-Hall(G) H -> reflect (K ><| H = G) (pi.-Hall(G) K). @@ -402,8 +399,7 @@ Qed. Lemma pHall_subl pi G K H : H \subset K -> K \subset G -> pi.-Hall(G) H -> pi.-Hall(K) H. Proof. -move=> sHK sKG; rewrite /pHall sHK; case/and3P=> _ ->. -by apply: pnat_dvd; exact: indexSg. +by move=> sHK sKG; rewrite /pHall sHK => /and3P[_ ->]; apply/pnat_dvd/indexSg. Qed. Lemma Hall1 G : Hall G 1. @@ -446,14 +442,14 @@ Lemma p_eltM_norm pi x y : x \in 'N(<[y]>) -> pi.-elt x -> pi.-elt y -> pi.-elt (x * y). Proof. move=> nyx pi_x pi_y; apply: (@mem_p_elt pi _ (<[x]> <*> <[y]>)%G). - by rewrite /= norm_joinEl ?cycle_subG // pgroupM; exact/andP. + by rewrite /= norm_joinEl ?cycle_subG // pgroupM; apply/andP. by rewrite groupM // mem_gen // inE cycle_id ?orbT. Qed. Lemma p_eltM pi x y : commute x y -> pi.-elt x -> pi.-elt y -> pi.-elt (x * y). Proof. move=> cxy; apply: p_eltM_norm; apply: (subsetP (cent_sub _)). -by rewrite cent_gen cent_set1; exact/cent1P. +by rewrite cent_gen cent_set1; apply/cent1P. Qed. Lemma p_elt1 pi : pi.-elt (1 : gT). @@ -469,10 +465,10 @@ Lemma p_eltJ pi x y : pi.-elt (x ^ y) = pi.-elt x. Proof. by congr pnat; rewrite orderJ. Qed. Lemma sub_p_elt pi1 pi2 x : {subset pi1 <= pi2} -> pi1.-elt x -> pi2.-elt x. -Proof. by move=> pi12; apply: sub_in_pnat => q _; exact: pi12. Qed. +Proof. by move=> pi12; apply: sub_in_pnat => q _; apply: pi12. Qed. Lemma eq_p_elt pi1 pi2 x : pi1 =i pi2 -> pi1.-elt x = pi2.-elt x. -Proof. by move=> pi12; exact: eq_pnat. Qed. +Proof. by move=> pi12; apply: eq_pnat. Qed. Lemma p_eltNK pi x : pi^'^'.-elt x = pi.-elt x. Proof. exact: pnatNK. Qed. @@ -480,7 +476,7 @@ Proof. exact: pnatNK. Qed. Lemma eq_constt pi1 pi2 x : pi1 =i pi2 -> x.`_pi1 = x.`_pi2. Proof. move=> pi12; congr (x ^+ (chinese _ _ 1 0)); apply: eq_partn => // a. -by congr (~~ _); exact: pi12. +by congr (~~ _); apply: pi12. Qed. Lemma consttNK pi x : x.`_pi^'^' = x.`_pi. @@ -514,8 +510,8 @@ Proof. by rewrite -{1}(consttC pi^' x) consttNK mulgK p_elt_constt. Qed. Lemma order_constt pi (x : gT) : #[x.`_pi] = #[x]`_pi. Proof. rewrite -{2}(consttC pi x) orderM; [|exact: commuteX2|]; last first. - by apply: (@pnat_coprime pi); exact: p_elt_constt. -by rewrite partnM // part_pnat_id ?part_p'nat ?muln1 //; exact: p_elt_constt. + by apply: (@pnat_coprime pi); apply: p_elt_constt. +by rewrite partnM // part_pnat_id ?part_p'nat ?muln1 //; apply: p_elt_constt. Qed. Lemma consttM pi x y : commute x y -> (x * y).`_pi = x.`_pi * y.`_pi. @@ -535,7 +531,7 @@ Qed. Lemma consttX pi x n : (x ^+ n).`_pi = x.`_pi ^+ n. Proof. elim: n => [|n IHn]; first exact: constt1. -rewrite !expgS consttM ?IHn //; exact: commuteX. +by rewrite !expgS consttM ?IHn //; apply: commuteX. Qed. Lemma constt1P pi x : reflect (x.`_pi = 1) (pi^'.-elt x). @@ -562,12 +558,12 @@ Qed. Lemma prod_constt x : \prod_(0 <= p < #[x].+1) x.`_p = x. Proof. pose lp n := [pred p | p < n]. -have: (lp #[x].+1).-elt x by apply/pnatP=> // p _; exact: dvdn_leq. +have: (lp #[x].+1).-elt x by apply/pnatP=> // p _; apply: dvdn_leq. move/constt_p_elt=> def_x; symmetry; rewrite -{1}def_x {def_x}. elim: _.+1 => [|p IHp]. - by rewrite big_nil; apply/constt1P; exact/pgroupP. + by rewrite big_nil; apply/constt1P; apply/pgroupP. rewrite big_nat_recr //= -{}IHp -(consttC (lp p) x.`__); congr (_ * _). - rewrite sub_in_constt // => q _; exact: leqW. + by rewrite sub_in_constt // => q _; apply: leqW. set y := _.`__; rewrite -(consttC p y) (constt1P p^' _ _) ?mulg1. by rewrite 2?sub_in_constt // => q _; move/eqnP->; rewrite !inE ?ltnn. rewrite /p_elt pnatNK !order_constt -partnI. @@ -604,7 +600,7 @@ Qed. Lemma norm_sub_max_pgroup pi H M G : [max M | pi.-subgroup(G) M] -> pi.-group H -> H \subset G -> H \subset 'N(M) -> H \subset M. -Proof. by move=> maxM piH sHG /normC; exact: comm_sub_max_pgroup piH sHG. Qed. +Proof. by move=> maxM piH sHG /normC; apply: comm_sub_max_pgroup piH sHG. Qed. Lemma sub_pHall pi H G K : pi.-Hall(G) H -> pi.-group K -> H \subset K -> K \subset G -> K :=: H. @@ -615,9 +611,9 @@ Qed. Lemma Hall_max pi H G : pi.-Hall(G) H -> [max H | pi.-subgroup(G) H]. Proof. -move=> hallH; apply/maxgroupP; split=> [|K]. +move=> hallH; apply/maxgroupP; split=> [|K /andP[sKG piK] sHK]. by rewrite /psubgroup; case/and3P: hallH => ->. -case/andP=> sKG piK sHK; exact: (sub_pHall hallH). +exact: (sub_pHall hallH). Qed. Lemma pHall_id pi H G : pi.-Hall(G) H -> pi.-group G -> H :=: G. @@ -644,7 +640,7 @@ have{pG n leGn IHn} pZ: p %| #|'C_G(G)|. by have /andP[] := no_x y. by apply/implyP; rewrite -index_cent1 indexgI implyNb -Euclid_dvdM ?LagrangeI. have [Q maxQ _]: {Q | [max Q | p^'.-subgroup('C_G(G)) Q] & 1%G \subset Q}. - apply: maxgroup_exists; exact: psubgroup1. + by apply: maxgroup_exists; apply: psubgroup1. case/andP: (maxgroupp maxQ) => sQC; rewrite /pgroup p'natE // => /negP[]. apply: dvdn_trans pZ (cardSg _); apply/subsetP=> x /setIP[Gx Cx]. rewrite -sub1set -gen_subG (normal_sub_max_pgroup maxQ) //; last first. @@ -670,7 +666,7 @@ Qed. Lemma mem_normal_Hall pi H G x : pi.-Hall(G) H -> H <| G -> x \in G -> (x \in H) = pi.-elt x. -Proof. by rewrite -!cycle_subG; exact: sub_normal_Hall. Qed. +Proof. by rewrite -!cycle_subG; apply: sub_normal_Hall. Qed. Lemma uniq_normal_Hall pi H G K : pi.-Hall(G) H -> H <| G -> [max K | pi.-subgroup(G) K] -> K :=: H. @@ -723,17 +719,17 @@ Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}). Implicit Types (pi : nat_pred) (G H P : {group aT}). Lemma morphim_pgroup pi G : pi.-group G -> pi.-group (f @* G). -Proof. by apply: pnat_dvd; exact: dvdn_morphim. Qed. +Proof. by apply: pnat_dvd; apply: dvdn_morphim. Qed. Lemma morphim_odd G : odd #|G| -> odd #|f @* G|. -Proof. by rewrite !odd_2'nat; exact: morphim_pgroup. Qed. +Proof. by rewrite !odd_2'nat; apply: morphim_pgroup. Qed. Lemma pmorphim_pgroup pi G : pi.-group ('ker f) -> G \subset D -> pi.-group (f @* G) = pi.-group G. Proof. move=> piker sGD; apply/idP/idP=> [pifG|]; last exact: morphim_pgroup. apply: (@pgroupS _ _ (f @*^-1 (f @* G))); first by rewrite -sub_morphim_pre. -by rewrite /pgroup card_morphpre ?morphimS // pnat_mul; exact/andP. +by rewrite /pgroup card_morphpre ?morphimS // pnat_mul; apply/andP. Qed. Lemma morphim_p_index pi G H : @@ -760,7 +756,7 @@ Qed. Lemma morphim_Hall G H : H \subset D -> Hall G H -> Hall (f @* G) (f @* H). Proof. -by move=> sHD /HallP[pi piH]; apply: (@pHall_Hall _ pi); exact: morphim_pHall. +by move=> sHD /HallP[pi piH]; apply: (@pHall_Hall _ pi); apply: morphim_pHall. Qed. Lemma morphim_pSylow p G P : @@ -768,7 +764,7 @@ Lemma morphim_pSylow p G P : Proof. exact: morphim_pHall. Qed. Lemma morphim_p_group P : p_group P -> p_group (f @* P). -Proof. by move/morphim_pgroup; exact: pgroup_p. Qed. +Proof. by move/morphim_pgroup; apply: pgroup_p. Qed. Lemma morphim_Sylow G P : P \subset D -> Sylow G P -> Sylow (f @* G) (f @* P). Proof. @@ -776,12 +772,12 @@ by move=> sPD /andP[pP hallP]; rewrite /Sylow morphim_p_group // morphim_Hall. Qed. Lemma morph_p_elt pi x : x \in D -> pi.-elt x -> pi.-elt (f x). -Proof. by move=> Dx; apply: pnat_dvd; exact: morph_order. Qed. +Proof. by move=> Dx; apply: pnat_dvd; apply: morph_order. Qed. Lemma morph_constt pi x : x \in D -> f x.`_pi = (f x).`_pi. Proof. move=> Dx; rewrite -{2}(consttC pi x) morphM ?groupX //. -rewrite consttM; last by rewrite !morphX //; exact: commuteX2. +rewrite consttM; last by rewrite !morphX //; apply: commuteX2. have: pi.-elt (f x.`_pi) by rewrite morph_p_elt ?groupX ?p_elt_constt //. have: pi^'.-elt (f x.`_pi^') by rewrite morph_p_elt ?groupX ?p_elt_constt //. by move/constt1P->; move/constt_p_elt->; rewrite mulg1. @@ -817,7 +813,7 @@ Lemma ltn_log_quotient : Proof. move=> pG ntH sHG; apply: contraLR (ltn_quotient ntH sHG); rewrite -!leqNgt. rewrite {2}(card_pgroup pG) {2}(card_pgroup (morphim_pgroup _ pG)). -by case: (posnP p) => [-> //|]; exact: leq_pexp2l. +by case: (posnP p) => [-> //|]; apply: leq_pexp2l. Qed. End Pquotient. @@ -883,7 +879,7 @@ Canonical pcore_mod_group pi B : {group gT} := Definition pseries := foldr pcore_mod 1 (rev pis). Lemma pseries_group_set : group_set pseries. -Proof. rewrite /pseries; case: rev => [|pi1 pi1']; exact: groupP. Qed. +Proof. by rewrite /pseries; case: rev => [|pi1 pi1']; apply: groupP. Qed. Canonical pseries_group : {group gT} := group pseries_group_set. @@ -906,7 +902,7 @@ Lemma pcore_psubgroup G : pi.-subgroup(G) 'O_pi(G). Proof. have [M maxM _]: {M | [max M | pi.-subgroup(G) M] & 1%G \subset M}. by apply: maxgroup_exists; rewrite /psubgroup sub1G pgroup1. -have sOM: 'O_pi(G) \subset M by exact: bigcap_inf. +have sOM: 'O_pi(G) \subset M by apply: bigcap_inf. have /andP[piM sMG] := maxgroupp maxM. by rewrite /psubgroup (pgroupS sOM) // (subset_trans sOM). Qed. @@ -918,7 +914,7 @@ Lemma pcore_sub G : 'O_pi(G) \subset G. Proof. by case/andP: (pcore_psubgroup G). Qed. Lemma pcore_sub_Hall G H : pi.-Hall(G) H -> 'O_pi(G) \subset H. -Proof. by move/Hall_max=> maxH; exact: bigcap_inf. Qed. +Proof. by move/Hall_max=> maxH; apply: bigcap_inf. Qed. Lemma pcore_max G H : pi.-group H -> H <| G -> H \subset 'O_pi(G). Proof. @@ -952,11 +948,11 @@ Qed. Lemma sub_Hall_pcore G K : pi.-Hall(G) 'O_pi(G) -> K \subset G -> (K \subset 'O_pi(G)) = pi.-group K. -Proof. by move=> hallGpi; exact: sub_normal_Hall (pcore_normal G). Qed. +Proof. by move=> hallGpi; apply: sub_normal_Hall (pcore_normal G). Qed. Lemma mem_Hall_pcore G x : pi.-Hall(G) 'O_pi(G) -> x \in G -> (x \in 'O_pi(G)) = pi.-elt x. -Proof. move=> hallGpi; exact: mem_normal_Hall (pcore_normal G). Qed. +Proof. by move=> hallGpi; apply: mem_normal_Hall (pcore_normal G). Qed. Lemma sdprod_Hall_pcoreP H G : pi.-Hall(G) 'O_pi(G) -> reflect ('O_pi(G) ><| H = G) (pi^'.-Hall(G) H). @@ -986,14 +982,14 @@ Lemma morphim_pcore pi : GFunctor.pcontinuous (pcore pi). Proof. move=> gT rT D G f; apply/bigcapsP=> M /normal_sub_max_pgroup; apply. by rewrite morphim_pgroup ?pcore_pgroup. -apply: morphim_normal; exact: pcore_normal. +by apply: morphim_normal; apply: pcore_normal. Qed. Lemma pcoreS pi gT (G H : {group gT}) : H \subset G -> H :&: 'O_pi(G) \subset 'O_pi(H). Proof. move=> sHG; rewrite -{2}(setIidPl sHG). -do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom; exact: morphim_pcore. +by do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom; apply: morphim_pcore. Qed. Canonical pcore_igFun pi := [igFun by pcore_sub pi & morphim_pcore pi]. @@ -1009,17 +1005,12 @@ Variable F : GFunctor.pmap. Lemma pcore_mod_sub pi gT (G : {group gT}) : pcore_mod G pi (F _ G) \subset G. Proof. -have nFD := gFnorm F G; rewrite sub_morphpre_im ?pcore_sub //=. - by rewrite ker_coset_prim subIset // gen_subG gFsub. -by apply: subset_trans (pcore_sub _ _) _; apply: morphimS. +by rewrite sub_morphpre_im ?gFsub_trans ?morphimS ?gFnorm //= ker_coset gFsub. Qed. Lemma quotient_pcore_mod pi gT (G : {group gT}) (B : {set gT}) : pcore_mod G pi B / B = 'O_pi(G / B). -Proof. -apply: morphpreK; apply: subset_trans (pcore_sub _ _) _. -by rewrite /= /quotient -morphimIdom morphimS ?subsetIl. -Qed. +Proof. exact/morphpreK/gFsub_trans/morphim_sub. Qed. Lemma morphim_pcore_mod pi gT rT (D G : {group gT}) (f : {morphism D >-> rT}) : f @* pcore_mod G pi (F _ G) \subset pcore_mod (f @* G) pi (F _ (f @* G)). @@ -1111,7 +1102,7 @@ Qed. Lemma pseries_pop2 pi1 pi2 gT (G : {group gT}) : 'O_pi1(G) = 1 -> 'O_{pi1, pi2}(G) = 'O_pi2(G). -Proof. by move/pseries_pop->; exact: pseries1. Qed. +Proof. by move/pseries_pop->; apply: pseries1. Qed. Lemma pseries_sub_catl pi1s pi2s gT (G : {group gT}) : pseries pi1s G \subset pseries (pi1s ++ pi2s) G. @@ -1126,9 +1117,7 @@ Proof. by rewrite pseries_rcons quotient_pcore_mod. Qed. Lemma pseries_norm2 pi1s pi2s gT (G : {group gT}) : pseries pi2s G \subset 'N(pseries pi1s G). -Proof. -apply: subset_trans (normal_norm (pseries_normal pi1s G)); exact: pseries_sub. -Qed. +Proof. by rewrite gFsub_trans ?gFnorm. Qed. Lemma pseries_sub_catr pi1s pi2s gT (G : {group gT}) : pseries pi2s G \subset pseries (pi1s ++ pi2s) G. @@ -1177,7 +1166,7 @@ rewrite /= cat_rcons -(IHpi (pi :: pi2s)) {1}quotient_pseries IHpi. apply/eqP; rewrite quotient_pseries eqEsubset !pcore_max ?pcore_pgroup //=. rewrite -quotient_pseries morphim_normal // /(_ <| _) pseries_norm2. by rewrite -cat_rcons pseries_sub_catl. -by rewrite (char_normal_trans (pcore_char _ _)) ?quotient_normal ?gFnormal. +by rewrite gFnormal_trans ?quotient_normal ?gFnormal. Qed. Lemma pseries_char_catl pi1s pi2s gT (G : {group gT}) : @@ -1197,8 +1186,7 @@ rewrite /= -Epis {1}quotient_pseries Epis quotient_pseries. apply/eqP; rewrite eqEsubset !pcore_max ?pcore_pgroup //=. rewrite -quotient_pseries morphim_normal // /(_ <| _) pseries_norm2. by rewrite pseries_sub_catr. -apply: char_normal_trans (pcore_char pi _) (morphim_normal _ _). -exact: pseries_normal. +by rewrite gFnormal_trans ?morphim_normal ?gFnormal. Qed. Lemma pseries_char_catr pi1s pi2s gT (G : {group gT}) : @@ -1208,12 +1196,11 @@ Proof. by rewrite -(pseries_catr_id pi1s pi2s G) pseries_char. Qed. Lemma pcore_modp pi gT (G H : {group gT}) : H <| G -> pi.-group H -> pcore_mod G pi H = 'O_pi(G). Proof. -move=> nsHG piH; apply/eqP; rewrite eqEsubset andbC. -have nHG := normal_norm nsHG; have sOG := subset_trans (pcore_sub pi _). -rewrite -sub_morphim_pre ?(sOG, morphim_pcore) // pcore_max //. - rewrite -(pquotient_pgroup piH) ?subsetIl //. - by rewrite quotient_pcore_mod pcore_pgroup. -by rewrite -{2}(quotientGK nsHG) morphpre_normal ?pcore_normal ?sOG ?morphimS. +move=> nsHG piH; have nHG := normal_norm nsHG; apply/eqP. +rewrite eqEsubset andbC -sub_morphim_pre ?(gFsub_trans, morphim_pcore) //=. +rewrite -[G in 'O_pi(G)](quotientGK nsHG) pcore_max //. + by rewrite -(pquotient_pgroup piH) ?subsetIl // cosetpreK pcore_pgroup. +by rewrite morphpre_normal ?gFnormal ?gFsub_trans ?morphim_sub. Qed. Lemma pquotient_pcore pi gT (G H : {group gT}) : @@ -1221,9 +1208,7 @@ Lemma pquotient_pcore pi gT (G H : {group gT}) : Proof. by move=> nsHG piH; rewrite -quotient_pcore_mod pcore_modp. Qed. Lemma trivg_pcore_quotient pi gT (G : {group gT}) : 'O_pi(G / 'O_pi(G)) = 1. -Proof. -by rewrite pquotient_pcore ?pcore_normal ?pcore_pgroup // trivg_quotient. -Qed. +Proof. by rewrite pquotient_pcore ?gFnormal ?pcore_pgroup ?trivg_quotient. Qed. Lemma pseries_rcons_id pis pi gT (G : {group gT}) : pseries (rcons (rcons pis pi) pi) G = pseries (rcons pis pi) G. @@ -1246,11 +1231,11 @@ Lemma sub_in_pcore pi rho G : Proof. move=> pi_sub_rho; rewrite pcore_max ?pcore_normal //. apply: sub_in_pnat (pcore_pgroup _ _) => p. -move/(piSg (pcore_sub _ _)); exact: pi_sub_rho. +by move/(piSg (pcore_sub _ _)); apply: pi_sub_rho. Qed. Lemma sub_pcore pi rho G : {subset pi <= rho} -> 'O_pi(G) \subset 'O_rho(G). -Proof. by move=> pi_sub_rho; exact: sub_in_pcore (in1W pi_sub_rho). Qed. +Proof. by move=> pi_sub_rho; apply: sub_in_pcore (in1W pi_sub_rho). Qed. Lemma eq_in_pcore pi rho G : {in \pi(G), pi =i rho} -> 'O_pi(G) = 'O_rho(G). Proof. @@ -1259,31 +1244,30 @@ by rewrite !sub_in_pcore // => p /eq_pi_rho->. Qed. Lemma eq_pcore pi rho G : pi =i rho -> 'O_pi(G) = 'O_rho(G). -Proof. by move=> eq_pi_rho; exact: eq_in_pcore (in1W eq_pi_rho). Qed. +Proof. by move=> eq_pi_rho; apply: eq_in_pcore (in1W eq_pi_rho). Qed. Lemma pcoreNK pi G : 'O_pi^'^'(G) = 'O_pi(G). -Proof. by apply: eq_pcore; exact: negnK. Qed. +Proof. by apply: eq_pcore; apply: negnK. Qed. Lemma eq_p'core pi rho G : pi =i rho -> 'O_pi^'(G) = 'O_rho^'(G). -Proof. by move/eq_negn; exact: eq_pcore. Qed. +Proof. by move/eq_negn; apply: eq_pcore. Qed. Lemma sdprod_Hall_p'coreP pi H G : pi^'.-Hall(G) 'O_pi^'(G) -> reflect ('O_pi^'(G) ><| H = G) (pi.-Hall(G) H). -Proof. by rewrite -(pHallNK pi G H); exact: sdprod_Hall_pcoreP. Qed. +Proof. by rewrite -(pHallNK pi G H); apply: sdprod_Hall_pcoreP. Qed. Lemma sdprod_p'core_HallP pi H G : pi.-Hall(G) H -> reflect ('O_pi^'(G) ><| H = G) (pi^'.-Hall(G) 'O_pi^'(G)). -Proof. by rewrite -(pHallNK pi G H); exact: sdprod_pcore_HallP. Qed. +Proof. by rewrite -(pHallNK pi G H); apply: sdprod_pcore_HallP. Qed. Lemma pcoreI pi rho G : 'O_[predI pi & rho](G) = 'O_pi('O_rho(G)). Proof. apply/eqP; rewrite eqEsubset !pcore_max //. -- rewrite /pgroup pnatI [pnat _ _]pcore_pgroup. - exact: pgroupS (pcore_sub _ _) (pcore_pgroup _ _). -- exact: char_normal_trans (pcore_char _ _) (pcore_normal _ _). -- by apply: sub_in_pnat (pcore_pgroup _ _) => p _ /andP[]. +- by rewrite /pgroup pnatI -!pgroupE !(pcore_pgroup, pgroupS (pcore_sub pi _)). +- by rewrite !gFnormal_trans. +- by apply: sub_pgroup (pcore_pgroup _ _) => p /andP[]. apply/andP; split; first by apply: sub_pcore => p /andP[]. -by rewrite (subset_trans (pcore_sub _ _)) ?gFnorm. +by rewrite gFnorm_trans ?normsG ?gFsub. Qed. Lemma bigcap_p'core pi G : @@ -1298,7 +1282,7 @@ apply/eqP; rewrite eqEsubset subsetI pcore_sub pcore_max /=. rewrite (dvdn_trans qGpi') ?cardSg ?subIset //= orbC. by rewrite (bigcap_inf (Ordinal ltqG)). rewrite /normal subsetIl normsI ?normG // norms_bigcap //. -by apply/bigcapsP => p _; exact: gFnorm. +by apply/bigcapsP => p _; apply: gFnorm. Qed. Lemma coprime_pcoreC (rT : finGroupType) pi G (R : {group rT}) : @@ -1310,10 +1294,9 @@ Proof. by rewrite coprime_TIg ?coprime_pcoreC. Qed. Lemma pcore_setI_normal pi G H : H <| G -> 'O_pi(G) :&: H = 'O_pi(H). Proof. -move=> nsHG; apply/eqP; rewrite eqEsubset subsetI pcore_sub. -rewrite !pcore_max ?(pgroupS (subsetIl _ H)) ?pcore_pgroup //=. - exact: char_normal_trans (pcore_char pi H) nsHG. -by rewrite setIC (normalGI (normal_sub nsHG)) ?pcore_normal. +move=> nsHG; apply/eqP; rewrite eqEsubset subsetI pcore_sub setIC. +rewrite !pcore_max ?(pgroupS (subsetIr H _)) ?pcore_pgroup ?gFnormal_trans //=. +by rewrite norm_normalI ?gFnorm_trans ?normsG ?normal_sub. Qed. End EqPcore. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 06ab30e..2d07bba 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -1,12 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype tuple finset. -From mathcomp.fingroup -Require Import fingroup action. -Require Import gseries. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat. +From mathcomp +Require Import div seq fintype tuple finset. +From mathcomp +Require Import fingroup action gseries. (******************************************************************************) (* n-transitive and primitive actions: *) @@ -65,7 +64,7 @@ move=> Sx trG; rewrite /primitive trG negb_exists. apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q]. split=> [|H sCH sHG]; first exact: subsetIl. pose X := orbit to H x; pose Q := orbit (to^*)%act G X. - have Xx: x \in X by exact: orbit_refl. + have Xx: x \in X by apply: orbit_refl. have defH: 'N_(G)(X | to) = H. have trH: [transitive H, on X | to] by apply/imsetP; exists x. have sHN: H \subset 'N_G(X | to) by rewrite subsetI sHG atrans_acts. @@ -79,13 +78,13 @@ apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q]. - rewrite card_orbit astab1_set defH -(@ltn_pmul2l #|H|) ?Lagrange // muln1. rewrite oHG -(@ltn_pmul2l #|H|) ?Lagrange // -(card_orbit_stab to G x). by rewrite -(atransP trG x Sx) mulnC card_orbit ltn_pmul2r. - - by apply/actsP=> a Ga Y; apply: orbit_transr; exact: mem_orbit. + - by apply/actsP=> a Ga Y; apply/orbit_transl/mem_orbit. apply/and3P; split; last 1 first. - rewrite orbit_sym; apply/imsetP=> [[a _]] /= defX. by rewrite defX /setact imset0 inE in Xx. - apply/eqP/setP=> y; apply/bigcupP/idP=> [[_ /imsetP[a Ga ->]] | Sy]. case/imsetP=> _ /imsetP[b Hb ->] ->. - by rewrite !(actsP (atrans_acts trG)) //; exact: subsetP Hb. + by rewrite !(actsP (atrans_acts trG)) //; apply: subsetP Hb. case: (atransP2 trG Sx Sy) => a Ga ->. by exists ((to^*)%act X a); apply: mem_imset; rewrite // orbit_refl. apply/trivIsetP=> _ _ /imsetP[a Ga ->] /imsetP[b Gb ->]. @@ -179,7 +178,7 @@ Lemma n_act_dtuple t a : Proof. move/astabsP=> toSa /dtuple_onP[t_inj St]; apply/dtuple_onP. split=> [i j | i]; rewrite !tnth_map ?[_ \in S]toSa //. -by move/act_inj; exact: t_inj. +by move/act_inj; apply: t_inj. Qed. End NTransitive. @@ -202,7 +201,7 @@ Variables (gT : finGroupType) (sT : finType). Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}). Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t -> #|t| = n. -Proof. by move/card_uniqP->; exact: size_tuple. Qed. +Proof. by move/card_uniqP->; apply: size_tuple. Qed. Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple]. Proof. exact: tuple0. Qed. @@ -223,7 +222,7 @@ Qed. Lemma dtuple_on_subset n (S1 S2 : {set sT}) t : S1 \subset S2 -> t \in n.-dtuple(S1) -> t \in n.-dtuple(S2). -Proof. by move=> sS12; rewrite !inE => /andP[-> /subset_trans]; exact. Qed. +Proof. by move=> sS12; rewrite !inE => /andP[-> /subset_trans]; apply. Qed. Lemma n_act_add n x (t : n.-tuple sT) a : n_act to [tuple of x :: t] a = [tuple of to x a :: n_act to t a]. @@ -254,7 +253,7 @@ case/and3P=> Sx ntx dt; set xt := [tuple of _] => tr_xt. apply/imsetP; exists t => //. apply/setP=> u; apply/idP/imsetP=> [du | [a Ga ->{u}]]. case: (ext_t u du) => y; rewrite tr_xt. - by case/imsetP=> a Ga [_ def_u]; exists a => //; exact: val_inj. + by case/imsetP=> a Ga [_ def_u]; exists a => //; apply: val_inj. have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt mem_imset. by rewrite n_act_add dtuple_on_add; case/and3P. Qed. @@ -267,14 +266,14 @@ have trdom1 x: ([tuple x] \in 1.-dtuple(S)) = (x \in S). move=> m_gt0 /(ntransitive_weak m_gt0) {m m_gt0}. case/imsetP; case/tupleP=> x t0; rewrite {t0}(tuple0 t0) trdom1 => Sx trx. apply/imsetP; exists x => //; apply/setP=> y; rewrite -trdom1 trx. -apply/imsetP/imsetP=> [[a ? [->]]|[a ? ->]]; exists a => //; exact: val_inj. +by apply/imsetP/imsetP=> [[a ? [->]]|[a ? ->]]; exists a => //; apply: val_inj. Qed. Lemma ntransitive_primitive m : 1 < m -> [transitive^m G, on S | to] -> [primitive G, on S | to]. Proof. move=> lt1m /(ntransitive_weak lt1m) {m lt1m}tr2G. -have trG: [transitive G, on S | to] by exact: ntransitive1 tr2G. +have trG: [transitive G, on S | to] by apply: ntransitive1 tr2G. have [x Sx _]:= imsetP trG; rewrite (trans_prim_astab Sx trG). apply/maximal_eqP; split=> [|H]; first exact: subsetIl; rewrite subEproper. case/predU1P; first by [left]; case/andP=> sCH /subsetPn[a Ha nCa] sHG. @@ -287,7 +286,7 @@ rewrite eqEsubset acts_sub_orbit // Sy andbT; apply/subsetP=> z Sz. have [-> | zx] := eqVneq z x; first by rewrite orbit_sym mem_orbit. pose ty := [tuple y; x]; pose tz := [tuple z; x]. have [Sty Stz]: ty \in 2.-dtuple(S) /\ tz \in 2.-dtuple(S). - rewrite !inE !memtE !subset_all /= !mem_seq1 !andbT; split; exact/and3P. + by rewrite !inE !memtE !subset_all /= !mem_seq1 !andbT; split; apply/and3P. case: (atransP2 tr2G Sty Stz) => b Gb [->] /esym/astab1P cxb. by rewrite mem_orbit // (subsetP sCH) // inE Gb. Qed. @@ -310,12 +309,12 @@ case/and3P=> Sx1 nt1x1 dt1 trt1; have Gtr1 := ntransitive1 (ltn0Sn _) Gtr. case: (atransP2 Gtr1 Sx1 Sx) => // a Ga x1ax. pose t := n_act to t1 a. have dxt: [tuple of x :: t] \in m.+1.-dtuple(S). - rewrite trt1 x1ax; apply/imsetP; exists a => //; exact: val_inj. + by rewrite trt1 x1ax; apply/imsetP; exists a => //; apply: val_inj. apply/imsetP; exists t; first by rewrite dtuple_on_add_D1 Sx in dxt. apply/setP=> t2; apply/idP/imsetP => [dt2|[b]]. have: [tuple of x :: t2] \in dtuple_on _ S by rewrite dtuple_on_add_D1 Sx. case/(atransP2 Gtr dxt)=> b Gb [xbx tbt2]. - exists b; [rewrite inE Gb; exact/astab1P | exact: val_inj]. + by exists b; [rewrite inE Gb; apply/astab1P | apply: val_inj]. case/setIP=> Gb /astab1P xbx ->{t2}. rewrite n_act_dtuple //; last by rewrite dtuple_on_add_D1 Sx in dxt. apply/astabsP=> y; rewrite !inE -{1}xbx (inj_eq (act_inj _ _)). diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index abaa2a5..e347a74 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -1,16 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype finset bigop prime. -From mathcomp.fingroup -Require Import fingroup morphism automorphism quotient action gproduct. -From mathcomp.algebra -Require Import ssralg poly ssrnum ssrint rat. -From mathcomp.algebra -Require Import polydiv finalg zmodp matrix mxalgebra vector cyclic. -Require Import commutator pgroup center nilpotent. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div fintype prime. +From mathcomp +Require Import bigop finset fingroup morphism automorphism quotient action. +From mathcomp +Require Import cyclic gproduct gfunctor commutator pgroup center nilpotent. (******************************************************************************) (* The Sylow theorem and its consequences, including the Frattini argument, *) @@ -68,11 +63,11 @@ Lemma pcore_sub_astab_irr G M : 'O_p(G) \subset 'C_G(M | to). Proof. move=> pM sMR /mingroupP[/andP[ntM nMG] minM]. -have [sGpG nGpG]:= andP (pcore_normal p G). -have sGD := acts_dom nMG; have sGpD := subset_trans sGpG sGD. +have /andP[sGpG nGpG]: 'O_p(G) <| G := gFnormal _ G. +have sGD := acts_dom nMG; have sGpD: 'O_p(G) \subset D := gFsub_trans _ sGD. rewrite subsetI sGpG -gacentC //=; apply/setIidPl; apply: minM (subsetIl _ _). rewrite nontrivial_gacent_pgroup ?pcore_pgroup //=; last first. - by split; rewrite ?(subset_trans sGpG). + by split; rewrite ?gFsub_trans. by apply: subset_trans (acts_subnorm_subgacent sGpD nMG); rewrite subsetI subxx. Qed. @@ -108,7 +103,7 @@ have S_pG P: P \in S -> P \subset G /\ p.-group P. have SmaxN P Q: Q \in S -> Q \subset 'N(P) -> maxp 'N_G(P) Q. rewrite inE => /maxgroupP[/andP[sQG pQ] maxQ] nPQ. apply/maxgroupP; rewrite /psubgroup subsetI sQG nPQ. - by split=> // R; rewrite subsetI -andbA andbCA => /andP[_]; exact: maxQ. + by split=> // R; rewrite subsetI -andbA andbCA => /andP[_]; apply: maxQ. have nrmG P: P \subset G -> P <| 'N_G(P). by move=> sPG; rewrite /normal subsetIr subsetI sPG normG. have sylS P: P \in S -> p.-Sylow('N_G(P)) P. @@ -123,7 +118,7 @@ have{defCS} oG_mod: {in S &, forall P Q, #|oG P| = (Q \in oG P) %[mod p]}. move=> P Q S_P S_Q; have [sQG pQ] := S_pG _ S_Q. have soP_S: oG P \subset S by rewrite acts_sub_orbit. have /pgroup_fix_mod-> //: [acts Q, on oG P | 'JG]. - apply/actsP=> x /(subsetP sQG) Gx R; apply: orbit_transr. + apply/actsP=> x /(subsetP sQG) Gx R; apply: orbit_transl. exact: mem_orbit. rewrite -{1}(setIidPl soP_S) -setIA defCS // (cardsD1 Q) setDE. by rewrite -setIA setICr setI0 cards0 addn0 inE set11 andbT. @@ -206,7 +201,7 @@ Lemma card_Syl P : p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)|. Proof. by case: Sylow's_theorem P. Qed. Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|. -Proof. by case Sylow_exists => P /card_Syl->; exact: dvdn_indexg. Qed. +Proof. by case Sylow_exists => P /card_Syl->; apply: dvdn_indexg. Qed. Lemma card_Syl_mod : prime p -> #|'Syl_p(G)| %% p = 1%N. Proof. by case Sylow's_theorem. Qed. @@ -262,13 +257,13 @@ Qed. Lemma p2group_abelian P : p.-group P -> logn p #|P| <= 2 -> abelian P. Proof. move=> pP lePp2; pose Z := 'Z(P); have sZP: Z \subset P := center_sub P. -case: (eqVneq Z 1); first by move/(trivg_center_pgroup pP)->; exact: abelian1. +case: (eqVneq Z 1); first by move/(trivg_center_pgroup pP)->; apply: abelian1. case/(pgroup_pdiv (pgroupS sZP pP)) => p_pr _ [k oZ]. apply: cyclic_center_factor_abelian. -case: (eqVneq (P / Z) 1) => [-> |]; first exact: cyclic1. +have [->|] := eqVneq (P / Z) 1; first exact: cyclic1. have pPq := quotient_pgroup 'Z(P) pP; case/(pgroup_pdiv pPq) => _ _ [j oPq]. rewrite prime_cyclic // oPq; case: j oPq lePp2 => //= j. -rewrite card_quotient ?gfunctor.gFnorm //. +rewrite card_quotient ?gFnorm //. by rewrite -(Lagrange sZP) lognM // => ->; rewrite oZ !pfactorK ?addnS. Qed. @@ -343,7 +338,7 @@ Proof. move=> defG nHG coKR; apply/eqP; rewrite eqEcard mulG_subG /= -defG. rewrite !setSI ?mulG_subl ?mulG_subr //=. rewrite coprime_cardMg ?(coKR, coprimeSg (subsetIl _ _), coprime_sym) //=. -pose pi := \pi(K); have piK: pi.-group K by exact: pgroup_pi. +pose pi := \pi(K); have piK: pi.-group K by apply: pgroup_pi. have pi'R: pi^'.-group R by rewrite /pgroup -coprime_pi' /=. have [hallK hallR] := coprime_mulpG_Hall defG piK pi'R. have nsHG: H :&: G <| G by rewrite /normal subsetIr normsI ?normG. @@ -372,7 +367,7 @@ by rewrite ltn_Pdiv // ltnNge -trivg_card_le1. Qed. Lemma pgroup_sol p P : p.-group P -> solvable P. -Proof. by move/pgroup_nil; exact: nilpotent_sol. Qed. +Proof. by move/pgroup_nil; apply: nilpotent_sol. Qed. Lemma small_nil_class G : nil_class G <= 5 -> nilpotent G. Proof. @@ -404,10 +399,10 @@ have nHN: H <| 'N_G(H) by rewrite normal_subnorm. have{maxH} hallH: pi.-Hall('N_G(H)) H. apply: normal_max_pgroup_Hall => //; apply/maxgroupP. rewrite /psubgroup normal_sub // piH; split=> // K. - by rewrite subsetI -andbA andbCA => /andP[_]; exact: maxH. -rewrite /normal sHG; apply/setIidPl; symmetry. -apply: nilpotent_sub_norm; rewrite ?subsetIl ?setIS //=. -by rewrite char_norms // -{1}(normal_Hall_pcore hallH) // pcore_char. + by rewrite subsetI -andbA andbCA => /andP[_ /maxH]. +rewrite /normal sHG; apply/setIidPl/esym. +apply: nilpotent_sub_norm; rewrite ?subsetIl ?setIS //= char_norms //. +by congr (_ \char _): (pcore_char pi 'N_G(H)); apply: normal_Hall_pcore. Qed. Lemma nilpotent_Hall_pcore pi G H : @@ -430,12 +425,12 @@ Qed. Lemma nilpotent_pcoreC pi G : nilpotent G -> 'O_pi(G) \x 'O_pi^'(G) = G. Proof. move=> nilG; have trO: 'O_pi(G) :&: 'O_pi^'(G) = 1. - by apply: coprime_TIg; apply: (@pnat_coprime pi); exact: pcore_pgroup. + by apply: coprime_TIg; apply: (@pnat_coprime pi); apply: pcore_pgroup. rewrite dprodE //. apply/eqP; rewrite eqEcard mul_subG ?pcore_sub // (TI_cardMg trO). by rewrite !(card_Hall (nilpotent_pcore_Hall _ _)) // partnC ?leqnn. rewrite (sameP commG1P trivgP) -trO subsetI commg_subl commg_subr. -by rewrite !(subset_trans (pcore_sub _ _)) ?normal_norm ?pcore_normal. +by rewrite !gFsub_trans ?gFnorm. Qed. Lemma sub_nilpotent_cent2 H K G : @@ -485,7 +480,7 @@ elim: c => // c IHc in gT P def_c pP *; set e := logn p _. have nilP := pgroup_nil pP; have sZP := center_sub P. have [e_le2 | e_gt2] := leqP e 2. by rewrite -def_c leq_max nil_class1 (p2group_abelian pP). -have pPq: p.-group (P / 'Z(P)) by exact: quotient_pgroup. +have pPq: p.-group (P / 'Z(P)) by apply: quotient_pgroup. rewrite -(subnKC e_gt2) ltnS (leq_trans (IHc _ _ _ pPq)) //. by rewrite nil_class_quotient_center ?def_c. rewrite geq_max /= -add1n -leq_subLR -subn1 -subnDA -subSS leq_sub2r //. @@ -534,7 +529,7 @@ have /cyclicP[x' def_p']: cyclic 'O_p^'(G). by have:= pcore_pgroup p^' G; rewrite def_p' /pgroup p'natE ?pG. apply/cyclicP; exists (x * x'); rewrite -{}defG def_p def_p' cycleM //. by red; rewrite -(centsP Cpp') // (def_p, def_p') cycle_id. -rewrite /order -def_p -def_p' (@pnat_coprime p) //; exact: pcore_pgroup. +by rewrite /order -def_p -def_p' (@pnat_coprime p) //; apply: pcore_pgroup. Qed. End Zgroups. @@ -582,8 +577,8 @@ have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. have sEG: <<E>> \subset G by rewrite gen_subG class_subG. -have nEG: G \subset 'N(E) by exact: class_norm. -have Ex: x \in E by exact: class_refl. +have nEG: G \subset 'N(E) by apply: class_norm. +have Ex: x \in E by apply: class_refl. have [P Px sylP]: exists2 P : {group gT}, x \in P & p.-Sylow(<<E>>) P. have sxxE: <<[set x; x]>> \subset <<E>> by rewrite genS // setUid sub1set. have{sxxE} [P sylP sxxP] := Sylow_superset sxxE (pE _ _ Ex Ex). @@ -600,14 +595,14 @@ have{Ex Px}: P_D [set x]. case/(@maxset_exists _ P_D)=> D /maxsetP[]; rewrite {P_yD P_D}/=. rewrite subsetI sub1set -andbA => /and3P[sDP sDE /existsP[y0]]. set B := _ |: D; rewrite inE -andbA => /and3P[Py0 Ey0 pB] maxD Dx. -have sDgE: D \subset <<E>> by exact: sub_gen. -have sDG: D \subset G by exact: subset_trans sEG. +have sDgE: D \subset <<E>> by apply: sub_gen. +have sDG: D \subset G by apply: subset_trans sEG. have sBE: B \subset E by rewrite subUset sub1set Ey0. -have sBG: <<B>> \subset G by exact: subset_trans (genS _) sEG. +have sBG: <<B>> \subset G by apply: subset_trans (genS _) sEG. have sDB: D \subset B by rewrite subsetUr. have defD: D :=: P :&: <<B>> :&: E. apply/eqP; rewrite eqEsubset ?subsetI sDP sDE sub_gen //=. - apply/setUidPl; apply: maxD; last exact: subsetUl. + apply/setUidPl; apply: maxD; last apply: subsetUl. rewrite subUset subsetI sDP sDE setIAC subsetIl. apply/existsP; exists y0; rewrite inE Py0 Ey0 /= setUA -/B. by rewrite -[<<_>>]joing_idl joingE setKI genGid. @@ -645,7 +640,7 @@ have [y1 Ny1 Py1]: exists2 y1, y1 \in 'N_E(D) & y1 \notin P. have [y2 Ny2 Dy2]: exists2 y2, y2 \in 'N_(P :&: E)(D) & y2 \notin D. case sNN: ('N_P('N_P(D)) \subset 'N_P(D)). have [z /= Ez sEzP] := Sylow_Jsub sylP (genS sBE) pB. - have Gz: z \in G by exact: subsetP Ez. + have Gz: z \in G by apply: subsetP Ez. have /subsetPn[y Bzy Dy]: ~~ (B :^ z \subset D). apply/negP; move/subset_leq_card; rewrite cardJg cardsU1. by rewrite {1}defD 2!inE (negPf Py0) ltnn. @@ -657,7 +652,7 @@ have [y2 Ny2 Dy2]: exists2 y2, y2 \in 'N_(P :&: E)(D) & y2 \notin D. case/subsetPn=> y Dzy Dy; exists y => //; apply: subsetP Dzy. rewrite -setIA setICA subsetI sub_conjg (normsP nEG) ?groupV //. by rewrite sDE -(normP NNz); rewrite conjSg subsetI sDP. - apply: subsetP Pz; exact: (subset_trans (pHall_sub sylP)). + by apply: subsetP Pz; apply: (subset_trans (pHall_sub sylP)). suff{Dy2} Dy2D: y2 |: D = D by rewrite -Dy2D setU11 in Dy2. apply: maxD; last by rewrite subsetUr. case/setIP: Ny2 => PEy2 Ny2; case/setIP: Ny1 => Ey1 Ny1. |
