proposition: Lemma extend_algC_subfield_aut (Qs : fieldExtType rat) (QsC : {rmorphism Qs -> algC}) (phi : {rmorphism Qs -> Qs}) : {nu : {rmorphism algC -> algC} | {morph QsC : x / phi x >-> nu x}}.
proof: Proof. pose numF_inj (Qr : fieldExtType rat) := {rmorphism Qr -> algC}. pose subAut := {Qr : _ & numF_inj Qr * {lrmorphism Qr -> Qr}}%type. pose SubAut := existT _ _ (_, _) : subAut. pose Sdom (mu : subAut) := projT1 mu. pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projT2 mu).1. pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projT2 mu).2. have SinjZ Qr (QrC : numF_inj Qr) a x: QrC (a *: x) = QtoC a * QrC x. rewrite mulrAC; apply: canRL (mulfK _) _. by rewrite intr_eq0 denq_neq0. by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -[x *~ _]scaler_int -mulrzr -numqE. have Sinj_poly Qr (QrC : numF_inj Qr) p: map_poly QrC (map_poly (in_alg Qr) p) = pQtoC p. - rewrite -map_poly_comp; apply: eq_map_poly => a. by rewrite /= SinjZ rmorph1 mulr1. have ext1 mu0 x : {mu1 | exists y, x = Sinj mu1 y & exists2 in01 : {lrmorphism _ -> _}, Sinj mu0 =1 Sinj mu1 \o in01 & {morph in01: y / Saut mu0 y >-> Saut mu1 y}}. - pose b0 := vbasis {:Sdom mu0}. have [z _ /sig_eqW[[|px ps] // [Dx Ds]]] := algC_PET (x :: map (Sinj mu0) b0). have [p [_ mon_p] /(_ p) pz0] := minCpolyP z; rewrite dvdpp in pz0. have [r Dr] := closed_field_poly_normal (pQtoC p : {poly algC}). rewrite lead_coef_map {mon_p}(monicP mon_p) rmorph1 scale1r in Dr. have{pz0} rz: z \in r by rewrite -root_prod_XsubC -Dr. have [Qr [QrC [rr Drr genQr]]] := num_field_exists r. have{rz} [zz Dz]: {zz | QrC zz = z}. by move: rz; rewrite -Drr => /mapP/sig2_eqW[zz]; exists zz. have{ps Ds} [in01 Din01]: {in01 : {lrmorphism _ -> _} | Sinj mu0 =1 QrC \o in01}. have in01P y: {yy | Sinj mu0 y = QrC yy}. exists (\sum_i coord b0 i y *: (map_poly (in_alg Qr) ps`_i).[zz]). rewrite {1}(coord_vbasis (memvf y)) !rmorph_sum /=; apply: eq_bigr => i _. rewrite !SinjZ; congr (_ * _); rewrite -(nth_map _ 0) ?size_tuple // Ds. rewrite -horner_map Dz Sinj_poly (nth_map 0) //. by have:= congr1 size Ds; rewrite !size_map size_tuple => <-. pose in01 y := sval (in01P y). have Din01 y: Sinj mu0 y = QrC (in01 y) by rewrite /in01; case: (in01P y). pose rwM := (=^~ Din01, SinjZ, rmorph1, rmorphB, rmorphM). have in01a : additive in01. by move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM. have in01m : multiplicative in01. by split; try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM /= ?rwM. have in01l : scalable in01. by try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM. pose in01aM := GRing.isAdditive.Build _ _ in01 in01a. pose in01mM := GRing.isMultiplicative.Build _ _ in01 in01m. pose in01lM := GRing.isScalable.Build _ _ _ _ in01 in01l. pose in01LRM : {lrmorphism _ -> _} := HB.pack in01 in01aM in01mM in01lM. by exists in01LRM. have {z zz Dz px} Dx: exists xx, x = QrC xx. exists (map_poly (in_alg Qr) px).[zz]. by rewrite -horner_map Dz Sinj_poly Dx. pose lin01 := linfun in01; pose K := (lin01 @: fullv)%VS. have memK y: reflect (exists yy, y = in01 yy) (y \in K). apply: (iffP memv_imgP) => [[yy _ ->] | [yy ->]]; by exists yy; rewrite ?lfunE ?memvf. have algK: is_aspace K. rewrite /is_aspace has_algid1; last first. by apply/memK; exists 1; rewrite rmorph1. apply/prodvP=> _ _ /memK[y1 ->] /memK[y2 ->]. by apply/memK; exists (y1 * y2); rewrite rmorphM. have ker_in01: lker lin01 == 0%VS. by apply/lker0P=> y1 y2; rewrite !lfunE; apply: fmorph_inj. pose f := (lin01 \o linfun (Saut mu0) \o lin01^-1)%VF. have Df y: f (in01 y) = in01 (Saut mu0 y). transitivity (f (lin01 y)); first by rewrite !lfunE. by do 4!rewrite lfunE /=; rewrite lker0_lfunK. have hom_f: kHom 1 (ASpace algK) f. apply/kHomP; split=> [_ _ /memK[y1 ->] /memK[y2 ->] |_ /vlineP[a ->]]. by rewrite -rmorphM !Df !rmorphM. by rewrite -(rmorph1 in01) -linearZ /= Df /= {1}linearZ /= rmorph1. pose pr := map_poly (in_alg Qr) p. have Qpr: pr \is a polyOver 1%VS. by apply/polyOverP=> i; rewrite coef_map memvZ ?memv_line. have splitQr: splittingFieldFor K pr fullv. apply: splittingFieldForS (sub1v (Sub K algK)) (subvf _) _; exists rr => //. congr (_ %= _): (eqpxx pr); apply/(map_poly_inj QrC). rewrite Sinj_poly Dr -Drr big_map rmorph_prod /=; apply: eq_bigr => zz _. by rewrite rmorphB /= map_polyX map_polyC. have [f1 aut_f1 Df1]:= kHom_extends (sub1v (ASpace algK)) hom_f Qpr splitQr. pose f1mM := GRing.isMultiplicative.Build _ _ f1 (kHom_lrmorphism aut_f1). pose nu : {lrmorphism _ -> _} := HB.pack (fun_of_lfun f1) f1mM. exists (SubAut Qr QrC nu) => //; exists in01 => //= y. by rewrite -Df -Df1 //; apply/memK; exists y. have phiZ: scalable phi. move=> a y; do 2!rewrite -mulr_algl -in_algE; rewrite -[a]divq_num_den. by rewrite fmorph_div rmorphM [X in X * _]fmorph_div !rmorph_int. pose philM := GRing.isScalable.Build _ _ _ _ phi phiZ. pose phiLRM : {lrmorphism _ -> _} := HB.pack (GRing.RMorphism.sort phi) philM. pose fix ext n := if n is i.+1 then oapp (fun x => s2val (ext1 (ext i) x)) (ext i) (unpickle i) else SubAut Qs QsC phiLRM. have mem_ext x n: (pickle x < n)%N -> {xx | Sinj (ext n) xx = x}. move=> ltxn; apply: sig_eqW; elim: n ltxn => // n IHn. rewrite ltnS leq_eqVlt => /predU1P[<- | /IHn[xx <-]] /=. by rewrite pickleK /=; case: (ext1 _ x) => mu [xx]; exists xx. case: (unpickle n) => /= [y|]; last by exists xx. case: (ext1 _ y) => mu /= _ [in_mu inj_in_mu _]. by exists (in_mu xx); rewrite inj_in_mu. pose nu x := Sinj _ (Saut _ (sval (mem_ext x _ (ltnSn _)))). have nu_inj n y: nu (Sinj (ext n) y) = Sinj (ext n) (Saut (ext n) y). rewrite /nu; case: (mem_ext _ _ _); move: _.+1 => n1 y1 Dy /=. without loss /subnK Dn1: n n1 y y1 Dy / (n <= n1)%N. by move=> IH; case/orP: (leq_total n n1) => /IH => [/(_ y) | /(_ y1)]->. move: (n1 - n)%N => k in Dn1; elim: k => [|k IHk] in n Dn1 y Dy *. by move: y1 Dy; rewrite -Dn1 => y1 /fmorph_inj ->. rewrite addSnnS in Dn1; move/IHk: Dn1 => /=. case: (unpickle _) => [z|] /=; last exact. case: (ext1 _ _) => mu /= _ [in_mu Dinj Daut]. by rewrite Dy => /(_ _ (Dinj _))->; rewrite -Daut Dinj. pose le_nu (x : algC) n := (pickle x < n)%N. have max3 x1 x2 x3: exists n, [/\ le_nu x1 n, le_nu x2 n & le_nu x3 n]. exists (maxn (pickle x1) (maxn (pickle x2) (pickle x3))).+1. by apply/and3P; rewrite /le_nu !ltnS -!geq_max. have nua : additive nu. move=> x1 x2; have [n] := max3 (x1 - x2) x1 x2. case=> /mem_ext[y Dx] /mem_ext[y1 Dx1] /mem_ext[y2 Dx2]. rewrite -Dx nu_inj; rewrite -Dx1 -Dx2 -rmorphB in Dx. by rewrite (fmorph_inj _ Dx) !rmorphB -!nu_inj Dx1 Dx2. have num : multiplicative nu. split=> [x1 x2|]; last by rewrite -(rmorph1 QsC) (nu_inj 0) !rmorph1. have [n] := max3 (x1 * x2) x1 x2. case=> /mem_ext[y Dx] /mem_ext[y1 Dx1] /mem_ext[y2 Dx2]. rewrite -Dx nu_inj; rewrite -Dx1 -Dx2 -rmorphM in Dx. by rewrite (fmorph_inj _ Dx) !rmorphM /= -!nu_inj Dx1 Dx2. pose nuaM := GRing.isAdditive.Build _ _ nu nua. pose numM := GRing.isMultiplicative.Build _ _ nu num. pose nuRM : {rmorphism _ -> _} := HB.pack nu nuaM numM. by exists nuRM => x; rewrite /= (nu_inj 0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)