Skip to content

Commit

Permalink
remove backported lemmas to solvable
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tragicus
Tragicus committed Mar 29, 2024
1 parent 12c8d85 commit a048ec8
Showing 1 changed file with 0 additions and 189 deletions.
189 changes: 0 additions & 189 deletions theories/xmathcomp/various.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

0 comments on commit a048ec8

Please sign in to comment.