math-comp
Abel-Galois for any characteristic
Generalizes the definition of radical extension and the Abel-Galois theorem to fields of any characteristic.
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?
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!
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 ?
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 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.
@Tragicus I performed some refactorings and simplifications. Tell me what you think.
@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.
@Tragicus FYI I'm porting this to mathcomp 2, then I'll squash and merge.