proposition: Lemma isog_2extraspecial (gT : finGroupType) (G : {group gT}) n : #|G| = (2 ^ n.*2.+1)%N -> extraspecial G -> G \isog 'D^n \/ G \isog 'D^n.-1*Q.
proof: Proof. elim: n G => [|n IHn] G oG esG. case/negP: (extraspecial_nonabelian esG). by rewrite cyclic_abelian ?prime_cyclic ?oG. have pG: 2.-group G by rewrite /pgroup oG pnatX. have oZ:= card_center_extraspecial pG esG. have: 'Z(G) \subset 'Ohm_1(G). apply/subsetP=> z Zz; rewrite (OhmE _ pG) mem_gen //. by rewrite !inE -order_dvdn -oZ order_dvdG ?(subsetP (center_sub G)). rewrite subEproper; case/predU1P=> [defG1 | ltZG1]. have [n' n'_gt2 isoG]: exists2 n', n' > 2 & G \isog 'Q_(2 ^ n'). apply/quaternion_classP; apply/eqP. have not_cycG: ~~ cyclic G. by apply: contra (extraspecial_nonabelian esG); apply: cyclic_abelian. move: oZ; rewrite defG1; move/prime_Ohm1P; rewrite (negPf not_cycG) /=. by apply=> //; apply: contra not_cycG; move/eqP->; apply: cyclic1. have [n0 n'3]: n = 0 /\ n' = 3. have [[x y] genG _] := generators_quaternion n'_gt2 isoG. have n'3: n' = 3. have [_ [_ _ oG' _] _ _ _] := quaternion_structure n'_gt2 genG isoG. apply/eqP; rewrite -(subnKC (ltnW n'_gt2)) subn2 !eqSS -(@eqn_exp2l 2) //. by rewrite -oG' -oZ; case: esG => [[_ ->]]. by move/eqP: oG; have [-> _ _ _] := genG; rewrite n'3 eqn_exp2l //; case n. right; rewrite (isog_trans isoG) // n'3 n0 /=. case: DnQ_P => z isoZ; rewrite -im_cpair mulSGid ?sub_isog ?injm_cpair1g //. apply/setIidPl; rewrite setI_im_cpair -injm_center ?injm_cpairg1 //. by rewrite center_ncprod0. case/andP: ltZG1 => _; rewrite (OhmE _ pG) gen_subG. case/subsetPn=> x; case/LdivP=> Gx x2 notZx. have ox: #[x] = 2 by apply: nt_prime_order (group1_contra notZx). have Z'x: x \in G :\: 'Z(G) by rewrite inE notZx. have [E [R [[oE oR] [defG ziER]]]] := split1_extraspecial pG esG Z'x. case=> defZE defZR [esE Ex] esR. have isoE: E \isog 2^{1+2}. apply: isog_trans (isog_symr isog_2X1p2). case/orP: (card_isog8_extraspecial oE esE) => // isoE; case/negP: notZx. have gt32: 3 > 2 by []. have [[y z] genE _] := generators_quaternion gt32 isoE. have [_ _ [defZx _ eq_y2 _ _] _ _] := quaternion_structure gt32 genE isoE. by rewrite (eq_y2 x) // -cycle_subG -defZx defZE. rewrite oG doubleS 2!expnS divnMl ?mulKn // in oR. case: ifP esR => [_ defR | _ esR]. have ->: n = 0 by move/eqP: oR; rewrite defR oZ (eqn_exp2l 1) //; case n. left; apply: isog_trans (isog_symr (ncprod1 _)). by rewrite -defG defR -defZE cprod_center_id. have AutZin2_1p2: Aut_in (Aut 2^{1+2}) 'Z(2^{1+2}) \isog Aut 'Z(2^{1+2}). exact: Aut_extraspecial_full (pX1p2_pgroup _) (pX1p2_extraspecial _). have [isoR | isoR] := IHn R oR esR. by left; case: pX1p2S => gz isoZ; rewrite (isog_cprod_by _ defG). have n_gt0: n > 0. have pR: 2.-group R by rewrite /pgroup oR pnatX. have:= min_card_extraspecial pR esR. by rewrite oR leq_exp2l // ltnS (leq_double 1). case: DnQ_P isoR => gR isoZR /=; rewrite isog_sym; case/isogP=> fR injfR im_fR. have [injDn injQ] := (injm_cpairg1 isoZR, injm_cpair1g isoZR). pose Dn1 := cpairg1 isoZR @* 'D^n.-1; pose Q := cpair1g isoZR @* 'Q_8. have defR: fR @* Dn1 \* fR @* Q = R. rewrite cprodE ?morphim_cents ?im_cpair_cent //. by rewrite -morphimMl ?subsetT ?im_cpair. rewrite -defR cprodA in defG. have [[Dn _ defDn _] _ _] := cprodP defG; rewrite defDn in defG. have isoDn: Dn \isog 'D^n. rewrite -(prednK n_gt0); case: pX1p2S => gz isoZ. rewrite (isog_cprod_by _ defDn) //; last 1 first. by rewrite isog_sym (isog_trans _ (sub_isog _ _)) ?subsetT // sub_isog. rewrite /= -morphimIim im_fR setIA ziER; apply/setIidPl. rewrite defZE -defZR -{1}im_fR -injm_center // morphimS //. by rewrite -cpairg1_center morphimS // center_sub. right; case: DnQ_P => gz isoZ; rewrite (isog_cprod_by _ defG) //; first 1 last. - exact: Aut_extraspecial_full (pX1p2n_pgroup _ _) (pX1p2n_extraspecial _ _). - by rewrite isog_sym (isog_trans _ (sub_isog _ _)) ?subsetT // sub_isog. rewrite /= -morphimIim; case/cprodP: defDn => _ defDn cDn1E. rewrite setICA setIA -defDn -group_modr ?morphimS ?subsetT //. rewrite /= im_fR (setIC R) ziER -center_prod // defZE -defZR. rewrite mulSGid /=; last first. by rewrite -{1}im_fR -injm_center // -cpairg1_center !morphimS ?center_sub. rewrite -injm_center ?subsetT // -injmI // setI_im_cpair. by rewrite -injm_center // cpairg1_center injm_center // im_fR mulGid. 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)