proposition: Lemma Qn_aut_exists k n : coprime k n -> {u : {rmorphism algC -> algC} | forall z, z ^+ n = 1 -> u z = z ^+ k}.
proof: Proof. have [-> /eqnP | n_gt0 co_k_n] := posnP n. by rewrite gcdn0 => ->; exists idfun. have [z prim_z] := C_prim_root_exists n_gt0. have [Qn [QnC [[|zn []] // [Dz]]] genQn] := num_field_exists [:: z]. pose phi := kHomExtend 1 \1 zn (zn ^+ k). have homQn1: kHom 1 1 (\1%VF : 'End(Qn)) by rewrite kHom1. have pzn_zk0: root (map_poly \1%VF (minPoly 1 zn)) (zn ^+ k). rewrite -(fmorph_root QnC) rmorphXn /= Dz -map_poly_comp. rewrite (@eq_map_poly _ _ _ QnC) => [|a]; last by rewrite /= id_lfunE. set p1 := map_poly _ _. have [q1 Dp1]: exists q1, p1 = pQtoC q1. have aP i: (minPoly 1 zn)`_i \in 1%VS. by apply/polyOverP; apply: minPolyOver. have{aP} a_ i := sig_eqW (vlineP _ _ (aP i)). exists (\poly_(i < size (minPoly 1 zn)) sval (a_ i)). apply/polyP=> i; rewrite coef_poly coef_map coef_poly /=. case: ifP => _; rewrite ?rmorph0 //; case: (a_ i) => a /= ->. apply: canRL (mulfK _) _; first by rewrite intr_eq0 denq_eq0. by rewrite mulrzr -rmorphMz scalerMzl -mulrzr -numqE scaler_int rmorph_int. have: root p1 z by rewrite -Dz fmorph_root root_minPoly. rewrite Dp1; have [q2 [Dq2 _] ->] := minCpolyP z. case/dvdpP=> r1 ->; rewrite rmorphM rootM /= -Dq2; apply/orP; right. rewrite (minCpoly_cyclotomic prim_z) /cyclotomic. rewrite (bigD1 (Ordinal (ltn_pmod k n_gt0))) ?coprime_modl //=. by rewrite rootM root_XsubC prim_expr_mod ?eqxx. have phim : multiplicative phi. by apply/kHom_lrmorphism; rewrite -genQn span_seq1 /= kHomExtendP. pose phimM := GRing.isMultiplicative.Build _ _ phi phim. pose phiRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun phi) phimM. have [nu Dnu] := extend_algC_subfield_aut QnC phiRM. exists nu => _ /(prim_rootP prim_z)[i ->]. rewrite rmorphXn /= exprAC -Dz -Dnu /= -{1}[zn]hornerX /phi. rewrite (kHomExtend_poly homQn1) ?polyOverX //. rewrite map_polyE map_id_in => [|?]; last by rewrite id_lfunE. by rewrite polyseqK hornerX rmorphXn. 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)