Skip to content

Commit

Permalink
comments
Browse files Browse the repository at this point in the history
  • Loading branch information
Quentin VERMANDE committed Apr 22, 2023
1 parent 959f75d commit bed5f3b
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 45 deletions.
28 changes: 14 additions & 14 deletions theories/xmathcomp/artin_scheier.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,17 +26,15 @@ Let p1 : (1 < p)%N.
Proof. by apply prime_gt1. Qed.

Lemma ArtinScheier_factorize :
'X^p - 'X - (x ^+ p - x)%:P =
\prod_(z <- [seq x + (val i)%:R | i <- (index_enum (ordinal_finType p))])
('X - z%:P).
'X^p - 'X - (x ^+ p - x)%:P = \prod_(i < p) ('X - (x + i%:R)%:P).
Proof.
case: p pchar pprim p0 p1 => // n nchar nprim n0 n1.
apply/eqP; rewrite -eqp_monic; first last.
- by apply monic_prod_XsubC.
- apply/monicP; rewrite -addrA -opprD lead_coefDl ?lead_coefXn//.
by rewrite size_opp size_XaddC size_polyXn ltnS.
- rewrite eqp_sym -dvdp_size_eqp.
rewrite big_map size_prod; last first.
rewrite size_prod; last first.
move=> [i]/= _ _; apply/negP => /eqP
/(congr1 (fun p : {poly L} => size p)).
by rewrite size_XsubC size_polyC eqxx.
Expand All @@ -47,13 +45,14 @@ apply/eqP; rewrite -eqp_monic; first last.
rewrite -add1n mul2n -addnn addnA card_ord -addnBA// subnn addn0 add1n.
rewrite -addrA -opprD size_addl size_polyXn// size_opp size_XaddC ltnS.
by move: pchar => /andP [ /prime_gt1 ].
apply uniq_roots_dvdp.
have: all (root ('X^n.+1 - 'X - (x ^+ n.+1 - x)%:P)) [seq (x + (val i)%:R) | i <- index_enum (ordinal_finType n.+1)].
apply/allP => + /mapP [i _ ->] => _.
rewrite/root !hornerE ?hornerXn -(Frobenius_autE nchar (x + (val i)%:R)).
(* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *)
rewrite rmorphD/= rmorph_nat (Frobenius_autE nchar x).
rewrite opprD opprB addrACA -addrA 2![x+_]addrA subrr add0r.
rewrite opprB opprD addrACA -addrA 2![x+_]addrA subrr add0r.
by rewrite addrAC addrCA subrr addr0 addrC subrr.
move=>/uniq_roots_dvdp; rewrite big_map; apply.
rewrite uniq_rootsE; apply/(uniqP 0) => i j.
rewrite 2!inE size_map => ilt jlt.
rewrite (nth_map ord0)// (nth_map ord0)// => /addrI/esym/eqP.
Expand Down Expand Up @@ -117,25 +116,26 @@ Lemma minPoly_ArtinSchreier : (x \notin E) ->
minPoly E x = 'X^p - 'X - (x ^+ p - x)%:P.
Proof.
move=> xE.
have pE: ('X^p - 'X - (x ^+ p - x)%:P) = \prod_(i <- [seq x + (val i)%:R | i : 'I_p]) ('X - i%:P).
by rewrite ArtinScheier_factorize big_map; apply congr_big => //; rewrite enumT.
have /(minPoly_dvdp ArtinSchreier_polyOver): root ('X^p - 'X - (x ^+ p - x)%:P) x.
rewrite ArtinScheier_factorize root_prod_XsubC.
rewrite pE root_prod_XsubC.
case: p pchar pprim p0 p1 => // n nchar nprim n0 n1.
apply/mapP; exists ord0; first by rewrite mem_index_enum.
apply/mapP; exists ord0; first by rewrite enumT mem_index_enum.
by rewrite addr0.
rewrite ArtinScheier_factorize big_map.
move=> /dvdp_prod_XsubC[m]; rewrite eqp_monic ?monic_minPoly//; last first.
rewrite pE => /dvdp_prod_XsubC[m]; rewrite eqp_monic ?monic_minPoly//; last first.
by rewrite monic_prod// => i _; rewrite monic_XsubC.
have [{}m sm ->] := resize_mask m (index_enum (ordinal_finType p)).
rewrite -map_mask.
have [{}m sm ->] := resize_mask m (enum 'I_p).
set s := mask _ _ => /eqP mEx.
have [|smp_gt0] := posnP (size s).
case: s mEx => // /(congr1 (horner^~x))/esym/eqP.
by rewrite minPolyxx big_nil hornerC oner_eq0.
suff leq_pm : (p <= size s)%N.
move: mEx; suff /eqP->: s == index_enum (ordinal_finType p) by [].
move: mEx; suff /eqP->: s == enum 'I_p by [].
rewrite -(geq_leqif (size_subseq_leqif _)) ?mask_subseq//.
by rewrite/index_enum; case: index_enum_key=>/=; rewrite -enumT size_enum_ord.
by rewrite/index_enum; case: index_enum_key=>/=; rewrite size_enum_ord.
have /polyOverP/(_ (size s).-1%N) := minPolyOver E x; rewrite {}mEx.
have ->: \prod_(i <- s) ('X - (x + (val i)%:R)%:P) = \prod_(i <- [seq x + (val i)%:R | i <- s]) ('X - i%:P) by rewrite big_map.
rewrite -(size_map (fun i => x + (val i)%:R)) coefPn_prod_XsubC size_map -?lt0n// big_map.
rewrite memvN big_split/= big_const_seq count_predT iter_addr_0 => DE.
have sE: \sum_(i <- s) i%:R \in E by apply rpred_sum => i _; apply rpred_nat.
Expand Down
61 changes: 30 additions & 31 deletions theories/xmathcomp/temp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,6 @@ Local Open Scope ring_scope.

Section Temp.

Lemma ord_S_split n (i: 'I_n.+1): {j: 'I_n | i = lift ord0 j} + {i = ord0}.
Proof.
case: i; case=>[| i] ilt.
by right; apply val_inj.
by left; exists (Ordinal (ltnSE ilt)); apply val_inj.
Qed.

(* NB : rpredM and mulrPred uses that 1 is in the subset, which is useless. Predicates should be defined for {aspace aT}. *)

Lemma memv_mulr_2closed [K : fieldType] [aT : FalgType K] (U : {aspace aT}) : GRing.mulr_2closed U.
Expand All @@ -41,22 +34,23 @@ Lemma ahom_eq_adjoin [F0 : fieldType] [K : fieldExtType F0] [rT : FalgType F0] (
(U : {subfield K}) (x : K) :
{in U, f =1 g} -> f x = g x -> {in <<U; x>>%VS, f =1 g}.
Proof.
move=>fgU fgx y /Fadjoin_poly_eq <-.
move:(Fadjoin_polyOver U x y); generalize (Fadjoin_poly U x y) => p /polyOverP pU.
move=> fgU fgx y /Fadjoin_poly_eq <-.
move: (Fadjoin_poly U x y) (Fadjoin_polyOver U x y) => p /polyOverP pU.
rewrite -(coefK p) horner_poly 2!rmorph_sum/=; apply eq_bigr => i _.
by rewrite 2!rmorphM /= fgU// 2!rmorphX/= fgx.
Qed.

Lemma ahom_eq_adjoin_seq [F0 : fieldType] [K : fieldExtType F0] [rT : FalgType F0] (f g : 'AHom(K, rT))
(U : {aspace K}) (xs : seq K) :
{in U, f =1 g} -> all (fun x => f x == g x) xs -> {in <<U & xs>>%VS, f =1 g}.
{in U, f =1 g} -> {in xs, forall x, f x = g x} -> {in <<U & xs>>%VS, f =1 g}.
Proof.
elim: xs U => [|x xs IHxs] U fgU fgxs.
by rewrite adjoin_nil subfield_closed.
rewrite adjoin_cons.
have ->: <<U; x>>%VS = ASpace (agenv_is_aspace <<U; x>>%VS) by rewrite /= agenv_id.
move: fgxs (IHxs (ASpace (agenv_is_aspace <<U; x>>))) => /andP[/eqP fgx fgxs] /=.
by rewrite agenv_id => /(_ (ahom_eq_adjoin fgU fgx) fgxs).
move: fgxs (IHxs (ASpace (agenv_is_aspace <<U; x>>))) => fgxs /=.
rewrite agenv_id; apply; first by apply/ahom_eq_adjoin/fgxs=>//; apply mem_head.
by move=>a axs; apply fgxs; rewrite in_cons axs orbT.
Qed.

Lemma agenv_span (K : fieldType) (L : fieldExtType K) (U : {subfield L}) (X : seq L) : <<X>>%VS = U -> <<1%VS & X>>%VS = U.
Expand All @@ -67,13 +61,13 @@ rewrite -{2}(subfield_closed U) (agenvEr U) subfield_closed.
by congr (1 + _)%VS; apply/esym/field_module_eq; rewrite sup_field_module.
Qed.

Lemma gal_ne (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L}) (f g : FinGroup.finType (gal_finGroupType E)) : f = g \/ exists x, x \in E /\ f x != g x.
Lemma gal_ne (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L}) (f g : gal_of E) : f = g \/ exists x, x \in E /\ f x != g x.
Proof.
move:(vbasisP E)=>/span_basis/agenv_span LE.
case/boolP: (all (fun x => f x == g x) (vbasis E)) => [fgE | /allPn[x] xE fgx]; [ left | right ].
case/boolP: (all (fun x => f x == g x) (vbasis E)) => [/allP fgE | /allPn[x] xE fgx]; [ left | right ].
2: by exists x; split=>//; apply vbasis_mem.
apply/eqP/gal_eqP.
rewrite -{1}LE; apply ahom_eq_adjoin_seq=>//.
rewrite -{1}LE; apply ahom_eq_adjoin_seq=>//; last by move=>x /fgE/eqP.
move:(gal1 f)(gal1 g).
rewrite gal_kHom ?sub1v// gal_kHom ?sub1v// => /andP [_ /subvP f1] /andP [_ /subvP g1].
by move=>x /[dup] /f1/fixedSpaceP -> /g1/fixedSpaceP ->.
Expand All @@ -82,7 +76,7 @@ Qed.
Lemma tnth_cons (T : Type) (x : T) (l : seq T) (i : 'I_(size l)): tnth (in_tuple (x :: l)) (lift ord0 i) = tnth (in_tuple l) i.
Proof. by rewrite/tnth/=; apply set_nth_default. Qed.

Lemma gal_free (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L}) (f : seq (FinGroup.finType (gal_finGroupType E))) (k : 'I_(size f) -> L) : uniq f -> (forall i, k i = 0) \/ (exists a, a \in E /\ \sum_(i < size f) k i * tnth (in_tuple f) i a != 0).
Lemma gal_free (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L}) (f : seq (gal_of E)) (k : 'I_(size f) -> L) : uniq f -> (forall i, k i = 0) \/ (exists a, a \in E /\ \sum_(i < size f) k i * tnth (in_tuple f) i a != 0).
Proof.
move:(Logic.eq_refl (size f)); generalize (size f) at 1 => n.
elim: n f k => [|n IHn] f k fsize funiq.
Expand All @@ -101,27 +95,30 @@ case: (gal_ne s s0) => [/eqP ss0E | [x [xE /negPf ss0x]]].
move:fsize=>/eqP; rewrite eqSS=>/eqP fsize.
case: (IHn [:: s0 & f] (fun i => (k (lift ord0 i) * (tnth (in_tuple [:: s0 & f]) i x - s x))) fsize s0f).
move=>/(_ ord0)/=/eqP; rewrite mulf_eq0 subr_eq0 [s0 x == _]eq_sym ss0x orbF => k10.
set k' := fun i : 'I_(size f).+1 => k (if ord_S_split i then lift ord0 i else ord0).
set k' := fun i : 'I_(size f).+1 => k
(match splitP (i : 'I_(1 + size f)%N) with
| SplitLo _ _ => ord0
| SplitHi _ _ => lift ord0 i
end).
move: (IHn [:: s & f] k' fsize).
have /[swap]/[apply]: uniq (s :: f) by apply/andP; split.
case => [k0 | [a [aE fne0]]]; [left => i | right; exists a].
case: i; case.
move: (k0 ord0); rewrite/k'.
case: (ord_S_split _) => [[i /=/(congr1 val)//] | /= _ /[swap] ilt].
by congr (k _ = 0); apply val_inj.
by case: splitP => // + _ + ilt => _; congr (k _ = 0); apply val_inj.
case => [|i] ilt.
by move: k10 => /eqP; congr (k _ = 0); apply val_inj.
have ile: (i.+1 < (size f).+1)%N by rewrite -ltnS.
move:(k0 (Ordinal ile)); rewrite/k'.
case: (ord_S_split _) => [/= _| /[dup]/(congr1 val)//].
case: splitP => [[j]/=/[swap]<-// | /= _ _].
by congr (k _ = 0); apply val_inj.
split=>//.
move:k10 fne0 => /eqP k10.
rewrite 3!big_ord_recl/= k10 mul0r add0r.
congr (_ * _ + _ != 0).
by rewrite/k'; case: (ord_S_split _) => // [[i]] /=/(congr1 val).
by rewrite/k'; case: splitP => // [[i]] /=/(congr1 val).
apply eq_bigr => i _; rewrite tnth_cons (@tnth_cons _ s (s0 :: f) (lift ord0 i)) tnth_cons; congr (_ * _).
by rewrite/k'; case: (ord_S_split _).
by rewrite/k'; case: splitP => // [[j]]/=/[swap]<-.
move=>[y [yE fne0]]; right.
case /boolP: (\sum_(i < (size f).+2) k i * tnth (in_tuple [:: s, s0 & f]) i y == 0) => [| yne0].
2: by exists y.
Expand Down Expand Up @@ -157,12 +154,14 @@ move=> a f IHf.
by rewrite 2!big_cons ffunE IHf.
Qed.


Definition Zp_succ n (i : 'I_n) := Ordinal (
match n with
| 0 => fun i0 : 'I_0 => match i0 with | @Ordinal _ _ i0 => i0 end
| n0.+1 => fun i0 => (ltn_pmod i0.+1 (is_true_true : (is_true (0 < n0.+1)%N)))
end i).
Definition Zp_succ n (i : 'I_n) :=
match i with
| @Ordinal _ k klt => Ordinal (
match n as n0 return (k < n0)%N -> (k.+1 %% n0 < n0)%N with
| 0 => id
| n0.+1 => fun=> ltn_pmod k.+1 (is_true_true : 0 < n0.+1)%N
end klt)
end.

Lemma cycle_imset [gT : finGroupType] (g : gT) : <[g]>%g = @Imset.imset (ordinal_finType #[g]%g) (FinGroup.finType gT) (fun i => (g ^+ (val i))%g) (mem setT).
Proof.
Expand Down Expand Up @@ -192,7 +191,7 @@ Proof. by apply congr_big => // i; rewrite in_setT. Qed.

Lemma Hilbert's_theorem_90_additive
[F : fieldType] [L : splittingFieldType F]
[K E : {subfield L}] [x : gal_finGroupType E]
[K E : {subfield L}] [x : gal_of E]
[a : L] :
galois K E ->
generator 'Gal(E / K) x ->
Expand Down Expand Up @@ -320,7 +319,7 @@ have ->: ((if p \in primes m then p ^ logn p m else 1) = p ^ logn p m)%N.
by rewrite -expnD subnK// vp_leq.
Qed.

Lemma muln_gt0 [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
Lemma prodn_gt0 [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
all (fun n : I => P n ==> (0 < F n)%N) r ->
(0 < \prod_(n <- r | P n) F n)%N.
Proof.
Expand All @@ -337,7 +336,7 @@ Proof.
elim: r => [|n r IHn /andP[Fn0 Fr0]]; first by rewrite 2!big_nil logn1.
rewrite 2!big_cons; case /boolP: (P n) => Pn; last by apply IHn.
move:Fn0; rewrite Pn => /= Fn0.
by rewrite lognM// ?muln_gt0// IHn.
by rewrite lognM// ?prodn_gt0// IHn.
Qed.

Lemma logn_partn (p n : nat) (pi : nat_pred) :
Expand Down

0 comments on commit bed5f3b

Please sign in to comment.