proposition: Theorem semidihedral_structure : n > 3 -> extremal_generators G 2 n (x, y) -> G \isog 'SD_m -> #[y] = 2 -> [/\ [/\ X ><| Y = G, #[x * y] = 4 & {in X & G :\: X, forall z t, z ^ t = z ^+ r.-1}], [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r & nil_class G = n.-1], [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2, 'Ohm_1(G) = My /\ 'Ohm_2(G) = G & forall k, k > 0 -> 'Mho^k(G) = <[x ^+ (2 ^ k)]>], [/\ yG :|: xyG = G :\: X /\ [disjoint yG & xyG] & forall H, maximal H G = pred3 X My Mxy H] & [/\ My \isog 'D_q, Mxy \isog 'Q_q & forall U, cyclic U -> U \subset G -> #|G : U| = 2 -> U = X]].
proof: Proof. move=> n_gt3 genG isoG oy. have [def2q def2r ltqm ltrq] := def2qr (ltnW (ltnW n_gt3)). 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 ox2: #[x ^+ 2] = r by rewrite orderXdiv ox -def2r ?dvdn_mulr ?mulKn. have oxr: #[x ^+ r] = 2 by rewrite orderXdiv ox -def2r ?dvdn_mull ?mulnK. have [[u v] [_ Gu ou U'v] [ov uv]] := generators_semidihedral n_gt3 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 ^+ r.-1}. move=> z t; case/cycleP=> i ->; case/rcosetP=> ?; case/cycleP=> j -> ->{z t}. by rewrite conjgM {2}/conjg commuteX2 // mulKg conjXg uv -!expgM mulnC. have [vV yV]: v^-1 = v /\ y^-1 = y by rewrite !invg_expg ov oy. have defU: {in G, forall z, #[z] = q -> <[z]> = <[u]>}. move=> z Gz /= oz; apply/eqP; rewrite eqEcard -!orderE oz ou leqnn andbT. apply: contraLR (n_gt3) => notUz; rewrite -leqNgt -(ltn_predK n_gt3) ltnS. rewrite -(@dvdn_Pexp2l 2) // -/q -{}oz order_dvdn expgM (expgS z). have{Gz notUz} [z' Uz' ->{z}]: exists2 z', z' \in <[u]> & z = z' * v. by apply/rcosetP; rewrite defUv inE -cycle_subG notUz Gz. rewrite {2}(conjgC z') invUV ?rcoset_refl // mulgA -{2}vV mulgK -expgS. by rewrite prednK // -expgM mulnC def2r -order_dvdn /q -ou order_dvdG. have{invUV} invXX': {in X & G :\: X, forall z t, z ^ t = z ^+ r.-1}. by rewrite /X defU -?defUv. have xy2: (x * y) ^+ 2 = x ^+ r. rewrite expgS {2}(conjgC x) invXX' ?cycle_id // mulgA -{2}yV mulgK -expgS. by rewrite prednK. have oxy: #[x * y] = 4 by rewrite (@orderXprime _ 2 2) ?xy2. have r_gt2: r > 2 by rewrite (ltn_exp2l 1) // -(subnKC n_gt3). have coXr1: coprime #[x] (2 ^ (n - 3)).-1. rewrite ox coprimeXl // -(@coprime_pexpl (n - 3)) ?coprimenP ?subn_gt0 //. by rewrite expn_gt0. have def2r1: (2 * (2 ^ (n - 3)).-1).+1 = r.-1. rewrite -!subn1 mulnBr -expnS [_.+1]subnSK ?(ltn_exp2l 0) //. by rewrite /r -(subnKC n_gt3). 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 /setIP[Gz cGz]. case X'z: (z \in G :\: X). move/eqP: (invXX' _ _ (cycle_id x) X'z). rewrite /conjg -(centP cGz) // mulKg -def2r1 eq_mulVg1 expgS mulKg mulnC. rewrite -order_dvdn Gauss_dvdr // order_dvdn -order_eq1. by rewrite ox2 -(subnKC r_gt2). move/idPn: X'z; rewrite inE Gz andbT negbK => Xz. have:= Ohm_p_cycle 1 (mem_p_elt pG Gx); rewrite ox pfactorK // subn1 => <-. rewrite (OhmE _ (mem_p_elt pG Gx)) mem_gen // !inE Xz /=. rewrite -(expgK coXr1 Xz) -!expgM mulnCA -order_dvdn dvdn_mull //. rewrite mulnC order_dvdn -(inj_eq (mulgI z)) -expgS mulg1 def2r1. by rewrite -(invXX' z y) // /conjg (centP cGz) ?mulKg. 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 -(expgK coXr1 (mem_cycle _ _)) groupX //. rewrite -expgM expnSr -mulnA expgM -(mulKg (x ^+ (2 ^ i)) (_ ^+ _)). by rewrite -expgS def2r1 -(invXX' _ y) ?mem_cycle ?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. have{Xz Gz} [xi Xxi ->{z}]: exists2 xi, xi \in X & z = xi * y. have Uvy: y \in <[u]> :* v by rewrite defUv -(defU x). apply/rcosetP; rewrite /X defU // (rcoset_eqP Uvy) defUv. by rewrite inE -(defU x) ?Xz. rewrite expn1 expgS {2}(conjgC xi) -{2}[y]/(y ^+ 2.-1) -{1}oy -invg_expg. rewrite mulgA mulgK invXX' // -expgS prednK // /r -(subnKC n_gt3) expnS. by case/cycleP: Xxi => i ->; rewrite -expgM mulnCA 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 ^+ r.-2 * t}. move=> z Xz /=; rewrite -(mulKg z (z ^+ _)) -expgS -subn2. have X'tV: t^-1 \in G :\: X by rewrite inE !groupV notXt. by rewrite subnSK 1?ltnW // subn1 -(invXX' _ t^-1) // -mulgA -conjgCV. 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 -> -> {t' t'z tz}. exists (z ^+ r.-2); last first. by rewrite conjgM {2}/conjg commuteX // mulKg defJt. case/cycleP: Xz => i ->{z}. by rewrite -def2r1 -expgM mulnCA expgM mem_cycle. case/cycleP=> i -> -> {z tz}. exists (x ^+ (i * expg_invn X (2 ^ (n - 3)).-1)); first by rewrite groupX. rewrite defJt ?mem_cycle // -def2r1 -!expgM. by rewrite mulnAC mulnA mulnC muln2 !expgM expgK ?mem_cycle. 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 -orderE. rewrite (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. split. - by rewrite sdprodE // setIC prime_TIg ?cycle_subG // -orderE oy. - rewrite defG'; split=> //. apply/eqP; rewrite eqn_leq (leq_trans (nil_class_pgroup pG)); last first. by rewrite oG pfactorK // -(subnKC n_gt3). rewrite -(subnKC (ltnW (ltnW n_gt3))) subn2 ltnNge. rewrite (sameP (lcn_nil_classP _ (pgroup_nil pG)) eqP). by apply/trivgPn; exists (x ^+ r); rewrite ?memL // -order_gt1 oxr. - rewrite defZ; split=> //; last exact: extend_cyclic_Mho. split; apply/eqP; last first. have sX'G2: {subset G :\: X <= 'Ohm_2(G)}. move=> t X't; have [Gt _] := setDP X't; rewrite -defX' in X't. rewrite (OhmE 2 pG) mem_gen // !inE Gt -order_dvdn. by case/setUP: X't; case/imsetP=> z _ ->; rewrite orderJ ?oy ?oxy. rewrite eqEsubset Ohm_sub -{1}defXY mulG_subG !cycle_subG. by rewrite -(groupMr _ (sX'G2 y X'y)) !sX'G2. rewrite eqEsubset andbC gen_subG class_sub_norm ?gFnorm //. rewrite (OhmE 1 pG) mem_gen ?inE ?Gy -?order_dvdn ?oy // gen_subG /= -/My. apply/subsetP=> t /[!inE]; case/andP=> Gt t2. have pX := pgroupS sXG pG. case Xt: (t \in X). have: t \in 'Ohm_1(X) by rewrite (OhmE 1 pX) mem_gen // !inE Xt. apply: subsetP; rewrite (Ohm_p_cycle 1 pX) ox pfactorK //. rewrite -(subnKC n_gt3) expgM (subset_trans (cycleX _ _)) //. by rewrite /My -defMt ?joing_subl. have{Xt}: t \in yG :|: xyG by rewrite defX' inE Xt. case/setUP; first exact: mem_gen. by case/imsetP=> z _ def_t; rewrite -order_dvdn def_t orderJ oxy in t2. - 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 => t Ht notXt. have: t \in yG :|: xyG by rewrite defX' inE notXt (subsetP sHG). rewrite !andbT !gen_subG /yG /xyG. by case/setUP=> /class_eqP <-; rewrite !class_sub_norm ?Ht ?orbT. have n1_gt2: n.-1 > 2 by [rewrite -(subnKC n_gt3)]; have n1_gt1 := ltnW n1_gt2. rewrite !isogEcard card_2dihedral ?card_quaternion ?oMt // leqnn !andbT. have invX2X': {in G :\: X, forall t, x ^+ 2 ^ t == x ^- 2}. move=> t X't; rewrite /= invXX' ?mem_cycle // eq_sym eq_invg_mul -expgS. by rewrite prednK // -order_dvdn ox2. rewrite Grp_2dihedral ?Grp_quaternion //; split=> [||C]. - apply/existsP; exists (x ^+ 2, y); rewrite /= defMt // !xpair_eqE. by rewrite -!expgM def2r -!order_dvdn ox oy dvdnn eqxx /= invX2X'. - apply/existsP; exists (x ^+ 2, x * y); rewrite /= defMt // !xpair_eqE. rewrite -!expgM def2r -order_dvdn ox xy2 dvdnn eqxx invX2X' //=. by rewrite andbT /r -(subnKC n_gt3). 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)