diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index b3f4c2e..c0d9c5e 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -469,192 +469,3 @@ have := EF; rewrite rs'E -aimg_adjoin_seq => /eqP. by rewrite eq_limg_ker0 ?AHom_lker0// => /eqP. Qed. -(********************) -(* package solvable *) -(********************) - -(*******************) -(* new sym library *) -(*******************) - -Lemma gen_tperm_step n (k : 'I_n.+2) : coprime n.+2 k -> - <<[set tperm i (i + k) | i : 'I_n.+2]>>%g = [set: 'S_n.+2]. -Proof. -rewrite -unitZpE// natr_Zp => k_unit. -apply/eqP; rewrite eqEsubset subsetT/= -(gen_tperm 0)/= gen_subG. -apply/subsetP => s /imsetP[/= i _ ->]. -rewrite -[i](mulVKr k_unit) -[_ * i]natr_Zp mulr_natr. -elim: (val _) => //= {i} [|[|i] IHi]; first by rewrite tperm1 group1. - by rewrite mulrSr mem_gen//; apply/imsetP; exists 0. -have [->|kS2N0] := eqVneq (k *+ i.+2) 0; first by rewrite tperm1 group1. -have kSSneqkS : k *+ i.+2 != k *+ i.+1. - rewrite -subr_eq0 -mulrnBr// subSnn mulr1n. - by apply: contraTneq k_unit => ->; rewrite unitr0. -rewrite -(@tpermJt _ (k *+ i.+1)) 1?eq_sym//. -rewrite groupJ// 1?tpermC// mulrSr 1?tpermC. -by rewrite mem_gen//; apply/imsetP; exists (k *+ i.+1). -Qed. - -Lemma gen_tpermS n : <<[set tperm i (i + 1) | i : 'I_n.+2]>>%g = [set: 'S_n.+2]. -Proof. by rewrite gen_tperm_step// coprimen1. Qed. - -Lemma perm_add1X n (j k : 'I_n.+2) : (perm (addrI 1%R) ^+ j)%g k = j + k. -Proof. by rewrite permX (eq_iter (permE _)) iter_addr natr_Zp. Qed. - -Lemma gen_tpermn_cycle n (i j : 'I_n.+2) - (c := perm (addrI 1)) : coprime n.+2 (j - i)%R -> - <<[set tperm i j ; c]>>%g = [set: 'S_n.+2]. -Proof. -move=> jBi_coprime; apply/eqP; rewrite eqEsubset subsetT/=. -rewrite -(gen_tperm_step jBi_coprime) gen_subG. -apply/subsetP => s /imsetP[/= k _ ->]. -suff -> : tperm k (k + (j - i)) = (tperm i j ^ c ^+ (k - i)%R)%g. - by rewrite groupJ ?groupX ?mem_gen ?inE ?eqxx ?orbT. -by rewrite tpermJ !perm_add1X addrNK addrAC addrA. -Qed. - -Lemma gen_tperm01_cycle n (c := perm (addrI 1)) : - <<[set tperm 0 1%R ; c]>>%g = [set: 'S_n.+2]. -Proof. by rewrite gen_tpermn_cycle// subr0 coprimen1. Qed. - -Lemma expgDzmod (gT : finGroupType) (x : gT) d (n m : 'Z_d) : (d > 0)%N -> - (#[x]%g %| d)%N -> (x ^+ (n + m)%R)%g = (x ^+ n * x ^+ m)%g. -Proof. -move=> d_gt0 xdvd; apply/eqP; rewrite -expgD eq_expg_mod_order/= modn_dvdm//. -by case: d d_gt0 {m n} xdvd => [|[|[]]]//= _; rewrite dvdn1 => /eqP->. -Qed. - -Lemma eq_expg_ord (gT : finGroupType) (x : gT) d (n m : 'I_d) : - (d <= #[x]%g)%N -> ((x ^+ m)%g == (x ^+ n)%g) = (m == n). -Proof. -by move=> d_leq; rewrite eq_expg_mod_order !modn_small// (leq_trans _ d_leq). -Qed. - -Lemma gen_tperm_cycle (X : finType) x y c : prime #|X| -> - x != y -> #[c]%g = #|X| -> - <<[set tperm x y; c]>>%g = ('Sym_X)%g. -Proof. -move=> Xprime neq_xy ord_c; apply/eqP; rewrite eqEsubset subsetT/=. -have c_gt1 : (1 < #[c]%g)%N by rewrite ord_c prime_gt1. -have cppSS : #[c]%g.-2.+2 = #|X| by rewrite ?prednK ?ltn_predRL. -pose f (i : 'Z_#[c]%g) : X := Zpm i x. -have [g fK gK] : bijective f. - apply: inj_card_bij; rewrite ?cppSS ?card_ord// /f /Zpm => i j cijx. - pose stabx := ('C_<[c]>[x | 'P])%g. - have cjix : (c ^+ (j - i)%R)%g x = x. - by apply: (@perm_inj _ (c ^+ i)%g); rewrite -permM -expgDzmod// addrNK. - have : (c ^+ (j - i)%R)%g \in stabx. - by rewrite !inE ?groupX ?mem_gen ?sub1set ?inE// ['P%act _ _]cjix eqxx. - rewrite [stabx]prime_astab// => /set1gP. - move=> /(congr1 (mulg (c ^+ i))); rewrite -expgDzmod// addrC addrNK mulg1. - by move=> /eqP; rewrite eq_expg_ord// ?cppSS ?ord_c// => /eqP->. -pose gsf s := g \o s \o f. -have gsf_inj (s : {perm X}) : injective (gsf s). - apply: inj_comp; last exact: can_inj fK. - by apply: inj_comp; [exact: can_inj gK|exact: perm_inj]. -pose fsg s := f \o s \o g. -have fsg_inj (s : {perm _}) : injective (fsg s). - apply: inj_comp; last exact: can_inj gK. - by apply: inj_comp; [exact: can_inj fK|exact: perm_inj]. -have gsf_morphic : morphic 'Sym_X (fun s => perm (gsf_inj s)). - apply/morphicP => u v _ _; apply/permP => /= i. - by rewrite !permE/= !permE /gsf /= gK permM. -pose phi := morphm gsf_morphic; rewrite /= in phi. -have phi_inj : ('injm phi)%g. - apply/subsetP => /= u /mker/=; rewrite morphmE => gsfu1. - apply/set1gP/permP=> z; have /permP/(_ (g z)) := gsfu1. - by rewrite !perm1 permE /gsf/= gK => /(can_inj gK). -have phiT : (phi @* 'Sym_X)%g = [set: {perm 'Z_#[c]%g}]. - apply/eqP; rewrite eqEsubset subsetT/=; apply/subsetP => /= u _. - apply/morphimP; exists (perm (fsg_inj u)); rewrite ?in_setT//. - by apply/permP => /= i; rewrite morphmE permE /gsf/fsg/= permE/= !fK. -have f0 : f 0 = x by rewrite /f /Zpm permX. -pose k := g y; have k_gt0 : (k > 0)%N. - by rewrite lt0n (val_eqE k 0) -(can_eq fK) eq_sym gK f0. -have phixy : phi (tperm x y) = tperm 0 k. - apply/permP => i; rewrite permE/= /gsf/=; apply: (canLR fK). - by rewrite !permE/= -f0 -[y]gK !(can_eq fK) -!fun_if. -have phic : phi c = perm (addrI 1%R). - apply/permP => i; rewrite permE /gsf/=; apply: (canLR fK). - by rewrite !permE /f /Zpm -permM addrC expgDzmod. -rewrite -(injmSK phi_inj)//= morphim_gen/= ?subsetT//= -/phi. -rewrite phiT /morphim !setTI/= -/phi imsetU1 imset_set1/= phixy phic. -suff /gen_tpermn_cycle<- : coprime #[c]%g.-2.+2 (k - 0)%R by []. -by rewrite subr0 prime_coprime ?gtnNdvd// ?cppSS. -Qed. - -(************) -(* solvable *) -(************) - -Lemma sol_setXn n (gT : 'I_n -> finGroupType) (G : forall i, {group gT i}) : - (forall i, solvable (G i)) -> solvable (setXn G). -Proof. -elim: n => [|n IHn] in gT G * => solG; first by rewrite setX0 solvable1. -pose gT' (i : 'I_n) := gT (lift ord0 i). -pose f (x : prod_group gT) : prod_group gT' := [ffun i => x (lift ord0 i)]. -have fm : morphic (setXn G) f. - apply/'forall_implyP => -[a b]; rewrite !inE/=. - by move=> /andP[/forallP aG /forallP bG]; apply/eqP/ffunP => i; rewrite !ffunE. -rewrite (@series_sol _ [group of setXn G] ('ker (morphm fm))) ?ker_normal//=. -rewrite (isog_sol (first_isog _))/=. -have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)). - apply/setP => v; rewrite !inE morphimEdom; apply/idP/forallP => /=. - move=> /imsetP[/=x]; rewrite inE => /forallP/= xG ->. - by move=> i; rewrite morphmE ffunE xG. - move=> vG; apply/imsetP. - pose w : prod_group gT := [ffun i : 'I_n.+1 => - match unliftP ord0 i with - | UnliftSome j i_eq => ecast i (gT i) (esym i_eq) (v j) - | UnliftNone i0 => 1%g - end]. - have wl i : w (lift ord0 i) = v i. - rewrite ffunE; case: unliftP => //= j elij. - have eij : i = j by case: elij; apply/val_inj. - by rewrite [elij](eq_irrelevance _ (congr1 _ eij)); case: _ / eij. - have w0 : w ord0 = 1%g by rewrite ffunE; case: unliftP. - exists w; last by apply/ffunP => i; rewrite morphmE ffunE/= wl. - rewrite inE; apply/forallP => i. - by case: (unliftP ord0 i) => [j|]->; rewrite ?wl ?w0 ?vG. -rewrite IHn ?andbT//; last by move=> i; apply: solG. -pose k (x : gT ord0) : prod_group gT := - [ffun i : 'I_n.+1 => if (ord0 =P i) is ReflectT P then ecast i (gT i) P x else 1%g]. -have km : morphic (G ord0) k. - apply/'forall_implyP => -[a b]; rewrite !inE/= => /andP[aG bG]. - apply/eqP/ffunP => i; rewrite !ffunE; case: eqP => //; rewrite ?mulg1//. - by case: _ /. -suff -> : ('ker (morphm fm) = morphm km @* G ord0)%g by rewrite morphim_sol. -apply/setP => x; rewrite morphimEdom; apply/idP/imsetP => [xker|]. - exists (x ord0). - by have := dom_ker xker; rewrite inE => /forallP/(_ ord0). - rewrite /= morphmE; apply/ffunP => i; rewrite ffunE; case: eqP => //=. - by case: _ /. - move/eqP; rewrite eq_sym; have /mker/= := xker; rewrite morphmE => /ffunP. - by case: (@unliftP _ ord0 i) => [j|] ->//= /(_ j); rewrite !ffunE. -move=> [x0 xG0 -> /=]; rewrite morphmE; apply/kerP; rewrite ?inE. - by apply/forallP => i; rewrite ffunE; case: eqP => //=; case: _ /. -by rewrite /= morphmE; apply/ffunP => i; rewrite !ffunE; case: eqP. -Qed. - -Section Perm_solvable. -Local Open Scope nat_scope. - -Variable T : finType. - -Lemma solvable_AltF : 4 < #|T| -> solvable 'Alt_T = false. -Proof. -move=> card_T; apply/negP => Alt_solvable. -have/simple_Alt5 Alt_simple := card_T. -have := simple_sol_prime Alt_solvable Alt_simple. -have lt_T n : n <= 4 -> n < #|T| by move/leq_ltn_trans; apply. -have -> : #|('Alt_T)%G| = #|T|`! %/ 2 by rewrite -card_Alt ?mulKn ?lt_T. -move/even_prime => [/eqP|]; apply/negP. - rewrite neq_ltn leq_divRL // mulnC -[2 * 3]/(3`!). - by apply/orP; right; apply/ltnW/fact_smonotone/lt_T. -by rewrite -dvdn2 dvdn_divRL dvdn_fact //=; apply/ltnW/lt_T. -Qed. - -Lemma solvable_SymF : 4 < #|T| -> solvable 'Sym_T = false. -Proof. by rewrite (series_sol (Alt_normal T)) => /solvable_AltF->. Qed. - -End Perm_solvable.