proposition: Theorem symplectic_type_group_structure gT p (G : {group gT}) : p.-group G -> (forall X : {group gT}, X \char G -> abelian X -> cyclic X) -> exists2 E : {group gT}, E :=: 1 \/ extraspecial E & exists R : {group gT}, [/\ cyclic R \/ [/\ p = 2, extremal2 R & #|R| >= 16], E \* R = G & E :&: R = 'Z(E)].
proof: Proof. move=> pG sympG; have [H [charH]] := Thompson_critical pG. have sHG := char_sub charH; have pH := pgroupS sHG pG. set U := 'Z(H) => sPhiH_U sHG_U defU; set Z := 'Ohm_1(U). have sZU: Z \subset U by rewrite Ohm_sub. have charU: U \char G := gFchar_trans _ charH. have cUU: abelian U := center_abelian H. have cycU: cyclic U by apply: sympG. have pU: p.-group U := pgroupS (char_sub charU) pG. have cHU: U \subset 'C(H) by rewrite subsetIr. have cHsHs: abelian (H / Z). rewrite sub_der1_abelian //= (OhmE _ pU) genS //= -/U. apply/subsetP=> _ /imset2P[h k Hh Hk ->]. have Uhk: [~ h, k] \in U by rewrite (subsetP sHG_U) ?mem_commg ?(subsetP sHG). rewrite inE Uhk inE -commXg; last by red; rewrite -(centsP cHU). apply/commgP; red; rewrite (centsP cHU) // (subsetP sPhiH_U) //. by rewrite (Phi_joing pH) mem_gen // inE orbC (Mho_p_elt 1) ?(mem_p_elt pH). have nsZH: Z <| H by rewrite sub_center_normal. have [K /=] := inv_quotientS nsZH (Ohm_sub 1 (H / Z)); fold Z => defKs sZK sKH. have nsZK: Z <| K := normalS sZK sKH nsZH; have [_ nZK] := andP nsZK. have abelKs: p.-abelem (K / Z) by rewrite -defKs Ohm1_abelem ?quotient_pgroup. have charK: K \char G. have charZ: Z \char H := gFchar_trans _ (center_char H). rewrite (char_trans _ charH) // (char_from_quotient nsZK) //. by rewrite -defKs Ohm_char. have cycZK: cyclic 'Z(K) by rewrite sympG ?center_abelian ?gFchar_trans. have [cKK | not_cKK] := orP (orbN (abelian K)). have defH: U = H. apply: center_idP; apply: cyclic_factor_abelian (Ohm_sub 1 _) _. rewrite /= -/Z abelian_rank1_cyclic //. have cKsKs: abelian (K / Z) by rewrite -defKs (abelianS (Ohm_sub 1 _)). have cycK: cyclic K by rewrite -(center_idP cKK). by rewrite -rank_Ohm1 defKs -abelian_rank1_cyclic ?quotient_cyclic. have scH: H \in 'SCN(G) by apply/SCN_P; rewrite defU char_normal. have [cGG | not_cGG] := orP (orbN (abelian G)). exists 1%G; [by left | exists G; rewrite cprod1g (setIidPl _) ?sub1G //]. by split; first left; rewrite ?center1 // sympG ?char_refl. have cycH: cyclic H by rewrite -{}defH. have [[p2 _ cG2]|[M [_ _ _]]] := cyclic_SCN pG scH not_cGG cycH; last first. do 2![case/setIdP] => _ abelE dimE_2 charE. have:= sympG _ charE (abelem_abelian abelE). by rewrite (abelem_cyclic abelE) (eqP dimE_2). have [n oG] := p_natP pG; rewrite p2 in oG. have [n_gt3 | n_le3] := ltnP 3 n. exists 1%G; [by left | exists G; rewrite cprod1g (setIidPl _) ?sub1G //]. by split; first right; rewrite ?center1 // oG (@leq_exp2l 2 4). have esG: extraspecial G. by apply: (p3group_extraspecial pG); rewrite // p2 oG pfactorK. exists G; [by right | exists ('Z(G))%G; rewrite cprod_center_id setIA setIid]. by split=> //; left; rewrite prime_cyclic; case: esG. have ntK: K :!=: 1 by apply: contra not_cKK => /eqP->; apply: abelian1. have [p_pr _ _] := pgroup_pdiv (pgroupS sKH pH) ntK. have p_gt1 := prime_gt1 p_pr; have p_gt0 := ltnW p_gt1. have oZ: #|Z| = p. apply: Ohm1_cyclic_pgroup_prime => //=; apply: contra ntK; move/eqP. by move/(trivg_center_pgroup pH)=> GH; rewrite -subG1 -GH. have sZ_ZK: Z \subset 'Z(K). by rewrite subsetI sZK gFsub_trans // subIset ?centS ?orbT. have sZsKs: 'Z(K) / Z \subset K / Z by rewrite quotientS ?center_sub. have [Es /= splitKs] := abelem_split_dprod abelKs sZsKs. have [_ /= defEsZs cEsZs tiEsZs] := dprodP splitKs. have sEsKs: Es \subset K / Z by rewrite -defEsZs mulG_subr. have [E defEs sZE sEK] := inv_quotientS nsZK sEsKs; rewrite /= -/Z in defEs sZE. have [nZE nZ_ZK] := (subset_trans sEK nZK, subset_trans (center_sub K) nZK). have defK: 'Z(K) * E = K. rewrite -(mulSGid sZ_ZK) -mulgA -quotientK ?mul_subG ?quotientMl //. by rewrite -defEs defEsZs quotientGK. have defZE: 'Z(E) = Z. have cEZK: 'Z(K) \subset 'C(E) by rewrite subIset // orbC centS. have cE_Z: E \subset 'C(Z) by rewrite centsC (subset_trans sZ_ZK). apply/eqP; rewrite eqEsubset andbC subsetI sZE centsC cE_Z /=. rewrite -quotient_sub1 ?subIset ?nZE //= -/Z -tiEsZs subsetI defEs. rewrite !quotientS ?center_sub //= subsetI subIset ?sEK //=. by rewrite -defK centM setSI // centsC. have sEH := subset_trans sEK sKH; have pE := pgroupS sEH pH. have esE: extraspecial E. split; last by rewrite defZE oZ. have sPhiZ: 'Phi(E) \subset Z. rewrite -quotient_sub1 ?gFsub_trans ?(quotient_Phi pE) //. rewrite subG1 (trivg_Phi (quotient_pgroup _ pE)) /= -defEs. by rewrite (abelemS sEsKs) //= -defKs Ohm1_abelem ?quotient_pgroup. have sE'Phi: E^`(1) \subset 'Phi(E) by rewrite (Phi_joing pE) joing_subl. have ntE': E^`(1) != 1. rewrite (sameP eqP commG1P) -abelianE; apply: contra not_cKK => cEE. by rewrite -defK mulGSid ?center_abelian // -(center_idP cEE) defZE. have defE': E^`(1) = Z. apply/eqP; rewrite eqEcard (subset_trans sE'Phi) //= oZ. have [_ _ [n ->]] := pgroup_pdiv (pgroupS (der_sub _ _) pE) ntE'. by rewrite (leq_exp2l 1) ?prime_gt1. by split; rewrite defZE //; apply/eqP; rewrite eqEsubset sPhiZ -defE'. have [spE _] := esE; have [defPhiE defE'] := spE. have{defE'} sEG_E': [~: E, G] \subset E^`(1). rewrite defE' defZE /Z (OhmE _ pU) commGC genS //. apply/subsetP=> _ /imset2P[g e Gg Ee ->]. have He: e \in H by rewrite (subsetP sKH) ?(subsetP sEK). have Uge: [~ g, e] \in U by rewrite (subsetP sHG_U) ?mem_commg. rewrite inE Uge inE -commgX; last by red; rewrite -(centsP cHU). have sZ_ZG: Z \subset 'Z(G). have charZ: Z \char G := gFchar_trans _ charU. have/implyP:= meet_center_nil (pgroup_nil pG) (char_normal charZ). rewrite -cardG_gt1 oZ prime_gt1 //=; apply: contraR => not_sZ_ZG. by rewrite prime_TIg ?oZ. have: e ^+ p \in 'Z(G). rewrite (subsetP sZ_ZG) // -defZE -defPhiE (Phi_joing pE) mem_gen //. by rewrite inE orbC (Mho_p_elt 1) ?(mem_p_elt pE). by case/setIP=> _ /centP cGep; apply/commgP; red; rewrite cGep. have sEG: E \subset G := subset_trans sEK (char_sub charK). set R := 'C_G(E). have{sEG_E'} defG: E \* R = G by apply: (critical_extraspecial pG). have [_ defER cRE] := cprodP defG. have defH: E \* 'C_H(E) = H by rewrite -(setIidPr sHG) setIAC (cprod_modl defG). have{defH} [_ defH cRH_E] := cprodP defH. have cRH_RH: abelian 'C_H(E). have sZ_ZRH: Z \subset 'Z('C_H(E)). rewrite subsetI -{1}defZE setSI //= (subset_trans sZU) // centsC. by rewrite subIset // centsC cHU. rewrite (cyclic_factor_abelian sZ_ZRH) //= -/Z. have defHs: Es \x ('C_H(E) / Z) = H / Z. rewrite defEs dprodE ?quotient_cents // -?quotientMl ?defH -?quotientGI //=. by rewrite setIA (setIidPl sEH) ['C_E(E)]defZE trivg_quotient. have:= Ohm_dprod 1 defHs; rewrite /= defKs (Ohm1_id (abelemS sEsKs abelKs)). rewrite dprodC; case/dprodP=> _ defEsRHs1 cRHs1Es tiRHs1Es. have sRHsHs: 'C_H(E) / Z \subset H / Z by rewrite quotientS ?subsetIl. have cRHsRHs: abelian ('C_H(E) / Z) by apply: abelianS cHsHs. have pHs: p.-group (H / Z) by rewrite quotient_pgroup. rewrite abelian_rank1_cyclic // (rank_pgroup (pgroupS sRHsHs pHs)). rewrite p_rank_abelian // -(leq_add2r (logn p #|Es|)) -lognM ?cardG_gt0 //. rewrite -TI_cardMg // defEsRHs1 /= -defEsZs TI_cardMg ?lognM ?cardG_gt0 //. by rewrite leq_add2r -abelem_cyclic ?(abelemS sZsKs) // quotient_cyclic. have{cRH_RH} defRH: 'C_H(E) = U. apply/eqP; rewrite eqEsubset andbC setIS ?centS // subsetI subsetIl /=. by rewrite -{2}defH centM subsetI subsetIr. have scUR: 'C_R(U) = U by rewrite -setIA -{1}defRH -centM defH. have sUR: U \subset R by rewrite -defRH setSI. have tiER: E :&: R = 'Z(E) by rewrite setIA (setIidPl (subset_trans sEH sHG)). have [cRR | not_cRR] := boolP (abelian R). exists E; [by right | exists [group of R]; split=> //; left]. by rewrite /= -(setIidPl (sub_abelian_cent cRR sUR)) scUR. have{} scUR: [group of U] \in 'SCN(R). by apply/SCN_P; rewrite (normalS sUR (subsetIl _ _)) // char_normal. have pR: p.-group R := pgroupS (subsetIl _ _) pG. have [R_le_3 | R_gt_3] := leqP (logn p #|R|) 3. have esR: extraspecial R := p3group_extraspecial pR not_cRR R_le_3. have esG: extraspecial G := cprod_extraspecial pG defG tiER esE esR. exists G; [by right | exists ('Z(G))%G; rewrite cprod_center_id setIA setIid]. by split=> //; left; rewrite prime_cyclic; case: esG. have [[p2 _ ext2R] | [M []]] := cyclic_SCN pR scUR not_cRR cycU. exists E; [by right | exists [group of R]; split=> //; right]. by rewrite dvdn_leq ?(@pfactor_dvdn 2 4) ?cardG_gt0 // -{2}p2. rewrite /= -/R => defM iUM modM _ _; pose N := 'C_G('Mho^1(U)). have charZN2: 'Z('Ohm_2(N)) \char G by rewrite !(gFchar_trans, subcent_char). have:= sympG _ charZN2 (center_abelian _). rewrite abelian_rank1_cyclic ?center_abelian // leqNgt; case/negP. have defN: E \* M = N. rewrite defM (cprod_modl defG) // centsC gFsub_trans //= -/U. by rewrite -defRH subsetIr. case/modular_group_classP: modM => q q_pr [n n_gt23 isoM]. have{n_gt23} n_gt2 := leq_trans (leq_addl _ _) n_gt23. have n_gt1 := ltnW n_gt2; have n_gt0 := ltnW n_gt1. have [[x y] genM modM] := generators_modular_group q_pr n_gt2 isoM. have{q_pr} defq: q = p; last rewrite {q}defq in genM modM isoM. have: p %| #|M| by rewrite -iUM dvdn_indexg. by have [-> _ _ _] := genM; rewrite Euclid_dvdX // dvdn_prime2 //; case: eqP. have [oM Mx ox X'y] := genM; have [My _] := setDP X'y; have [oy _] := modM. have [sUM sMR]: U \subset M /\ M \subset R. by rewrite defM subsetI sUR subsetIl centsC gFsub_trans. have oU1: #|'Mho^1(U)| = (p ^ n.-2)%N. have oU: #|U| = (p ^ n.-1)%N. by rewrite -(divg_indexS sUM) iUM oM -subn1 expnB. case/cyclicP: cycU pU oU => u -> p_u ou. by rewrite (Mho_p_cycle 1 p_u) -orderE (orderXexp 1 ou) subn1. have sZU1: Z \subset 'Mho^1(U). rewrite -(cardSg_cyclic cycU) ?gFsub // oZ oU1. by rewrite -(subnKC n_gt2) expnS dvdn_mulr. case/modular_group_structure: genM => // _ [defZM _ oZM] _ _. have:= n_gt2; rewrite leq_eqVlt eq_sym !xpair_eqE andbC. case: eqP => [n3 _ _ | _ /= n_gt3 defOhmM]. have eqZU1: Z = 'Mho^1(U) by apply/eqP; rewrite eqEcard sZU1 oZ oU1 n3 /=. rewrite (setIidPl _) in defM; first by rewrite -defM oM n3 pfactorK in R_gt_3. by rewrite -eqZU1 subIset ?centS ?orbT. have{defOhmM} [|defM2 _] := defOhmM 2; first by rewrite -subn1 ltn_subRL. do [set xpn3 := x ^+ _; set X2 := <[_]>] in defM2. have oX2: #|X2| = (p ^ 2)%N. by rewrite -orderE (orderXexp _ ox) -{1}(subnKC n_gt2) addSn addnK. have sZX2: Z \subset X2. have cycXp: cyclic <[x ^+ p]> := cycle_cyclic _. rewrite -(cardSg_cyclic cycXp) /=; first by rewrite oZ oX2 dvdn_mull. rewrite -defZM subsetI (subset_trans (Ohm_sub _ _)) //=. by rewrite (subset_trans sZU1) // centsC defM subsetIr. by rewrite /xpn3 -subnSK //expnS expgM cycleX. have{defM2} [_ /= defM2 cYX2 tiX2Y] := dprodP defM2. have{defN} [_ defN cME] := cprodP defN. have cEM2: E \subset 'C('Ohm_2(M)). by rewrite centsC (subset_trans _ cME) ?centS ?Ohm_sub. have [cEX2 cYE]: X2 \subset 'C(E) /\ E \subset 'C(<[y]>). by apply/andP; rewrite centsC -subsetI -centM defM2. have pN: p.-group N := pgroupS (subsetIl _ _) pG. have defN2: (E <*> X2) \x <[y]> = 'Ohm_2(N). rewrite dprodE ?centY ?subsetI 1?centsC ?cYE //=; last first. rewrite -cycle_subG in My; rewrite joingC cent_joinEl //= -/X2. rewrite -(setIidPr My) setIA -group_modl ?cycle_subG ?groupX //. by rewrite mulGSid // (subset_trans _ sZX2) // -defZE -tiER setIS. apply/eqP; rewrite cent_joinEr // -mulgA defM2 eqEsubset mulG_subG. rewrite OhmS ?andbT; last by rewrite -defN mulG_subr. have expE: exponent E %| p ^ 2 by rewrite exponent_special ?(pgroupS sEG). rewrite /= (OhmE 2 pN) sub_gen /=; last 1 first. by rewrite subsetI -defN mulG_subl sub_LdivT expE. rewrite -cent_joinEl // -genM_join genS // -defN. apply/subsetP=> _ /setIP[/imset2P[e z Ee Mz ->]]. rewrite inE expgMn; last by red; rewrite -(centsP cME). rewrite (exponentP expE) // mul1g => zp2; rewrite mem_mulg //=. by rewrite (OhmE 2 (pgroupS sMR pR)) mem_gen // !inE Mz. have{defN2} defZN2: X2 \x <[y]> = 'Z('Ohm_2(N)). rewrite -[X2](mulSGid sZX2) /= -/Z -defZE -(center_dprod defN2). do 2!rewrite -{1}(center_idP (cycle_abelian _)) -/X2; congr (_ \x _). by case/cprodP: (center_cprod (cprodEY cEX2)). have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)). by rewrite unlock /= dprodg1. rewrite -size_abelian_type ?center_abelian //. have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub. rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE. rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2. by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0). 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)