proposition: Theorem Fundamental_Theorem_of_Algebraics : {L : closedFieldType & {conj : {rmorphism L -> L} | involutive conj & ~ conj =1 id}}.
proof: Proof. have maxn3 n1 n2 n3: {m | [/\ n1 <= m, n2 <= m & n3 <= m]%N}. by exists (maxn n1 (maxn n2 n3)); apply/and3P; rewrite -!geq_max. have [C [/= QtoC algC]] := countable_algebraic_closure rat. exists C; have [i Di2] := GRing.imaginary_exists C. pose Qfield := fieldExtType rat. pose Cmorph (L : Qfield) := {rmorphism L -> C}. have charQ (L : Qfield): [char L] =i pred0 := ftrans (char_lalg L) (char_num _). have sepQ (L : Qfield) (K E : {subfield L}): separable K E. by apply/separableP=> u _; apply: charf0_separable. pose genQfield z L := {LtoC : Cmorph L & {u | LtoC u = z & <<1; u>> = fullv}}. have /all_tag[Q /all_tag[ofQ genQz]] z: {Qz : Qfield & genQfield z Qz}. have [|p [/monic_neq0 nzp pz0 irr_p]] := minPoly_decidable_closure _ (algC z). exact: rat_algebraic_decidable. pose Qz := SubFieldExtType pz0 irr_p. pose QzC : {rmorphism _ -> _} := @subfx_inj _ _ QtoC z p. exists Qz, QzC, (subfx_root QtoC z p); first exact: subfx_inj_root. apply/vspaceP=> u; rewrite memvf; apply/Fadjoin1_polyP. by have [q] := subfxEroot pz0 nzp u; exists q. have pQof z p: p^@ ^ ofQ z = p ^ QtoC. by rewrite -map_poly_comp; apply: eq_map_poly => x; rewrite !fmorph_eq_rat. have pQof2 z p u: ofQ z p^@.[u] = (p ^ QtoC).[ofQ z u]. by rewrite -horner_map pQof. have PET_Qz z (E : {subfield Q z}): {u | <<1; u>> = E}. exists (separable_generator 1 E). by rewrite -eq_adjoin_separable_generator ?sub1v. pose gen z x := exists q, x = (q ^ QtoC).[z]. have PET2 x y: {z | gen z x & gen z y}. pose Gxy := (x, y) = let: (p, q, z) := _ in ((p ^ QtoC).[z], (q ^ QtoC).[z]). suffices [[[p q] z] []]: {w | Gxy w} by exists z; [exists p | exists q]. apply/sig_eqW; have /integral_algebraic[px nz_px pxx0] := algC x. have /integral_algebraic[py nz_py pyy0] := algC y. have [n [[p Dx] [q Dy]]] := char0_PET nz_px pxx0 nz_py pyy0 (char_num _). by exists (p, q, y *+ n - x); congr (_, _). have gen_inQ z x: gen z x -> {u | ofQ z u = x}. have [u Dz _] := genQz z => /sig_eqW[q ->]. by exists q^@.[u]; rewrite pQof2 Dz. have gen_ofP z u v: reflect (gen (ofQ z u) (ofQ z v)) (v \in <<1; u>>). apply: (iffP Fadjoin1_polyP) => [[q ->]|]; first by rewrite pQof2; exists q. by case=> q; rewrite -pQof2 => /fmorph_inj->; exists q. have /all_tag[sQ genP] z: {s : pred C & forall x, reflect (gen z x) (x \in s)}. apply: all_tag (fun x => reflect (gen z x)) _ => x. have [w /gen_inQ[u <-] /gen_inQ[v <-]] := PET2 z x. by exists (v \in <<1; u>>)%VS; apply: gen_ofP. have sQtrans: transitive (fun x z => x \in sQ z). move=> x y z /genP[p ->] /genP[q ->]; apply/genP; exists (p \Po q). by rewrite map_comp_poly horner_comp. have sQid z: z \in sQ z by apply/genP; exists 'X; rewrite map_polyX hornerX. have{gen_ofP} sQof2 z u v: (ofQ z u \in sQ (ofQ z v)) = (u \in <<1; v>>%VS). exact/genP/(gen_ofP z). have sQof z v: ofQ z v \in sQ z. by have [u Dz defQz] := genQz z; rewrite -[in sQ z]Dz sQof2 defQz memvf. have{gen_inQ} sQ_inQ z x z_x := gen_inQ z x (genP z x z_x). have /all_sig[inQ inQ_K] z: {inQ | {in sQ z, cancel inQ (ofQ z)}}. by apply: all_sig_cond (fun x u => ofQ z u = x) 0 _ => x /sQ_inQ. have ofQ_K z: cancel (ofQ z) (inQ z). by move=> x; have /inQ_K/fmorph_inj := sQof z x. have sQring z: divring_closed (sQ z). have sQ_1: 1 \in sQ z by rewrite -(rmorph1 (ofQ z)) sQof. by split=> // x y /inQ_K<- /inQ_K<- /=; rewrite -(rmorphB, fmorph_div) sQof. pose sQoM z := GRing.isOppClosed.Build _ _ (sQring z). pose sQaM z := GRing.isAddClosed.Build _ _ (sQring z). pose sQmM z := GRing.isMulClosed.Build _ _ (sQring z). pose sQiM z := GRing.isInvClosed.Build _ _ (sQring z). pose sQC z : divringClosed _ := HB.pack (sQ z) (sQaM z) (sQoM z) (sQmM z) (sQiM z). pose morph_ofQ x z Qxz := forall u, ofQ z (Qxz u) = ofQ x u. have QtoQ z x: x \in sQ z -> {Qxz : 'AHom(Q x, Q z) | morph_ofQ x z Qxz}. move=> z_x; pose Qxz u := inQ z (ofQ x u). have QxzE u: ofQ z (Qxz u) = ofQ x u by apply/inQ_K/(sQtrans x). have Qxza : additive Qxz. by move=> u v; apply: (canLR (ofQ_K z)); rewrite !rmorphB !QxzE. have Qxzm : multiplicative Qxz. by split=> [u v|]; apply: (canLR (ofQ_K z)); rewrite ?rmorph1 ?rmorphM /= ?QxzE. have QxzaM := GRing.isAdditive.Build _ _ _ Qxza. have QxzmM := GRing.isMultiplicative.Build _ _ _ Qxzm. have QxzlM := GRing.isScalable.Build _ _ _ _ _ (rat_linear Qxza). pose QxzLRM : {lrmorphism _ -> _} := HB.pack Qxz QxzaM QxzmM QxzlM. by exists (linfun_ahom QxzLRM) => u; rewrite lfunE QxzE. pose sQs z s := all (mem (sQ z)) s. have inQsK z s: sQs z s -> map (ofQ z) (map (inQ z) s) = s. by rewrite -map_comp => /allP/(_ _ _)/inQ_K; apply: map_id_in. have inQpK z p: p \is a polyOver (sQ z) -> (p ^ inQ z) ^ ofQ z = p. by move=> /allP/(_ _ _)/inQ_K/=/map_poly_id; rewrite -map_poly_comp. have{gen PET2 genP} PET s: {z | sQs z s & <<1 & map (inQ z) s>>%VS = fullv}. have [y /inQsK Ds]: {y | sQs y s}. elim: s => [|x s /= [y IHs]]; first by exists 0. have [z /genP z_x /genP z_y] := PET2 x y. by exists z; rewrite /= {x}z_x; apply: sub_all IHs => x /sQtrans/= ->. have [w defQs] := PET_Qz _ <<1 & map (inQ y) s>>%AS; pose z := ofQ y w. have z_s: sQs z s. rewrite -Ds /sQs all_map; apply/allP=> u s_u /=. by rewrite sQof2 defQs seqv_sub_adjoin. have [[u Dz defQz] [Qzy QzyE]] := (genQz z, QtoQ y z (sQof y w)). exists z => //; apply/eqP; rewrite eqEsubv subvf /= -defQz. rewrite -(limg_ker0 _ _ (AHom_lker0 Qzy)) aimg_adjoin_seq aimg_adjoin aimg1. rewrite -[map _ _](mapK (ofQ_K y)) -(map_comp (ofQ y)) (eq_map QzyE) inQsK //. by rewrite -defQs -(canLR (ofQ_K y) Dz) -QzyE ofQ_K. pose rp s := \prod_(z <- s) ('X - z%:P). have map_rp (f : {rmorphism _ -> _}) s: rp _ s ^ f = rp _ (map f s). rewrite rmorph_prod /rp big_map; apply: eq_bigr => x _ /=. by rewrite rmorphB /= map_polyX map_polyC. pose is_Gal z := SplittingField.axiom (Q z). have galQ x: {z | x \in sQ z & is_Gal z}. have /sig2W[p mon_p pz0] := algC x. have [s Dp] := closed_field_poly_normal (p ^ QtoC). rewrite (monicP _) ?monic_map // scale1r in Dp; have [z z_s defQz] := PET s. exists z; first by apply/(allP z_s); rewrite -root_prod_XsubC -Dp. exists p^@; first exact: alg_polyOver. exists (map (inQ z) s); last by apply/vspaceP=> u; rewrite defQz memvf. by rewrite -(eqp_map (ofQ z)) pQof Dp map_rp inQsK ?eqpxx. pose is_realC x := {R : archiFieldType & {rmorphism Q x -> R}}. pose realC := {x : C & is_realC x}. pose has_Rroot (xR : realC) p c (Rx := sQ (tag xR)) := [&& p \is a polyOver Rx, p \is monic, c \in Rx & p.[0] == - c ^+ 2]. pose root_in (xR : realC) p := exists2 w, w \in sQ (tag xR) & root p w. pose extendsR (xR yR : realC) := tag xR \in sQ (tag yR). have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. rewrite {}/extendsR; case: (has_Rroot xR p c) / and4P; last by exists xR. case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {}p mon_p /inQ_K<- Dc. have{c Dc} p0_le0: (p ^ QxR).[0] <= 0. rewrite horner_coef0 coef_map -[p`_0]ofQ_K -coef_map -horner_coef0 (eqP Dc). by rewrite -rmorphXn -rmorphN ofQ_K /= rmorphN rmorphXn oppr_le0 sqr_ge0. have [s Dp] := closed_field_poly_normal (p ^ ofQ x). have{Dp} /all_and2[s_p p_s] y: root (p ^ ofQ x) y <-> (y \in s). by rewrite Dp (monicP mon_p) scale1r root_prod_XsubC. rewrite map_monic in mon_p; have [z /andP[z_x /allP/=z_s] _] := PET (x :: s). have{z_x} [[Qxz QxzE] Dx] := (QtoQ z x z_x, inQ_K z x z_x). pose Qx := <<1; inQ z x>>%AS. have pQwx q1: q1 \is a polyOver Qx -> {q | q1 = q ^ Qxz}. move/polyOverP=> Qx_q1; exists ((q1 ^ ofQ z) ^ inQ x). apply: (map_poly_inj (ofQ z)); rewrite -map_poly_comp (eq_map_poly QxzE). by rewrite inQpK ?polyOver_poly // => j _; rewrite -Dx sQof2 Qx_q1. have /all_sig[t_ Dt] u: {t | <<1; t>> = <<Qx; u>>} by apply: PET_Qz. suffices{p_s}[u Ry px0]: {u : Q z & is_realC (ofQ z (t_ u)) & ofQ z u \in s}. exists (Tagged is_realC Ry) => [|_] /=. by rewrite -Dx sQof2 Dt subvP_adjoin ?memv_adjoin. by exists (ofQ z u); rewrite ?p_s // sQof2 Dt memv_adjoin. without loss{z_s s_p} [u Dp s_y]: p mon_p p0_le0 / {u | minPoly Qx u = p ^ Qxz & ofQ z u \in s}. - move=> IHp; move: {2}_.+1 (ltnSn (size p)) => d. elim: d => // d IHd in p mon_p s_p p0_le0 *; rewrite ltnS => le_p_d. have /closed_rootP/sig_eqW[y py0]: size (p ^ ofQ x) != 1. rewrite size_map_poly size_poly_eq1 eqp_monic ?rpred1 //. by apply: contraTneq p0_le0 => ->; rewrite rmorph1 hornerC lt_geF ?ltr01. have /s_p s_y := py0; have /z_s/sQ_inQ[u Dy] := s_y. have /pQwx[q Dq] := minPolyOver Qx u. have mon_q: q \is monic by have:= monic_minPoly Qx u; rewrite Dq map_monic. have /dvdpP/sig_eqW[r Dp]: q %| p. rewrite -(dvdp_map Qxz) -Dq minPoly_dvdp //. by apply: polyOver_poly => j _; rewrite -sQof2 QxzE Dx. by rewrite -(fmorph_root (ofQ z)) Dy -map_poly_comp (eq_map_poly QxzE). have mon_r: r \is monic by rewrite Dp monicMr in mon_p. have [q0_le0 | q0_gt0] := lerP ((q ^ QxR).[0]) 0. by apply: (IHp q) => //; exists u; rewrite ?Dy. have r0_le0: (r ^ QxR).[0] <= 0. by rewrite -(ler_pM2r q0_gt0) mul0r -hornerM -rmorphM -Dp. apply: (IHd r mon_r) => // [w rw0|]. by rewrite s_p // Dp rmorphM rootM rw0. apply: leq_trans le_p_d; rewrite Dp size_Mmonic ?monic_neq0 // addnC. by rewrite -(size_map_poly Qxz q) -Dq size_minPoly !ltnS leq_addl. exists u => {s s_y}//; set y := ofQ z (t_ u); set p1 := minPoly Qx u in Dp. have /QtoQ[Qyz QyzE]: y \in sQ z := sQof z (t_ u). pose q1_ v := Fadjoin_poly Qx u (Qyz v). have{} QyzE v: Qyz v = (q1_ v).[u]. by rewrite Fadjoin_poly_eq // -Dt -sQof2 QyzE sQof. have /all_sig2[q_ coqp Dq] v: {q | v != 0 -> coprimep p q & q ^ Qxz = q1_ v}. have /pQwx[q Dq]: q1_ v \is a polyOver Qx by apply: Fadjoin_polyOver. exists q => // nz_v; rewrite -(coprimep_map Qxz) -Dp -Dq -gcdp_eqp1. have /minPoly_irr/orP[] // := dvdp_gcdl p1 (q1_ v). by rewrite gcdp_polyOver ?minPolyOver ?Fadjoin_polyOver. rewrite -/p1 {1}/eqp dvdp_gcd => /and3P[_ _ /dvdp_leq/=/implyP]. rewrite size_minPoly ltnNge size_poly (contraNneq _ nz_v) // => q1v0. by rewrite -(fmorph_eq0 Qyz) /= QyzE q1v0 horner0. pose h2 : R := 2^-1; have nz2: 2 != 0 :> R by rewrite pnatr_eq0. pose itv ab := [pred c : R | ab.1 <= c <= ab.2]. pose wid ab : R := ab.2 - ab.1; pose mid ab := (ab.1 + ab.2) * h2. pose sub_itv ab cd := cd.1 <= ab.1 :> R /\ ab.2 <= cd.2 :> R. pose xup q ab := [/\ q.[ab.1] <= 0, q.[ab.2] >= 0 & ab.1 <= ab.2 :> R]. pose narrow q ab (c := mid ab) := if q.[c] >= 0 then (ab.1, c) else (c, ab.2). pose find k q := iter k (narrow q). have findP k q ab (cd := find k q ab): xup q ab -> [/\ xup q cd, sub_itv cd ab & wid cd = wid ab / (2 ^ k)%:R]. - rewrite {}/cd; case: ab => a b xq_ab. elim: k => /= [|k]; first by rewrite divr1. case: (find k q _) => c d [[/= qc_le0 qd_ge0 le_cd] [/= le_ac le_db] Dcd]. have [/= le_ce le_ed] := midf_le le_cd; set e := _ / _ in le_ce le_ed. rewrite expnSr natrM invfM mulrA -{}Dcd /narrow /= -[mid _]/e. have [qe_ge0 // | /ltW qe_le0] := lerP 0 q.[e]. do ?split=> //=; [exact: (le_trans le_ed) | apply: canRL (mulfK nz2) _]. by rewrite mulrBl divfK // mulr_natr opprD addrACA subrr add0r. do ?split=> //=; [exact: (le_trans le_ac) | apply: canRL (mulfK nz2) _]. by rewrite mulrBl divfK // mulr_natr opprD addrACA subrr addr0. have find_root r q ab: xup q ab -> {n | forall x, x \in itv (find n q ab) ->`|(r * q).[x]| < h2}. - move=> xab; have ub_ab := poly_itv_bound _ ab.1 ab.2. have [Mu MuP] := ub_ab r; have /all_sig[Mq MqP] j := ub_ab q^`N(j). pose d := wid ab; pose dq := \poly_(i < (size q).-1) Mq i.+1. have d_ge0: 0 <= d by rewrite subr_ge0; case: xab. have [Mdq MdqP] := poly_disk_bound dq d. pose n := Num.bound (Mu * Mdq * d); exists n => c /andP[]. have{xab} [[]] := findP n _ _ xab; case: (find n q ab) => a1 b1 /=. rewrite -/d => qa1_le0 qb1_ge0 le_ab1 [/= le_aa1 le_b1b] Dab1 le_a1c le_cb1. have /MuP lbMu: c \in itv ab. by rewrite inE (le_trans le_aa1) ?(le_trans le_cb1). have Mu_ge0: 0 <= Mu by rewrite (le_trans _ lbMu). have Mdq_ge0: 0 <= Mdq. by rewrite (le_trans _ (MdqP 0 _)) ?normr0. suffices lb1 a2 b2 (ab1 := (a1, b1)) (ab2 := (a2, b2)) : xup q ab2 /\ sub_itv ab2 ab1 -> q.[b2] - q.[a2] <= Mdq * wid ab1. + apply: le_lt_trans (_ : Mu * Mdq * wid (a1, b1) < h2); last first. rewrite {}Dab1 mulrA ltr_pdivrMr ?ltr0n ?expn_gt0 //. rewrite (lt_le_trans (archi_boundP _)) ?mulr_ge0 ?ltr_nat // -/n. rewrite ler_pdivlMl ?ltr0n // -natrM ler_nat. by case: n => // n; rewrite expnS leq_pmul2l // ltn_expl. rewrite -mulrA hornerM normrM ler_pM //. have [/ltW qc_le0 | qc_ge0] := ltrP q.[c] 0. by apply: le_trans (lb1 c b1 _); rewrite ?ler0_norm ?ler_wpDl. by apply: le_trans (lb1 a1 c _); rewrite ?ger0_norm ?ler_wpDr ?oppr_ge0. case{c le_a1c le_cb1 lbMu}=> [[/=qa2_le0 qb2_ge0 le_ab2] [/=le_a12 le_b21]]. pose h := b2 - a2; have h_ge0: 0 <= h by rewrite subr_ge0. have [-> | nz_q] := eqVneq q 0. by rewrite !horner0 subrr mulr_ge0 ?subr_ge0. rewrite -(subrK a2 b2) (addrC h) (nderiv_taylor q (mulrC a2 h)). rewrite (polySpred nz_q) big_ord_recl /= mulr1 nderivn0 addrC addKr. have [le_aa2 le_b2b] := (le_trans le_aa1 le_a12, le_trans le_b21 le_b1b). have /MqP MqPx1: a2 \in itv ab by rewrite inE le_aa2 (le_trans le_ab2). apply: le_trans (le_trans (ler_norm _) (ler_norm_sum _ _ _)) _. apply: le_trans (_ : `|dq.[h] * h| <= _); last first. by rewrite normrM ler_pM ?normr_ge0 ?MdqP // ?ger0_norm ?lerB ?h_ge0. rewrite horner_poly ger0_norm ?mulr_ge0 ?sumr_ge0 // => [|j _]; last first. by rewrite mulr_ge0 ?exprn_ge0 // (le_trans _ (MqPx1 _)). rewrite mulr_suml ler_sum // => j _; rewrite normrM -mulrA -exprSr. by rewrite ler_pM // normrX ger0_norm. have [ab0 xab0]: {ab | xup (p ^ QxR) ab}. have /monic_Cauchy_bound[b pb_gt0]: p ^ QxR \is monic by apply: monic_map. by exists (0, `|b|); rewrite /xup normr_ge0 p0_le0 ltW ?pb_gt0 ?ler_norm. pose ab_ n := find n (p ^ QxR) ab0; pose Iab_ n := itv (ab_ n). pose lim v a := (q_ v ^ QxR).[a]; pose nlim v n := lim v (ab_ n).2. have lim0 a: lim 0 a = 0. rewrite /lim; suffices /eqP ->: q_ 0 == 0 by rewrite rmorph0 horner0. by rewrite -(map_poly_eq0 Qxz) Dq /q1_ !raddf0. have limN v a: lim (- v) a = - lim v a. rewrite /lim; suffices ->: q_ (- v) = - q_ v by rewrite rmorphN hornerN. apply: (map_poly_inj Qxz). by rewrite Dq /q1_ (raddfN _ v) (raddfN _ (Qyz v)) [RHS]raddfN /= Dq. pose lim_nz n v := exists2 e, e > 0 & {in Iab_ n, forall a, e < `|lim v a| }. have /(all_sig_cond 0)[n_ nzP] v: v != 0 -> {n | lim_nz n v}. move=> nz_v; do [move/(_ v nz_v); rewrite -(coprimep_map QxR)] in coqp. have /sig_eqW[r r_pq_1] := Bezout_eq1_coprimepP _ _ coqp. have /(find_root r.1)[n ub_rp] := xab0; exists n. have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}. have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2. exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite lt_max ltr01. by rewrite le_max orbC vM. exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n. rewrite ltr_pdivrMr // -(ltrD2l h2) -mulr2n -mulr_natl divff //. rewrite -normr1 -(hornerC 1 a) -[1%:P]r_pq_1 hornerD. rewrite ?(le_lt_trans (ler_normD _ _)) ?ltr_leD ?ub_rp //. by rewrite mulrC hornerM normrM ler_wpM2l ?ubM. have ab_le m n: (m <= n)%N -> (ab_ n).2 \in Iab_ m. move/subnKC=> <-; move: {n}(n - m)%N => n; rewrite /ab_. have /(findP m)[/(findP n)[[_ _]]] := xab0. rewrite /find -iterD -!/(find _ _) -!/(ab_ _) addnC !inE. by move: (ab_ _) => /= ab_mn le_ab_mn [/le_trans->]. pose lt v w := 0 < nlim (w - v) (n_ (w - v)). have posN v: lt 0 (- v) = lt v 0 by rewrite /lt subr0 add0r. have posB v w: lt 0 (w - v) = lt v w by rewrite /lt subr0. have posE n v: (n_ v <= n)%N -> lt 0 v = (0 < nlim v n). rewrite /lt subr0 /nlim => /ab_le; set a := _.2; set b := _.2 => Iv_a. have [-> | /nzP[e e_gt0]] := eqVneq v 0; first by rewrite !lim0 ltxx. move: (n_ v) => m in Iv_a b * => v_gte. without loss lt0v: v v_gte / 0 < lim v b. move=> IHv; apply/idP/idP => [v_gt0 | /ltW]; first by rewrite -IHv. rewrite lt_def -normr_gt0 ?(lt_trans _ (v_gte _ _)) ?ab_le //=. rewrite !leNgt -!oppr_gt0 -!limN; apply: contra => v_lt0. by rewrite -IHv // => c /v_gte; rewrite limN normrN. rewrite lt0v (lt_trans e_gt0) ?(lt_le_trans (v_gte a Iv_a)) //. rewrite ger0_norm // leNgt; apply/negP=> /ltW lev0. have [le_a le_ab] : _ /\ a <= b := andP Iv_a. have xab: xup (q_ v ^ QxR) (a, b) by move/ltW in lt0v. have /(find_root (h2 / e)%:P)[n1] := xab; have /(findP n1)[[_ _]] := xab. case: (find _ _ _) => c d /= le_cd [/= le_ac le_db] _ /(_ c)/implyP. rewrite inE lexx le_cd hornerM hornerC normrM le_gtF //. rewrite ger0_norm ?divr_ge0 ?invr_ge0 ?ler0n ?(ltW e_gt0) // mulrAC. rewrite ler_pdivlMr // ler_wpM2l ?invr_ge0 ?ler0n // ltW // v_gte //=. by rewrite inE -/b (le_trans le_a) //= (le_trans le_cd). pose lim_pos m v := exists2 e, e > 0 & forall n, (m <= n)%N -> e < nlim v n. have posP v: reflect (exists m, lim_pos m v) (lt 0 v). apply: (iffP idP) => [v_gt0|[m [e e_gt0 v_gte]]]; last first. by rewrite (posE _ _ (leq_maxl _ m)) (lt_trans e_gt0) ?v_gte ?leq_maxr. have [|e e_gt0 v_gte] := nzP v. by apply: contraTneq v_gt0 => ->; rewrite /lt subr0 /nlim lim0 ltxx. exists (n_ v), e => // n le_vn; rewrite (posE n) // in v_gt0. by rewrite -(ger0_norm (ltW v_gt0)) v_gte ?ab_le. have posNneg v: lt 0 v -> ~~ lt v 0. case/posP=> m [d d_gt0 v_gtd]; rewrite -posN. apply: contraL d_gt0 => /posP[n [e e_gt0 nv_gte]]. rewrite lt_gtF // (lt_trans (v_gtd _ (leq_maxl m n))) // -oppr_gt0. by rewrite /nlim -limN (lt_trans e_gt0) ?nv_gte ?leq_maxr. have posVneg v: v != 0 -> lt 0 v || lt v 0. case/nzP=> e e_gt0 v_gte; rewrite -posN; set w := - v. have [m [le_vm le_wm _]] := maxn3 (n_ v) (n_ w) 0; rewrite !(posE m) //. by rewrite /nlim limN -ltr_normr (lt_trans e_gt0) ?v_gte ?ab_le. have posD v w: lt 0 v -> lt 0 w -> lt 0 (v + w). move=> /posP[m [d d_gt0 v_gtd]] /posP[n [e e_gt0 w_gte]]. apply/posP; exists (maxn m n), (d + e) => [|k]; first exact: addr_gt0. rewrite geq_max => /andP[le_mk le_nk]; rewrite /nlim /lim. have ->: q_ (v + w) = q_ v + q_ w. by apply: (map_poly_inj Qxz); rewrite rmorphD /= !{1}Dq /q1_ !raddfD. by rewrite rmorphD hornerD ltrD ?v_gtd ?w_gte. have posM v w: lt 0 v -> lt 0 w -> lt 0 (v * w). move=> /posP[m [d d_gt0 v_gtd]] /posP[n [e e_gt0 w_gte]]. have /dvdpP[r /(canRL (subrK _))Dqvw]: p %| q_ (v * w) - q_ v * q_ w. rewrite -(dvdp_map Qxz) rmorphB rmorphM /= !Dq -Dp minPoly_dvdp //. by rewrite rpredB 1?rpredM ?Fadjoin_polyOver. by rewrite rootE !hornerE -!QyzE rmorphM subrr. have /(find_root ((d * e)^-1 *: r ^ QxR))[N ub_rp] := xab0. pose f := d * e * h2; apply/posP; exists (maxn N (maxn m n)), f => [|k]. by rewrite !mulr_gt0 ?invr_gt0 ?ltr0n. rewrite !geq_max => /and3P[/ab_le/ub_rp{}ub_rp le_mk le_nk]. rewrite -(ltrD2r f) -mulr2n -mulr_natr divfK // /nlim /lim Dqvw. rewrite rmorphD hornerD /= -addrA -ltrBlDl ler_ltD //. by rewrite rmorphM hornerM ler_pM ?ltW ?v_gtd ?w_gte. rewrite -ltr_pdivrMl ?mulr_gt0 // (le_lt_trans _ ub_rp) //. by rewrite -scalerAl hornerZ -rmorphM mulrN -normrN ler_norm. pose le v w := (v == w) || lt v w. pose abs v := if le 0 v then v else - v. have absN v: abs (- v) = abs v. rewrite /abs /le !(eq_sym 0) oppr_eq0 opprK posN. have [-> | /posVneg/orP[v_gt0 | v_lt0]] := eqVneq; first by rewrite oppr0. by rewrite v_gt0 /= -if_neg posNneg. by rewrite v_lt0 /= -if_neg -(opprK v) posN posNneg ?posN. have absE v: le 0 v -> abs v = v by rewrite /abs => ->. pose RyM := Num.IntegralDomain_isLtReal.Build (Q y) posD posM posNneg posB posVneg absN absE (rrefl _). pose Ry : realFieldType := HB.pack (Q y) RyM. have QisArchi : Num.NumDomain_bounded_isArchimedean Ry. by constructor; apply: (@rat_algebraic_archimedean Ry _ alg_integral). exists (HB.pack_for archiFieldType _ QisArchi); apply: idfun. have some_realC: realC. suffices /all_sig[f QfK] x: {a | in_alg (Q 0) a = x}. have fA : additive f. exact: can2_additive (inj_can_sym QfK (fmorph_inj _)) QfK. have fM : multiplicative f. exact: can2_rmorphism (inj_can_sym QfK (fmorph_inj _)) QfK. pose faM := GRing.isAdditive.Build _ _ _ fA. pose fmM := GRing.isMultiplicative.Build _ _ _ fM. pose fRM : GRing.RMorphism.type _ _ := HB.pack f faM fmM. by exists 0, rat; exact: fRM. have /Fadjoin1_polyP/sig_eqW[q]: x \in <<1; 0>>%VS by rewrite -sQof2 rmorph0. by exists q.[0]; rewrite -horner_map rmorph0. pose fix xR n : realC := if n isn't n'.+1 then some_realC else if unpickle (nth 0 (CodeSeq.decode n') 1) isn't Some (p, c) then xR n' else tag (add_Rroot (xR n') p c). pose x_ n := tag (xR n). have sRle m n: (m <= n)%N -> {subset sQ (x_ m) <= sQ (x_ n)}. move/subnK <-; elim: {n}(n - m)%N => // n IHn x /IHn{IHn}Rx. rewrite addSn /x_ /=; case: (unpickle _) => [[p c]|] //=. by case: (add_Rroot _ _ _) => yR /= /(sQtrans _ x)->. have xRroot n p c: has_Rroot (xR n) p c -> {m | n <= m & root_in (xR m) p}%N. case/and4P=> Rp mon_p Rc Dc; pose m := CodeSeq.code [:: n; pickle (p, c)]. have le_n_m: (n <= m)%N by apply/ltnW/(allP (CodeSeq.ltn_code _))/mem_head. exists m.+1; rewrite ?leqW /x_ //= CodeSeq.codeK pickleK. case: (add_Rroot _ _ _) => yR /= _; apply; apply/and4P. by split=> //; first apply: polyOverS Rp; apply: (sRle n). have /all_sig[z_ /all_and3[Ri_R Ri_i defRi]] n (x := x_ n): {z | [/\ x \in sQ z, i \in sQ z & <<<<1; inQ z x>>; inQ z i>> = fullv]}. - have [z /and3P[z_x z_i _] Dzi] := PET [:: x; i]. by exists z; rewrite -adjoin_seq1 -adjoin_cons. pose i_ n := inQ (z_ n) i; pose R_ n := <<1; inQ (z_ n) (x_ n)>>%AS. have memRi n: <<R_ n; i_ n>> =i predT by move=> u; rewrite defRi memvf. have sCle m n: (m <= n)%N -> {subset sQ (z_ m) <= sQ (z_ n)}. move/sRle=> Rmn _ /sQ_inQ[u <-]. have /Fadjoin_polyP[p /polyOverP Rp ->] := memRi m u. rewrite -horner_map inQ_K ?(@rpred_horner _ (sQC _)) //=. apply/polyOver_poly=> j _. by apply: sQtrans (Ri_R n); rewrite Rmn // -(inQ_K _ _ (Ri_R m)) sQof2. have R'i n: i \notin sQ (x_ n). rewrite /x_; case: (xR n) => x [Rn QxR] /=. apply: contraL (@ltr01 Rn) => /sQ_inQ[v Di]. suffices /eqP <-: - QxR v ^+ 2 == 1 by rewrite oppr_gt0 -leNgt sqr_ge0. rewrite -rmorphXn -rmorphN fmorph_eq1 -(fmorph_eq1 (ofQ x)) rmorphN eqr_oppLR. by rewrite rmorphXn /= Di Di2. have szX2_1: size ('X^2 + 1) = 3%N. by move=> R; rewrite size_addl ?size_polyXn ?size_poly1. have minp_i n (p_i := minPoly (R_ n) (i_ n)): p_i = 'X^2 + 1. have p_dv_X2_1: p_i %| 'X^2 + 1. rewrite minPoly_dvdp ?rpredD ?rpredX ?rpred1 ?polyOverX //. rewrite -(fmorph_root (ofQ _)) inQ_K // rmorphD rmorph1 /= map_polyXn. by rewrite rootE hornerD hornerXn hornerC Di2 addNr. apply/eqP; rewrite -eqp_monic ?monic_minPoly //; last first. by rewrite monicE lead_coefE szX2_1 coefD coefXn coefC addr0. rewrite -dvdp_size_eqp // eqn_leq dvdp_leq -?size_poly_eq0 ?szX2_1 //= ltnNge. by rewrite size_minPoly ltnS leq_eqVlt orbF adjoin_deg_eq1 -sQof2 !inQ_K. have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. without loss [z_i gal_z]: z / i \in sQ z /\ is_Gal z. have [y /and3P[/sQtrans y_z /sQtrans y_i _] _] := PET [:: z; i]. have [t /sQtrans t_y gal_t] := galQ y. by case/(_ t)=> [|n]; last exists n; rewrite ?y_z ?y_i ?t_y. apply/sig_eqW; have n := 0%N. have [p]: exists p, [&& p \is monic, root p z & p \is a polyOver (sQ (z_ n))]. have [p mon_p pz0] := algC z; exists (p ^ QtoC). by rewrite map_monic mon_p pz0 -(pQof (z_ n)); apply/polyOver_poly. have [d lepd] := ubnP (size p); elim: d => // d IHd in p n lepd * => pz0. have [t [t_C t_z gal_t]]: exists t, [/\ z_ n \in sQ t, z \in sQ t & is_Gal t]. have [y /and3P[y_C y_z _]] := PET [:: z_ n; z]. by have [t /(sQtrans y)t_y] := galQ y; exists t; rewrite !t_y. pose QtMixin := FieldExt_isSplittingField.Build _ (Q t) gal_t. pose Qt : splittingFieldType rat := HB.pack (Q t) QtMixin. have /QtoQ[CnQt CnQtE] := t_C. pose Rn : {subfield Qt} := (CnQt @: R_ n)%AS; pose i_t : Qt := CnQt (i_ n). pose Cn : {subfield Qt} := <<Rn; i_t>>%AS. have defCn: Cn = limg CnQt :> {vspace Q t} by rewrite /= -aimg_adjoin defRi. have memRn u: (u \in Rn) = (ofQ t u \in sQ (x_ n)). by rewrite /= aimg_adjoin aimg1 -sQof2 CnQtE inQ_K. have memCn u: (u \in Cn) = (ofQ t u \in sQ (z_ n)). have [v Dv genCn] := genQz (z_ n). by rewrite -Dv -CnQtE sQof2 defCn -genCn aimg_adjoin aimg1. have Dit: ofQ t i_t = i by rewrite CnQtE inQ_K. have Dit2: i_t ^+ 2 = -1. by apply: (fmorph_inj (ofQ t)); rewrite rmorphXn rmorphN1 /= Dit. have dimCn: \dim_Rn Cn = 2%N. rewrite -adjoin_degreeE adjoin_degree_aimg. by apply: succn_inj; rewrite -size_minPoly minp_i szX2_1. have /sQ_inQ[u_z Dz] := t_z; pose Rz := <<Cn; u_z>>%AS. have{p lepd pz0} le_Rz_d: (\dim_Cn Rz < d)%N. rewrite -ltnS -adjoin_degreeE -size_minPoly (leq_trans _ lepd) // !ltnS. have{pz0} [mon_p pz0 Cp] := and3P pz0. have{Cp} Dp: ((p ^ inQ (z_ n)) ^ CnQt) ^ ofQ t = p. by rewrite -map_poly_comp (eq_map_poly CnQtE) inQpK. rewrite -Dp size_map_poly dvdp_leq ?monic_neq0 -?(map_monic (ofQ _)) ?Dp //. rewrite defCn minPoly_dvdp //; try by rewrite -(fmorph_root (ofQ t)) Dz Dp. by apply/polyOver_poly=> j _; rewrite memv_img ?memvf. have [sRCn sCnRz]: (Rn <= Cn)%VS /\ (Cn <= Rz)%VS by rewrite !subv_adjoin. have sRnRz := subv_trans sRCn sCnRz. have{gal_z} galRz: galois Rn Rz. apply/and3P; split; [by []|by apply: sepQ|]. apply/splitting_normalField=> //. pose QzMixin := FieldExt_isSplittingField.Build _ (Q z) gal_z. pose Qz : splittingFieldType _ := HB.pack (Q z) QzMixin. pose u : Qz := inQ z z. have /QtoQ[Qzt QztE] := t_z; exists (minPoly 1 u ^ Qzt). have /polyOver1P[q ->] := minPolyOver 1 u; apply/polyOver_poly=> j _. by rewrite coef_map linearZZ rmorph1 rpredZ ?rpred1. have [s /eqP Ds] := splitting_field_normal 1 u. rewrite Ds; exists (map Qzt s); first by rewrite map_rp eqpxx. apply/eqP; rewrite eqEsubv; apply/andP; split. apply/Fadjoin_seqP; split=> // _ /mapP[w s_w ->]. by rewrite (subvP (adjoinSl u_z (sub1v _))) // -sQof2 Dz QztE. rewrite /= adjoinC (Fadjoin_idP _) -/Rz; last first. by rewrite (subvP (adjoinSl _ (sub1v _))) // -sQof2 Dz Dit. rewrite /= -adjoin_seq1 adjoin_seqSr //; apply/allP=> /=; rewrite andbT. rewrite -(mem_map (fmorph_inj (ofQ _))) -map_comp (eq_map QztE); apply/mapP. by exists u; rewrite ?inQ_K // -root_prod_XsubC -Ds root_minPoly. have galCz: galois Cn Rz by rewrite (galoisS _ galRz) ?sRCn. have [Cz | C'z]:= boolP (u_z \in Cn); first by exists n; rewrite -Dz -memCn. pose G := 'Gal(Rz / Cn)%G; have{C'z} ntG: G :!=: 1%g. rewrite trivg_card1 -galois_dim 1?(galoisS _ galCz) ?subvv //=. by rewrite -adjoin_degreeE adjoin_deg_eq1. pose extRz m := exists2 w, ofQ t w \in sQ (z_ m) & w \in [predD Rz & Cn]. suffices [m le_n_m [w Cw /andP[C'w Rz_w]]]: exists2 m, (n <= m)%N & extRz m. pose p := minPoly <<Cn; w>> u_z; apply: (IHd (p ^ ofQ t) m). apply: leq_trans le_Rz_d; rewrite size_map_poly size_minPoly ltnS. rewrite adjoin_degreeE adjoinC (addv_idPl Rz_w) agenv_id. rewrite ltn_divLR ?adim_gt0 // mulnC. rewrite muln_divCA ?field_dimS ?subv_adjoin // ltn_Pmulr ?adim_gt0 //. by rewrite -adjoin_degreeE ltnNge leq_eqVlt orbF adjoin_deg_eq1. rewrite map_monic monic_minPoly -Dz fmorph_root root_minPoly /=. have /polyOverP Cw_p: p \is a polyOver <<Cn; w>>%VS by apply: minPolyOver. apply/polyOver_poly=> j _; have /Fadjoin_polyP[q Cq {j}->] := Cw_p j. rewrite -horner_map (@rpred_horner _ (sQC _)) //. apply/polyOver_poly=> j _. by rewrite (sCle n) // -memCn (polyOverP Cq). have [evenG | oddG] := boolP (2.-group G); last first. have [P /and3P[sPG evenP oddPG]] := Sylow_exists 2 'Gal(Rz / Rn). have [w defQw] := PET_Qz t [aspace of fixedField P]. pose pw := minPoly Rn w; pose p := (- pw * (pw \Po - 'X)) ^ ofQ t. have sz_pw: (size pw).-1 = #|'Gal(Rz / Rn) : P|. rewrite size_minPoly adjoin_degreeE -dim_fixed_galois //= -defQw. congr (\dim_Rn _); apply/esym/eqP; rewrite eqEsubv adjoinSl ?sub1v //=. by apply/FadjoinP; rewrite memv_adjoin /= defQw -galois_connection. have mon_p: p \is monic. have mon_pw: pw \is monic := monic_minPoly _ _. rewrite map_monic mulNr -mulrN monicMl // monicE. rewrite !(lead_coefN, lead_coef_comp) ?size_opp ?size_polyX //. by rewrite lead_coefX sz_pw -signr_odd odd_2'nat oddPG mulrN1 opprK. have Dp0: p.[0] = - ofQ t pw.[0] ^+ 2. rewrite -(rmorph0 (ofQ t)) horner_map hornerM rmorphM. by rewrite horner_comp !hornerN hornerX oppr0 /= rmorphN mulNr. have Rpw: pw \is a polyOver Rn by apply: minPolyOver. have Rp: p \is a polyOver (sQ (x_ n)). apply/polyOver_poly=> j _; rewrite -memRn; apply: polyOverP j => /=. by rewrite rpredM 1?polyOver_comp ?rpredN ?polyOverX. have Rp0: ofQ t pw.[0] \in sQ (x_ n) by rewrite -memRn rpred_horner ?rpred0. have [|{mon_p Rp Rp0 Dp0}m lenm p_Rm_0] := xRroot n p (ofQ t pw.[0]). by rewrite /has_Rroot mon_p Rp Rp0 -Dp0 /=. have{p_Rm_0} [y Ry pw_y]: {y | y \in sQ (x_ m) & root (pw ^ ofQ t) y}. apply/sig2W; have [y Ry] := p_Rm_0. rewrite [p]rmorphM /= map_comp_poly !rmorphN /= map_polyX. rewrite rootM rootN root_comp hornerN hornerX. by case/orP; [exists y | exists (- y)]; rewrite ?(rpredN (sQC _)). have [u Rz_u Dy]: exists2 u, u \in Rz & y = ofQ t u. have Rz_w: w \in Rz by rewrite -sub_adjoin1v defQw capvSl. have [sg [Gsg _ Dpw]] := galois_factors sRnRz galRz w Rz_w. set s := map _ sg in Dpw. have /mapP[u /mapP[g Gg Du] ->]: y \in map (ofQ t) s. by rewrite -root_prod_XsubC -/(rp C _) -map_rp -[rp _ _]Dpw. by exists u; rewrite // Du memv_gal. have{pw_y} pw_u: root pw u by rewrite -(fmorph_root (ofQ t)) -Dy. exists m => //; exists u; first by rewrite -Dy; apply: sQtrans Ry _. rewrite inE /= Rz_u andbT; apply: contra oddG => Cu. suffices: 2.-group 'Gal(Rz / Rn). apply: pnat_dvd; rewrite -!galois_dim // ?(galoisS _ galQr) ?sRCz //. rewrite dvdn_divLR ?field_dimS ?adim_gt0 //. by rewrite mulnC muln_divCA ?field_dimS ?dvdn_mulr. congr (2.-group _): evenP; apply/eqP. rewrite eqEsubset sPG -indexg_eq1 (pnat_1 _ oddPG) // -sz_pw. have (pu := minPoly Rn u): (pu %= pw) || (pu %= 1). by rewrite minPoly_irr ?minPoly_dvdp ?minPolyOver. rewrite /= -size_poly_eq1 {1}size_minPoly orbF => /eqp_size <-. rewrite size_minPoly /= adjoin_degreeE (@pnat_dvd _ 2) // -dimCn. rewrite dvdn_divLR ?divnK ?adim_gt0 ?field_dimS ?subv_adjoin //. exact/FadjoinP. have [w Rz_w deg_w]: exists2 w, w \in Rz & adjoin_degree Cn w = 2%N. have [P sPG iPG]: exists2 P : {group gal_of Rz}, P \subset G & #|G : P| = 2%N. have [_ _ [k oG]] := pgroup_pdiv evenG ntG. have [P [sPG _ oP]] := normal_pgroup evenG (normal_refl G) (leq_pred _). by exists P => //; rewrite -divgS // oP oG pfactorK // -expnB ?subSnn. have [w defQw] := PET_Qz _ [aspace of fixedField P]. exists w; first by rewrite -sub_adjoin1v defQw capvSl. rewrite adjoin_degreeE -iPG -dim_fixed_galois // -defQw; congr (\dim_Cn _). apply/esym/eqP; rewrite eqEsubv adjoinSl ?sub1v //=; apply/FadjoinP. by rewrite memv_adjoin /= defQw -galois_connection. have nz2: 2 != 0 :> Qt by move/charf0P: (charQ (Q t)) => ->. without loss{deg_w} [C'w Cw2]: w Rz_w / w \notin Cn /\ w ^+ 2 \in Cn. pose p := minPoly Cn w; pose v := p`_1 / 2. have /polyOverP Cp: p \is a polyOver Cn := minPolyOver Cn w. have Cv: v \in Cn by rewrite rpred_div ?rpred_nat ?Cp. move/(_ (v + w)); apply; first by rewrite rpredD // subvP_adjoin. split; first by rewrite rpredDl // -adjoin_deg_eq1 deg_w. rewrite addrC -[_ ^+ 2]subr0 -(rootP (root_minPoly Cn w)) -/p. rewrite sqrrD [_ - _]addrAC rpredD ?rpredX // -mulr_natr -mulrA divfK //. rewrite [w ^+ 2 + _]addrC mulrC -rpredN opprB horner_coef. have /monicP := monic_minPoly Cn w; rewrite lead_coefE size_minPoly deg_w. by rewrite 2!big_ord_recl big_ord1 => ->; rewrite mulr1 mul1r addrK Cp. without loss R'w2: w Rz_w C'w Cw2 / w ^+ 2 \notin Rn. move=> IHw; have [Rw2 | /IHw] := boolP (w ^+ 2 \in Rn); last exact. have R'it: i_t \notin Rn by rewrite memRn Dit. pose v := 1 + i_t; have R'v: v \notin Rn by rewrite rpredDl ?rpred1. have Cv: v \in Cn by rewrite rpredD ?rpred1 ?memv_adjoin. have nz_v: v != 0 by rewrite (memPnC R'v) ?rpred0. apply: (IHw (v * w)); last 1 [|] || by rewrite fpredMl // subvP_adjoin. by rewrite exprMn rpredM // rpredX. rewrite exprMn fpredMr //=; last by rewrite expf_eq0 (memPnC C'w) ?rpred0. by rewrite sqrrD Dit2 expr1n addrC addKr -mulrnAl fpredMl ?rpred_nat. pose rect_w2 u v := [/\ u \in Rn, v \in Rn & u + i_t * (v * 2) = w ^+ 2]. have{Cw2} [u [v [Ru Rv Dw2]]]: {u : Qt & {v | rect_w2 u v}}. rewrite /rect_w2 -(Fadjoin_poly_eq Cw2); set p := Fadjoin_poly Rn i_t _. have /polyOverP Rp: p \is a polyOver Rn by apply: Fadjoin_polyOver. exists p`_0, (p`_1 / 2); split; rewrite ?rpred_div ?rpred_nat //. rewrite divfK // (horner_coef_wide _ (size_Fadjoin_poly _ _ _)) -/p. by rewrite adjoin_degreeE dimCn big_ord_recl big_ord1 mulr1 mulrC. pose p := Poly [:: - (ofQ t v ^+ 2); 0; - ofQ t u; 0; 1]. have [|m lenm [x Rx px0]] := xRroot n p (ofQ t v). rewrite /has_Rroot 2!unfold_in/= lead_coefE horner_coef0 -memRn Rv. rewrite (@PolyK _ 1) ?oner_eq0 //= !eqxx. rewrite !(rpred0 (sQC _)) ?(rpred1 (sQC _)) ?(rpredN (sQC _)) //=. by rewrite !andbT (@rpredX _ (sQC _)) -memRn. suffices [y Cy Dy2]: {y | y \in sQ (z_ m) & ofQ t w ^+ 2 == y ^+ 2}. exists m => //; exists w; last by rewrite inE C'w. by move: Dy2; rewrite eqf_sqr => /pred2P[]->; rewrite ?(rpredN (sQC _)). exists (x + i * (ofQ t v / x)). rewrite (@rpredD _ (sQC _)) 1?(@rpredM _ (sQC _)) //=. exact: (sQtrans (x_ m)). by rewrite (@rpred_div _ (sQC _)) // (sQtrans (x_ m)) // (sRle n) // -memRn. rewrite rootE /horner (@PolyK _ 1) ?oner_eq0 //= ?addr0 ?mul0r in px0. rewrite add0r mul1r -mulrA -expr2 subr_eq0 in px0. have nz_x2: x ^+ 2 != 0. apply: contraNneq R'w2 => y2_0; rewrite -Dw2 mulrCA. suffices /eqP->: v == 0 by rewrite mul0r addr0. by rewrite y2_0 mulr0 eq_sym sqrf_eq0 fmorph_eq0 in px0. apply/eqP/esym/(mulIf nz_x2); rewrite -exprMn -rmorphXn -Dw2 rmorphD rmorphM. rewrite /= Dit mulrDl -expr2 mulrA divfK; last by rewrite expf_eq0 in nz_x2. rewrite mulr_natr addrC sqrrD exprMn Di2 mulN1r -(eqP px0) -mulNr opprB. by rewrite -mulrnAl -mulrnAr -rmorphMn -!mulrDl addrAC subrK. have inFTA n z: (n_ z <= n)%N -> z = ofQ (z_ n) (inQ (z_ n) z). by move/sCle=> le_zn; rewrite inQ_K ?le_zn. pose is_cj n cj := {in R_ n, cj =1 id} /\ cj (i_ n) = - i_ n. have /all_sig[cj_ /all_and2[cj_R cj_i]] n: {cj : 'AEnd(Q (z_ n)) | is_cj n cj}. have cj_P: root (minPoly (R_ n) (i_ n) ^ \1%VF) (- i_ n). rewrite minp_i -(fmorph_root (ofQ _)) !rmorphD !rmorph1 /= !map_polyXn. by rewrite rmorphN inQ_K // rootE hornerD hornerXn hornerC sqrrN Di2 addNr. have cj_M: ahom_in fullv (kHomExtend (R_ n) \1 (i_ n) (- i_ n)). by rewrite -defRi -k1HomE kHomExtendP ?sub1v ?kHom1. exists (AHom cj_M); split=> [y /kHomExtend_id->|]; first by rewrite ?id_lfunE. by rewrite (kHomExtend_val (kHom1 1 _)). pose conj_ n z := ofQ _ (cj_ n (inQ _ z)); pose conj z := conj_ (n_ z) z. have conjK n m z: (n_ z <= n)%N -> (n <= m)%N -> conj_ m (conj_ n z) = z. move/sCle=> le_z_n le_n_m; have /le_z_n/sQ_inQ[u <-] := FTA z. have /QtoQ[Qmn QmnE]: z_ n \in sQ (z_ m) by rewrite (sCle n). rewrite /conj_ ofQ_K -!QmnE !ofQ_K -!comp_lfunE; congr (ofQ _ _). move: u (memRi n u); apply/eqlfun_inP/FadjoinP; split=> /=. apply/eqlfun_inP=> y Ry; rewrite !comp_lfunE !cj_R //. by move: Ry; rewrite -!sQof2 QmnE !inQ_K //; apply: sRle. apply/eqlfunP; rewrite !comp_lfunE cj_i !linearN /=. suffices ->: Qmn (i_ n) = i_ m by rewrite cj_i ?opprK. by apply: (fmorph_inj (ofQ _)); rewrite QmnE !inQ_K. have conjE n z: (n_ z <= n)%N -> conj z = conj_ n z. move/leq_trans=> le_zn; set x := conj z; set y := conj_ n z. have [m [le_xm le_ym le_nm]] := maxn3 (n_ x) (n_ y) n. by have /conjK/=/can_in_inj := leqnn m; apply; rewrite ?conjK // le_zn. have conjA : additive conj. move=> x y. have [m [le_xm le_ym le_xym]] := maxn3 (n_ x) (n_ y) (n_ (x - y)). by rewrite !(conjE m) // (inFTA m x) // (inFTA m y) -?rmorphB /conj_ ?ofQ_K. have conjM : multiplicative conj. split=> [x y|]; last pose n1 := n_ 1. have [m [le_xm le_ym le_xym]] := maxn3 (n_ x) (n_ y) (n_ (x * y)). by rewrite !(conjE m) // (inFTA m x) // (inFTA m y) -?rmorphM /conj_ ?ofQ_K. by rewrite /conj -/n1 -(rmorph1 (ofQ (z_ n1))) /conj_ ofQ_K !rmorph1. have conjaM := GRing.isAdditive.Build _ _ _ conjA. have conjmM := GRing.isMultiplicative.Build _ _ _ conjM. pose conjRM : GRing.RMorphism.type _ _ := HB.pack conj conjaM conjmM. exists conjRM => [z | /(_ i)/eqP/idPn[]] /=. by have [n [/conjE-> /(conjK (n_ z))->]] := maxn3 (n_ (conj z)) (n_ z) 0. rewrite /conj/conj_ cj_i rmorphN inQ_K // eq_sym -addr_eq0 -mulr2n -mulr_natl. rewrite mulf_neq0 ?(memPnC (R'i 0)) ?(rpred0 (sQC _)) //. by have /charf0P-> := ftrans (fmorph_char QtoC) (char_num _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path tuple bigop finset prime order) mathcomp(ssralg poly polydiv mxpoly countalg closed_field) mathcomp(ssrnum ssrint archimedean rat intdiv fingroup) mathcomp(finalg zmodp cyclic pgroup sylow vector falgebra) mathcomp(fieldext separable galois)