proposition: Lemma solvable_formula (p : {poly rat}) : p != 0 -> solvable_by_radical_poly p <-> {in root (p ^^ ratr), forall x, exists f : algterm rat, algT_eval ratr f = x}.
proof: Proof. have Cchar := Cchar => p_neq0; split. move=> /solvable_poly_rat[]// L [iota [rs [prs [E rE KE]]]] x. have pirs : p ^^ ratr %= \prod_(x <- map iota rs) ('X - x%:P). have := prs; rewrite -(eqp_map iota) map_prod_XsubC => /eqp_rtrans<-. by rewrite -map_poly_comp (eq_map_poly (fmorph_eq_rat _)) eqpxx. rewrite -topredE/= (eqp_root pirs) root_prod_XsubC => /mapP[{}r rrs ->]. suff [f <- /=]: exists f : algterm (subvs_of (1%VS : {vspace L})), algT_eval (iota \o vsval) f = iota r. elim: f => //= [[/= _/vlineP[s ->]]|cst|op|op]. - exists (Base s) => /=. by rewrite [RHS](fmorph_eq_rat (iota \o in_alg L)). - by exists (Const cst). - by move=> _ [f1 <-]; exists (UnOp op f1). - by move=> _ [f1 <-] _ [f2 <-]; exists (BinOp op f1 f2). have: r \in E by rewrite (subvP KE)// seqv_sub_adjoin. case: rE => -[/= n e pw] epw <-. rewrite -[1%VS]/(1%AS : {vspace _}) in epw *. elim: n 1%AS => [|n IHn] k /= in e pw epw *. by rewrite tuple0 Fadjoin_nil => rk; exists (Base (Subvs rk)). case: (tupleP e) (tupleP pw) epw => [u e'] [i pw']/= epw. rewrite adjoin_cons => /IHn-/(_ pw')[]. apply/towerP => j /=. have /towerP/(_ (lift ord0 j))/= := epw. by rewrite !tnthS/= adjoin_cons. move=> f <-; elim: f => //= [s|cst|op|op]; last 3 first. - by exists (Const cst). - by move=> _ [f1 <-]; exists (UnOp op f1). - by move=> _ [f1 <-] _ [f2 <-]; exists (BinOp op f1 f2). have /Fadjoin_polyP[q qk ->] := subvsP s. have /towerP/(_ ord0) := epw; rewrite !tnth0/= Fadjoin_nil. move=> /radicalP[]; case: i => // i in epw * => _ uik. pose v := i.+1.-root (iota (u ^+ i.+1)). have : ('X ^+ i.+1 - (v ^+ i.+1)%:P).[iota u] == 0. by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr. have /Xn_sub_xnE->// := prim1rootP (isT : 0 < i.+1)%N. rewrite horner_prod prodf_seq_eq0/= => /hasP[/= l _]. rewrite hornerXsubC subr_eq0 => /eqP u_eq. pose fu := (i.+1-root (Base (Subvs uik)) * (i.+1-prim1root ^+ l))%algT. rewrite -horner_map; have -> : iota u = algT_eval (iota \o vsval) fu by []. move: fu => fu; elim/poly_ind: q qk => //= [|q c IHq] qXDck. by exists 0%algT; rewrite rmorph0 horner0. have ck : c \in k. by have /polyOverP/(_ 0%N) := qXDck; rewrite coefD coefMX coefC/= add0r. have qk : q \is a polyOver k. apply/polyOverP => j; have /polyOverP/(_ j.+1) := qXDck. by rewrite coefD coefMX coefC/= addr0. case: IHq => // fq fq_eq. exists (fq * fu + Base (Subvs ck))%algT => /=. by rewrite rmorphD rmorphM/= map_polyX map_polyC !hornerE fq_eq. move=> mkalg; apply/solvable_by_radical_polyP => //=; first exact: char_num. have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)). have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P). rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx//. by rewrite lead_coef_map//= fmorph_eq0 lead_coef_eq0. have [fs fsE] : exists fs, map (algT_eval ratr) fs = rsalg. have /(_ _ _)/sig_eqW-/(all_sig_cond (Base 0)) [h hE] : forall x : algC, x \in rsalg -> exists f, algT_eval ratr f = x. by move=> *; apply: mkalg; rewrite -topredE/= (eqp_root pE) root_prod_XsubC. by exists (map h rsalg); rewrite -map_comp map_id_in//. pose algs := flatten (map (subeval ratr) fs). pose mp := \prod_(x <- algs) projT1 (minCpolyP x). have mp_monic : mp \is monic. by rewrite monic_prod => // i _; case: minCpolyP => /= ? []. have mpratr : mp ^^ ratr = \prod_(x <- algs) minCpoly x. rewrite rmorph_prod/=; apply: eq_bigr => x _. by case: minCpolyP => //= ? []. have [rsmpalg mpE] := closed_field_poly_normal (mp ^^ ratr : {poly algC}). have mp_neq0 : mp != 0. rewrite prodf_seq_eq0; apply/hasPn => /= x xalgs. by case: minCpolyP => //= ? [_ /monic_neq0->]. have {}mpE : mp ^^ ratr = \prod_(z <- rsmpalg) ('X - z%:P). by rewrite mpE lead_coef_map/= (eqP mp_monic) rmorph1 scale1r. have [L [iota [rsmp iota_rs rsf]]] := num_field_exists rsmpalg. have charL : has_char0 L by move=> x; rewrite char_lalg char_num. have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P). rewrite -(eqp_map iota) map_prod_XsubC iota_rs -map_poly_comp -mpE. by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx. have splitL : SplittingField.axiom L. by exists (mp ^^ in_alg L); [apply/polyOver1P; exists mp | exists rsmp]. pose sM := FieldExt_isSplittingField.Build rat L splitL. pose S : splittingFieldType rat := HB.pack L sM. have algsW: {subset rsalg <= algs}. move=> x; rewrite -fsE => /mapP[{x}f ffs ->]. apply/flattenP; exists (subeval ratr f); rewrite ?map_f//. by rewrite subevalE mem_head. have rsmpW: {subset algs <= rsmpalg}. move=> x xalgs; rewrite -root_prod_XsubC -mpE mpratr. by rewrite (big_rem _ xalgs)/= rootM root_minCpoly. have := rsmpW; rewrite -iota_rs => /subset_mapP[als _ /esym alsE]. have := algsW; rewrite -alsE => /subset_mapP[rs _ /esym rsE]. have prs : p ^^ in_alg S %= \prod_(x <- rs) ('X - x%:P). rewrite -(eqp_map iota) -map_poly_comp (eq_map_poly (fmorph_eq_rat _)). by rewrite map_prod_XsubC rsE. apply/classicW; exists S, rs; split => //. exists <<1 & als>>%AS; last first. rewrite adjoin_seqSr// => x /(map_f iota); rewrite rsE => /algsW. by rewrite -[X in _ \in X]alsE (mem_map (fmorph_inj _)). rewrite {p p_neq0 mkalg pE prs rsmp iota_rs mprs rsf rs rsE mp mp_monic mpratr rsmpalg mp_neq0 mpE algsW rsmpW charL}/=. suff: forall (L : splittingFieldType rat) (iota : {rmorphism L -> algC}) als, map iota als = algs -> radical.-ext 1%VS <<1 & als>>%VS. by move=> /(_ S iota als alsE). move=> {sM}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE. elim: fs => [|f fs IHfs]//= in rsalg fsE als alsE *. case: als => []// in alsE *. by rewrite Fadjoin_nil; apply: rext_refl. move: rsalg fsE => [|r rsalg]// [fr fsE]. pose n := size (subeval ratr f); rewrite -[als](cat_take_drop n). have /(congr1 (take n)) := alsE; rewrite take_size_cat//. rewrite -map_take; move: (take _ _) => als1 als1E. have /(congr1 (drop n)) := alsE; rewrite drop_size_cat//. rewrite -map_drop; move: (drop _ _) => als2 als2E. have /rext_trans := IHfs _ fsE _ als2E; apply. have -> : <<1 & als1 ++ als2>>%AS = <<<<1 & als2>>%AS & als1>>%AS. apply/val_inj; rewrite /= -adjoin_cat; apply/eq_adjoin => x. by rewrite !mem_cat orbC. move: <<1 & als2>>%AS => /= k {als2 als2E n fs fsE IHfs rsalg als alsE}. elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *. - case: als1 als1E => [|y []]//= [yx]/=. rewrite adjoin_seq1 (Fadjoin_idP _); first exact: rext_refl. suff: y \in 1%VS by apply/subvP; rewrite sub1v. apply/vlineP; exists x; apply: (fmorph_inj iota); rewrite yx. by rewrite [RHS](fmorph_eq_rat (iota \o in_alg _)). - case: als1 als1E => [|y []]//= []/=; rewrite adjoin_seq1. case: c => [/eqP|/eqP|n yomega]. + rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0//. exact: rext_refl. + rewrite fmorph_eq1 => /eqP->; rewrite (Fadjoin_idP _) ?rpred1//. exact: rext_refl. + apply/(@rext_r _ _ _ n.+1)/radicalP; split => //. rewrite prim_expr_order ?rpred1//. by rewrite -(fmorph_primitive_root iota) yomega prim1rootP. - case: als1 als1E => //= a l [IHl IHlu]. rewrite -(eq_adjoin _ (mem_rcons _ _)) adjoin_rcons. apply: rext_trans (IHf1 k l IHlu) _ => /=. move: IHlu; rewrite subevalE; case: l => // x1 l [iotax1 _]. rewrite -iotax1 -rmorphN -fmorphV in IHl. have x1kx1 : x1 \in <<k & x1 :: l>>%VS by rewrite seqv_sub_adjoin ?mem_head. case: u => [||n|n]/= in IHl. + rewrite (Fadjoin_idP _); first exact: rext_refl. by have /fmorph_inj-> := IHl; rewrite rpredN. + rewrite (Fadjoin_idP _); first exact: rext_refl. by have /fmorph_inj-> := IHl; rewrite rpredV. + rewrite (Fadjoin_idP _); first exact: rext_refl. by have := IHl; rewrite -rmorphX => /fmorph_inj->; rewrite rpredX. apply/(@rext_r _ _ _ n.+1)/radicalP; split => //. have /(congr1 ((@GRing.exp _)^~ n.+1)) := IHl. by rewrite rootCK// -rmorphX => /fmorph_inj->. - case: als1 als1E => //= a l [IHl IHlu]. rewrite -(eq_adjoin _ (mem_rcons _ _)) adjoin_rcons. pose n := size (subeval ratr f1); rewrite -[l](cat_take_drop n). have /(congr1 (take n)) := IHlu; rewrite take_size_cat//. rewrite -map_take; move: (take _ _) => l1 l1E. have /(congr1 (drop n)) := IHlu; rewrite drop_size_cat//. rewrite -map_drop; move: (drop _ _) => l2 l2E. apply: rext_trans (IHf1 _ l1 l1E) _ => /=. apply: rext_trans (IHf2 _ l2 l2E) _ => /=. rewrite -adjoin_cat (Fadjoin_idP _); first exact: rext_refl. rewrite subevalE in l1E; rewrite subevalE in l2E. case: l1 l1E => // b1 l1 [iotab1 _]. case: l2 l2E => // b2 l2 [iotab2 _]. rewrite -iotab1 -iotab2 -rmorphM -rmorphD in IHl. have b2l : b2 \in (b1 :: l1) ++ (b2 :: l2) by rewrite mem_cat mem_head orbT. have b1l : b1 \in (b1 :: l1) ++ (b2 :: l2) by rewrite mem_head. by case: b IHl => /fmorph_inj ->; rewrite ?(rpredD, rpredM)// seqv_sub_adjoin. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)