proposition: Lemma splitting_field_normal K x : exists r, minPoly K x == \prod_(y <- r) ('X - y%:P).
proof: Proof. pose q1 := minPoly 1 x; pose fx_root q (f : 'AEnd(L)) := root q (f x). have [[p F0p splitLp] [autL DautL]] := (splittingFieldP, enum_AEnd). suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. set q := minPoly K x; have: q \is monic := monic_minPoly K x. have: q %| q1 by rewrite minPolyS // sub1v. have [d] := ubnP (size q); elim: d q => // d IHd q leqd q_dv_q1 mon_q. have nz_q: q != 0 := monic_neq0 mon_q. have [|q_gt1|q_1] := ltngtP (size q) 1; last first; last by rewrite polySpred. by exists nil; rewrite big_nil -eqp_monic ?monic1 // -size_poly_eq1 q_1. have /hasP[f autLf /factor_theorem[q2 Dq]] := autL_px q nz_q q_dv_q1 q_gt1. have mon_q2: q2 \is monic by rewrite -(monicMr _ (monicXsubC (f x))) -Dq. rewrite Dq size_monicM -?size_poly_eq0 ?size_XsubC ?addn2 //= ltnS in leqd. have q2_dv_q1: q2 %| q1 by rewrite (dvdp_trans _ q_dv_q1) // Dq dvdp_mulr. rewrite Dq; have [r /eqP->] := IHd q2 leqd q2_dv_q1 mon_q2. by exists (f x :: r); rewrite big_cons mulrC. have [d] := ubnP (size q); elim: d q => // d IHd q leqd nz_q q_dv_q1 q_gt1. without loss{d leqd IHd nz_q q_gt1} irr_q: q q_dv_q1 / irreducible_poly q. move=> IHq; apply: wlog_neg => not_autLx_q; apply: IHq => //. split=> // q2 q2_neq1 q2_dv_q; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. rewrite leqNgt; apply: contra not_autLx_q => ltq2q. have nz_q2: q2 != 0 by apply: contraTneq q2_dv_q => ->; rewrite dvd0p. have{q2_neq1} q2_gt1: size q2 > 1 by rewrite neq_ltn polySpred in q2_neq1 *. have{leqd ltq2q} ltq2d: size q2 < d by apply: leq_trans ltq2q _. apply: sub_has (IHd _ ltq2d nz_q2 (dvdp_trans q2_dv_q q_dv_q1) q2_gt1) => f. by rewrite /fx_root !root_factor_theorem => /dvdp_trans->. have{irr_q} [Lz [inLz [z qz0]]]: {Lz : fieldExtType F & {inLz : 'AHom(L, Lz) & {z : Lz | root (map_poly inLz q) z}}}. - have [Lz0 _ [z qz0 defLz]] := irredp_FAdjoin irr_q. pose Lz : fieldExtType _ := baseFieldType Lz0. pose inLz : {rmorphism L -> Lz} := in_alg Lz0. have inLzL_linear: linear (locked inLz). by move=> a u v; rewrite -[in LHS]mulr_algl rmorphD rmorphM -lock mulr_algl. pose inLzLlM := GRing.isLinear.Build _ _ _ _ _ inLzL_linear. pose inLzLL : {linear _ -> _} := HB.pack (locked inLz : _ -> _) inLzLlM. have ihLzZ: ahom_in {:L} (linfun inLzLL). by apply/ahom_inP; split=> [u v|]; rewrite !lfunE (rmorphM, rmorph1). exists Lz, (AHom ihLzZ), z; congr (root _ z): qz0. by apply: eq_map_poly => y; rewrite lfunE /= -lock. pose imL := [aspace of limg inLz]; pose pz := map_poly inLz p. have in_imL u: inLz u \in imL by rewrite memv_img ?memvf. have F0pz: pz \is a polyOver 1%VS. apply/polyOverP=> i; rewrite -(aimg1 inLz) coef_map /= memv_img //. exact: (polyOverP F0p). have{splitLp} splitLpz: splittingFieldFor 1 pz imL. have [r def_p defL] := splitLp; exists (map inLz r) => [|{def_p}]. move: def_p; rewrite -(eqp_map inLz) rmorph_prod. rewrite big_map; congr (_ %= _); apply: eq_big => //= y _. by rewrite rmorphB /= map_polyX map_polyC. apply/eqP; rewrite eqEsubv /= -{2}defL {defL}; apply/andP; split. by apply/Fadjoin_seqP; rewrite sub1v; split=> // _ /mapP[y r_y ->]. elim/last_ind: r => [|r y IHr] /=; first by rewrite !Fadjoin_nil aimg1. rewrite map_rcons !adjoin_rcons /=. apply/subvP=> _ /memv_imgP[_ /Fadjoin_polyP[p1 r_p1 ->] ->]. rewrite -horner_map /= mempx_Fadjoin //=; apply/polyOverP=> i. by rewrite coef_map (subvP IHr) //= memv_img ?(polyOverP r_p1). have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose q1z := minPoly 1 (inLz x). have Dq1z: map_poly inLz q1 %| q1z. have F0q1z i: exists a, q1z`_i = a%:A by apply/vlineP/polyOverP/minPolyOver. have [q2 Dq2]: exists q2, q1z = map_poly inLz q2. exists (\poly_(i < size q1z) (sval (sig_eqW (F0q1z i)))%:A). rewrite -{1}[q1z]coefK; apply/polyP=> i; rewrite coef_map !{1}coef_poly. by case: sig_eqW => a; case: ifP; rewrite /= ?rmorph0 ?linearZ ?rmorph1. rewrite Dq2 dvdp_map minPoly_dvdp //. apply/polyOverP=> i; have[a] := F0q1z i. rewrite -(rmorph1 inLz) -linearZ. by rewrite Dq2 coef_map => /fmorph_inj->; rewrite rpredZ ?mem1v. by rewrite -(fmorph_root inLz) -Dq2 root_minPoly. have q1z_z: root q1z z. rewrite !root_factor_theorem in qz0 *. by apply: dvdp_trans qz0 (dvdp_trans _ Dq1z); rewrite dvdp_map. have map1q1z_z: root (map_poly \1%VF q1z) z. by rewrite map_poly_id => // ? _; rewrite lfunE. pose f0 := kHomExtend 1 \1 (inLz x) z. have{map1q1z_z} hom_f0 : kHom 1 <<1; inLz x>> f0. by apply: kHomExtendP map1q1z_z => //; apply: kHom1. have{} splitLpz: splittingFieldFor <<1; inLz x>> pz imL. have [r def_pz defLz] := splitLpz; exists r => //. apply/eqP; rewrite eqEsubv -{2}defLz adjoin_seqSl ?sub1v // andbT. apply/Fadjoin_seqP; split; last first. by rewrite /= -[limg _]defLz; apply: seqv_sub_adjoin. by apply/FadjoinP/andP; rewrite sub1v memv_img ?memvf. have [f homLzf Df] := kHom_extends (sub1v _) hom_f0 F0pz splitLpz. have [-> | x'z] := eqVneq (inLz x) z. by exists \1%VF; rewrite ?lfunE ?kHom1. exists f => //; rewrite -Df ?memv_adjoin ?(kHomExtend_val (kHom1 1 1)) //. by rewrite lfun1_poly. pose f1 := (inLz^-1 \o f \o inLz)%VF; have /kHomP[fM fFid] := homLf. have Df1 u: inLz (f1 u) = f (inLz u). rewrite !comp_lfunE limg_lfunVK //= -[limg _]/(asval imL). have [r def_pz defLz] := splitLpz; set r1 := r. have: inLz u \in <<1 & r1>>%VS by rewrite defLz. have: all [in r] r1 by apply/allP. elim/last_ind: r1 {u}(inLz u) => [|r1 y IHr1] u. by rewrite Fadjoin_nil => _ Fu; rewrite fFid // (subvP (sub1v _)). rewrite all_rcons adjoin_rcons => /andP[rr1 ry] /Fadjoin_polyP[pu r1pu ->]. rewrite (kHom_horner homLf) -defLz; last exact: seqv_sub_adjoin; last first. by apply: polyOverS r1pu; apply/subvP/adjoin_seqSr/allP. apply: rpred_horner. by apply/polyOverP=> i; rewrite coef_map /= defLz IHr1 ?(polyOverP r1pu). rewrite seqv_sub_adjoin // -root_prod_XsubC -(eqp_root def_pz). rewrite (kHom_root_id _ homLf) ?sub1v //. by rewrite -defLz seqv_sub_adjoin. by rewrite (eqp_root def_pz) root_prod_XsubC. suffices f1_is_ahom : ahom_in {:L} f1. apply/hasP; exists (AHom f1_is_ahom); first exact: DautL. by rewrite /fx_root -(fmorph_root inLz) /= Df1 fxz. apply/ahom_inP; split=> [a b _ _|]; apply: (fmorph_inj inLz). by rewrite rmorphM /= !Df1 rmorphM fM ?in_imL. by rewrite /= Df1 /= fFid ?rmorph1 ?mem1v. 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)