# Library MathComp.algebraics_fundamentals

(* (c) Copyright Microsoft Corporation and Inria.

You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice div fintype.

Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.

Require Import countalg ssrnum ssrint rat intdiv.

Require Import fingroup finalg zmodp cyclic pgroup sylow.

Require Import vector falgebra fieldext separable galois.

You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice div fintype.

Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.

Require Import countalg ssrnum ssrint rat intdiv.

Require Import fingroup finalg zmodp cyclic pgroup sylow.

Require Import vector falgebra fieldext separable galois.

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.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.

Local Notation "p ^@" := (p ^ in_alg _) (at level 2, format "p ^@"): ring_scope.

Local Notation "<< E ; u >>" := <<E; u>>%VS.

Local Notation Qmorphism C := {rmorphism rat → C}.

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

Lemma imaginary_exists (C : closedFieldType) : {i : C | i ^+ 2 = -1}.

Import DefaultKeying GRing.DefaultPred.

Implicit Arguments map_poly_inj [[F] [R] x1 x2].

Theorem Fundamental_Theorem_of_Algebraics :

{L : closedFieldType &

{conj : {rmorphism L → L} | involutive conj & ¬ conj =1 id}}.