proposition: Lemma solvable_poly_rat (p : {poly rat}) : p != 0 -> solvable_by_radical_poly p -> {L : splittingFieldType rat & {iota : {rmorphism L -> algC} & { rs : seq L | p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) /\ solvable_by radical 1 <<1 & rs>>}}}.
proof: Proof. move=> p_neq0 p_sol. 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 [L [iota [rs iota_rs rsf]]] := num_field_exists rsalg. have prs : p ^^ in_alg L %= \prod_(z <- rs) ('X - z%:P). rewrite -(eqp_map iota) map_prod_XsubC iota_rs -map_poly_comp. by rewrite (eq_map_poly (fmorph_eq_rat _)). have splitL : SplittingField.axiom L. by exists (p ^^ in_alg L); [by apply/polyOver1P; exists p | exists rs]. pose Frat := [the fieldType of rat : Type]. pose sM := FieldExt_isSplittingField.Build Frat L splitL. pose S : splittingFieldType Frat := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have d_gt0 : (d > 0)%N by rewrite adim_gt0. have [ralg ralg_prim] := C_prim_root_exists d_gt0. have [L' [iota' [[]//= w rs' [iotaw iota_rs' wrsf]]]] := num_field_exists (ralg :: rsalg). have prs' : p ^^ in_alg L' %= \prod_(z <- rs') ('X - z%:P). rewrite -(eqp_map iota') map_prod_XsubC iota_rs' -map_poly_comp. by rewrite (eq_map_poly (fmorph_eq_rat _)). have w_prim : d.-primitive_root w. by move: ralg_prim; rewrite -iotaw fmorph_primitive_root. have splitL' : SplittingField.axiom L'. exists (cyclotomic w d * p ^^ in_alg L'). by rewrite rpredM ?cyclotomic_over//; apply/polyOver1P; exists p. have [us cycloE usw] := splitting_Fadjoin_cyclotomic 1%AS w_prim. exists (us ++ rs'); last by rewrite adjoin_cat usw -adjoin_cons. by rewrite big_cat/= (eqp_trans (eqp_mulr _ cycloE))// eqp_mull//. pose sM' := FieldExt_isSplittingField.Build Frat L' splitL'. pose S' : splittingFieldType Frat := HB.pack L' sM'. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs. have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'. have [f /= imgf] := splitting_ahom splitS splitS'. exists S', iota', rs'; split => //. by apply: (p_sol S' rs' prs' w); rewrite -imgf dim_aimg/= -rsf. 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)