proposition: Lemma countable_field_extension (F : countFieldType) (p : {poly F}) : size p > 1 -> {E : countFieldType & {FtoE : {rmorphism F -> E} & {w : E | root (map_poly FtoE p) w & forall u : E, exists q, u = (map_poly FtoE q).[w]}}}.
proof: Proof. pose fix d i := if i is i1.+1 then let d1 := oapp (gcdp (d i1)) 0 (unpickle i1) in if size d1 > 1 then d1 else d i1 else p. move=> p_gt1; have sz_d i: size (d i) > 1 by elim: i => //= i IHi; case: ifP. have dv_d i j: i <= j -> d j %| d i. move/subnK <-; elim: {j}(j - i)%N => //= j IHj; case: ifP => //=. case: (unpickle _) => /= [q _|]; last by rewrite size_poly0. exact: dvdp_trans (dvdp_gcdl _ _) IHj. pose I : pred {poly F} := [pred q | d (pickle q).+1 %| q]. have I'co q i: q \notin I -> i > pickle q -> coprimep q (d i). rewrite inE => I'q /dv_d/coprimep_dvdl-> //; apply: contraR I'q. rewrite coprimep_sym /coprimep /= pickleK /= neq_ltn. case: ifP => [_ _| ->]; first exact: dvdp_gcdr. rewrite orbF ltnS leqn0 size_poly_eq0 gcdp_eq0 -size_poly_eq0. by rewrite -leqn0 leqNgt ltnW //. have memI q: reflect (exists i, d i %| q) (q \in I). apply: (iffP idP) => [|[i dv_di_q]]; first by exists (pickle q).+1. have [le_i_q | /I'co i_co_q] := leqP i (pickle q). rewrite inE /= pickleK /=; case: ifP => _; first exact: dvdp_gcdr. exact: dvdp_trans (dv_d _ _ le_i_q) dv_di_q. apply: contraR i_co_q _. by rewrite /coprimep (eqp_size (dvdp_gcd_idr dv_di_q)) neq_ltn sz_d orbT. have I_ideal : idealr_closed I. split=> [||a q1 q2 Iq1 Iq2]; first exact: dvdp0. by apply/memI=> [[i /idPn[]]]; rewrite dvdp1 neq_ltn sz_d orbT. apply/memI; exists (maxn (pickle q1).+1 (pickle q2).+1); apply: dvdp_add. by apply: dvdp_mull; apply: dvdp_trans Iq1; apply/dv_d/leq_maxl. by apply: dvdp_trans Iq2; apply/dv_d/leq_maxr. pose IaM := GRing.isAddClosed.Build _ I (idealr_closedB I_ideal). pose IoM := GRing.isOppClosed.Build _ I (idealr_closedB I_ideal). pose IpM := isProperIdeal.Build _ I (idealr_closed_nontrivial I_ideal). pose Iid : idealr _ := HB.pack I IaM IoM IpM. pose EMixin := GRing.Ring_hasCommutativeMul.Build _ (@Quotient.mulqC _ Iid). pose E : comRingType := HB.pack _ EMixin. pose PtoE : {rmorphism {poly F} -> E} := \pi_E%qT. have PtoEd i: PtoE (d i) = 0. by apply/eqP; rewrite piE Quotient.equivE subr0; apply/memI; exists i. pose Einv (z : E) (q := repr z) (dq := d (pickle q).+1) := let q_unitP := Bezout_eq1_coprimepP q dq in if q_unitP is ReflectT ex_uv then PtoE (sval (sig_eqW ex_uv)).1 else 0. have Einv0 : Einv 0 = 0. rewrite /Einv; case: Bezout_eq1_coprimepP => // ex_uv. case/negP: (oner_neq0 E); rewrite [X in X == _]piE. rewrite -[_ 1]/(PtoE 1); have [uv <-] := ex_uv. by rewrite rmorphD !rmorphM [X in _ + _ * X]PtoEd /= reprK !mulr0 addr0. have EmulV : forall x, x != 0 -> Einv x * x = 1. rewrite /Einv=> z nz_z; case: Bezout_eq1_coprimepP => [ex_uv |]; last first. move/Bezout_eq1_coprimepP; rewrite I'co //. by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z. apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *. rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. rewrite -[X in _ - X]uv1 opprD addNKr -mulNr. by apply/memI; exists i; apply: dvdp_mull. pose EfieldMixin := GRing.ComRing_isField.Build _ EmulV Einv0. pose Efield : fieldType := HB.pack E EfieldMixin. pose EIsCountable := isCountable.Build E (pcan_pickleK (can_pcan (reprK))). pose Ecount : countFieldType := HB.pack E Efield EIsCountable. pose FtoE : {rmorphism _ -> _} := PtoE \o polyC; pose w : E := PtoE 'X. have defPtoE q: (map_poly FtoE q).[w] = PtoE q. by rewrite (map_poly_comp PtoE polyC) horner_map [_.['X]]comp_polyXr. exists Ecount, FtoE, w => [|u]. by rewrite /root defPtoE (PtoEd 0). by exists (repr u); rewrite defPtoE /= reprK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)