- -

Library mathcomp.field.algebraics_fundamentals

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- The main result in this file is the existence theorem that underpins the - construction of the algebraic numbers in file algC.v. This theorem simply - asserts the existence of an algebraically closed field with an - automorphism of order 2, and dubbed the Fundamental_Theorem_of_Algebraics - because it is essentially the Fundamental Theorem of Algebra for algebraic - numbers (the more familiar version for complex numbers can be derived by - continuity). - Although our proof does indeed construct exactly the algebraics, we - choose not to expose this in the statement of our Theorem. In algC.v we - construct the norm and partial order of the "complex field" introduced by - the Theorem; as these imply is has characteristic 0, we then get the - algebraics as a subfield. To avoid some duplication a few basic properties - of the algebraics, such as the existence of minimal polynomials, that are - required by the proof of the Theorem, are also proved here. - The main theorem of closed_field supplies us directly with an algebraic - closure of the rationals (as the rationals are a countable field), so all - we really need to construct is a conjugation automorphism that exchanges - the two roots (i and -i) of X^2 + 1, and fixes a (real) subfield of - index 2. This does not require actually constructing this field: the - kHomExtend construction from galois.v supplies us with an automorphism - conj_n of the number field Q[z_n] = Q[x_n, i] for any x_n such that Q[x_n] - does not contain i (e.g., such that Q[x_n] is real). As conj_n will extend - conj_m when Q[x_n] contains x_m, it therefore suffices to construct a - sequence x_n such that - (1) For each n, Q[x_n] is a REAL field containing Q[x_m] for all m <= n. - (2) Each z in C belongs to Q[z_n] = Q[x_n, i] for large enough n. - This, of course, amounts to proving the Fundamental Theorem of Algebra. - Indeed, we use a constructive variant of Artin's algebraic proof of that - Theorem to replace (2) by - (3) Each monic polynomial over Q[x_m] whose constant term is -c^2 for some - c in Q[x_m] has a root in Q[x_n] for large enough n. - We then ensure (3) by setting Q[x_n+1] = Q[x_n, y] where y is the root of - of such a polynomial p found by dichotomy in some interval [0, b] with b - suitably large (such that p[b] >= 0), and p is obtained by decoding n into - a triple (m, p, c) that satisfies the conditions of (3) (taking x_n+1=x_n - if this is not the case), thereby ensuring that all such triples are - ultimately considered. - In more detail, the 600-line proof consists in six (uneven) parts: - (A) - Construction of number fields (~ 100 lines): in order to make use of - the theory developped in falgebra, fieldext, separable and galois we - construct a separate fielExtType Q z for the number field Q[z], with - z in C, the closure of rat supplied by countable_algebraic_closure. - The morphism (ofQ z) maps Q z to C, and the Primitive Element Theorem - lets us define a predicate sQ z characterizing the image of (ofQ z), - as well as a partial inverse (inQ z) to (ofQ z). - (B) - Construction of the real extension Q[x, y] (~ 230 lines): here y has - to be a root of a polynomial p over Q[x] satisfying the conditions of - (3), and Q[x] should be real and archimedean, which we represent by - a morphism from Q x to some archimedean field R, as the ssrnum and - fieldext structures are not compatible. The construction starts by - weakening the condition p[0] = -c^2 to p[0] <= 0 (in R), then reducing - to the case where p is the minimal polynomial over Q[x] of some y (in - some Q[w] that contains x and all roots of p). Then we only need to - construct a realFieldType structure for Q[t] = Q[x,y] (we don't even - need to show it is consistent with that of R). This amounts to fixing - the sign of all z != 0 in Q[t], consistently with arithmetic in Q[t]. - Now any such z is equal to q[y] for some q in Q[x] [X] coprime with p. - Then up + vq = 1 for Bezout coefficients u and v. As p is monic, there - is some b0 >= 0 in R such that p changes sign in ab0 = [0; b0]. As R - is archimedean, some iteration of the binary search for a root of p in - ab0 will yield an interval ab_n such that |up[d]| < 1/2 for d in ab_n. - Then |q[d]| > 1/2M > 0 for any upper bound M on |v[X]| in ab0, so q - cannot change sign in ab_n (as then root-finding in ab_n would yield a - d with |Mq[d]| < 1/2), so we can fix the sign of z to that of q in - ab_n. - (C) - Construction of the x_n and z_n (~50 lines): x n is obtained by - iterating (B), starting with x_0 = 0, and then (A) and the PET yield - z n. We establish (1) and (3), and that the minimal polynomial of the - preimage i n of i over the preimage R n of Q[x_n] is X^2 + 1. - (D) - Establish (2), i.e., prove the FTA (~180 lines). We must depart from - Artin's proof because deciding membership in the union of the Q[x_n] - requires the FTA, i.e., we cannot (yet) construct a maximal real - subfield of C. We work around this issue by first reducing to the case - where Q[z] is Galois over Q and contains i, then using induction over - the degree of z over Q[z n] (i.e., the degree of a monic polynomial - over Q[z_n] that has z as a root). We can assume that z is not in - Q[z_n]; then it suffices to find some y in Q[z_n, z] \ Q[z_n] that is - also in Q[z_m] for some m > n, as then we can apply induction with the - minimal polynomial of z over Q[z_n, y]. In any Galois extension Q[t] - of Q that contains both z and z_n, Q[x_n, z] = Q[z_n, z] is Galois - over both Q[x_n] and Q[z_n]. If Gal(Q[x_n,z] / Q[x_n]) isn't a 2-group - take one of its Sylow 2-groups P; the minimal polynomial p of any - generator of the fixed field F of P over Q[x_n] has odd degree, hence - by (3) - p[X]p[-X] and thus p has a root y in some Q[x_m], hence in - Q[z_m]. As F is normal, y is in F, with minimal polynomial p, and y - is not in Q[z_n] = Q[x_n, i] since p has odd degree. Otherwise, - Gal(Q[z_n,z] / Q[z_n]) is a proper 2-group, and has a maximal subgroup - P of index 2. The fixed field F of P has a generator w over Q[z_n] - with w^2 in Q[z_n] \ Q[x_n], i.e. w^2 = u + 2iv with v != 0. From (3) - X^4 - uX^2 - v^2 has a root x in some Q[x_m]; then x != 0 as v != 0, - hence w^2 = y^2 for y = x + iv/x in Q[z_m], and y generates F. - (E) - Construct conj and conclude (~40 lines): conj z is defined as - conj n z with the n provided by (2); since each conj m is a morphism - of order 2 and conj z = conj m z for any m >= n, it follows that conj - is also a morphism of order 2. - Note that (C), (D) and (E) only depend on Q[x_n] not containing i; the - order structure is not used (hence we need not prove that the ordering of - Q[x_m] is consistent with that of Q[x_n] for m >= n). -

- -
-Set Implicit Arguments.
- -
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
- -
- -
-Lemma rat_algebraic_archimedean (C : numFieldType) (QtoC : Qmorphism C) :
-  integralRange QtoC → Num.archimedean_axiom C.
- -
-Definition decidable_embedding sT T (f : sT → T) :=
-  ∀ y, decidable (∃ x, y = f x).
- -
-Lemma rat_algebraic_decidable (C : fieldType) (QtoC : Qmorphism C) :
-  integralRange QtoC → decidable_embedding QtoC.
- -
-Lemma minPoly_decidable_closure
-  (F : fieldType) (L : closedFieldType) (FtoL : {rmorphism F → L }) x :
-    decidable_embedding FtoL → integralOver FtoL x →
-  {p | [/\ p \is monic , root (p ^ FtoL) x & irreducible_poly p ]}.
- -
-Lemma alg_integral (F : fieldType) (L : fieldExtType F) :
-  integralRange (in_alg L).
- -
-Import DefaultKeying GRing.DefaultPred.
- -
-Theorem Fundamental_Theorem_of_Algebraics :
-  {L : closedFieldType &
-     {conj : {rmorphism L → L } | involutive conj & ¬ conj =1 id }}.
-