proposition: Lemma cyclic_pgroup_Aut_structure gT p (G : {group gT}) : p.-group G -> cyclic G -> G :!=: 1 -> let q := #|G| in let n := (logn p q).-1 in let A := Aut G in let P := 'O_p(A) in let F := 'O_p^'(A) in exists m : {perm gT} -> 'Z_q, [/\ [/\ {in A & G, forall a x, x ^+ m a = a x}, m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}}, {in A &, injective m} /\ image m A =i GRing.unit, forall k, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}} & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}], [/\ abelian A, cyclic F, #|F| = p.-1 & [faithful F, on 'Ohm_1(G) | [Aut G]]] & if n == 0 then A = F else exists t, [/\ t \in A, #[t] = 2, m t = (- 1)%R & if odd p then [/\ cyclic A /\ cyclic P, exists s, [/\ s \in A, #[s] = (p ^ n)%N, m s = p.+1%:R & P = <[s]>] & exists s0, [/\ s0 \in A, #[s0] = p, m s0 = (p ^ n).+1%:R & 'Ohm_1(P) = <[s0]>]] else if n == 1%N then A = <[t]> else exists s, [/\ s \in A, #[s] = (2 ^ n.-1)%N, m s = 5%:R, <[s]> \x <[t]> = A & exists s0, [/\ s0 \in A, #[s0] = 2, m s0 = (2 ^ n).+1%:R, m (s0 * t) = (2 ^ n).-1%:R & 'Ohm_1(<[s]>) = <[s0]>]]]].
proof: Proof. move=> pG cycG ntG q n0 A P F; have [p_pr p_dvd_G [n oG]] := pgroup_pdiv pG ntG. have [x0 defG] := cyclicP cycG; have Gx0: x0 \in G by rewrite defG cycle_id. rewrite {1}/q oG pfactorK //= in n0 *; rewrite {}/n0. have [p_gt1 min_p] := primeP p_pr; have p_gt0 := ltnW p_gt1. have q_gt1: q > 1 by rewrite cardG_gt1. have cAA: abelian A := Aut_cyclic_abelian cycG; have nilA := abelian_nil cAA. have oA: #|A| = (p.-1 * p ^ n)%N. by rewrite card_Aut_cyclic // oG totient_pfactor. have [sylP hallF]: p.-Sylow(A) P /\ p^'.-Hall(A) F. by rewrite !nilpotent_pcore_Hall. have [defPF tiPF]: P * F = A /\ P :&: F = 1. by case/dprodP: (nilpotent_pcoreC p nilA). have oP: #|P| = (p ^ n)%N. by rewrite (card_Hall sylP) oA p_part logn_Gauss ?coprimenP ?pfactorK. have oF: #|F| = p.-1. apply/eqP; rewrite -(@eqn_pmul2l #|P|) ?cardG_gt0 // -TI_cardMg // defPF. by rewrite oA oP mulnC. have [m' [inj_m' defA def_m']]: exists m' : {morphism units_Zp q >-> {perm gT}}, [/\ 'injm m', m' @* setT = A & {in G, forall x u, m' u x = x ^+ val u}]. - rewrite /A /q defG; exists (Zp_unit_morphism x0). by have [->]:= isomP (Zp_unit_isom x0); split=> // y Gy u; rewrite permE Gy. pose m (a : {perm gT}) : 'Z_q := val (invm inj_m' a). have{def_m'} def_m: {in A & G, forall a x, x ^+ m a = a x}. by move=> a x Aa Gx /=; rewrite -{2}[a](invmK inj_m') ?defA ?def_m'. have m1: m 1 = 1%R by rewrite /m morph1. have mM: {in A &, {morph m : a b / a * b >-> (a * b)%R}}. by move=> a b Aa Ab; rewrite /m morphM ?defA. have mX k: {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}. by elim: k => // k IHk a Aa; rewrite expgS exprS mM ?groupX ?IHk. have inj_m: {in A &, injective m}. apply: can_in_inj (fun u => m' (insubd (1 : {unit 'Z_q}) u)) _ => a Aa. by rewrite valKd invmK ?defA. have{defA} im_m: image m A =i GRing.unit. move=> u; apply/imageP/idP=> [[a Aa ->]| Uu]; first exact: valP. exists (m' (Sub u Uu)) => /=; first by rewrite -defA mem_morphim ?inE. by rewrite /m invmE ?inE. have mV: {in A, {morph m : a / a^-1 >-> (a^-1)%R}}. move=> a Aa /=; rewrite -div1r; apply: canRL (mulrK (valP _)) _. by rewrite -mM ?groupV ?mulVg. have inv_m (u : 'Z_q) : coprime q u -> {a | a \in A & m a = u}. rewrite -?unitZpE // natr_Zp -im_m => m_u. by exists (iinv m_u); [apply: mem_iinv | rewrite f_iinv]. have [cycF ffulF]: cyclic F /\ [faithful F, on 'Ohm_1(G) | [Aut G]]. have Um0 a: ((m a)%:R : 'F_p) \in GRing.unit. have: m a \in GRing.unit by apply: valP. by rewrite -{1}[m a]natr_Zp unitFpE ?unitZpE // {1}/q oG coprime_pexpl. pose fm0 a := FinRing.unit 'F_p (Um0 a). have natZqp u: (u%:R : 'Z_q)%:R = u %:R :> 'F_p. by rewrite val_Zp_nat // -Fp_nat_mod // modn_dvdm ?Fp_nat_mod. have m0M: {in A &, {morph fm0 : a b / a * b}}. move=> a b Aa Ab; apply: val_inj; rewrite /= -natrM mM //. by rewrite -[(_ * _)%R]Zp_nat natZqp. pose m0 : {morphism A >-> {unit 'F_p}} := Morphism m0M. have im_m0: m0 @* A = [set: {unit 'F_p}]. apply/setP=> [[/= u Uu]]; rewrite in_setT morphimEdom; apply/imsetP. have [|a Aa m_a] := inv_m u%:R. by rewrite {1}[q]oG coprime_pexpl // -unitFpE // natZqp natr_Zp. by exists a => //; apply: val_inj; rewrite /= m_a natZqp natr_Zp. have [x1 defG1]: exists x1, 'Ohm_1(G) = <[x1]>. by apply/cyclicP; apply: cyclicS (Ohm_sub _ _) cycG. have ox1: #[x1] = p by rewrite orderE -defG1 (Ohm1_cyclic_pgroup_prime _ pG). have Gx1: x1 \in G by rewrite -cycle_subG -defG1 Ohm_sub. have ker_m0: 'ker m0 = 'C('Ohm_1(G) | [Aut G]). apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => Aa. rewrite 3!inE /= -2!val_eqE /= val_Fp_nat // [1 %% _]modn_small // defG1. apply/idP/subsetP=> [ma1 x1i | ma1]. case/cycleP=> i ->{x1i}; rewrite inE gactX // -[_ a]def_m //. by rewrite -(expg_mod_order x1) ox1 (eqP ma1). have:= ma1 x1 (cycle_id x1); rewrite inE -[_ a]def_m //. by rewrite (eq_expg_mod_order x1 _ 1) ox1 (modn_small p_gt1). have card_units_Fp: #|[set: {unit 'F_p}]| = p.-1. by rewrite card_units_Zp // pdiv_id // (@totient_pfactor p 1) ?muln1. have ker_m0_P: 'ker m0 = P. apply: nilpotent_Hall_pcore nilA _. rewrite pHallE -(card_Hall sylP) oP subsetIl /=. rewrite -(@eqn_pmul2r #|m0 @* A|) ?cardG_gt0 //; apply/eqP. rewrite -{1}(card_isog (first_isog _)) card_quotient ?ker_norm //. by rewrite Lagrange ?subsetIl // oA im_m0 mulnC card_units_Fp. have inj_m0: 'ker_F m0 \subset [1] by rewrite setIC ker_m0_P tiPF. split; last by rewrite /faithful -ker_m0. have isogF: F \isog [set: {unit 'F_p}]. have sFA: F \subset A by apply: pcore_sub. apply/isogP; exists (restrm_morphism sFA m0); first by rewrite ker_restrm. apply/eqP; rewrite eqEcard subsetT card_injm ?ker_restrm //= oF. by rewrite card_units_Fp. rewrite (isog_cyclic isogF) pdiv_id // -ox1 (isog_cyclic (Zp_unit_isog x1)). by rewrite Aut_prime_cyclic // -orderE ox1. exists m; split=> {im_m mV}//; have [n0 | n_gt0] := posnP n. by apply/eqP; rewrite eq_sym eqEcard pcore_sub oF oA n0 muln1 /=. have [t At mt]: {t | t \in A & m t = -1}%R. apply: inv_m; rewrite /= Zp_cast // coprime_modr modn_small // subn1. by rewrite coprimenP // ltnW. have ot: #[t] = 2. apply/eqP; rewrite eqn_leq order_gt1 dvdn_leq ?order_dvdn //=. apply/eqP; move/(congr1 m); apply/eqP; rewrite mt m1 eq_sym -subr_eq0. rewrite opprK -val_eqE /= Zp_cast ?modn_small // /q oG ltnW //. by rewrite (leq_trans (_ : 2 ^ 2 <= p ^ 2)) ?leq_sqr ?leq_exp2l. by apply/eqP; apply: inj_m; rewrite ?groupX ?group1 ?mX // mt -signr_odd. exists t; split=> //. case G4: (~~ odd p && (n == 1%N)). case: (even_prime p_pr) G4 => [p2 | -> //]; rewrite p2 /=; move/eqP=> n1. rewrite n1 /=; apply/eqP; rewrite eq_sym eqEcard cycle_subG At /=. by rewrite -orderE oA ot p2 n1. pose e0 : nat := ~~ odd p. have{inv_m} [s As ms]: {s | s \in A & m s = (p ^ e0.+1).+1%:R}. apply: inv_m; rewrite val_Zp_nat // coprime_modr /q oG coprime_pexpl //. by rewrite -(@coprime_pexpl e0.+1) // coprimenS. have lt_e0_n: e0 < n. by rewrite /e0; case: (~~ _) G4 => //=; rewrite ltn_neqAle eq_sym => ->. pose s0 := s ^+ (p ^ (n - e0.+1)). have [ms0 os0]: m s0 = (p ^ n).+1%:R /\ #[s0] = p. have m_se e: exists2 k, k = 1 %[mod p] & m (s ^+ (p ^ e)) = (k * p ^ (e + e0.+1)).+1%:R. - elim: e => [|e [k k1 IHe]]; first by exists 1%N; rewrite ?mul1n. rewrite expnSr expgM mX ?groupX // {}IHe -natrX -(add1n (k * _)). rewrite expnDn -(prednK p_gt0) 2!big_ord_recl /= prednK // !exp1n bin1. rewrite bin0 muln1 mul1n mulnCA -expnS (addSn e). set f := (e + _)%N; set sum := (\sum_i _)%N. exists (sum %/ p ^ f.+2 * p + k)%N; first by rewrite modnMDl. rewrite -(addnC k) mulnDl -mulnA -expnS divnK // {}/sum. apply big_ind => [||[i _] /= _]; [exact: dvdn0 | exact: dvdn_add |]. rewrite exp1n mul1n /bump !add1n expnMn mulnCA dvdn_mull // -expnM. case: (ltnP f.+1 (f * i.+2)) => [le_f_fi|]. by rewrite dvdn_mull ?dvdn_exp2l. rewrite {1}mulnS -(addn1 f) leq_add2l {}/f addnS /e0. case: i e => [] // [] //; case odd_p: (odd p) => //= _. by rewrite bin2odd // mulnAC dvdn_mulr. have [[|d]] := m_se (n - e0.+1)%N; first by rewrite mod0n modn_small. move/eqP; rewrite -/s0 eqn_mod_dvd ?subn1 //=; case/dvdnP=> f -> {d}. rewrite subnK // mulSn -mulnA -expnS -addSn natrD natrM -oG char_Zp //. rewrite mulr0 addr0 => m_s0; split => //. have [d _] := m_se (n - e0)%N; rewrite -subnSK // expnSr expgM -/s0. rewrite addSn subnK // -oG mulrS natrM char_Zp // {d}mulr0 addr0. move/eqP; rewrite -m1 (inj_in_eq inj_m) ?group1 ?groupX // -order_dvdn. move/min_p; rewrite order_eq1; case/predU1P=> [s0_1 | ]; last by move/eqP. move/eqP: m_s0; rewrite eq_sym s0_1 m1 -subr_eq0 mulrSr addrK -val_eqE /=. have pf_gt0: p ^ _ > 0 by move=> e; rewrite expn_gt0 p_gt0. by rewrite val_Zp_nat // /q oG [_ == _]pfactor_dvdn // pfactorK ?ltnn. have os: #[s] = (p ^ (n - e0))%N. have: #[s] %| p ^ (n - e0). by rewrite order_dvdn -subnSK // expnSr expgM -order_dvdn os0. case/dvdn_pfactor=> // d; rewrite leq_eqVlt. case/predU1P=> [-> // | lt_d os]; case/idPn: (p_gt1); rewrite -os0. by rewrite order_gt1 negbK -order_dvdn os dvdn_exp2l // -ltnS -subSn. have p_s: p.-elt s by rewrite /p_elt os pnatX ?pnat_id. have defS1: 'Ohm_1(<[s]>) = <[s0]>. apply/eqP; rewrite eq_sym eqEcard cycle_subG -orderE os0. rewrite (Ohm1_cyclic_pgroup_prime _ p_s) ?cycle_cyclic ?leqnn ?cycle_eq1 //=. rewrite (OhmE _ p_s) mem_gen ?groupX //= !inE mem_cycle //. by rewrite -order_dvdn os0 ?dvdnn. by apply/eqP=> s1; rewrite -os0 /s0 s1 expg1n order1 in p_gt1. case: (even_prime p_pr) => [p2 | oddp]; last first. rewrite {+}/e0 oddp subn0 in s0 os0 ms0 os ms defS1 *. have [f defF] := cyclicP cycF; have defP: P = <[s]>. apply/eqP; rewrite eq_sym eqEcard -orderE oP os leqnn andbT. by rewrite cycle_subG (mem_normal_Hall sylP) ?pcore_normal. rewrite defP; split; last 1 [by exists s | by exists s0; rewrite ?groupX]. rewrite -defPF defP defF -cycleM ?cycle_cyclic // /order. by red; rewrite (centsP cAA) // -cycle_subG -defF pcore_sub. by rewrite -defF -defP (pnat_coprime (pcore_pgroup _ _) (pcore_pgroup _ _)). rewrite {+}/e0 p2 subn1 /= in s0 os0 ms0 os ms G4 defS1 lt_e0_n *. rewrite G4; exists s; split=> //; last first. exists s0; split; rewrite ?groupX //; apply/eqP; rewrite mM ?groupX //. rewrite ms0 mt eq_sym mulrN1 -subr_eq0 opprK -natrD -addSnnS. by rewrite prednK ?expn_gt0 // addnn -mul2n -expnS -p2 -oG char_Zp. suffices TIst: <[s]> :&: <[t]> = 1. rewrite dprodE //; last by rewrite (sub_abelian_cent2 cAA) ?cycle_subG. apply/eqP; rewrite eqEcard mulG_subG !cycle_subG As At oA. by rewrite TI_cardMg // -!orderE os ot p2 mul1n /= -expnSr prednK. rewrite setIC; apply: prime_TIg; first by rewrite -orderE ot. rewrite cycle_subG; apply/negP=> St. have: t \in <[s0]>. by rewrite -defS1 (OhmE _ p_s) mem_gen // !inE St -order_dvdn ot p2. have ->: <[s0]> = [set 1; s0]. apply/eqP; rewrite eq_sym eqEcard subUset !sub1set group1 cycle_id /=. by rewrite -orderE cards2 eq_sym -order_gt1 os0. rewrite !inE -order_eq1 ot /=; move/eqP; move/(congr1 m); move/eqP. rewrite mt ms0 eq_sym -subr_eq0 opprK -mulrSr. rewrite -val_eqE [val _]val_Zp_nat //= /q oG p2 modn_small //. by rewrite -addn3 expnS mul2n -addnn leq_add2l (ltn_exp2l 1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal)