proposition: Lemma Ohm1_extraspecial_odd (gT : finGroupType) (G : {group gT}) : p.-group G -> extraspecial G -> odd #|G| -> let Y := 'Ohm_1(G) in [/\ exponent Y = p, #|G : Y| %| p & Y != G -> exists E : {group gT}, [/\ #|G : Y| = p, #|E| = p \/ extraspecial E, exists2 X : {group gT}, #|X| = p & X \x E = Y & exists M : {group gT}, [/\ M \isog 'Mod_(p ^ 3), M \* E = G & M :&: E = 'Z(M)]]].
proof: Proof. move=> pG esG oddG Y; have [spG _] := esG. have [defPhiG defG'] := spG; set Z := 'Z(G) in defPhiG defG'. have{spG} expG: exponent G %| p ^ 2 by apply: exponent_special. have p_pr := extraspecial_prime pG esG. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have oZ: #|Z| = p := card_center_extraspecial pG esG. have nsZG: Z <| G := center_normal G; have [sZG nZG] := andP nsZG. have nsYG: Y <| G := Ohm_normal 1 G; have [sYG nYG] := andP nsYG. have ntZ: Z != 1 by rewrite -cardG_gt1 oZ. have sZY: Z \subset Y. by apply: contraR ntZ => ?; rewrite -(setIidPl sZG) TI_Ohm1 ?prime_TIg ?oZ. have ntY: Y != 1 by apply: subG1_contra ntZ. have p_odd: odd p by rewrite -oZ (oddSg sZG). have expY: exponent Y %| p by rewrite exponent_Ohm1_class2 // nil_class2 defG'. rewrite (prime_nt_dvdP p_pr _ expY) -?dvdn1 -?trivg_exponent //. have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n; split. have sG1Z: 'Mho^1(G) \subset Z by rewrite -defPhiG (Phi_joing pG) joing_subr. have Z_Gp: {in G, forall x, x ^+ p \in Z}. by move=> x Gx; rewrite /= (subsetP sG1Z) ?(Mho_p_elt 1) ?(mem_p_elt pG). have{expG} oY': {in G :\: Y, forall u, #[u] = (p ^ 2)%N}. move=> u /setDP[Gu notYu]; apply/eqP. have [k ou] := p_natP (mem_p_elt pG Gu). rewrite eqn_dvd order_dvdn (exponentP expG) // eqxx ou dvdn_Pexp2l // ltnNge. apply: contra notYu => k_le_1; rewrite [Y](OhmE _ pG) mem_gen // !inE Gu /=. by rewrite -order_dvdn ou dvdn_exp2l. have isoMod3 (M : {group gT}): M \subset G -> ~~ abelian M -> ~~ (M \subset Y) -> #|M| = (p ^ 3)%N -> M \isog 'Mod_(p ^ 3). - move=> sMG not_cMM /subsetPn[u Mu notYu oM]. have pM := pgroupS sMG pG; have sUM: <[u]> \subset M by rewrite cycle_subG. have Y'u: u \in G :\: Y by rewrite inE notYu (subsetP sMG). have iUM: #|M : <[u]>| = p by rewrite -divgS // oM expnS -(oY' u) ?mulnK. have cM := maximal_cycle_extremal pM not_cMM (cycle_cyclic u) sUM iUM. rewrite (sameP eqP (prime_oddPn p_pr)) p_odd orbF in cM. rewrite /extremal_class oM pdiv_pfactor // pfactorK //= in cM. by do 3!case: ifP => // _ in cM. have iYG: #|G : Y| = p. have [V maxV sYV]: {V : {group gT} | maximal V G & Y \subset V}. by apply: maxgroup_exists; rewrite properEneq neYG. have [sVG [u Gu notVu]] := properP (maxgroupp maxV). without loss [v Vv notYv]: / exists2 v, v \in V & v \notin Y. have [->| ] := eqVneq Y V; first by rewrite (p_maximal_index pG). by rewrite eqEsubset sYV => not_sVY; apply; apply/subsetPn. pose U := <[u]> <*> <[v]>; have Gv := subsetP sVG v Vv. have sUG: U \subset G by rewrite join_subG !cycle_subG Gu. have Uu: u \in U by rewrite -cycle_subG joing_subl. have Uv: v \in U by rewrite -cycle_subG joing_subr. have not_sUY: ~~ (U \subset Y) by apply/subsetPn; exists v. have sU1U: 'Ohm_1(U) \subset U := Ohm_sub 1 _. have sU1Y: 'Ohm_1(U) \subset Y := OhmS 1 sUG. suffices defUV: U :&: V = 'Ohm_1(U). by rewrite (subsetP sU1Y) // -defUV inE Uv in notYv. suffices iU1U: #|U : 'Ohm_1(U)| = p. have: maximal 'Ohm_1(U) U by rewrite p_index_maximal ?Ohm_sub ?iU1U. case/maxgroupP=> _; apply; rewrite /= -/U. by apply/properP; split; last exists u; rewrite ?subsetIl ?inE ?Uu. by rewrite subsetI Ohm_sub (subset_trans sU1Y). apply/prime_nt_dvdP=> //. by apply: contra not_sUY; rewrite /U; move/eqP; move/(index1g sU1U)=> <-. have ov: #[v] = (p ^ 2)%N by rewrite oY' // inE notYv. have sZv: Z \subset <[v]>. suffices defZ: <[v ^+ p]> == Z by rewrite -(eqP defZ) cycleX. by rewrite eqEcard cycle_subG Z_Gp //= oZ -orderE (orderXexp 1 ov). have nvG: G \subset 'N(<[v]>) by rewrite sub_der1_norm ?cycle_subG // defG'. have [cUU | not_cUU] := orP (orbN (abelian U)). rewrite -divgS ?Ohm_sub // -(mul_card_Ohm_Mho_abelian 1 cUU) /= -/U. by rewrite mulKn ?cardG_gt0 //= -oZ cardSg ?(subset_trans (MhoS 1 sUG)). have oU: #|U| = (p ^ 3)%N. have nvu := subsetP nvG u Gu; have nvU := subset_trans sUG nvG. rewrite -(Lagrange (joing_subr _ _)) -orderE ov mulnC; congr (_ * _)%N. rewrite -card_quotient //= quotientYidr ?cycle_subG //=. rewrite quotient_cycle // -orderE; apply: nt_prime_order => //. by rewrite -morphX //= coset_id // (subsetP sZv) // Z_Gp. have svV: <[v]> \subset V by rewrite cycle_subG. by apply: contra notVu; move/eqP=> v_u; rewrite (subsetP svV) // coset_idr. have isoU := isoMod3 _ sUG not_cUU not_sUY oU; rewrite /= -/U in isoU. have [//|[x y] genU modU] := generators_modular_group p_pr _ isoU. case/modular_group_structure: genU => // _ _ _ _. case: eqP (p_odd) => [[-> //] | _ _]; case/(_ 1%N)=> // _ oU1. by rewrite -divgS // oU oU1 mulnK // muln_gt0 p_gt0. have iC1U (U : {group gT}) x: U \subset G -> x \in G :\: 'C(U) -> #|U : 'C_U[x]| = p. - move=> sUG /setDP[Gx not_cUx]; apply/prime_nt_dvdP=> //. apply: contra not_cUx; rewrite -sub_cent1 => /eqP sUCx. by rewrite -(index1g _ sUCx) ?subsetIl ?subsetIr. rewrite -(@dvdn_pmul2l (#|U| * #|'C_G[x]|)) ?muln_gt0 ?cardG_gt0 //. have maxCx: maximal 'C_G[x] G. rewrite cent1_extraspecial_maximal //; apply: contra not_cUx. by rewrite inE Gx; apply: subsetP (centS sUG) _. rewrite {1}mul_cardG setIA (setIidPl sUG) -(p_maximal_index pG maxCx) -!mulnA. rewrite !Lagrange ?subsetIl // mulnC dvdn_pmul2l //. have [sCxG nCxG] := andP (p_maximal_normal pG maxCx). by rewrite -norm_joinEl ?cardSg ?join_subG ?(subset_trans sUG). have oCG (U : {group gT}): Z \subset U -> U \subset G -> #|'C_G(U)| = (p * #|G : U|)%N. - have [m] := ubnP #|U|; elim: m U => // m IHm U leUm sZU sUG. have [<- | neZU] := eqVneq Z U. by rewrite -oZ Lagrange // (setIidPl _) // centsC subsetIr. have{neZU} [x Gx not_cUx]: exists2 x, x \in G & x \notin 'C(U). by apply/subsetPn; rewrite eqEsubset sZU subsetI sUG centsC in neZU. pose W := 'C_U[x]; have iWU: #|U : W| = p by rewrite iC1U // inE not_cUx. have maxW: maximal W U by rewrite p_index_maximal ?subsetIl ?iWU. have ltWU: W \proper U by apply: maxgroupp maxW. have [sWU [u Uu notWu]] := properP ltWU. have defU: W * <[u]> = U. have nsWU: W <| U := p_maximal_normal (pgroupS sUG pG) maxW. by rewrite (mulg_normal_maximal nsWU) ?cycle_subG. have sWG := subset_trans sWU sUG. have sZW: Z \subset W. by rewrite subsetI sZU -cent_set1 subIset ?centS ?orbT ?sub1set. have iCW_CU: #|'C_G(W) : 'C_G(U)| = p. rewrite -defU centM cent_cycle setIA /= -/W. rewrite iC1U ?subsetIl ?setIS ?centS // inE andbC (subsetP sUG) //=. rewrite -sub_cent1; apply/subsetPn; exists x. by rewrite inE Gx -sub_cent1 subsetIr. by rewrite -defU centM cent_cycle inE -sub_cent1 subsetIr in not_cUx. apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU Lagrange ?setIS ?centS //. rewrite IHm ?(leq_trans (proper_card ltWU)) //= -/W. by rewrite -(Lagrange_index sUG sWU) iWU mulnA. have oCY: #|'C_G(Y)| = (p ^ 2)%N by rewrite oCG // iYG. have [x cYx notZx]: exists2 x, x \in 'C_G(Y) & x \notin Z. apply/subsetPn; rewrite proper_subn // properEcard setIS ?centS //=. by rewrite oZ oCY (ltn_exp2l 1 2). have{cYx} [Gx cYx] := setIP cYx; have nZx := subsetP nZG x Gx. have defCx: 'C_G[x] = Y. apply/eqP; rewrite eq_sym eqEcard subsetI sYG sub_cent1 cYx /=. rewrite -(leq_pmul2r p_gt0) -{2}iYG -(iC1U G x) ?Lagrange ?subsetIl //. by rewrite !inE Gx ?andbT in notZx *. have Yx: x \in Y by rewrite -defCx inE Gx cent1id. have ox: #[x] = p. by apply: nt_prime_order; rewrite ?(exponentP expY) // (group1_contra notZx). have defCy: 'C_G(Y) = Z * <[x]>. apply/eqP; rewrite eq_sym eqEcard mulG_subG setIS ?centS //=. rewrite cycle_subG inE Gx cYx oCY TI_cardMg ?oZ -?orderE ?ox //=. by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. have abelYt: p.-abelem (Y / Z). by rewrite (abelemS (quotientS _ sYG)) //= -/Z -defPhiG Phi_quotient_abelem. have Yxt: coset Z x \in Y / Z by rewrite mem_quotient. have{Yxt} [Et [sEtYt oEt defYt]] := p_abelem_split1 abelYt Yxt. have nsZY: Z <| Y := normalS sZY sYG nsZG. have [E defEt sZE sEY] := inv_quotientS nsZY sEtYt. have{defYt} [_ defYt _ tiXEt] := dprodP defYt. have defY: <[x]> \x E = Y. have nZX: <[x]> \subset 'N(Z) by rewrite cycle_subG. have TIxE: <[x]> :&: E = 1. rewrite prime_TIg -?orderE ?ox // -(quotientSGK _ sZE) ?quotient_cycle //. rewrite (sameP setIidPl eqP) eq_sym -defEt tiXEt -quotient_cycle //. by rewrite -subG1 quotient_sub1 // cycle_subG. rewrite dprodE //; last 1 first. by rewrite cent_cycle (subset_trans sEY) //= -/Y -defCx subsetIr. rewrite -[Y](quotientGK nsZY) -defYt cosetpreM -quotient_cycle //. rewrite quotientK // -(normC nZX) defEt quotientGK ?(normalS _ sEY) //. by rewrite -mulgA (mulSGid sZE). have sEG := subset_trans sEY sYG; have nZE := subset_trans sEG nZG. have defZE: 'Z(E) = Z. apply/eqP; rewrite eqEsubset andbC subsetI sZE subIset ?centS ?orbT //. rewrite -quotient_sub1 ?subIset ?nZE //= -tiXEt defEt subsetI andbC. rewrite quotientS ?center_sub //= -quotient_cycle //. rewrite -(quotientMidl _ <[x]>) /= -defCy quotientS // /Y. by case/dprodP: defY => _ <- _ _; rewrite centM setIA cent_cycle defCx setSI. have pE := pgroupS sEG pG. rewrite iYG; split=> // _; exists E. split=> //; first 2 [by exists [group of <[x]>]]. have:= sZE; rewrite subEproper; case/predU1P=> [<- | ltZE]; [by left | right]. split; rewrite /special defZE ?oZ // (Phi_joing pE). have defE': E^`(1) = Z. have sE'Z: E^`(1) \subset Z by rewrite -defG' dergS. apply/eqP; rewrite eqEcard sE'Z -(prime_nt_dvdP _ _ (cardSg sE'Z)) ?oZ //=. rewrite -trivg_card1 (sameP eqP commG1P). by rewrite /proper sZE /= -/Z -defZE subsetI subxx in ltZE. split=> //; rewrite -defE'; apply/joing_idPl. by rewrite /= defE' -defPhiG (Phi_joing pG) joingC sub_gen ?subsetU ?MhoS. have iEG: #|G : E| = (p ^ 2)%N. apply/eqP; rewrite -(@eqn_pmul2l #|E|) // Lagrange // -(Lagrange sYG) iYG. by rewrite -(dprod_card defY) -mulnA mulnCA -orderE ox. pose M := 'C_G(E); exists [group of M] => /=. have sMG: M \subset G := subsetIl _ _; have pM: p.-group M := pgroupS sMG pG. have sZM: Z \subset M by rewrite setIS ?centS. have oM: #|M| = (p ^ 3)%N by rewrite oCG ?iEG. have defME: M * E = G. apply/eqP; rewrite eqEcard mulG_subG sMG sEG /= -(leq_pmul2r p_gt0). rewrite -{2}oZ -defZE /('Z(E)) -{2}(setIidPr sEG) setIAC -mul_cardG /= -/M. by rewrite -(Lagrange sEG) mulnAC -mulnA mulnC iEG oM. have defZM: 'Z(M) = Z. apply/eqP; rewrite eqEsubset andbC subsetI sZM subIset ?centS ?orbT //=. by rewrite /Z /('Z(G)) -{2}defME centM setIA setIAC. rewrite cprodE 1?centsC ?subsetIr //. rewrite defME setIAC (setIidPr sEG) defZM isoMod3 //. rewrite abelianE (sameP setIidPl eqP) eqEcard subsetIl /= -/('Z(M)) -/M. by rewrite defZM oZ oM (leq_exp2l 3 1). by apply: contra neYG => sMY; rewrite eqEsubset sYG -defME mulG_subG sMY. Qed.
imports: 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 finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)