proposition: Lemma countable_algebraic_closure (F : countFieldType) : {K : countClosedFieldType & {FtoK : {rmorphism F -> K} | integralRange FtoK}}.
proof: Proof. pose minXp (R : ringType) (p : {poly R}) := if size p > 1 then p else 'X. have minXp_gt1 R p: size (minXp R p) > 1. by rewrite /minXp; case: ifP => // _; rewrite size_polyX. have minXpE (R : ringType) (p : {poly R}) : size p > 1 -> minXp R p = p. by rewrite /minXp => ->. have ext1 p := countable_field_extension (minXp_gt1 _ p). pose ext1fT E p := tag (ext1 E p). pose ext1to E p : {rmorphism _ -> ext1fT E p} := tag (tagged (ext1 E p)). pose ext1w E p : ext1fT E p := s2val (tagged (tagged (ext1 E p))). have ext1root E p: root (map_poly (ext1to E p) (minXp E p)) (ext1w E p). by rewrite /ext1w; case: (tagged (tagged (ext1 E p))). have ext1gen E p u: {q | u = (map_poly (ext1to E p) q).[ext1w E p]}. by apply: sig_eqW; rewrite /ext1w; case: (tagged (tagged (ext1 E p))) u. pose pExtEnum (E : countFieldType) := nat -> {poly E}. pose Ext := {E : countFieldType & pExtEnum E}; pose MkExt : Ext := Tagged _ _. pose EtoInc (E : Ext) i := ext1to (tag E) (tagged E i). pose incEp E i j := let v := map_poly (EtoInc E i) (tagged E j) in if decode j is [:: i1; k] then if i1 == i then odflt v (unpickle k) else v else v. pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0. pose E i := tag (E_ i); pose Krep := {i : nat & E i}. pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} := if k isn't k1.+1 then idfun else EtoInc _ (k1 + i)%N \o toEadd _ _. pose toE i j (le_ij : i <= j) := ecast j {rmorphism E i -> E j} (subnK le_ij) (toEadd i (j - i)%N). have toEeq i le_ii: toE i i le_ii =1 id. by rewrite /toE; move: (subnK _); rewrite subnn => ?; rewrite eq_axiomK. have toEleS i j leij leiSj z: toE i j.+1 leiSj z = EtoInc _ _ (toE i j leij z). rewrite /toE; move: (j - i)%N {leij leiSj}(subnK _) (subnK _) => k. by case: j /; rewrite (addnK i k.+1) => eq_kk; rewrite [eq_kk]eq_axiomK. have toEirr := congr1 ((toE _ _)^~ _) (bool_irrelevance _ _). have toEtrans j i k leij lejk leik z: toE i k leik z = toE j k lejk (toE i j leij z). - elim: k leik lejk => [|k IHk] leiSk lejSk. by case: j => // in leij lejSk *; rewrite toEeq. have:= lejSk; rewrite {1}leq_eqVlt ltnS => /predU1P[Dk | lejk]. by rewrite -Dk in leiSk lejSk *; rewrite toEeq. by have leik := leq_trans leij lejk; rewrite !toEleS -IHk. have [leMl leMr] := (leq_maxl, leq_maxr); pose le_max := (leq_max, leqnn, orbT). pose pairK (x y : Krep) (m := maxn _ _) := (toE _ m (leMl _ _) (tagged x), toE _ m (leMr _ _) (tagged y)). pose eqKrep x y := uncurry (@eq_op _) (pairK x y). have eqKrefl : reflexive eqKrep by move=> z; apply/eqP; apply: toEirr. have eqKsym : symmetric eqKrep. move=> z1 z2; rewrite {1}/eqKrep /= eq_sym; move: (leMl _ _) (leMr _ _). by rewrite maxnC => lez1m lez2m; congr (_ == _); apply: toEirr. have eqKtrans : transitive eqKrep. rewrite /eqKrep /= => z2 z1 z3 /eqP eq_z12 /eqP eq_z23. rewrite -(inj_eq (fmorph_inj (toE _ _ (leMr (tag z2) _)))). rewrite -!toEtrans ?le_max // maxnCA maxnA => lez3m lez1m. rewrite {lez1m}(toEtrans (maxn (tag z1) (tag z2))) // {}eq_z12. do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *. by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans. pose K := {eq_quot EquivRel _ eqKrefl eqKsym eqKtrans}%qT. pose cntK := isCountable.Build K (pcan_pickleK (can_pcan (reprK))). pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x). have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep. pose FtoK := EtoK 0; rewrite {}/EtoKrep in piEtoK. have eqEtoK i j x y: toE i _ (leMl i j) x = toE j _ (leMr i j) y -> EtoK i x = EtoK j y. - by move/eqP=> eq_xy; rewrite -!piEtoK; apply/eqmodP. have toEtoK j i leij x : EtoK j (toE i j leij x) = EtoK i x. by apply: eqEtoK; rewrite -toEtrans. have EtoK_0 i: EtoK i 0 = FtoK 0 by apply: eqEtoK; rewrite !rmorph0. have EtoK_1 i: EtoK i 1 = FtoK 1 by apply: eqEtoK; rewrite !rmorph1. have EtoKeq0 i x: (EtoK i x == FtoK 0) = (x == 0). by rewrite /FtoK -!piEtoK eqmodE /= /eqKrep /= rmorph0 fmorph_eq0. have toErepr m i leim x lerm: toE _ m lerm (tagged (repr (EtoK i x))) = toE i m leim x. - have: (Tagged E x == repr (EtoK i x) %[mod K])%qT by rewrite reprK piEtoK. rewrite eqmodE /= /eqKrep; case: (repr _) => j y /= in lerm * => /eqP /=. have leijm: maxn i j <= m by rewrite geq_max leim. by move/(congr1 (toE _ _ leijm)); rewrite -!toEtrans. pose Kadd (x y : K) := EtoK _ (uncurry +%R (pairK (repr x) (repr y))). pose Kopp (x : K) := EtoK _ (- tagged (repr x)). pose Kmul (x y : K) := EtoK _ (uncurry *%R (pairK (repr x) (repr y))). pose Kinv (x : K) := EtoK _ (tagged (repr x))^-1. have EtoK_D i: {morph EtoK i : x y / x + y >-> Kadd x y}. move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphD. rewrite -![X in _ = X + _]toEtrans ?le_max// => lexm. rewrite -![X in _ = _ + X]toEtrans ?le_max// => leym. by rewrite !toErepr. have EtoK_N i: {morph EtoK i : x / - x >-> Kopp x}. by move=> x; apply: eqEtoK; set j := tag _; rewrite !rmorphN toErepr. have EtoK_M i: {morph EtoK i : x y / x * y >-> Kmul x y}. move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphM. rewrite -![X in _ = X * _]toEtrans ?le_max// => lexm. rewrite -![X in _ = _ * X]toEtrans ?le_max// => leym. by rewrite !toErepr. have EtoK_V i: {morph EtoK i : x / x^-1 >-> Kinv x}. by move=> x; apply: eqEtoK; set j := tag _; rewrite !fmorphV toErepr. case: {toErepr}I in (Kadd) (Kopp) (Kmul) (Kinv) EtoK_D EtoK_N EtoK_M EtoK_V. pose inEi i z := {x : E i | z = EtoK i x}; have KtoE z: {i : nat & inEi i z}. by elim/quotW: z => [[i x] /=]; exists i, x; rewrite piEtoK. have inEle i j z: i <= j -> inEi i z -> inEi j z. by move=> leij [x ->]; exists (toE i j leij x); rewrite toEtoK. have KtoE2 z1 z2: {i : nat & inEi i z1 & inEi i z2}. have [[i1 Ez1] [i2 Ez2]] := (KtoE z1, KtoE z2). by exists (maxn i1 i2); [apply: inEle Ez1 | apply: inEle Ez2]. have KtoE3 z1 z2 z3: {i : nat & inEi i z1 & inEi i z2 * inEi i z3}%type. have [[i1 Ez1] [i2 Ez2 Ez3]] := (KtoE z1, KtoE2 z2 z3). by exists (maxn i1 i2); [apply: inEle Ez1 | split; apply: inEle (leMr _ _) _]. have KaddC: commutative Kadd. by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_D addrC. have KaddA: associative Kadd. move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. by rewrite -!EtoK_D addrA. have Kadd0: left_id (FtoK 0) Kadd. by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_0 i) -EtoK_D add0r. have KaddN: left_inverse (FtoK 0) Kopp Kadd. by move=> u; have [i [x ->]] := KtoE u; rewrite -EtoK_N -EtoK_D addNr EtoK_0. pose KzmodMixin := GRing.isZmodule.Build K KaddA KaddC Kadd0 KaddN. pose Kzmod : countZmodType := HB.pack K KzmodMixin. have KmulC: commutative Kmul. by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_M mulrC. have KmulA: @associative Kzmod Kmul. move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. by rewrite -!EtoK_M mulrA. have Kmul1: left_id (FtoK 1) Kmul. by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_1 i) -EtoK_M mul1r. have KmulD: left_distributive Kmul Kadd. move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. by rewrite -!(EtoK_M, EtoK_D) mulrDl. have Kone_nz: FtoK 1 != FtoK 0 by rewrite EtoKeq0 oner_neq0. pose KringMixin := GRing.Zmodule_isComRing.Build _ KmulA KmulC Kmul1 KmulD Kone_nz. pose Kring : comRingType := HB.pack K Kzmod KringMixin cntK. have KmulV: forall x : Kring, x != 0 -> (Kinv x : Kring) * x = 1. move=> u; have [i [x ->]] := KtoE u; rewrite EtoKeq0 => nz_x. by rewrite -EtoK_V -[_ * _]EtoK_M mulVf ?EtoK_1. have Kinv0: Kinv (FtoK 0) = FtoK 0 by rewrite -EtoK_V invr0. pose KfieldMixin := GRing.ComRing_isField.Build _ KmulV Kinv0. pose Kfield : fieldType := HB.pack K Kring KfieldMixin. have EtoKAdd i : additive (EtoK i : E i -> Kfield). by move=> x y; rewrite EtoK_D EtoK_N. have EtoKMul i : multiplicative (EtoK i : E i -> Kfield). by split=> [x y|]; rewrite ?EtoK_M ?EtoK_1. pose EtoKMa i := GRing.isAdditive.Build _ _ _ (EtoKAdd i). pose EtoKMm i := GRing.isMultiplicative.Build _ _ _ (EtoKMul i). pose EtoKM i : GRing.RMorphism.type _ _ := HB.pack (EtoK i : E i -> Kfield) (EtoKMa i) (EtoKMm i). have EtoK_E: EtoK _ = EtoKM _ by []. have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _). have Kclosed: GRing.closed_field_axiom Kfield. move=> n pK n_gt0; pose m0 := \max_(i < n) tag (KtoE (pK i)); pose m := m0.+1. have /fin_all_exists[pE DpE] (i : 'I_n): exists y, EtoK m y = pK i. pose u := KtoE (pK i); have leum0: tag u <= m0 by rewrite (bigmax_sup i). by have [y ->] := tagged u; exists (toE _ _ (leqW leum0) y); rewrite toEtoK. pose p := 'X^n - rVpoly (\row_i pE i); pose j := code [:: m0; pickle p]. pose pj := tagged (E_ j) j; pose w : E j.+1 := ext1w (E j) pj. have lemj: m <= j by rewrite (allP (ltn_code _)) ?mem_head. exists (EtoKM j.+1 w); apply/eqP; rewrite -subr_eq0; apply/eqP. transitivity (EtoKM j.+1 (map_poly (toE m j.+1 (leqW lemj)) p).[w]). rewrite -horner_map -map_poly_comp toEtoKp EtoK_E. move: (EtoKM j.+1 w) => {}w. rewrite rmorphB [_ 'X^n]map_polyXn !hornerE; congr (_ - _ : Kring). rewrite (@horner_coef_wide _ n) ?size_map_poly ?size_poly //. by apply: eq_bigr => i _; rewrite coef_map coef_rVpoly valK mxE /= DpE. suffices Dpj: map_poly (toE m j lemj) p = pj. apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. rewrite {w}/pj; set j0 := (j in tagged (E_ _) j). elim: {+}j lemj => // k IHk lemSk; rewrite {}/j0 in IHk *. have:= lemSk; rewrite leq_eqVlt ltnS => /predU1P[Dm | lemk]. rewrite -{}Dm in lemSk *; rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)). by rewrite map_poly_id //= /incEp codeK eqxx pickleK. rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. by rewrite -if_neg neq_ltn lemk. suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. pose Kcc := Field_isAlgClosed.Build Kfield Kclosed. by exists (HB.pack_for countClosedFieldType K Kfield Kcc). exists (EtoKM 0) => /= z; have [i [{}z ->]] := KtoE z. suffices{z} /(_ z)[p mon_p]: integralRange (toE 0 i isT). by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. move: (i - 0)%N (subnK _) => n; case: i /. elim: n => [|n IHn] /= z; first exact: integral_id. have{z} [q ->] := ext1gen _ _ z; set pn := tagged (E_ _) _. apply: integral_horner. by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. apply: integral_root (ext1root _ _) _. by rewrite map_poly_eq0 -size_poly_gt0 ltnW. by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. 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)