proposition: Lemma cyclic_SCN gT p (G U : {group gT}) : p.-group G -> U \in 'SCN(G) -> ~~ abelian G -> cyclic U -> [/\ p = 2, #|G : U| = 2 & extremal2 G] \/ exists M : {group gT}, [/\ M :=: 'C_G('Mho^1(U)), #|M : U| = p, extremal_class M = ModularGroup, 'Ohm_1(M)%G \in 'E_p^2(G) & 'Ohm_1(M) \char G].
proof: Proof. move=> pG /SCN_P[nsUG scUG] not_cGG cycU; have [sUG nUG] := andP nsUG. have [cUU pU] := (cyclic_abelian cycU, pgroupS sUG pG). have ltUG: ~~ (G \subset U). by apply: contra not_cGG => sGU; apply: abelianS cUU. have ntU: U :!=: 1. by apply: contraNneq ltUG => U1; rewrite -scUG subsetIidl U1 cents1. have [p_pr _ [n oU]] := pgroup_pdiv pU ntU. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have [u defU] := cyclicP cycU; have Uu: u \in U by rewrite defU cycle_id. have Gu := subsetP sUG u Uu; have p_u := mem_p_elt pG Gu. have defU1: 'Mho^1(U) = <[u ^+ p]> by rewrite defU (Mho_p_cycle _ p_u). have modM1 (M : {group gT}): [/\ U \subset M, #|M : U| = p & extremal_class M = ModularGroup] -> M :=: 'C_M('Mho^1(U)) /\ 'Ohm_1(M)%G \in 'E_p^2(M). - case=> sUM iUM /modular_group_classP[q q_pr {n oU}[n n_gt23 isoM]]. have n_gt2: n > 2 by apply: leq_trans (leq_addl _ _) n_gt23. have def_n: n = (n - 3).+3 by rewrite -{1}(subnKC n_gt2). have oM: #|M| = (q ^ n)%N by rewrite (card_isog isoM) card_modular_group. have pM: q.-group M by rewrite /pgroup oM pnatX pnat_id. have def_q: q = p; last rewrite {q q_pr}def_q in oM pM isoM n_gt23. by apply/eqP; rewrite eq_sym [p == q](pgroupP pM) // -iUM dvdn_indexg. have [[x y] genM modM] := generators_modular_group p_pr n_gt2 isoM. case/modular_group_structure: genM => // _ [defZ _ oZ] _ defMho. have ->: 'Mho^1(U) = 'Z(M). apply/eqP; rewrite eqEcard oZ defZ -(defMho 1%N) ?MhoS //= defU1 -orderE. suff ou: #[u] = (p * p ^ n.-2)%N by rewrite orderXdiv ou ?dvdn_mulr ?mulKn. by rewrite orderE -defU -(divg_indexS sUM) iUM oM def_n mulKn. case: eqP => [[p2 n3] | _ defOhm]; first by rewrite p2 n3 in n_gt23. have{defOhm} [|defM1 oM1] := defOhm 1%N; first by rewrite def_n. split; rewrite ?(setIidPl _) //; first by rewrite centsC subsetIr. rewrite inE oM1 pfactorK // andbT inE Ohm_sub abelem_Ohm1 //. exact: (card_p2group_abelian p_pr oM1). have ou: #[u] = (p ^ n.+1)%N by rewrite defU in oU. pose Gs := G / U; have pGs: p.-group Gs by rewrite quotient_pgroup. have ntGs: Gs != 1 by rewrite -subG1 quotient_sub1. have [_ _ [[|k] oGs]] := pgroup_pdiv pGs ntGs. have iUG: #|G : U| = p by rewrite -card_quotient ?oGs. case: (predU1P (maximal_cycle_extremal _ _ _ _ iUG)) => // [modG | ext2G]. by right; exists G; case: (modM1 G) => // <- ->; rewrite Ohm_char. by left; case: eqP ext2G => // <-. pose M := 'C_G('Mho^1(U)); right; exists [group of M]. have sMG: M \subset G by apply: subsetIl. have [pM nUM] := (pgroupS sMG pG, subset_trans sMG nUG). have sUM: U \subset M by rewrite subsetI sUG sub_abelian_cent ?Mho_sub. pose A := Aut U; have cAA: abelian A by rewrite Aut_cyclic_abelian. have sylAp: p.-Sylow(A) 'O_p(A) by rewrite nilpotent_pcore_Hall ?abelian_nil. have [f [injf sfGsA fG]]: exists f : {morphism Gs >-> {perm gT}}, [/\ 'injm f, f @* Gs \subset A & {in G, forall y, f (coset U y) u = u ^ y}]. - have [] := first_isom_loc [morphism of conj_aut U] nUG. rewrite ker_conj_aut scUG /= -/Gs => f injf im_f. exists f; rewrite im_f ?Aut_conj_aut //. split=> // y Gy; have nUy := subsetP nUG y Gy. suffices ->: f (coset U y) = conj_aut U y by rewrite norm_conj_autE. by apply: set1_inj; rewrite -!morphim_set1 ?mem_quotient // im_f ?sub1set. have cGsGs: abelian Gs by rewrite -(injm_abelian injf) // (abelianS sfGsA). have p_fGs: p.-group (f @* Gs) by rewrite morphim_pgroup. have sfGsAp: f @* Gs \subset 'O_p(A) by rewrite (sub_Hall_pcore sylAp). have [a [fGa oa au n_gt01 cycGs]]: exists a, [/\ a \in f @* Gs, #[a] = p, a u = u ^+ (p ^ n).+1, (p == 2) + 1 <= n & cyclic Gs \/ p = 2 /\ (exists2 c, c \in f @* Gs & c u = u^-1)]. - have [m [[def_m _ _ _ _] _]] := cyclic_pgroup_Aut_structure pU cycU ntU. have ->: logn p #|U| = n.+1 by rewrite oU pfactorK. rewrite /= -/A; case: posnP => [_ defA | n_gt0 [c [Ac oc m_c defA]]]. have:= cardSg sfGsAp; rewrite (card_Hall sylAp) /= -/A defA card_injm //. by rewrite oGs (part_p'nat (pcore_pgroup _ _)) pfactor_dvdn // logn1. have [p2 | odd_p] := even_prime p_pr; last first. case: eqP => [-> // | _] in odd_p *; rewrite odd_p in defA. have [[cycA _] _ [a [Aa oa m_a defA1]]] := defA. exists a; rewrite -def_m // oa m_a expg_znat //. split=> //; last by left; rewrite -(injm_cyclic injf) ?(cyclicS sfGsA). have: f @* Gs != 1 by rewrite morphim_injm_eq1. rewrite -cycle_subG; apply: contraR => not_sfGs_a. by rewrite -(setIidPl sfGsAp) TI_Ohm1 // defA1 setIC prime_TIg -?orderE ?oa. do [rewrite {1}p2 /= eqn_leq n_gt0; case: leqP => /= [_ | n_gt1]] in defA. have:= cardSg sfGsAp; rewrite (card_Hall sylAp) /= -/A defA -orderE oc p2. by rewrite card_injm // oGs p2 pfactor_dvdn // p_part. have{defA} [s [As os _ defA [a [Aa oa m_a _ defA1]]]] := defA; exists a. have fGs_a: a \in f @* Gs. suffices: f @* Gs :&: <[s]> != 1. apply: contraR => not_fGs_a; rewrite TI_Ohm1 // defA1 setIC. by rewrite prime_TIg -?orderE ?oa // cycle_subG. have: (f @* Gs) * <[s]> \subset A by rewrite mulG_subG cycle_subG sfGsA. move/subset_leq_card; apply: contraL; move/eqP; move/TI_cardMg->. rewrite -(dprod_card defA) -ltnNge mulnC -!orderE ltn_pmul2r // oc. by rewrite card_injm // oGs p2 (ltn_exp2l 1). rewrite -def_m // oa m_a expg_znat // p2; split=> //. rewrite abelian_rank1_cyclic // (rank_pgroup pGs) //. rewrite -(injm_p_rank injf) // p_rank_abelian 1?morphim_abelian //= p2 -/Gs. case: leqP => [|fGs1_gt1]; [by left | right]. split=> //; exists c; last by rewrite -def_m // m_c expg_zneg. have{} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U). by rewrite -(Ohm_dprod 1 defA) defA1 (@Ohm_p_cycle 1 _ 2) /p_elt oc. have def_fGs1: 'Ohm_1(f @* Gs) = 'Ohm_1(A). apply/eqP; rewrite eqEcard OhmS // -(dprod_card defA1) -!orderE oa oc. by rewrite dvdn_leq ?(@pfactor_dvdn 2 2) ?cardG_gt0. rewrite (subsetP (Ohm_sub 1 _)) // def_fGs1 -cycle_subG. by case/dprodP: defA1 => _ <- _ _; rewrite mulG_subr. have n_gt0: n > 0 := leq_trans (leq_addl _ _) n_gt01. have [ys Gys _ def_a] := morphimP fGa. have oys: #[ys] = p by rewrite -(order_injm injf) // -def_a oa. have defMs: M / U = <[ys]>. apply/eqP; rewrite eq_sym eqEcard -orderE oys cycle_subG; apply/andP; split. have [y nUy Gy /= def_ys] := morphimP Gys. rewrite def_ys mem_quotient //= inE Gy defU1 cent_cycle cent1C. rewrite (sameP cent1P commgP) commgEl conjXg -fG //= -def_ys -def_a au. by rewrite -expgM mulSn expgD mulKg -expnSr -ou expg_order. rewrite card_quotient // -(setIidPr sUM) -scUG setIA (setIidPl sMG). rewrite defU cent_cycle index_cent1 -(card_imset _ (mulgI u^-1)) -imset_comp. have <-: #|'Ohm_1(U)| = p. rewrite defU (Ohm_p_cycle 1 p_u) -orderE (orderXexp _ ou) ou pfactorK //. by rewrite subKn. rewrite (OhmE 1 pU) subset_leq_card ?sub_gen //. apply/subsetP=> _ /imsetP[z /setIP[/(subsetP nUG) nUz cU1z] ->]. have Uv' := groupVr Uu; have Uuz: u ^ z \in U by rewrite memJ_norm. rewrite !inE groupM // expgMn /commute 1?(centsP cUU u^-1) //= expgVn -conjXg. by rewrite (sameP commgP cent1P) cent1C -cent_cycle -defU1. have iUM: #|M : U| = p by rewrite -card_quotient ?defMs. have not_cMM: ~~ abelian M. apply: contraL p_pr => cMM; rewrite -iUM -indexgI /= -/M. by rewrite (setIidPl _) ?indexgg // -scUG subsetI sMG sub_abelian_cent. have modM: extremal_class M = ModularGroup. have sU1Z: 'Mho^1(U) \subset 'Z(M). by rewrite subsetI gFsub_trans // centsC subsetIr. have /maximal_cycle_extremal/predU1P[] //= := iUM; rewrite -/M. case/andP=> /eqP-p2 ext2M; rewrite p2 add1n in n_gt01. suffices{sU1Z}: #|'Z(M)| = 2. move/eqP; rewrite eqn_leq leqNgt (leq_trans _ (subset_leq_card sU1Z)) //. by rewrite defU1 -orderE (orderXexp 1 ou) subn1 p2 (ltn_exp2l 1). move: ext2M; rewrite /extremal2 !inE orbC -orbA; case/or3P; move/eqP. - case/semidihedral_classP=> m m_gt3 isoM. have [[x z] genM [oz _]] := generators_semidihedral m_gt3 isoM. by case/semidihedral_structure: genM => // _ _ []. - case/quaternion_classP=> m m_gt2 isoM. have [[x z] genM _] := generators_quaternion m_gt2 isoM. by case/quaternion_structure: genM => // _ _ []. case/dihedral_classP=> m m_gt1 isoM. have [[x z] genM _] := generators_2dihedral m_gt1 isoM. case/dihedral2_structure: genM not_cMM => // _ _ _ _. by case: (m == 2) => [|[]//]; move/abelem_abelian->. split=> //. have [//|_] := modM1 [group of M]; rewrite !inE -andbA /=. by case/andP=> /subset_trans->. have{cycGs} [cycGs | [p2 [c fGs_c u_c]]] := cycGs. suffices ->: 'Ohm_1(M) = 'Ohm_1(G) by apply: Ohm_char. suffices sG1M: 'Ohm_1(G) \subset M. by apply/eqP; rewrite eqEsubset -{2}(Ohm_id 1 G) !OhmS. rewrite -(quotientSGK _ sUM) ?(subset_trans (Ohm_sub _ G)) //= defMs. suffices ->: <[ys]> = 'Ohm_1(Gs) by rewrite morphim_Ohm. apply/eqP; rewrite eqEcard -orderE cycle_subG /= {1}(OhmE 1 pGs) /=. rewrite mem_gen ?inE ?Gys -?order_dvdn oys //=. rewrite -(part_pnat_id (pgroupS (Ohm_sub _ _) pGs)) p_part (leq_exp2l _ 1) //. by rewrite -p_rank_abelian -?rank_pgroup -?abelian_rank1_cyclic. suffices charU1: 'Mho^1(U) \char G^`(1). by rewrite gFchar_trans // subcent_char ?(char_trans charU1) ?gFchar. suffices sUiG': 'Mho^1(U) \subset G^`(1). have /cyclicP[zs cycG']: cyclic G^`(1) by rewrite (cyclicS _ cycU) ?der1_min. by rewrite cycG' in sUiG' *; apply: cycle_subgroup_char. rewrite defU1 cycle_subG p2 -groupV invMg -{2}u_c. by have [_ _ /morphimP[z _ Gz ->] ->] := morphimP fGs_c; rewrite fG ?mem_commg. 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)