+ +

Library mathcomp.field.algebraics_fundamentals

+ +

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

+ +

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