proposition: Theorem dihedral2_structure : n > 1 -> extremal_generators G 2 n (x, y) -> G \isog 'D_m -> [/\ [/\ X ><| Y = G, {in G :\: X, forall t, #[t] = 2} & {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], 'Ohm_1(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] & if n == 2 then (2.-abelem G : Prop) else [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2, My \isog 'D_q, Mxy \isog 'D_q & forall U, cyclic U -> U \subset G -> #|G : U| = 2 -> U = X]].
proof: Proof. move=> n_gt1 genG isoG; have [def2q def2r ltqm ltrq] := def2qr n_gt1. 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_2dihedral n_gt1 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=> z'; case/cycleP=> j -> ->{z t}. by rewrite conjgM {2}/conjg commuteX2 // mulKg conjXg uv expgVn. have oU': {in <[u]> :* v, forall t, #[t] = 2}. move=> t Uvt; apply: nt_prime_order => //; last first. by case: eqP Uvt => // ->; rewrite defUv !inE group1. case/rcosetP: Uvt => z Uz ->{t}; rewrite expgS {1}(conjgC z) -mulgA. by rewrite invUV ?rcoset_refl // mulKg -(expgS v 1) -ov expg_order. have defU: n > 2 -> {in G, forall z, #[z] = q -> <[z]> = <[u]>}. move=> n_gt2 z Gz oz; apply/eqP; rewrite eqEcard -!orderE oz cycle_subG. apply: contraLR n_gt2; rewrite ou leqnn andbT -(ltn_predK n_gt1) => notUz. by rewrite ltnS -(@ltn_exp2l 2) // -/q -oz oU' // defUv inE notUz. have n2_abelG: (n > 2) || 2.-abelem G. rewrite ltn_neqAle eq_sym n_gt1; case: eqP => //= n2. apply/abelemP=> //; split=> [|z Gz]. by apply: (p2group_abelian pG); rewrite oG pfactorK ?n2. case Uz: (z \in <[u]>); last by rewrite -expg_mod_order oU' // defUv inE Uz. apply/eqP; rewrite -order_dvdn (dvdn_trans (order_dvdG Uz)) // -orderE. by rewrite ou /q n2. have{oU'} oX': {in G :\: X, forall t, #[t] = 2}. have [n_gt2 | abelG] := orP n2_abelG; first by rewrite [X]defU // -defUv. move=> t /setDP[Gt notXt]; apply: nt_prime_order (group1_contra notXt) => //. by case/abelemP: abelG => // _ ->. have{invUV} invXX': {in X & G :\: X, forall z t, z ^ t = z^-1}. have [n_gt2 | abelG] := orP n2_abelG; first by rewrite [X]defU // -defUv. have [//|cGG oG2] := abelemP _ abelG. move=> t z Xt /setDP[Gz _]; apply/eqP; rewrite eq_sym eq_invg_mul. by rewrite /conjg -(centsP cGG z) // ?mulKg ?[t * t]oG2 ?(subsetP sXG). 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); last by rewrite -{1}(oX' z) ?expg_order ?group1 // inE Xz. by case/cycleP: Xz => i ->; rewrite expgAC 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=> _ z /cycleP[j ->] Xz -> -> {tz t'z}. 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 expgAC. have defMt: {in G :\: X, forall t, <[x ^+ 2]> ><| <[t]> = <<t ^: G>>}. move=> t X't; have [Gt notXt] := setDP X't. rewrite sdprodEY ?cycle_subG ?(subsetP (nXiG 2)) //; first 1 last. rewrite setIC prime_TIg -?orderE ?oX' // cycle_subG. by apply: contra notXt; apply: subsetP; rewrite cycleX. 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 oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}. move=> t X't /=; rewrite -(sdprod_card (defMt t X't)) -!orderE ox2 oX' //. by rewrite mulnC. have sMtG: {in G :\: X, forall t, <<t ^: G>> \subset G}. by move=> t; case/setDP=> Gt _; rewrite gen_subG class_subG. 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 ?oX'. - rewrite defG'; split=> //. apply/eqP; rewrite eqn_leq (leq_trans (nil_class_pgroup pG)); last first. by rewrite oG pfactorK // geq_max leqnn -(subnKC n_gt1). rewrite -(subnKC n_gt1) subn2 ltnNge. rewrite (sameP (lcn_nil_classP _ (pgroup_nil pG)) eqP). by apply/trivgPn; exists (x ^+ r); rewrite ?memL // -order_gt1 oxr. - split; last exact: extend_cyclic_Mho. have sX'G1: {subset G :\: X <= 'Ohm_1(G)}. move=> t X't; have [Gt _] := setDP X't. by rewrite (OhmE 1 pG) mem_gen // !inE Gt -(oX' t) //= expg_order. apply/eqP; rewrite eqEsubset Ohm_sub -{1}defXY mulG_subG !cycle_subG. by rewrite -(groupMr _ (sX'G1 y X'y)) !sX'G1. - 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; move/class_eqP <-; rewrite !class_sub_norm ?Ht ?orbT. rewrite eqn_leq n_gt1; case: leqP n2_abelG => //= n_gt2 _. have ->: '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=> t; case/setIP=> Gt cGt. case X't: (t \in G :\: X). move/eqP: (invXX' _ _ (cycle_id x) X't). rewrite /conjg -(centP cGt) // mulKg eq_sym eq_invg_mul -order_eq1 ox2. by rewrite (eqn_exp2l _ 0) // -(subnKC n_gt2). move/idPn: X't; rewrite inE Gt andbT negbK => Xt. have:= Ohm_p_cycle 1 (mem_p_elt pG Gx); rewrite ox pfactorK // subn1 => <-. rewrite (OhmE _ (pgroupS sXG pG)) mem_gen // !inE Xt /=. by rewrite -eq_invg_mul -(invXX' _ y) // /conjg (centP cGt) // mulKg. have isoMt: {in G :\: X, forall t, <<t ^: G>> \isog 'D_q}. have n1_gt1: n.-1 > 1 by rewrite -(subnKC n_gt2). move=> t X't /=; rewrite isogEcard card_2dihedral ?oMt // leqnn andbT. rewrite Grp_2dihedral //; apply/existsP; exists (x ^+ 2, t) => /=. have [_ <- nX2T _] := sdprodP (defMt t X't); rewrite norm_joinEr //. rewrite -/q -/r !xpair_eqE eqxx -expgM def2r -ox -{1}(oX' t X't). by rewrite !expg_order !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)