proposition: Theorem quaternion_structure : n > 2 -> extremal_generators G 2 n (x, y) -> G \isog 'Q_m -> [/\ [/\ pprod X Y = G, {in G :\: X, forall t, #[t] = 4} & {in X & G :\: X, forall z t, z ^ t = z^-1}], [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r & nil_class G = n.-1], [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2, forall u, u \in G -> #[u] = 2 -> u = x ^+ r, 'Ohm_1(G) = <[x ^+ r]> /\ 'Ohm_2(G) = G & forall k, k > 0 -> 'Mho^k(G) = <[x ^+ (2 ^ k)]>], [/\ yG :|: xyG = G :\: X /\ [disjoint yG & xyG] & forall M, maximal M G = pred3 X My Mxy M] & n > 3 -> [/\ My \isog 'Q_q, Mxy \isog 'Q_q & forall U, cyclic U -> U \subset G -> #|G : U| = 2 -> U = X]].
proof: Proof. move=> n_gt2 genG isoG; have [def2q def2r ltqm ltrq] := def2qr (ltnW n_gt2). have [oG Gx ox X'y] := genG; rewrite -/m -/q -/X in oG ox X'y. case/extremal_generators_facts: genG; rewrite -/X // => pG maxX nsXG defXY nXY. have [sXG nXG]:= andP nsXG; have [Gy notXy]:= setDP X'y. have oxr: #[x ^+ r] = 2 by rewrite orderXdiv ox -def2r ?dvdn_mull ?mulnK. have ox2: #[x ^+ 2] = r by rewrite orderXdiv ox -def2r ?dvdn_mulr ?mulKn. have [[u v] [_ Gu ou U'v] [ov v2 uv]] := generators_quaternion n_gt2 isoG. have defUv: <[u]> :* v = G :\: <[u]>. apply: rcoset_index2; rewrite -?divgS ?cycle_subG //. by rewrite oG -orderE ou -def2q mulnK. have invUV: {in <[u]> & <[u]> :* v, forall z t, z ^ t = z^-1}. move=> z t; case/cycleP=> i ->; case/rcosetP=> ?; case/cycleP=> j -> ->{z t}. by rewrite conjgM {2}/conjg commuteX2 // mulKg conjXg uv expgVn. have U'2: {in <[u]> :* v, forall t, t ^+ 2 = u ^+ r}. move=> t; case/rcosetP=> z Uz ->; rewrite expgS {1}(conjgC z) -mulgA. by rewrite invUV ?rcoset_refl // mulKg -(expgS v 1) v2. have our: #[u ^+ r] = 2 by rewrite orderXdiv ou -/q -def2r ?dvdn_mull ?mulnK. have def_ur: {in G, forall t, #[t] = 2 -> t = u ^+ r}. move=> t Gt /= ot; case Ut: (t \in <[u]>); last first. move/eqP: ot; rewrite eqn_dvd order_dvdn -order_eq1 U'2 ?our //. by rewrite defUv inE Ut. have p2u: 2.-elt u by rewrite /p_elt ou pnatX. have: t \in 'Ohm_1(<[u]>). by rewrite (OhmE _ p2u) mem_gen // !inE Ut -order_dvdn ot. rewrite (Ohm_p_cycle _ p2u) ou pfactorK // subn1 -/r cycle_traject our !inE. by rewrite -order_eq1 ot /= mulg1; move/eqP. have defU: n > 3 -> {in G, forall z, #[z] = q -> <[z]> = <[u]>}. move=> n_gt3 z Gz oz; apply/eqP; rewrite eqEcard -!orderE oz cycle_subG. rewrite ou leqnn andbT; apply: contraLR n_gt3 => notUz. rewrite -(ltn_predK n_gt2) ltnS -(@ltn_exp2l 2) // -/q -oz. by rewrite (@orderXprime _ 2 2) // U'2 // defUv inE notUz. have def_xr: x ^+ r = u ^+ r by apply: def_ur; rewrite ?groupX. have X'2: {in G :\: X, forall t, t ^+ 2 = u ^+ r}. case: (ltngtP n 3) => [|n_gt3|n3 t]; first by rewrite ltnNge n_gt2. by rewrite /X defU // -defUv. case/setDP=> Gt notXt. case Ut: (t \in <[u]>); last by rewrite U'2 // defUv inE Ut. rewrite [t ^+ 2]def_ur ?groupX //. have:= order_dvdG Ut; rewrite -orderE ou /q n3 dvdn_divisors ?inE //=. rewrite order_eq1 (negbTE (group1_contra notXt)) /=. case/pred2P=> oz; last by rewrite orderXdiv oz. by rewrite [t]def_ur // -def_xr mem_cycle in notXt. have oX': {in G :\: X, forall z, #[z] = 4}. by move=> t X't /=; rewrite (@orderXprime _ 2 2) // X'2. have defZ: 'Z(G) = <[x ^+ r]>. apply/eqP; rewrite eqEcard andbC -orderE oxr -{1}(setIidPr (center_sub G)). rewrite cardG_gt1 /= meet_center_nil ?(pgroup_nil pG) //; last first. by rewrite -cardG_gt1 oG (leq_trans _ ltqm). apply/subsetP=> z; case/setIP=> Gz cGz; have [Gv _]:= setDP U'v. case Uvz: (z \in <[u]> :* v). move/eqP: (invUV _ _ (cycle_id u) Uvz). rewrite /conjg -(centP cGz) // mulKg eq_sym eq_invg_mul -(order_dvdn _ 2). by rewrite ou pfactor_dvdn // -(subnKC n_gt2). move/idPn: Uvz; rewrite defUv inE Gz andbT negbK def_xr => Uz. have p_u: 2.-elt u := mem_p_elt pG Gu. suff: z \in 'Ohm_1(<[u]>) by rewrite (Ohm_p_cycle 1 p_u) ou pfactorK // subn1. rewrite (OhmE _ p_u) mem_gen // !inE Uz /= -eq_invg_mul. by rewrite -(invUV _ v) ?rcoset_refl // /conjg (centP cGz) ?mulKg. have{invUV} invXX': {in X & G :\: X, forall z t, z ^ t = z^-1}. case: (ltngtP n 3) => [|n_gt3|n3 t z Xt]; first by rewrite ltnNge n_gt2. by rewrite /X defU // -defUv. case/setDP=> Gz notXz; rewrite /q /r n3 /= in oxr ox. suff xz: x ^ z = x^-1 by case/cycleP: Xt => i ->; rewrite conjXg xz expgVn. have: x ^ z \in X by rewrite memJ_norm ?cycle_id ?(subsetP nXG). rewrite invg_expg /X cycle_traject ox !inE /= !mulg1 -order_eq1 orderJ ox /=. case/or3P; move/eqP=> //; last by move/(congr1 order); rewrite orderJ ox oxr. move/conjg_fixP; rewrite (sameP commgP cent1P) cent1C -cent_cycle -/X => cXz. have defXz: X * <[z]> = G by rewrite (mulg_normal_maximal nsXG) ?cycle_subG. have: z \in 'Z(G) by rewrite inE Gz -defXz centM inE cXz cent_cycle cent1id. by rewrite defZ => Xr_z; rewrite (subsetP (cycleX x r)) in notXz. have nXiG k: G \subset 'N(<[x ^+ k]>). apply: char_norm_trans nXG. by rewrite cycle_subgroup_char // cycle_subG mem_cycle. have memL i: x ^+ (2 ^ i) \in 'L_i.+1(G). elim: i => // i IHi; rewrite -groupV expnSr expgM invMg. by rewrite -{2}(invXX' _ y) ?mem_cycle ?cycle_id ?mem_commg. have defG': G^`(1) = <[x ^+ 2]>. apply/eqP; rewrite eqEsubset cycle_subG (memL 1%N) ?der1_min //=. rewrite (p2group_abelian (quotient_pgroup _ pG)) ?card_quotient //=. rewrite -divgS ?cycle_subG ?groupX // oG -orderE ox2. by rewrite -def2q -def2r mulnA mulnK. have defG1: 'Mho^1(G) = <[x ^+ 2]>. apply/eqP; rewrite (MhoE _ pG) eqEsubset !gen_subG sub1set andbC. rewrite mem_gen; last exact: imset_f. apply/subsetP=> z2; case/imsetP=> z Gz ->{z2}. case Xz: (z \in X). by case/cycleP: Xz => i ->; rewrite -expgM mulnC expgM mem_cycle. rewrite (X'2 z) ?inE ?Xz // -def_xr. by rewrite /r -(subnKC n_gt2) expnS expgM mem_cycle. have defPhi: 'Phi(G) = <[x ^+ 2]>. by rewrite (Phi_joing pG) defG' defG1 (joing_idPl _). have def_tG: {in G :\: X, forall t, t ^: G = <[x ^+ 2]> :* t}. move=> t X't; have [Gt notXt] := setDP X't. have defJt: {in X, forall z, t ^ z = z ^- 2 * t}. move=> z Xz; rewrite /= invMg -mulgA (conjgC _ t). by rewrite (invXX' _ t) ?groupV ?invgK. have defGt: X * <[t]> = G by rewrite (mulg_normal_maximal nsXG) ?cycle_subG. apply/setP=> tz; apply/imsetP/rcosetP=> [[t'z] | [z]]. rewrite -defGt -normC ?cycle_subG ?(subsetP nXG) //. case/imset2P=> t' z; case/cycleP=> j -> Xz -> -> {tz t'z t'}. exists (z ^- 2); last by rewrite conjgM {2}/conjg commuteX // mulKg defJt. case/cycleP: Xz => i ->{z}. by rewrite groupV -expgM mulnC expgM mem_cycle. case/cycleP=> i -> -> {z tz}; exists (x ^- i); first by rewrite groupV groupX. by rewrite defJt ?groupV ?mem_cycle // expgVn invgK -!expgM mulnC. have defMt: {in G :\: X, forall t, <[x ^+ 2]> <*> <[t]> = <<t ^: G>>}. move=> t X't; have [Gt notXt] := setDP X't. apply/eqP; have: t \in <<t ^: G>> by rewrite mem_gen ?class_refl. rewrite def_tG // eqEsubset join_subG !cycle_subG !gen_subG => tGt. rewrite tGt -(groupMr _ tGt) mem_gen ?mem_mulg ?cycle_id ?set11 //=. by rewrite mul_subG ?joing_subl // -gen_subG joing_subr. have sMtG: {in G :\: X, forall t, <<t ^: G>> \subset G}. by move=> t; case/setDP=> Gt _; rewrite gen_subG class_subG. have oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}. move=> t X't; have [Gt notXt] := setDP X't. rewrite -defMt // -(Lagrange (joing_subl _ _)) -orderE ox2 -def2r mulnC. congr (_ * r)%N; rewrite -card_quotient /=; last first. by rewrite defMt // (subset_trans _ (nXiG 2)) ?sMtG. rewrite joingC quotientYidr ?(subset_trans _ (nXiG 2)) ?cycle_subG //. rewrite quotient_cycle ?(subsetP (nXiG 2)) //= -defPhi. rewrite -orderE (abelem_order_p (Phi_quotient_abelem pG)) ?mem_quotient //. apply: contraNneq notXt; move/coset_idr; move/implyP=> /=. by rewrite defPhi ?(subsetP (nXiG 2)) //; apply: subsetP; apply: cycleX. have maxMt: {in G :\: X, forall t, maximal <<t ^: G>> G}. move=> t X't; rewrite /= p_index_maximal -?divgS ?sMtG ?oMt //. by rewrite oG -def2q mulnK. have X'xy: x * y \in G :\: X by rewrite !inE !groupMl ?cycle_id ?notXy. have ti_yG_xyG: [disjoint yG & xyG]. apply/pred0P=> t; rewrite /= /yG /xyG !def_tG //; apply/andP=> [[yGt]]. rewrite rcoset_sym (rcoset_eqP yGt) mem_rcoset mulgK; move/order_dvdG. by rewrite -orderE ox2 ox gtnNdvd. have s_tG_X': {in G :\: X, forall t, t ^: G \subset G :\: X}. by move=> t X't /=; rewrite class_sub_norm // normsD ?normG. have defX': yG :|: xyG = G :\: X. apply/eqP; rewrite eqEcard subUset !s_tG_X' //= -(leq_add2l q) -{1}ox orderE. rewrite -/X -{1}(setIidPr sXG) cardsID oG -def2q mul2n -addnn leq_add2l. rewrite -(leq_add2r #|yG :&: xyG|) cardsUI disjoint_setI0 // cards0 addn0. by rewrite /yG /xyG !def_tG // !card_rcoset addnn -mul2n -orderE ox2 def2r. rewrite pprodE //; split=> // [|||n_gt3]. - rewrite defG'; split=> //; apply/eqP; rewrite eqn_leq. rewrite (leq_trans (nil_class_pgroup pG)); last first. by rewrite oG pfactorK // -(subnKC n_gt2). rewrite -(subnKC (ltnW n_gt2)) subn2 ltnNge. rewrite (sameP (lcn_nil_classP _ (pgroup_nil pG)) eqP). by apply/trivgPn; exists (x ^+ r); rewrite ?memL // -order_gt1 oxr. - rewrite {2}def_xr defZ; split=> //; last exact: extend_cyclic_Mho. split; apply/eqP; last first. have sX'G2: {subset G :\: X <= 'Ohm_2(G)}. move=> z X'z; have [Gz _] := setDP X'z. by rewrite (OhmE 2 pG) mem_gen // !inE Gz -order_dvdn oX'. rewrite eqEsubset Ohm_sub -{1}defXY mulG_subG !cycle_subG. by rewrite -(groupMr _ (sX'G2 y X'y)) !sX'G2. rewrite eqEsubset (OhmE 1 pG) cycle_subG gen_subG andbC. rewrite mem_gen ?inE ?groupX -?order_dvdn ?oxr //=. apply/subsetP=> t; case/setIP=> Gt; rewrite inE -order_dvdn /=. rewrite dvdn_divisors ?inE //= order_eq1. case/pred2P=> [->|]; first exact: group1. by move/def_ur=> -> //; rewrite def_xr cycle_id. - split=> //= H; apply/idP/idP=> [maxH |]; last first. by case/or3P=> /eqP->; rewrite ?maxMt. have [sHG nHG]:= andP (p_maximal_normal pG maxH). have oH: #|H| = q. apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //. by rewrite oG -mul2n. rewrite !(eq_sym (gval H)) -eq_sym !eqEcard oH -orderE ox !oMt // !leqnn. case sHX: (H \subset X) => //=; case/subsetPn: sHX => z Hz notXz. have: z \in yG :|: xyG by rewrite defX' inE notXz (subsetP sHG). rewrite !andbT !gen_subG /yG /xyG. by case/setUP=> /class_eqP <-; rewrite !class_sub_norm ?Hz ?orbT. have isoMt: {in G :\: X, forall z, <<z ^: G>> \isog 'Q_q}. have n1_gt2: n.-1 > 2 by rewrite -(subnKC n_gt3). move=> z X'z /=; rewrite isogEcard card_quaternion ?oMt // leqnn andbT. rewrite Grp_quaternion //; apply/existsP; exists (x ^+ 2, z) => /=. rewrite defMt // -/q -/r !xpair_eqE -!expgM def2r -order_dvdn ox dvdnn. rewrite -expnS prednK; last by rewrite -subn2 subn_gt0. by rewrite X'2 // def_xr !eqxx /= invXX' ?mem_cycle. rewrite !isoMt //; split=> // C; case/cyclicP=> z ->{C} sCG iCG. rewrite [X]defU // defU -?cycle_subG //. by apply: double_inj; rewrite -muln2 -iCG Lagrange // oG -mul2n. 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)