proposition: Lemma img_map_gal (K : {subfield L}) : (map_gal @* 'Gal(E / K))%g = 'Gal(iota @: E / iota @: K)%g.
proof: Proof. wlog subKE : K / (K <= E)%VS => [hwlog|]. by rewrite gal_cap hwlog ?capvSr// aimg_cap -gal_cap. rewrite /'Gal(_ / _)%g -aimg_cap !genGid/= (capv_idPl _)//. rewrite -!gal_kAEndf ?limgS// -morphim_comp/=. apply/setP => u; apply/imsetP/imsetP => /= [[f faut ->]|[f' f'aut ->]] {u}. have := faut; rewrite !inE !kAut1E !kAutE/= !subfield_closed !subvf !andbT. move=> /andP[fE /kAHomP fK]. exists (map_ahom iota f). rewrite !inE !kAut1E !kAutE/= !subvf !andbT limg_map_ahom limgS//=. by apply/kAHomP => _/memv_imgP[x xK ->]; rewrite map_ahomE ?fK. apply/eqP/gal_eqP => _/memv_imgP[x xK ->]. by rewrite map_galE// !galK ?memv_img ?limg_map_ahom ?map_ahomE// limg_ker0//. have := f'aut; rewrite !inE !kAut1E !kAutE/= !subvf !andbT. have -> : agenv (iota @: E) = (iota @: E)%VS by rewrite subfield_closed. move=> /andP[f'E /kAHomP f'K]. have /kHom_to_AEnd[f eqf] : kHom K E (inv_map_hom iota f'). by rewrite inv_map_hom_kHom ?(subv_trans f'E) ?limgS ?subvf//; apply/kAHomP. have fE : (f @: E <= E)%VS. rewrite -(eq_in_limg eqf) -(limg_ker0 _ _ (AHom_lker0 iota)). by rewrite limg_inv_map_ahom//. exists f; rewrite ?inE ?kAut1E ?kAutE/= ?subfield_closed ?subvf ?andbT ?fE. apply/kAHomP => x xK; rewrite -eqf ?(subvP subKE)// !comp_lfunE. by rewrite f'K ?memv_img// lker0_lfunK. apply/eqP/gal_eqP => _/memv_imgP[x xE ->]; rewrite map_galE//. rewrite !galK ?memv_img// -eqf//= inv_map_homE//. apply: subv_trans (limgS _ (subvf E)); apply: subv_trans f'E. by do !apply: memv_img. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)