Skip to content

Commit 11a16d5

Browse files
CohenCyrilTragicus
CohenCyril
authored and
Tragicus
committed
refactoring
1 parent a4b96f3 commit 11a16d5

2 files changed

Lines changed: 79 additions & 117 deletions

File tree

‎theories/abel.v‎

Lines changed: 77 additions & 111 deletions
Original file line numberDiff line numberDiff line change
@@ -207,7 +207,7 @@ have [prime_n|primeN_n] := boolP (prime n).
207207
case/boolP: (2 <= n)%N; last first.
208208
case: n {lenk primeN_n} => [|[]]// in xnE n_gt0 * => _.
209209
by move: n_gt0; rewrite eqxx.
210-
suff ->: <<E; x>>%VS = E by apply: rext_refl.
210+
suff -> : <<E; x>>%VS = E by apply: rext_refl.
211211
by rewrite (Fadjoin_idP _).
212212
move: primeN_n => /primePn[|[d /andP[d_gt1 d_ltn] dvd_dn n_gt1]].
213213
by case: ltngtP.
@@ -293,6 +293,7 @@ Local Notation "r .-tower" := (tower r)
293293
(at level 2, format "r .-tower") : ring_scope.
294294
Local Notation "r .-ext" := (extension_of r)
295295
(at level 2, format "r .-ext") : ring_scope.
296+
#[global] Hint Resolve rext_refl : core.
296297

297298
(* Following the french wikipedia proof :
298299
https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_d%27Abel_(alg%C3%A8bre)#D%C3%A9monstration_du_th%C3%A9or%C3%A8me_de_Galois
@@ -366,116 +367,83 @@ Section Part1.
366367
Variables (F0 : fieldType) (L : splittingFieldType F0).
367368
Implicit Types (E F K : {subfield L}) (w : L) (n : nat).
368369

370+
Lemma muln_div_trans d m n : (d %| m)%N -> (n %| d)%N ->
371+
((m %/ d) * (d %/ n))%N = (m %/ n)%N.
372+
Proof. by move=> dm nd; rewrite muln_divA// divnK. Qed.
373+
374+
Lemma muln_dimv E F K :
375+
(K <= E)%VS -> (E <= F)%VS -> (\dim_K E * \dim_E F)%N = \dim_K F.
376+
Proof. by move=> KE EF; rewrite mulnC muln_div_trans// ?field_dimS. Qed.
377+
378+
Lemma galX E n (x : gal_of E) [a : L] : a \in E -> (x ^+ n)%g a = iter n x a.
379+
Proof.
380+
by elim: n => [|n IHn] aE; rewrite (expg0, expgSr)/= (gal_id, galM)/= ?IHn.
381+
Qed.
382+
369383
Lemma cyclic_radical_ext w E F : ((\dim_E F)`_[char L]^').-primitive_root w ->
370384
w \in E -> galois E F -> cyclic 'Gal(F / E) -> radical.-ext E F.
371385
Proof.
372-
case /boolP: (E == F :> {vspace L}) => [/eqP -> _ _ _ _ | EneF].
373-
by apply: rext_refl.
374-
remember (\dim_E F) as n.
375-
move: w E F Heqn EneF.
376-
refine (@ltn_ind
377-
(fun n => forall (w : L) (E F : {subfield L}),
378-
n = \dim_E F ->
379-
((E : {vspace L}) != F)%VS ->
380-
(n`_[char L]^').-primitive_root w ->
381-
w \in E ->
382-
galois E F ->
383-
cyclic 'Gal(F / E) ->
384-
radical.-ext E F)
385-
_ n).
386-
move: n => _ n IHn w E F dimEF EneF wroot wE galEF /[dup] cycEF /cyclicP[g GE].
386+
have [->|NEF] := eqVneq (E : {vspace _}) F; first by [].
387+
have [n] := ubnP (\dim_E F); elim: n => // n IHn in w E F NEF *.
388+
rewrite ltnS leq_eqVlt => /predU1P[/[dup] dimEF ->|]; last exact: IHn.
389+
move=> wroot wE galEF /[dup] cycEF /cyclicP[/= g GE].
387390
have ggen : generator ('Gal(F / E))%g g by rewrite GE generator_cycle.
388391
have ggal : g \in ('Gal(F / E))%g by rewrite GE cycle_id.
389392
have EF := galois_subW galEF.
390-
have n_gt0: (0 < n)%N by rewrite dimEF divn_gt0 ?adim_gt0//; apply/dimvS.
391-
have [k [a [k0 [aE [aF /rext_r arad]]]]]:
392-
exists (k : nat) (a : L), (0 < k)%N /\ a \notin E /\ a \in F /\ radical E a k.
393-
case /boolP: (n%:R == (0 : L)) => [n0 | n_ne0].
394-
move: (natf0_char n_gt0 n0) => [p pchar]; exists p.
395-
have /eqP: galTrace E F (-1) = 0.
396-
rewrite /galTrace.
397-
transitivity (\sum_(x in ('Gal(F / E))%g) (-1 : L)).
398-
apply: eq_bigr => x xgal.
399-
by rewrite (fixed_gal EF) ?rpredN1.
400-
move: n0 => /eqP n0.
401-
by rewrite sumr_const -(galois_dim galEF) -dimEF -mulr_natl n0 mul0r.
402-
have FN1: -1 \in F by rewrite rpredN1.
403-
move=> /(Hilbert's_theorem_90_additive galEF ggen FN1) [a] aF.
404-
move=> /(congr1 (@GRing.opp L))/(congr1 (GRing.add a)).
405-
rewrite opprK opprB addrCA subrr addr0 => /esym ga.
406-
have apF: a ^+ p - a \in F by rewrite rpredB// rpredX.
407-
have: a ^+ p - a \in fixedField ('Gal(F / E))%g.
408-
apply/fixedFieldP => //.
409-
move=> x; rewrite GE => /cycleP[+ ->]; elim => [|m IHm].
410-
by rewrite expg0 gal_id.
411-
rewrite expgSr galM// IHm rmorphB/= rmorphX/= ga.
412-
rewrite -(Frobenius_autE pchar (a+1)) rmorphD/= (Frobenius_autE pchar a).
413-
by rewrite rmorph1 opprD addrACA subrr addr0.
414-
move: (galEF) => /galois_fixedField -> apE.
415-
case /boolP: (a \in E) => aE.
416-
move: ga; rewrite (fixed_gal EF)//.
417-
move=> /(congr1 (fun x => x-a))/esym/eqP.
418-
by rewrite addrAC subrr add0r oner_eq0.
419-
exists a; repeat split => //.
420-
by move: pchar => /andP [/prime_gt0].
421-
by apply/orP; right; apply/andP.
422-
move: (n_ne0) wroot => /negPf; rewrite natf0_partn//.
423-
move=> /negbT; rewrite negbK.
424-
move=> /eqP/(congr1 (fun x => (x * n`_[char L]^'))%N).
425-
rewrite mul1n partnC => // <- wroot.
426-
exists n.
427-
have HT90g := Hilbert's_theorem_90 ggen (subvP EF _ wE).
428-
have /eqP/HT90g[x [xF xN0]] : galNorm E F w = 1.
429-
rewrite /galNorm; under eq_bigr => g' g'G;
430-
first by rewrite (fixed_gal EF g'G)//; over.
431-
by rewrite prodr_const -galois_dim// -dimEF (prim_expr_order wroot).
432-
have gxN0 : g x != 0 by rewrite fmorph_eq0.
433-
have wN0 : w != 0. rewrite (primitive_root_eq0 wroot) -lt0n //.
434-
move=> /(canLR (mulfVK gxN0))/(canRL (mulKf wN0)) gx.
435-
have gXx i : (g ^+ i)%g x = w ^- i * x.
436-
elim: i => [|i IHi].
437-
by rewrite expg0 expr0 invr1 mul1r gal_id.
438-
rewrite expgSr exprSr invfM galM// IHi rmorphM/= gx mulrA.
439-
by rewrite (fixed_gal EF ggal) ?rpredV ?rpredX.
440-
exists x; repeat split=> //.
441-
- apply/negP=> xE.
442-
move: gx; rewrite (fixed_gal EF)// => /(congr1 (fun y => w * y / x)).
443-
rewrite mulrA -2!mulrA mulfV// 2!mulr1 mulfV// => w1; subst w.
444-
move: wroot; rewrite prim_root1 => /eqP n1; subst n.
445-
move: n1 => /eqP; rewrite -eqn_mul ?adim_gt0 ?(field_dimS EF)//.
446-
rewrite mul1n => /eqP dimEFe.
447-
by move: EneF => /negP; apply => /=; rewrite eqEdim EF dimEFe leqnn.
448-
- apply/orP; left; apply/andP; split.
449-
apply/negP => /eqP n0.
450-
by move: n_ne0; rewrite -scaler_nat n0 scale0r eqxx.
451-
move: galEF => /galois_fixedField <-; apply/fixedFieldP.
452-
by apply: rpredX.
453-
rewrite GE => + /cycleP [i ->] => _.
454-
rewrite rmorphX/= gXx exprMn exprVn exprAC (prim_expr_order wroot)//.
455-
by rewrite expr1n invr1 mul1r.
456-
apply: (rext_trans arad).
457-
have gala: galois <<E; a>> F.
458-
refine (galoisS _ galEF); apply/andP; split; first by apply: subv_adjoin.
459-
by apply/FadjoinP; split=> //; apply/galois_subW.
460-
have dimEaF: (\dim_(<<E; a>>) F < n)%N.
461-
rewrite dimEF ltn_divRL; last by apply/field_dimS/galois_subW.
462-
rewrite mulnC muln_divA; last by apply/field_dimS/galois_subW.
463-
rewrite ltn_divLR ?adim_gt0// mulnC ltn_mul2l adim_gt0/=.
464-
rewrite ltnNge; apply/negP => dimE.
465-
move: (eqEdim E <<E; a>>); rewrite dimE subv_adjoin/= => /eqP EE.
466-
by move: aE; rewrite EE memv_adjoin.
467-
case /boolP: (<<E; a>>%AS == F) => [FE | Fne].
468-
move: FE => /eqP ->; apply: rext_refl.
469-
apply: (IHn _ dimEaF
470-
(w ^+ (n`_[char L]^' %/ (\dim_(<<E; a>>) F)`_[char L]^')%N)) => //.
471-
- rewrite dvdn_prim_root// partn_dvd//.
472-
rewrite dimEF dvdn_divRL; last by apply/field_dimS/galois_subW.
473-
rewrite mulnC muln_divA; last by apply/field_dimS/galois_subW.
474-
rewrite dvdn_divLR ?adim_gt0//.
475-
by rewrite mulnC dvdn_mul//; apply/field_dimS/subv_adjoin.
476-
by apply/dvdn_mull/field_dimS/FadjoinP; rewrite EF aF.
477-
- by apply/rpredX/subvP_adjoin.
478-
- exact (cyclicS (galS F (subv_adjoin E a)) cycEF).
393+
have n_gt1 : (n > 1)%N.
394+
rewrite -dimEF ltn_divRL ?mul1n// ?field_dimS//.
395+
by rewrite eqEdim EF/= -ltnNge in NEF.
396+
have n_gt0: (0 < n)%N by apply: leq_trans n_gt1.
397+
suff [k [a [k0 aE aF /rext_r arad]]]:
398+
exists (k : nat) (a : L), [/\ (0 < k)%N, a \notin E, a \in F & radical E a k].
399+
have gala: galois <<E; a>> F.
400+
refine (galoisS _ galEF); apply/andP; split; first by apply: subv_adjoin.
401+
by apply/FadjoinP; split=> //; apply/galois_subW.
402+
have dimEaF: (\dim_(<<E; a>>) F < n)%N.
403+
rewrite dim_Fadjoin mulnC divnMA dimEF ltn_Pdiv//.
404+
by rewrite ltn_neqAle eq_sym adjoin_deg_eq1 aE//.
405+
apply: rext_trans arad _; have [->//|Fne] := eqVneq <<E; a>>%AS F.
406+
apply: (IHn (w ^+ (n`_[char L]^' %/ (\dim_(<<E; a>>) F)`_[char L]^')%N)) => //.
407+
- rewrite dvdn_prim_root// partn_dvd//; apply/dvdnP; exists (\dim_E <<E; a>>).
408+
by rewrite muln_dimv// ?subv_adjoin// galois_subW.
409+
- by apply/rpredX/subvP_adjoin.
410+
- exact (cyclicS (galS F (subv_adjoin E a)) cycEF).
411+
have [n0 | n_ne0] := boolP (n%:R == 0 :> L).
412+
have [p pchar] := natf0_char n_gt0 n0; exists p.
413+
have p_gt0 : (p > 0)%N by move: pchar => /andP [/prime_gt0].
414+
have [|a aF] := Hilbert's_theorem_90_additive galEF ggen (rpredN1 _) _.
415+
rewrite /galTrace; under eq_bigr do rewrite (fixed_gal EF) ?rpredN1//.
416+
by rewrite sumr_const -galois_dim// dimEF -mulr_natl (eqP n0) mul0r.
417+
have [aE|aNE] := boolP (a \in E).
418+
by rewrite (fixed_gal EF)// subrr => /eqP; rewrite oppr_eq0 oner_eq0.
419+
move=> /(canLR (addrNK _))/(canRL (addNKr _)) ga.
420+
suff apE : a ^+ p - a \in E.
421+
by exists a; split => //; apply/orP; right; apply/andP.
422+
rewrite -(galois_fixedField galEF).
423+
have apF : a ^+ p - a \in F by rewrite rpredB// rpredX.
424+
apply/fixedFieldP => // h /[!GE]/cycleP[+ ->].
425+
elim=> [|m IHm]; first by rewrite expg0 gal_id.
426+
rewrite expgSr galM// IHm rmorphB/= rmorphX/= ga -Frobenius_autE.
427+
by rewrite rmorphD/= rmorph1 !Frobenius_autE opprD addrACA subrr add0r.
428+
exists n; rewrite part_pnat_id -?natf_neq0// in wroot.
429+
have [|x [xF xN0]] := Hilbert's_theorem_90 ggen (subvP EF _ wE) _.
430+
rewrite /galNorm; under eq_bigr do rewrite (fixed_gal EF)//.
431+
by rewrite prodr_const -galois_dim// dimEF (prim_expr_order wroot).
432+
have gxN0 : g x != 0 by rewrite fmorph_eq0.
433+
have wN0 : w != 0 by rewrite (primitive_root_eq0 wroot) -lt0n // dimEF.
434+
have [xE|xNE] := boolP (x \in E).
435+
rewrite (fixed_gal EF)// divff// => w1.
436+
by rewrite w1 prim_root1// gtn_eqF in wroot.
437+
move=> /(canLR (mulfVK gxN0))/(canRL (mulKf wN0)) gx.
438+
have nF0_ne0: n%:R != 0 :> F0.
439+
by rewrite natf0_partn// -(eq_partn _ (@char_lalg _ L)) -natf0_partn.
440+
suff: x ^+ n \in E by exists x; split => //; apply/orP; left; apply/andP.
441+
rewrite -(galois_fixedField galEF).
442+
have xnF : x ^+ n \in F by rewrite rpredX.
443+
apply/fixedFieldP => //= h /[!GE]/cycleP[+ ->].
444+
elim=> [|m IHm]; first by rewrite expg0 gal_id.
445+
rewrite expgSr galM// IHm rmorphX/= gx exprMn exprVn.
446+
by rewrite (prim_expr_order wroot) invr1 mul1r.
479447
Qed.
480448

481449
Lemma solvableWradical_ext w E F (n := \dim_E F) :
@@ -706,7 +674,7 @@ rewrite (@pradical_solvable p _ _ w)// ?memv_adjoin//.
706674
by rewrite (isog_sol (normalField_isog _ _ _)) ?galois_normalW ?subv_adjoin.
707675
Qed.
708676

709-
Lemma ArtinSchreier_solvable_ext (p : nat) (F0 : fieldType)
677+
Lemma ArtinSchreier_solvable_ext (p : nat) (F0 : fieldType)
710678
(L : splittingFieldType F0) (E : {subfield L}) (x : L) : p \in [char L] ->
711679
x ^+ p - x \in E -> x \notin E -> solvable_ext E <<E; x>>.
712680
Proof.
@@ -773,7 +741,7 @@ Definition solvable_ext_poly (F : fieldType) (p : {poly F}) :=
773741
solvable 'Gal(<<1 & rs>> / 1).
774742

775743
Definition separable_splittingField (F : fieldType) (p : {poly F}) :=
776-
forall (L : splittingFieldType F) (rs : seq L),
744+
forall (L : splittingFieldType F) (rs : seq L),
777745
p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) -> separable 1 <<1 & rs>>.
778746

779747
Lemma galois_solvable (F0 : fieldType) (L : splittingFieldType F0)
@@ -1783,10 +1751,8 @@ elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *.
17831751
by rewrite [RHS](fmorph_eq_rat (iota \o in_alg _)).
17841752
- case: als1 als1E => [|y []]//= []/=; rewrite adjoin_seq1.
17851753
case: c => [/eqP|/eqP|n yomega].
1786-
+ rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0//.
1787-
exact: rext_refl.
1788-
+ rewrite fmorph_eq1 => /eqP->; rewrite (Fadjoin_idP _) ?rpred1//.
1789-
exact: rext_refl.
1754+
+ by rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0.
1755+
+ by rewrite fmorph_eq1 => /eqP->; rewrite (Fadjoin_idP _) ?rpred1.
17901756
+ apply/(@rext_r _ _ _ n.+1)/radicalP; left; split.
17911757
by apply/negP; rewrite pnatr_eq0.
17921758
rewrite prim_expr_order ?rpred1//.

‎theories/xmathcomp/various.v‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -115,13 +115,9 @@ End tnth_shift.
115115
(**********)
116116

117117
Lemma ffun_sum [T : finType] [R : ringType] [E : vectType R]
118-
(f : seq (ffun_vectType T E)) (x : T) :
118+
(f : seq {ffun T -> E}) (x : T) :
119119
((\sum_(i <- f) i) x = \sum_(i <- f) i x)%R.
120-
Proof.
121-
elim: f; first by rewrite 2!big_nil ffunE.
122-
move=> a f IHf.
123-
by rewrite 2!big_cons ffunE IHf.
124-
Qed.
120+
Proof. by elim/big_rec2: _ => [|? ? ? ? <-]; rewrite ffunE. Qed.
125121

126122
(*********)
127123
(* prime *)

0 commit comments

Comments
 (0)