proposition: Lemma make_pi_cfAut a k : coprime k a -> exists2 u : {rmorphism algC -> algC}, forall (gT0 : finGroupType) (G0 : {group gT0}) chi x, chi \in 'Z[irr G0] -> #[x] %| a -> cfAut u chi x = chi (x ^+ k)%g & forall chi x, chi \in 'Z[irr G] -> coprime #[x] a -> cfAut u chi x = chi x.
proof: Proof. move=> co_k_a; have [v Dv] := Qn_aut_exists co_k_a. have [u Du_a Du_a'] := dvd_restrict_cfAut a v. exists u => [gt0 G0 | ] chi x Zchi a_x; last by rewrite cfunE/= Du_a'. rewrite cfunE/= {u Du_a'}Du_a //. without loss{Zchi} Nchi: chi / chi \is a character. move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]]. by rewrite !cfunE rmorphB !IH. have [sXG0 | G0'x] := boolP (<[x]> \subset G0); last first. have /(<[x]> =P _) gen_xk: generator <[x]> (x ^+ k). by rewrite generator_coprime coprime_sym (coprime_dvdr a_x). by rewrite !cfun0 ?rmorph0 -?cycle_subG -?gen_xk. rewrite -!(cfResE chi sXG0) ?cycle_id ?mem_cycle //. rewrite ['Res _]cfun_sum_cfdot !sum_cfunE rmorph_sum; apply: eq_bigr => i _. have chiX := lin_charX (char_abelianP _ (cycle_abelian x) i) _ (cycle_id x). rewrite !cfunE/= rmorphM/= aut_Cnat ?Cnat_cfdot_char_irr ?cfRes_char //. by congr (_ * _); rewrite Dv -chiX // -expg_mod_order (eqnP a_x) chiX. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)