Abel-Galois for any characteristic #83

Tragicus · 2023-02-03T15:22:57Z

Generalizes the definition of radical extension and the Abel-Galois theorem to fields of any characteristic.

Tragicus · 2023-02-03T15:32:31Z

Lines 714-811 contain the roots-coefficients relations for a polynomial. Should it go to mathcomp or should I put it in the xmathcomp directory (or have I just not seen it in the library)?

Should I try to go further, hopefully replacing the 0 characteristic hypothesis by some separability hypothesis?

CohenCyril · 2023-02-03T15:50:28Z

theories/abel.v

+Lemma primitive_unity_root_char (w : L) (n : nat) :
+  n.-primitive_root w -> n%:R != (0 : F0).


This was here:

Abel/theories/xmathcomp/various.v

Lines 265 to 266 in 9449966

Lemma prim_root_natf_neq0 (F : fieldType) n (w : F) :

n.-primitive_root w -> (n%:R != 0 :> F).

And it's being ported to mathcomp in this PR: https://github.com/math-comp/math-comp/pull/944/files#diff-2d6a4ea70d7630c940ac8075abbc6ff46d30c54f80c29291131b711b195368e6R1839

CohenCyril · 2023-02-03T15:53:40Z

theories/abel.v

+
+Lemma big_split_cond (R : Type) (idx : R) (op : Monoid.com_law idx) (I : Type)
+  (r : seq I) (P Q : pred I) (F G : I -> R) :
+  \big[op/idx]_(i <- r | P i) (if Q i then F i else G i) =
+  op (\big[op/idx]_(i <- r | P i && Q i) F i)
+     (\big[op/idx]_(i <- r | P i && ~~ Q i) G i).


this should be renamed big_if and ported back to mathcomp.

CohenCyril · 2023-02-03T15:58:08Z

Lines 714-811 contain the roots-coefficients relations for a polynomial. Should it go to mathcomp or should I put it in the xmathcomp directory (or have I just not seen it in the library)?

Both! (To my knowledge it's been done only for multivariate polynomials)

Should I try to go further, hopefully replacing the 0 characteristic hypothesis by some separability hypothesis?

If you want, yes please!

Tragicus · 2023-02-24T13:49:20Z

In fact, what I did is not complete. I proved that any extension that is solvable by radical is solvable in any characteristic, but not the converse, so AbelGalois still requires a root of unity, which makes my generalization pretty useless. When I try to prove the missing part following Lang's Algebra book, I need to prove that the galois trace is not 0, which relies on the independance of characters, whose proof takes two different characters and chooses a point where they differ. This is supposed to be applied to members of a galois group, whose domains are infinite, which makes this step non-constructive. Is there a constructive proof of this theorem, or else what should I do, I guess we do not want to rely on boolp from mathcomp-analysis ?

Tragicus · 2023-04-21T13:10:00Z

I managed to do it using (essentially) the decidability of equality between elements of the galois group. I have quite a few auxiliary lemmas, that I have temporarily put in theories/xmathcomp/temp.v for review (in particular in case I missed some relevant part of the library). The generalization of the AbelGalois theorem is now complete (and I believe optimal given the model of field extension that we use).

CohenCyril

Indeed, we should discuss a few results and in particular if they can be rephrased to better reuse the contents of the library ?
Also the statements should reuse maximally predefined notations and definitions and if it does not look "close enough" to what one writes on paper, it means it requires some thinking to make it more beautiful (despite ASCII-style notations).

CohenCyril · 2023-04-21T13:13:36Z

theories/xmathcomp/artin_scheier.v

+
+Lemma ArtinScheier_factorize :
+  'X^p - 'X - (x ^+ p - x)%:P =
+  \prod_(z <- [seq x + (val i)%:R | i <- (index_enum (ordinal_finType p))])


I suggest this instead

Suggested change

\prod_(z <- [seq x + (val i)%:R | i <- (index_enum (ordinal_finType p))])

\prod_(i < p) 'X - (x + i%:R)%:P

CohenCyril · 2023-04-21T13:14:17Z

theories/xmathcomp/temp.v

+
+Section Temp.
+
+Lemma ord_S_split n (i: 'I_n.+1): {j: 'I_n | i = lift ord0 j} + {i = ord0}.


case: splitP should perform this kind of analysis.

CohenCyril · 2023-04-21T13:15:59Z

theories/xmathcomp/temp.v

+move=>fgU fgx y /Fadjoin_poly_eq <-.
+move:(Fadjoin_polyOver U x y); generalize (Fadjoin_poly U x y) => p /polyOverP pU.


Suggested change

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.

CohenCyril · 2023-04-21T13:17:11Z

theories/xmathcomp/temp.v

+
+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}.


Is it really useful to have a all here rather than forall:

Suggested change

{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}.

CohenCyril · 2023-04-21T13:48:13Z

theories/xmathcomp/temp.v

+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.


I believe this result is a consequence of a more general one stating that for linear maps in finite dimension we can find a witness of disequality.

I would expect so, but I spent too much time trying to find it.

theories/xmathcomp/temp.v

CohenCyril · 2023-04-21T13:55:38Z

theories/xmathcomp/temp.v

+  | 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)))


That would make sense, but I want val (Zp_succ i) to reduce to i.+1 %% n without having to destruct n (which is the issue I have with all the Zp_* definitions in the library). That being said, I think I do not need this definition anymore, we can discuss whether we want to keep it as an independently interesting object.

CohenCyril · 2023-04-21T14:12:25Z

theories/xmathcomp/temp.v

+  | n0.+1 => fun i0 => (ltn_pmod i0.+1 (is_true_true : (is_true (0 < n0.+1)%N)))
+  end i).
+
+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).


Suggested change

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).

Lemma cycle_imset [gT : finGroupType] (g : gT) : <[g]>%g = [set g ^+ (val i) | i : 'I_#[g]%g]

I'm surprised not to see this result in the library indeed ... I will investigate...

This change breaks lemma Hilbert's_theorem_90_additive when I rewrite big_imset_cond. I wanted to write it this way at first, but I have been fighting for so long that I ended up copy-pasting what the lemma wants.

CohenCyril · 2023-04-21T14:13:04Z

theories/xmathcomp/temp.v

+
+Lemma Hilbert's_theorem_90_additive
+  [F : fieldType] [L : splittingFieldType F] 
+    [K E : {subfield L}] [x : gal_finGroupType E] 


Suggested change

[K E : {subfield L}] [x : gal_finGroupType E]

[K E : {subfield L}] [x : gal E]

CohenCyril · 2023-04-21T14:15:17Z

theories/xmathcomp/temp.v

+by rewrite -expnD subnK// vp_leq.
+Qed.
+
+Lemma muln_gt0 [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :


I believe this is prodn_gt0

I need the predicate when I want to prove that every F n is greater than 0, which prodn_gt0 does not allow me to do. That being said, it should be named prodn_gt0.

It's because it's supposed to be chained with big_seq_cond

Tragicus · 2023-06-08T17:36:49Z

@CohenCyril I did most of what we discussed, but not right away due to other obligations. Hopefully I did not forget anything. I have issues with generalizing cycle_imset, I added a comment.

CohenCyril · 2023-07-21T10:33:17Z

@Tragicus I performed some refactorings and simplifications. Tell me what you think.

Tragicus · 2023-07-21T16:46:55Z

@CohenCyril Thank you, I moved the results in temp to their (hopefully) right location in various.v, I also had to move some of the results in map_gal.v there because of dependency issues in the galois section. There are a few things left in temp.v that need to be discussed about. In particular, I think we can simply remove big_condT and Zp_succ.

CohenCyril · 2023-07-25T08:07:45Z

theories/xmathcomp/temp.v

+(* J'ai l'impression que je veux garder la quantification sur $r$ dans la première hypothèse. Je laisse ma version dans various.v le temps qu'on en discute. *)
+Lemma logn_prod [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
+  (forall n,  P n -> (0 < F n)%N) ->
+  (logn p (\prod_(n <- r | P n) F n) = \sum_(n <- r | P n) logn p (F n))%N.
+Proof.
+move=> F_gt0; elim/(big_load (fun n => (n > 0)%N)): _.
+elim/big_rec2: _; first by rewrite logn1.
+by move=> i m n Pi [n_gt0 <-]; rewrite muln_gt0 lognM ?F_gt0.
+Qed.


As usual with bigop lemmas, the lemma is more general when not "relativised" to the sequence. Indeed {in r, ...} forces I to be an eqType whereas the current phrasing does not.
Moreover, it is seldom the case that we need to know i is in r in real situtations, mostly because most sums are performed over a finite type, in which case r is the enumeration of all elements of the finite type, making the assumption i \in r spurious.

That being said, in the (very) rare case where we need to know i \in r to prove the side condition, one may use big_seq_cond to load the condition in the predicate part of the bigop. As an example, here is how to prove your version from this one:

Lemma logn_prod_seq [I : eqType] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) : {in r, forall n, P n -> (0 < F n)%N} -> (logn p (\prod_(n <- r | P n) F n) = \sum_(n <- r | P n) logn p (F n))%N. Proof. by move=> F0; rewrite big_seq_cond logn_prod -?big_seq_cond// => i /andP[/F0]. Qed.

(note also that the concatenation of these two proofs is still shorter than the initial one)

I tried to summarize this here:
https://github.com/math-comp/math-comp/wiki/FAQ#bigops
please tell me if this is clear.

The paragraph on "\big_(i <- r | P i) F i" is clear and helpful. Concerning "\big_(i in A | P i) F i", is that not syntactic sugar for "\big_(i | (i \in A) && P i) F i", in which case the lemmas for the previous form of bigop would apply ?
I updated logn_prod_seq in various.v. I will push when we decide what we do with big_condT and Zp_succ. Also, is there something we should do about the checks that keep failing?

Concerning "\big_(i in A | P i) F i", is that not syntactic sugar for "\big_(i | (i \in A) && P i) F i", in which case the lemmas for the previous form of bigop would apply ?

yes indeed, the lemmas of the form \big_(i <- r | P i) F i will apply, but my point in this paragraph, is the other way around: lemmas of the form big_(i in A | P i) F i do not apply to goals of the form \big_(i <- r | P i) F i. That was not clear?

I updated logn_prod_seq in various.v. I will push when we decide what we do with big_condT and Zp_succ.

I'd be fine if you did two PR to mathcomp

for big_condT it can be useful even though big_mkcondr subsumes it in a trivial way for coq but nontrivial for humans,

for Zp_succ, I realized I actually defined pred rather than succ 😆.
I prefer this definition though:
Fact Zp_succ_subproof n (i : 'I_n) : i.+1 %% n < n. Proof. by case: n i => [|n] [m m_lt]//=; rewrite ltn_pmod. Qed. Definition Zp_succ n (i : 'I_n) := Ordinal (Zp_succ_subproof i).
it is very similar to your definition except it separates the computational part from the proof part and opacifies the latter, and it does not start with a match at all.

Also, is there something we should do about the checks that keep failing?

I will update the CI and we'll see

Concerning "\big_(i in A | P i) F i", is that not syntactic sugar for "\big_(i | (i \in A) && P i) F i", in which case the lemmas for the previous form of bigop would apply ?

yes indeed, the lemmas of the form \big_(i <- r | P i) F i will apply, but my point in this paragraph, is the other way around: lemmas of the form big_(i in A | P i) F i do not apply to goals of the form \big_(i <- r | P i) F i. That was not clear?

Maybe the title of the section mislead me, I read it as "what should I do when I see a "\big_(i in A | P i) F i"" and not "how to apply lemmas containing a "\big_(i in A | P i) F i"". It might be worth it to mention that the notation is syntactic sugar for the previous one, I can easily see people getting confused (as I have got myself for some time) about it.

I updated logn_prod_seq in various.v. I will push when we decide what we do with big_condT and Zp_succ.

I'd be fine if you did two PR to mathcomp

* for `big_condT` it can be useful even though `big_mkcondr` subsumes it in a trivial way for coq but nontrivial for humans, * for `Zp_succ`, I realized I actually defined pred rather than succ laughing. I prefer this definition though: ```coq Fact Zp_succ_subproof n (i : 'I_n) : i.+1 %% n < n. Proof. by case: n i => [|n] [m m_lt]//=; rewrite ltn_pmod. Qed. Definition Zp_succ n (i : 'I_n) := Ordinal (Zp_succ_subproof i). ``` it is very similar to your definition except it separates the computational part from the proof part and opacifies the latter, and it does not start with a match at all.

Yes, this match on i is a mistake. I will do the PR. While I am at it, is there something else I should port to mathcomp (in particular the results in various.v)?

CohenCyril · 2023-11-07T11:19:46Z

@Tragicus FYI I'm porting this to mathcomp 2, then I'll squash and merge.

Abel-Galois for any characteristic

06ea22a

Tragicus marked this pull request as draft February 3, 2023 15:24

CohenCyril reviewed Feb 3, 2023

View reviewed changes

Quentin VERMANDE added 2 commits February 3, 2023 18:52

fix hornerE changing behaviour between mc versions

4ab6ab8

update on suggestions

6664b11

Quentin VERMANDE added 2 commits April 21, 2023 14:54

byproducts

a57ab3e

characteristic independant AbelGalois

959f75d

CohenCyril requested changes Apr 21, 2023

View reviewed changes

comments

e5b4036

Tragicus force-pushed the AG branch from bed5f3b to e5b4036 Compare April 22, 2023 14:22

Quentin VERMANDE and others added 2 commits April 22, 2023 22:25

remove has_char0 hypotheses

4848812

cleanup

08606fc

Simplifications

9a91e8a

CohenCyril and others added 3 commits July 21, 2023 12:49

set -> pose

d46aedd

started cleaning temp

77a6cf7

Merge branch 'AG' of github.com:Tragicus/Abel into AG

49fd41e

CohenCyril reviewed Jul 25, 2023

View reviewed changes

qvermande and others added 3 commits July 25, 2023 13:13

remove duplicate in map_gal; remove temp

7dff68d

refactoring

e632d24

shortens a few lines and puts lemmas away

51af6b8

Tragicus marked this pull request as ready for review August 17, 2023 11:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Abel-Galois for any characteristic #83

Abel-Galois for any characteristic #83

Tragicus commented Feb 3, 2023

Tragicus commented Feb 3, 2023

CohenCyril Feb 3, 2023 •

edited

Loading

CohenCyril Feb 3, 2023

CohenCyril commented Feb 3, 2023 •

edited

Loading

Tragicus commented Feb 24, 2023

Tragicus commented Apr 21, 2023

CohenCyril left a comment

CohenCyril Apr 21, 2023

CohenCyril Apr 21, 2023

CohenCyril Apr 21, 2023

CohenCyril Apr 21, 2023

CohenCyril Apr 21, 2023

Tragicus Apr 22, 2023

CohenCyril Apr 21, 2023

Tragicus Apr 22, 2023

CohenCyril Apr 21, 2023

Tragicus Apr 22, 2023

CohenCyril Apr 21, 2023

CohenCyril Apr 21, 2023

Tragicus Apr 22, 2023

CohenCyril Apr 22, 2023

Tragicus commented Jun 8, 2023

CohenCyril commented Jul 21, 2023

Tragicus commented Jul 21, 2023

CohenCyril Jul 25, 2023 •

edited

Loading

CohenCyril Jul 25, 2023

Tragicus Jul 25, 2023 •

edited

Loading

CohenCyril Jul 25, 2023

CohenCyril Jul 25, 2023 •

edited

Loading

CohenCyril Jul 25, 2023

Tragicus Jul 25, 2023

Tragicus Jul 25, 2023

CohenCyril commented Nov 7, 2023

		Lemma primitive_unity_root_char (w : L) (n : nat) :
		n.-primitive_root w -> n%:R != (0 : F0).

	Lemma prim_root_natf_neq0 (F : fieldType) n (w : F) :
	n.-primitive_root w -> (n%:R != 0 :> F).

	\prod_(z <- [seq x + (val i)%:R \| i <- (index_enum (ordinal_finType p))])
	\prod_(i < p) 'X - (x + i%:R)%:P


		Section Temp.

		Lemma ord_S_split n (i: 'I_n.+1): {j: 'I_n \| i = lift ord0 j} + {i = ord0}.

		move=>fgU fgx y /Fadjoin_poly_eq <-.
		move:(Fadjoin_polyOver U x y); generalize (Fadjoin_poly U x y) => p /polyOverP pU.

	{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}.

		\| 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)))

	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).
	Lemma cycle_imset [gT : finGroupType] (g : gT) : <[g]>%g = [set g ^+ (val i) \| i : 'I_#[g]%g]

	[K E : {subfield L}] [x : gal_finGroupType E]
	[K E : {subfield L}] [x : gal E]

Abel-Galois for any characteristic #83

Are you sure you want to change the base?

Abel-Galois for any characteristic #83

Conversation

Tragicus commented Feb 3, 2023

Tragicus commented Feb 3, 2023

CohenCyril Feb 3, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

CohenCyril commented Feb 3, 2023 • edited Loading

Tragicus commented Feb 24, 2023

Tragicus commented Apr 21, 2023

CohenCyril left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Tragicus commented Jun 8, 2023

CohenCyril commented Jul 21, 2023

Tragicus commented Jul 21, 2023

CohenCyril Jul 25, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Tragicus Jul 25, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

CohenCyril Jul 25, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

CohenCyril commented Nov 7, 2023

CohenCyril Feb 3, 2023 •

edited

Loading

CohenCyril commented Feb 3, 2023 •

edited

Loading

CohenCyril Jul 25, 2023 •

edited

Loading

Tragicus Jul 25, 2023 •

edited

Loading

CohenCyril Jul 25, 2023 •

edited

Loading