proposition: Lemma modular_group_structure gT (G : {group gT}) x y : extremal_generators G p n (x, y) -> G \isog 'Mod_m -> modular_group_generators (x, y) -> let X := <[x]> in [/\ [/\ X ><| <[y]> = G, ~~ abelian G & {in X, forall z j, z ^ (y ^+ j) = z ^+ (j * r).+1}], [/\ 'Z(G) = <[x ^+ p]>, 'Phi(G) = 'Z(G) & #|'Z(G)| = r], [/\ G^`(1) = <[x ^+ r]>, #|G^`(1)| = p & nil_class G = 2], forall k, k > 0 -> 'Mho^k(G) = <[x ^+ (p ^ k)]> & if (p, n) == (2, 3) then 'Ohm_1(G) = G else forall k, 0 < k < n.-1 -> <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G) /\ #|'Ohm_k(G)| = (p ^ k.+1)%N].
proof: Proof. move=> genG isoG [oy xy] X. have [oG Gx ox /setDP[Gy notXy]] := genG; rewrite -/m -/q in ox oG. have [pG _ nsXG defXY nXY] := extremal_generators_facts p_pr genG. have [sXG nXG] := andP nsXG; have sYG: <[y]> \subset G by rewrite cycle_subG. have n1_gt1: n.-1 > 1 by [rewrite def_n]; have n1_gt0 := ltnW n1_gt1. have def_n1 := prednK n1_gt0. have def_m: (q * p)%N = m by rewrite -expnSr /m def_n. have notcxy: y \notin 'C[x]. apply: contraL (introT eqP xy); move/cent1P=> cxy. rewrite /conjg -cxy // eq_mulVg1 expgS !mulKg -order_dvdn ox. by rewrite pfactor_dvdn ?expn_gt0 ?p_gt0 // pfactorK // -ltnNge prednK. have tiXY: <[x]> :&: <[y]> = 1. rewrite setIC prime_TIg -?orderE ?oy //; apply: contra notcxy. by rewrite cycle_subG; apply: subsetP; rewrite cycle_subG cent1id. have notcGG: ~~ abelian G. by rewrite -defXY abelianM !cycle_abelian cent_cycle cycle_subG. have cXpY: <[y]> \subset 'C(<[x ^+ p]>). rewrite cent_cycle cycle_subG cent1C (sameP cent1P commgP) /commg conjXg xy. by rewrite -expgM mulSn expgD mulKg -expnSr def_n1 -/q -ox expg_order. have oxp: #[x ^+ p] = r by rewrite orderXdiv ox ?dvdn_exp //. have [sZG nZG] := andP (center_normal G). have defZ: 'Z(G) = <[x ^+ p]>. apply/eqP; rewrite eq_sym eqEcard subsetI -{2}defXY centM subsetI cent_cycle. rewrite 2!cycle_subG !groupX ?cent1id //= centsC cXpY /= -orderE oxp leqNgt. apply: contra notcGG => gtZr; apply: cyclic_center_factor_abelian. rewrite (dvdn_prime_cyclic p_pr) // card_quotient //. rewrite -(dvdn_pmul2l (cardG_gt0 'Z(G))) Lagrange // oG -def_m dvdn_pmul2r //. case/p_natP: (pgroupS sZG pG) gtZr => k ->. by rewrite ltn_exp2l // def_n1; apply: dvdn_exp2l. have Zxr: x ^+ r \in 'Z(G) by rewrite /r def_n expnS expgM defZ mem_cycle. have rxy: [~ x, y] = x ^+ r by rewrite /commg xy expgS mulKg. have defG': G^`(1) = <[x ^+ r]>. case/setIP: Zxr => _; rewrite -rxy -defXY -(norm_joinEr nXY). exact: der1_joing_cycles. have oG': #|G^`(1)| = p. by rewrite defG' -orderE orderXdiv ox /q -def_n1 ?dvdn_exp2l // expnS mulnK. have sG'Z: G^`(1) \subset 'Z(G) by rewrite defG' cycle_subG. have nil2_G: nil_class G = 2. by apply/eqP; rewrite eqn_leq andbC ltnNge nil_class1 notcGG nil_class2. have XYp: {in X & <[y]>, forall z t, (z * t) ^+ p \in z ^+ p *: <[x ^+ r ^+ 'C(p, 2)]>}. - move=> z t Xz Yt; have Gz := subsetP sXG z Xz; have Gt := subsetP sYG t Yt. have Rtz: [~ t, z] \in G^`(1) by apply: mem_commg. have cGtz: [~ t, z] \in 'C(G) by case/setIP: (subsetP sG'Z _ Rtz). rewrite expMg_Rmul /commute ?(centP cGtz) //. have ->: t ^+ p = 1 by apply/eqP; rewrite -order_dvdn -oy order_dvdG. rewrite defG' in Rtz; case/cycleP: Rtz => i ->. by rewrite mem_lcoset mulg1 mulKg expgAC mem_cycle. have defMho: 'Mho^1(G) = <[x ^+ p]>. apply/eqP; rewrite eqEsubset cycle_subG (Mho_p_elt 1) ?(mem_p_elt pG) //. rewrite andbT (MhoE 1 pG) gen_subG -defXY; apply/subsetP=> ztp. case/imsetP=> zt; case/imset2P=> z t Xz Yt -> -> {zt ztp}. apply: subsetP (XYp z t Xz Yt); case/cycleP: Xz => i ->. by rewrite expgAC mul_subG ?sub1set ?mem_cycle //= -defZ cycle_subG groupX. split=> //; try exact: extend_cyclic_Mho. - rewrite sdprodE //; split=> // z; case/cycleP=> i ->{z} j. rewrite conjXg -expgM mulnC expgM actX; congr (_ ^+ i). elim: j {i} => //= j ->; rewrite conjXg xy -!expgM mulnS mulSn addSn. rewrite addnA -mulSn -addSn expgD mulnCA (mulnC j). rewrite {3}/r def_n expnS mulnA -expnSr def_n1 -/q -ox -mulnA expgM. by rewrite expg_order expg1n mulg1. - by rewrite (Phi_joing pG) defMho -defZ (joing_idPr _) ?defZ. have G1y: y \in 'Ohm_1(G). by rewrite (OhmE _ pG) mem_gen // !inE Gy -order_dvdn oy /=. case: eqP => [[p2 n3] | notG8 k]; last case/andP=> k_gt0 lt_k_n1. apply/eqP; rewrite eqEsubset Ohm_sub -{1}defXY mulG_subG !cycle_subG. rewrite G1y -(groupMr _ G1y) /= (OhmE _ pG) mem_gen // !inE groupM //. rewrite /q /r p2 n3 in oy ox xy *. by rewrite expgS -mulgA -{1}(invg2id oy) -conjgE xy -expgS -order_dvdn ox. have le_k_n2: k <= n.-2 by rewrite -def_n1 in lt_k_n1. suffices{lt_k_n1} defGk: <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G). split=> //; case/dprodP: defGk => _ <- _ tiXkY; rewrite expnSr TI_cardMg //. rewrite -!orderE oy (subnDA 1) subn1 orderXdiv ox ?dvdn_exp2l ?leq_subr //. by rewrite /q -{1}(subnK (ltnW lt_k_n1)) expnD mulKn // expn_gt0 p_gt0. suffices{k k_gt0 le_k_n2} defGn2: <[x ^+ p]> \x <[y]> = 'Ohm_(n.-2)(G). have:= Ohm_dprod k defGn2; have p_xp := mem_p_elt pG (groupX p Gx). rewrite (Ohm_p_cycle _ p_xp) (Ohm_p_cycle _ (mem_p_elt pG Gy)) oxp oy. rewrite pfactorK ?(pfactorK 1) // (eqnP k_gt0) expg1 -expgM -expnS. rewrite -subSn // -subSS def_n1 def_n => -> /=; rewrite subnSK // subn2. by apply/eqP; rewrite eqEsubset OhmS ?Ohm_sub //= -{1}Ohm_id OhmS ?Ohm_leq. rewrite dprodEY //=; last by apply/trivgP; rewrite -tiXY setSI ?cycleX. apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= [in y \in _]def_n. rewrite (subsetP (Ohm_leq G (ltn0Sn _)) y) //= (OhmE _ pG) -/r. rewrite mem_gen /=; last by rewrite !inE -order_dvdn oxp groupX /=. rewrite gen_subG /= cent_joinEr // -defXY; apply/subsetP=> uv; case/setIP. case/imset2P=> u v Xu Yv ->{uv}; rewrite /r inE def_n expnS expgM. case/lcosetP: (XYp u v Xu Yv) => _ /cycleP[j ->] ->. case/cycleP: Xu => i ->{u}; rewrite -!(expgM, expgD) -order_dvdn ox. rewrite (mulnC r) /r {1}def_n expnSr mulnA -mulnDl -mulnA -expnS. rewrite subnSK // subn2 /q -def_n1 expnS dvdn_pmul2r // dvdn_addl. by case/dvdnP=> k ->; rewrite mulnC expgM mem_mulg ?mem_cycle. case: (ltngtP n 3) => [|n_gt3|n3]; first by rewrite ltnNge n_gt2. by rewrite -subnSK // expnSr mulnA dvdn_mull. case: (even_prime p_pr) notG8 => [-> | oddp _]; first by rewrite n3. by rewrite bin2odd // -!mulnA dvdn_mulr. 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)