proposition: Lemma map_ahom_kAut s (E F : {subfield L}) : kAut (iota @: E)%VS (iota @: F)%VS (map_ahom s) = kAut E F s.
proof: Proof. rewrite !kAutE limg_map_ahom limg_ker0 ?AHom_lker0// [LHS]andbC [RHS]andbC. have [sF_sub_F|]//= := boolP (s @: F <= F)%VS. apply/kAHomP/kAHomP => [s_id x xE|s_id _/memv_imgP[x xE ->]]; last first. by rewrite map_ahomE s_id. apply: (fmorph_inj iota). by rewrite /= -map_ahomE s_id// memv_img. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)