proposition: Lemma kHom_extends K E f p U : (K <= E)%VS -> kHom K E f -> p \is a polyOver K -> splittingFieldFor E p U -> {g | kHom K U g & {in E, f =1 g}}.
proof: Proof. move=> sKE homEf Kp /sig2_eqW[rs Dp <-{U}]. set r := rs; have rs_r: all [in rs] r by apply/allP. elim: r rs_r => [_|z r IHr /=/andP[rs_z rs_r]] /= in E f sKE homEf *. by exists f; rewrite ?Fadjoin_nil. set Ez := <<E; z>>%AS; pose fpEz := map_poly f (minPoly E z). suffices{IHr} /sigW[y fpEz_y]: exists y, root fpEz y. have homEz_fz: kHom K Ez (kHomExtend E f z y) by apply: kHomExtendP. have sKEz: (K <= Ez)%VS := subv_trans sKE (subv_adjoin E z). have [g homGg Dg] := IHr rs_r _ _ sKEz homEz_fz. exists g => [|x Ex]; first by rewrite adjoin_cons. by rewrite -Dg ?subvP_adjoin // kHomExtend_id. have [m DfpEz]: {m | fpEz %= \prod_(w <- mask m rs) ('X - w%:P)}. apply: dvdp_prod_XsubC; rewrite -(eqp_dvdr _ Dp) -(kHom_poly_id homEf Kp). have /polyOver_subvs[q Dq] := polyOverSv sKE Kp. have /polyOver_subvs[qz Dqz] := minPolyOver E z. rewrite /fpEz Dq Dqz -2?{1}map_poly_comp (dvdp_map (kHom_rmorphism homEf)). rewrite -(dvdp_map (@vsval _ _ E)) -Dqz -Dq. by rewrite minPoly_dvdp ?(polyOverSv sKE) // (eqp_root Dp) root_prod_XsubC. exists (mask m rs)`_0; rewrite (eqp_root DfpEz) root_prod_XsubC mem_nth //. rewrite -ltnS -(size_prod_XsubC _ id) -(eqp_size DfpEz). rewrite size_poly_eq -?lead_coefE ?size_minPoly // (monicP (monic_minPoly E z)). by have [_ idKf] := kHomP homEf; rewrite idKf ?mem1v ?oner_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)