Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Abel-Galois for any characteristic #83

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Conversation

Tragicus
Copy link

@Tragicus Tragicus commented Feb 3, 2023

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

@Tragicus Tragicus marked this pull request as draft February 3, 2023 15:24
@Tragicus
Copy link
Author

Tragicus commented Feb 3, 2023

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?

theories/abel.v Outdated
Comment on lines 128 to 129
Lemma primitive_unity_root_char (w : L) (n : nat) :
n.-primitive_root w -> n%:R != (0 : F0).
Copy link
Member

@CohenCyril CohenCyril Feb 3, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was here:

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

theories/abel.v Outdated
Comment on lines 715 to 720

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).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this should be renamed big_if and ported back to mathcomp.

@CohenCyril
Copy link
Member

CohenCyril commented Feb 3, 2023

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
Copy link
Author

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
Copy link
Author

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

Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


Section Temp.

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

case: splitP should perform this kind of analysis.

Comment on lines 44 to 45
move=>fgU fgx y /Fadjoin_poly_eq <-.
move:(Fadjoin_polyOver U x y); generalize (Fadjoin_poly U x y) => p /polyOverP pU.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


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}.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

theories/xmathcomp/temp.v Outdated Show resolved Hide resolved
Comment on lines 163 to 164
| 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)))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
| 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)))
| 0 | 1 => id
| n.+2 => fun i => (i + 1)%R

?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

| 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).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

by rewrite -expnD subnK// vp_leq.
Qed.

Lemma muln_gt0 [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this is prodn_gt0

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Quentin VERMANDE and others added 2 commits April 22, 2023 22:25
@Tragicus
Copy link
Author

Tragicus commented Jun 8, 2023

@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
Copy link
Member

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

@Tragicus
Copy link
Author

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

Comment on lines 28 to 36
(* 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.
Copy link
Member

@CohenCyril CohenCyril Jul 25, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Author

@Tragicus Tragicus Jul 25, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

@CohenCyril CohenCyril Jul 25, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

I will update the CI and we'll see

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@Tragicus Tragicus marked this pull request as ready for review August 17, 2023 11:09
@CohenCyril
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants