proposition: Lemma maximal_cycle_extremal gT p (G X : {group gT}) : p.-group G -> ~~ abelian G -> cyclic X -> X \subset G -> #|G : X| = p -> (extremal_class G == ModularGroup) || (p == 2) && extremal2 G.
proof: Proof. move=> pG not_cGG cycX sXG iXG; rewrite /extremal2; set cG := extremal_class G. have [|p_pr _ _] := pgroup_pdiv pG. by case: eqP not_cGG => // ->; rewrite abelian1. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have [n oG] := p_natP pG; have n_gt2: n > 2. apply: contraR not_cGG; rewrite -leqNgt => n_le2. by rewrite (p2group_abelian pG) // oG pfactorK. have def_n := subnKC n_gt2; have n_gt1 := ltnW n_gt2; have n_gt0 := ltnW n_gt1. pose q := (p ^ n.-1)%N; pose r := (p ^ n.-2)%N. have q_gt1: q > 1 by rewrite (ltn_exp2l 0) // -(subnKC n_gt2). have r_gt0: r > 0 by rewrite expn_gt0 p_gt0. have def_pr: (p * r)%N = q by rewrite /q /r -def_n. have oX: #|X| = q by rewrite -(divg_indexS sXG) oG iXG /q -def_n mulKn. have ntX: X :!=: 1 by rewrite -cardG_gt1 oX. have maxX: maximal X G by rewrite p_index_maximal ?iXG. have nsXG: X <| G := p_maximal_normal pG maxX; have [_ nXG] := andP nsXG. have cXX: abelian X := cyclic_abelian cycX. have scXG: 'C_G(X) = X. apply/eqP; rewrite eqEsubset subsetI sXG -abelianE cXX !andbT. apply: contraR not_cGG; case/subsetPn=> y; case/setIP=> Gy cXy notXy. rewrite -!cycle_subG in Gy notXy; rewrite -(mulg_normal_maximal nsXG _ Gy) //. by rewrite abelianM cycle_abelian cyclic_abelian ?cycle_subG. have [x defX] := cyclicP cycX; have pX := pgroupS sXG pG. have Xx: x \in X by [rewrite defX cycle_id]; have Gx := subsetP sXG x Xx. have [ox p_x]: #[x] = q /\ p.-elt x by rewrite defX in pX oX. pose Z := <[x ^+ r]>. have defZ: Z = 'Ohm_1(X) by rewrite defX (Ohm_p_cycle _ p_x) ox subn1 pfactorK. have oZ: #|Z| = p by rewrite -orderE orderXdiv ox -def_pr ?dvdn_mull ?mulnK. have cGZ: Z \subset 'C(G). have nsZG: Z <| G by rewrite defZ gFnormal_trans. move/implyP: (meet_center_nil (pgroup_nil pG) nsZG). rewrite -cardG_gt1 oZ p_gt1 setIA (setIidPl (normal_sub nsZG)). by apply: contraR; move/prime_TIg=> -> //; rewrite oZ. have X_Gp y: y \in G -> y ^+ p \in X. move=> Gy; have nXy: y \in 'N(X) := subsetP nXG y Gy. rewrite coset_idr ?groupX // morphX //; apply/eqP. by rewrite -order_dvdn -iXG -card_quotient // order_dvdG ?mem_quotient. have [y X'y]: exists2 y, y \in G :\: X & (p == 2) + 3 <= n /\ x ^ y = x ^+ r.+1 \/ p = 2 /\ x * x ^ y \in Z. - have [y Gy notXy]: exists2 y, y \in G & y \notin X. by apply/subsetPn; rewrite proper_subn ?(maxgroupp maxX). have nXy: y \in 'N(X) := subsetP nXG y Gy; pose ay := conj_aut X y. have oay: #[ay] = p. apply: nt_prime_order => //. by rewrite -morphX // mker // ker_conj_aut (subsetP cXX) ?X_Gp. rewrite (sameP eqP (kerP _ nXy)) ker_conj_aut. by apply: contra notXy => cXy; rewrite -scXG inE Gy. have [m []]:= cyclic_pgroup_Aut_structure pX cycX ntX. set Ap := 'O_p(_); case=> def_m [m1 _] [m_inj _] _ _ _. have sylAp: p.-Sylow(Aut X) Ap. by rewrite nilpotent_pcore_Hall // abelian_nil // Aut_cyclic_abelian. have Ap1ay: ay \in 'Ohm_1(Ap). rewrite (OhmE _ (pcore_pgroup _ _)) mem_gen // !inE -order_dvdn oay dvdnn. rewrite (mem_normal_Hall sylAp) ?pcore_normal ?Aut_aut //. by rewrite /p_elt oay pnat_id. rewrite {1}oX pfactorK // -{1}def_n /=. have [p2 | odd_p] := even_prime p_pr; last first. rewrite (sameP eqP (prime_oddPn p_pr)) odd_p n_gt2. case=> _ [_ _ _] [_ _ [s [As os m_s defAp1]]]. have [j def_s]: exists j, s = ay ^+ j. apply/cycleP; rewrite -cycle_subG subEproper eq_sym eqEcard -!orderE. by rewrite -defAp1 cycle_subG Ap1ay oay os leqnn . exists (y ^+ j); last first. left; rewrite -(norm_conj_autE _ Xx) ?groupX // morphX // -def_s. by rewrite -def_m // m_s expg_znat // oX pfactorK ?eqxx. rewrite -scXG !inE groupX //= andbT -ker_conj_aut !inE morphX // -def_s. rewrite andbC -(inj_in_eq m_inj) ?group1 // m_s m1 oX pfactorK // -/r. rewrite mulrSr -subr_eq0 addrK -val_eqE /= val_Zp_nat //. by rewrite [_ == 0]dvdn_Pexp2l // -def_n ltnn. rewrite {1}p2 /= => [[t [At ot m_t]]]; rewrite {1}oX pfactorK // -{1}def_n. rewrite eqSS subn_eq0 => defA; exists y; rewrite ?inE ?notXy //. rewrite p2 -(norm_conj_autE _ Xx) //= -/ay -def_m ?Aut_aut //. case Tay: (ay \in <[t]>). rewrite cycle2g // !inE -order_eq1 oay p2 /= in Tay. by right; rewrite (eqP Tay) m_t expg_zneg // mulgV group1. case: leqP defA => [_ defA|le3n [a [Aa _ _ defA [s [As os m_s m_st defA1]]]]]. by rewrite -defA Aut_aut in Tay. have: ay \in [set s; s * t]. have: ay \in 'Ohm_1(Aut X) := subsetP (OhmS 1 (pcore_sub _ _)) ay Ap1ay. case/dprodP: (Ohm_dprod 1 defA) => _ <- _ _. rewrite defA1 (@Ohm_p_cycle _ _ 2) /p_elt ot //= expg1 cycle2g //. by rewrite mulUg mul1g inE Tay cycle2g // mulgU mulg1 mulg_set1. case/set2P=> ->; [left | right]. by rewrite ?le3n m_s expg_znat // oX pfactorK // -p2. by rewrite m_st expg_znat // oX pfactorK // -p2 -/r -expgS prednK ?cycle_id. have [Gy notXy] := setDP X'y; have nXy := subsetP nXG y Gy. have defG j: <[x]> <*> <[x ^+ j * y]> = G. rewrite -defX -genM_join. by rewrite (mulg_normal_maximal nsXG) ?cycle_subG ?groupMl ?groupX ?genGid. have[i def_yp]: exists i, y ^- p = x ^+ i. by apply/cycleP; rewrite -defX groupV X_Gp. have p_i: p %| i. apply: contraR notXy; rewrite -prime_coprime // => co_p_j. have genX: generator X (y ^- p). by rewrite def_yp defX generator_coprime ox coprimeXl. rewrite -scXG (setIidPl _) // centsC ((X :=P: _) genX) cycle_subG groupV. rewrite /= -(defG 0) mul1g centY inE -defX (subsetP cXX) ?X_Gp //. by rewrite (subsetP (cycle_abelian y)) ?mem_cycle. case=> [[n_gt23 xy] | [p2 Z_xxy]]. suffices ->: cG = ModularGroup by []; apply/modular_group_classP. exists p => //; exists n => //; rewrite isogEcard card_modular_group //. rewrite oG leqnn andbT Grp_modular_group // -/q -/r. have{i def_yp p_i} [i def_yp]: exists i, y ^- p = x ^+ i ^+ p. by case/dvdnP: p_i => j def_i; exists j; rewrite -expgM -def_i. have Zyx: [~ y, x] \in Z. by rewrite -groupV invg_comm commgEl xy expgS mulKg cycle_id. have def_yxj j: [~ y, x ^+ j] = [~ y, x] ^+ j. by rewrite commgX /commute ?(centsP cGZ _ Zyx). have Zyxj j: [~ y, x ^+ j] \in Z by rewrite def_yxj groupX. have x_xjy j: x ^ (x ^+ j * y) = x ^+ r.+1. by rewrite conjgM {2}/conjg commuteX //= mulKg. have [cyxi | not_cyxi] := eqVneq ([~ y, x ^+ i] ^+ 'C(p, 2)) 1. apply/existsP; exists (x, x ^+ i * y); rewrite /= !xpair_eqE. rewrite defG x_xjy -order_dvdn ox dvdnn !eqxx andbT /=. rewrite expMg_Rmul /commute ?(centsP cGZ _ (Zyxj _)) ?groupX // cyxi. by rewrite -def_yp -mulgA mulKg. have [p2 | odd_p] := even_prime p_pr; last first. by rewrite -order_dvdn bin2odd ?dvdn_mulr // -oZ order_dvdG in not_cyxi. have def_yxi: [~ y, x ^+ i] = x ^+ r. have:= Zyxj i; rewrite /Z cycle_traject orderE oZ p2 !inE mulg1. by case/pred2P=> // cyxi; rewrite cyxi p2 eqxx in not_cyxi. apply/existsP; exists (x, x ^+ (i + r %/ 2) * y); rewrite /= !xpair_eqE. rewrite defG x_xjy -order_dvdn ox dvdnn !eqxx andbT /=. rewrite expMg_Rmul /commute ?(centsP cGZ _ (Zyxj _)) ?groupX // def_yxj. rewrite -expgM mulnDl addnC !expgD (expgM x i) -def_yp mulgKV. rewrite -def_yxj def_yxi p2 mulgA -expgD in n_gt23 *. rewrite -expg_mod_order ox /q /r p2 -(subnKC n_gt23) mulnC !expnS mulKn //. rewrite addnn -mul2n modnn mul1g -order_dvdn dvdn_mulr //. by rewrite -p2 -oZ order_dvdG. have{i def_yp p_i} Zy2: y ^+ 2 \in Z. rewrite defZ (OhmE _ pX) -groupV -p2 def_yp mem_gen // !inE groupX //= p2. rewrite expgS -{2}def_yp -(mulKg y y) -conjgE -conjXg -conjVg def_yp conjXg. rewrite -expgMn //; last by apply: (centsP cXX); rewrite ?memJ_norm. by rewrite -order_dvdn (dvdn_trans (order_dvdG Z_xxy)) ?oZ. rewrite !cycle_traject !orderE oZ p2 !inE !mulg1 /= in Z_xxy Zy2 *. rewrite -eq_invg_mul eq_sym -[r]prednK // expgS (inj_eq (mulgI _)) in Z_xxy. case/pred2P: Z_xxy => xy; last first. suffices ->: cG = SemiDihedral by []; apply/semidihedral_classP. have n_gt3: n > 3. case: ltngtP notXy => // [|n3]; first by rewrite ltnNge n_gt2. rewrite -scXG inE Gy defX cent_cycle; case/cent1P; red. by rewrite (conjgC x) xy /r p2 -n3. exists n => //; rewrite isogEcard card_semidihedral // oG p2 leqnn andbT. rewrite Grp_semidihedral //; apply/existsP=> /=. case/pred2P: Zy2 => y2; [exists (x, y) | exists (x, x * y)]. by rewrite /= -{1}[y]mul1g (defG 0) y2 xy -p2 -/q -ox expg_order. rewrite /= (defG 1%N) conjgM {2}/conjg mulKg -p2 -/q -ox expg_order -xy. rewrite !xpair_eqE !eqxx /= andbT p2 expgS {2}(conjgC x) xy mulgA -(mulgA x). rewrite [y * y]y2 -expgS -expgD addSnnS prednK // addnn -mul2n -p2 def_pr. by rewrite -ox expg_order. case/pred2P: Zy2 => y2. suffices ->: cG = Dihedral by []; apply/dihedral_classP. exists n => //; rewrite isogEcard card_2dihedral // oG p2 leqnn andbT. rewrite Grp_2dihedral //; apply/existsP; exists (x, y) => /=. by rewrite /= -{1}[y]mul1g (defG 0) y2 xy -p2 -/q -ox expg_order. suffices ->: cG = Quaternion by []; apply/quaternion_classP. exists n => //; rewrite isogEcard card_quaternion // oG p2 leqnn andbT. rewrite Grp_quaternion //; apply/existsP; exists (x, y) => /=. by rewrite /= -{1}[y]mul1g (defG 0) y2 xy -p2 -/q -ox expg_order. 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)