proposition: Lemma solvable_ext_polyP (F : fieldType) (p : {poly F}) : p != 0 -> has_char0 F -> solvable_ext_poly p <-> classically (exists (L : splittingFieldType F) (rs : seq L), p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) /\ solvable 'Gal(<<1 & rs>> / 1)).
proof: Proof. move=> p_neq0 charF; split => sol_p. have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1. apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0). move=> [L [rs [iota rsf p_eq]]]; apply/classicW. have iotaF : iota =1 in_alg L by move=> v; rewrite [v in LHS]FoE rmorph_alg. have splitL : SplittingField.axiom L. exists (p ^^ iota). by apply/polyOver1P; exists p; apply: eq_map_poly. exists rs => //; suff <- : limg iota = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite iotaF/= rpredZ// rpred1. pose sM := FieldExt_isSplittingField.Build F L splitL. pose S : splittingFieldType F := HB.pack L sM. exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF). by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF). move=> L rs prs; apply: sol_p => -[M [rs' [prs']]]. have charL : has_char0 L by move=> n; rewrite char_lalg charF. have charM : has_char0 M by move=> n; rewrite char_lalg charF. pose K : fieldExtType F := subvs_of <<1 & rs>>%VS. pose rsK := map (vsproj <<1 & rs>>%VS) rs. have pKrs : p ^^ in_alg K %= \prod_(x <- rsK) ('X - x%:P). rewrite -(eqp_map vsval)/= map_prod_XsubC/= -map_poly_comp/=. rewrite -map_comp (@eq_map_poly _ _ _ (in_alg L)); last first. by move=> v; rewrite /= algid1. have /eq_in_map-> : {in rs, cancel (vsproj <<1 & rs>>%VS) vsval}. by move=> x xrs; rewrite vsprojK// seqv_sub_adjoin. by rewrite big_map. have splitK : splittingFieldFor 1 (p ^^ in_alg K) fullv. exists rsK => //; apply/eqP; rewrite eqEsubv subvf/=. rewrite -(@limg_ker0 _ _ _ (linfun vsval)) ?AHom_lker0//. rewrite aimg_adjoin_seq/= aimg1 -map_comp/=. have /eq_in_map-> : {in rs, cancel (vsproj <<1 & rs>>%VS) (linfun vsval)}. by move=> x xrs; rewrite lfunE/= vsprojK// seqv_sub_adjoin. rewrite map_id; apply/subvP => _/memv_imgP[v _ ->]. by rewrite lfunE subvsP. have sfK : SplittingField.axiom K. by exists (p ^^ in_alg K) => //; apply/polyOver1P; exists p. pose sM := FieldExt_isSplittingField.Build F K sfK. pose S : splittingFieldType F := HB.pack K sM. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by []. have splitM : splittingFieldFor 1 (p ^^ in_alg M) <<1 & rs'>> by exists rs'. have splitL : splittingFieldFor 1 (p ^^ in_alg L) <<1 & rs>> by exists rs. have [f imgf] := splitting_ahom splitS splitM. have [g imgg] := splitting_ahom splitS splitL. rewrite -imgf -(aimg1 f)/= -img_map_gal injm_sol ?map_gal_inj ?subsetT//. by rewrite -imgg -(aimg1 g)/= -img_map_gal injm_sol ?map_gal_inj ?subsetT//. 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)