proposition: Lemma enum_AEnd : {kAutL : seq 'AEnd(L) | forall f, f \in kAutL}.
proof: Proof. pose isAutL (s : seq 'AEnd(L)) (f : 'AEnd(L)) := kHom 1 {:L} f = (f \in s). suffices [kAutL in_kAutL] : {kAutL : seq 'AEnd(L) | forall f, isAutL kAutL f}. by exists kAutL => f; rewrite -in_kAutL k1AHom. have [p Kp /sig2_eqW[rs Dp defL]] := splittingPoly. do [rewrite {}/isAutL -(erefl (asval 1)); set r := rs; set E := 1%AS] in defL *. have [sKE rs_r]: (1 <= E)%VS /\ all [in rs] r by split; last apply/allP. elim: r rs_r => [_|z r IHr /=/andP[rs_z rs_r]] /= in (E) sKE defL *. rewrite Fadjoin_nil in defL; exists [tuple \1%AF] => f; rewrite defL inE. apply/idP/eqP=> [/kAHomP f1 | ->]; last exact: kHom1. by apply/val_inj/lfunP=> x; rewrite id_lfunE f1 ?memvf. do [set Ez := <<E; z>>%VS; rewrite adjoin_cons] in defL. have sEEz: (E <= Ez)%VS := subv_adjoin E z; have sKEz := subv_trans sKE sEEz. have{IHr} [homEz DhomEz] := IHr rs_r _ sKEz defL. have Ep: p \in polyOver E := polyOverSv sKE Kp. have{rs_z} pz0: root p z by rewrite (eqp_root Dp) root_prod_XsubC. pose pEz := minPoly E z; pose n := \dim_E Ez. have{pz0} [rz DpEz]: {rz : n.-tuple L | pEz %= \prod_(w <- rz) ('X - w%:P)}. have /dvdp_prod_XsubC[m DpEz]: pEz %| \prod_(w <- rs) ('X - w%:P). by rewrite -(eqp_dvdr _ Dp) minPoly_dvdp ?(polyOverSv sKE). suffices sz_rz: size (mask m rs) == n by exists (Tuple sz_rz). rewrite -[n]adjoin_degreeE -eqSS -size_minPoly. by rewrite (eqp_size DpEz) size_prod_XsubC. have fEz i (y := tnth rz i): {f : 'AEnd(L) | kHom E {:L} f & f z = y}. have homEfz: kHom E Ez (kHomExtend E \1 z y). rewrite kHomExtendP ?kHom1 // lfun1_poly. by rewrite (eqp_root DpEz) -/rz root_prod_XsubC mem_tnth. have splitFp: splittingFieldFor Ez p {:L}. exists rs => //; apply/eqP; rewrite eqEsubv subvf -defL adjoin_seqSr //. exact/allP. have [f homLf Df] := kHom_extends sEEz homEfz Ep splitFp. have [ahomf _] := andP homLf; exists (AHom ahomf) => //. rewrite -Df ?memv_adjoin ?(kHomExtend_val (kHom1 E E)) // lfun1_poly. by rewrite (eqp_root DpEz) root_prod_XsubC mem_tnth. exists [seq (s2val (fEz i) \o f)%AF| i <- enum 'I_n, f <- homEz] => f. apply/idP/allpairsP => [homLf | [[i g] [_ Hg ->]] /=]; last first. by case: (fEz i) => fi /= /comp_kHom->; rewrite ?(kHomSl sEEz) ?DhomEz. have /tnthP[i Dfz]: f z \in rz. rewrite memtE /= -root_prod_XsubC -(eqp_root DpEz). by rewrite (kHom_root_id _ homLf) ?memvf ?subvf ?minPolyOver ?root_minPoly. case Dfi: (fEz i) => [fi homLfi fi_z]; have kerfi0 := kAutf_lker0 homLfi. set fj := (fi ^-1 \o f)%AF; suffices Hfj : fj \in homEz. exists (i, fj) => //=; rewrite mem_enum inE Hfj; split => //. by apply/val_inj; rewrite {}Dfi /= (lker0_compVKf kerfi0). rewrite -DhomEz; apply/kAHomP => _ /Fadjoin_polyP[q Eq ->]. have homLfj: kHom E {:L} fj := comp_kHom (inv_kHomf homLfi) homLf. have /kHom_lrmorphism fjM := kHomSl (sub1v _) homLfj. pose fjmM := GRing.isMultiplicative.Build _ _ _ fjM. pose fjRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun fj) fjmM. rewrite -[fj _](horner_map fjRM) (kHom_poly_id homLfj) //=. by rewrite (@lfunE _ _ L) /= Dfz -fi_z lker0_lfunK. 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)