Library mathcomp.field.algebraics_fundamentals

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