proposition: Lemma inv_map_hom_kHom (E F : {subfield L}) (f : 'End(L')) : (E <= F)%VS -> ((f @: (iota @: F)) <= (limg iota))%VS -> kHom E F (inv_map_hom iota f) = kHom (iota @: E) (iota @: F) f.
proof: Proof. move=> EF fiotaF; have fiotaf u : u \in F -> f (iota u) \in limg iota. by move=> uF; apply: subv_trans fiotaF; do !apply: memv_img. apply/kHomP/kHomP => -[/= fM s_id]. split=> [_ _/memv_imgP[x xF ->]|_] /memv_imgP[y yF ->]. rewrite -!rmorphM/= -3?inv_map_homE ?memv_img ?memvf ?fiotaf ?rpredM//. by rewrite fM// rmorphM. by rewrite -inv_map_homE ?s_id// fiotaf//; apply: subv_trans EF. split=> [x y xF yF|x xF]; apply: (fmorph_inj iota) => /=. by rewrite rmorphM/= !inv_map_homE ?fiotaf ?rpredM// rmorphM fM ?memv_img. by rewrite inv_map_homE s_id ?memv_img ?memvf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)