proposition: Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) : irreducible_poly p -> {L : fieldExtType F & \dim {:L} = (size p).-1 & {z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.
proof: Proof. case=> p_gt1 irr_p; set n := (size p).-1; pose vL : vectType F := 'rV_n. have Dn: n.+1 = size p := ltn_predK p_gt1. have nz_p: p != 0 by rewrite -size_poly_eq0 -Dn. suffices [L dimL [toPF [toL toPF_K toL_K]]]: {L : fieldExtType F & \dim {:L} = (size p).-1 & {toPF : {linear L -> {poly F}} & {toL : {lrmorphism {poly F} -> L} | cancel toPF toL & forall q, toPF (toL q) = q %% p}}}. - exists L => //; pose z := toL 'X; set iota := in_alg _. suffices q_z q: toPF (map_poly iota q).[z] = q %% p. exists z; first by rewrite /root -(can_eq toPF_K) q_z modpp linear0. apply/vspaceP=> x; rewrite memvf; apply/Fadjoin_polyP. exists (map_poly iota (toPF x)). by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v. by apply: (can_inj toPF_K); rewrite q_z -toL_K toPF_K. elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. rewrite linearZ /= -(rmorph1 toL) toL_K -modpZl alg_polyC modpD. congr (_ + _); rewrite -toL_K rmorphM /= -/z; congr (toPF (_ * z)). by apply: (can_inj toPF_K); rewrite toL_K. pose toL q : vL := poly_rV (q %% p); pose toPF (x : vL) := rVpoly x. have toL_K q : toPF (toL q) = q %% p. by rewrite /toPF poly_rV_K // -ltnS Dn ?ltn_modp -?Dn. have toPF_K: cancel toPF toL. by move=> x; rewrite /toL modp_small ?rVpolyK // -Dn ltnS size_poly. have toPinj := can_inj toPF_K. pose mul x y := toL (toPF x * toPF y); pose L1 := toL 1. have L1K: toPF L1 = 1 by rewrite toL_K modp_small ?size_poly1. have mulC: commutative mul by rewrite /mul => x y; rewrite mulrC. have mulA: associative mul. by move=> x y z; apply: toPinj; rewrite -!(mulC z) !toL_K !modp_mul mulrCA. have mul1: left_id L1 mul. by move=> x; apply: toPinj; rewrite mulC !toL_K modp_mul mulr1 -toL_K toPF_K. have mulD: left_distributive mul +%R. move=> x y z; apply: toPinj; rewrite /toPF raddfD /= -!/(toPF _). by rewrite !toL_K /toPF raddfD mulrDl modpD. have nzL1: L1 != 0 by rewrite -(inj_eq toPinj) L1K /toPF raddf0 oner_eq0. pose mulM := GRing.Zmodule_isComRing.Build _ mulA mulC mul1 mulD nzL1. pose rL : comRingType := HB.pack vL mulM. have mulZlM : GRing.Lmodule_isLalgebra F rL. constructor => a x y; apply: toPinj. by rewrite toL_K /toPF !linearZ /= -!/(toPF _) toL_K -scalerAl modpZl. pose laL : lalgType F := HB.pack rL mulZlM. have mulZrM : GRing.Lalgebra_isAlgebra F laL. by constructor => a x y; rewrite !(mulrC x) scalerAl. pose aL : algType F := HB.pack laL mulZrM. pose uLM := Algebra_isFalgebra.Build F aL. pose cuL : comUnitRingType := HB.pack aL uLM. have unitM : GRing.ComUnitRing_isField cuL. constructor => x nz_x; apply/unitrP; set q := toPF x. have nz_q: q != 0 by rewrite -(inj_eq toPinj) /toPF raddf0 in nz_x. have /Bezout_eq1_coprimepP[u upq1]: coprimep p q. apply: contraLR (leq_gcdpr p nz_q) => /irr_p/implyP. rewrite dvdp_gcdl -ltnNge /= => /eqp_size->. by rewrite (polySpred nz_p) ltnS size_poly. suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC. apply: toPinj; rewrite !toL_K -upq1 modp_mul modpD mulrC. by rewrite modp_mull add0r. pose feL : fieldExtType F := HB.pack vL aL cuL unitM. exists feL; first by rewrite dimvf; apply: mul1n. exists toPF. have tol_lin: linear toL by move=> a q1 q2; rewrite -linearP -modpZl -modpD. have tol_mul : multiplicative (toL : {poly F} -> aL). by split=> [q r|]; apply: toPinj; rewrite !toL_K // modp_mul -!(mulrC r) modp_mul. pose toLlM := GRing.isLinear.Build _ _ _ _ toL tol_lin. pose toLmM := GRing.isMultiplicative.Build _ _ _ tol_mul. pose toLLRM : {lrmorphism _ -> feL} := HB.pack toL toLlM toLmM. by exists toLLRM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)