proposition: Lemma large_field_PET q : root (q ^ iota) y -> separable_poly q -> exists2 r, r != 0 & forall t (z := iota t * y - x), ~~ root r (iota t) -> inFz z x /\ inFz z y.
proof: Proof. move=> qy_0 sep_q; have nz_q := separable_poly_neq0 sep_q. have /factor_theorem[q0 Dq] := qy_0. set p1 := p ^ iota \Po ('X + x%:P); set q1 := q0 \Po ('X + y%:P). have nz_p1: p1 != 0. apply: contraNneq nz_p => /(canRL (fun r => comp_polyXaddC_K r _))/eqP. by rewrite comp_poly0 map_poly_eq0. have{sep_q} nz_q10: q1.[0] != 0. move: sep_q; rewrite -(separable_map iota) Dq separable_root => /andP[_]. by rewrite horner_comp !hornerE. have nz_q1: q1 != 0 by apply: contraNneq nz_q10 => ->; rewrite horner0. pose p2 := p1 ^ polyC \Po ('X * 'Y); pose q2 := q1 ^ polyC. have /Bezout_coprimepP[[u v]]: coprimep p2 q2. rewrite coprimep_def eqn_leq leqNgt andbC size_poly_gt0 gcdp_eq0 poly_XmY_eq0. by rewrite map_polyC_eq0 (negPf nz_p1) -resultant_eq0 div_annihilant_neq0. rewrite -size_poly_eq1 => /size_poly1P[r nzr Dr]; exists r => {nzr}// t z nz_rt. have [r1 nz_r1 r1z_0]: algebraicOver iota z. apply/algebraic_sub; last by exists p. by apply: algebraic_mul; [apply: algebraic_id | exists q]. pose Fz := subFExtend iota z r1; pose kappa : Fz -> L := subfx_inj. pose kappa' := inj_subfx iota z r1. have /eq_map_poly Diota: kappa \o kappa' =1 iota. by move=> w; rewrite /kappa /= subfx_inj_eval // map_polyC hornerC. suffices [y3]: exists y3, y = kappa y3. have [q3 ->] := subfxE y3; rewrite /kappa subfx_inj_eval // => Dy. split; [exists (t *: q3 - 'X) | by exists q3]. by rewrite rmorphB /= linearZ map_polyX !hornerE -Dy opprB addrC addrNK. pose p0 := p ^ iota \Po (iota t *: 'X - z%:P). have co_p0_q0: coprimep p0 q0. pose at_t := horner_eval (iota t); have at_t0: at_t 0 = 0 by apply: rmorph0. have /map_polyK polyCK: cancel polyC at_t by move=> w; apply: hornerC. have ->: p0 = p2 ^ at_t \Po ('X - y%:P). rewrite map_comp_poly polyCK // rmorphM /= map_polyC map_polyX /=. rewrite horner_evalE hornerX. rewrite -!comp_polyA comp_polyM comp_polyD !comp_polyC !comp_polyX. by rewrite mulrC mulrBr mul_polyC addrAC -addrA -opprB -rmorphM -rmorphB. have ->: q0 = q2 ^ at_t \Po ('X - y%:P) by rewrite polyCK ?comp_polyXaddC_K. apply/coprimep_comp_poly/Bezout_coprimepP; exists (u ^ at_t, v ^ at_t). by rewrite /= -!rmorphM -rmorphD Dr /= map_polyC polyC_eqp1. have{co_p0_q0}: gcdp p0 (q ^ iota) %= 'X - y%:P. rewrite /eqp Dq (eqp_dvdl _ (Gauss_gcdpr _ _)) // dvdp_gcdr dvdp_gcd. rewrite dvdp_mull // -root_factor_theorem rootE horner_comp !hornerE. by rewrite opprB addrC subrK. have{p0} [p3 ->]: exists p3, p0 = p3 ^ kappa. exists (p ^ kappa' \Po (kappa' t *: 'X - (subfx_eval iota z r1 'X)%:P)). rewrite map_comp_poly rmorphB /= linearZ /= map_polyC map_polyX /=. rewrite !subfx_inj_eval // map_polyC hornerC map_polyX hornerX. by rewrite -map_poly_comp Diota. rewrite -Diota map_poly_comp -gcdp_map /= -/kappa. move: (gcdp _ _) => r3 /eqpf_eq[c nz_c Dr3]. exists (- (r3`_0 / r3`_1)); rewrite [kappa _]rmorphN fmorph_div -!coef_map Dr3. by rewrite !coefZ polyseqXsubC mulr1 mulrC mulKf ?opprK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)