proposition: Theorem rank2_coprime_comm_cprod gT p (R A : {group gT}) : p.-group R -> odd #|R| -> R :!=: 1 -> 'r(R) <= 2 -> [~: R, A] = R -> p^'.-group A -> odd #|A| -> [/\ p > 3 & [\/ abelian R | exists2 S : {group gT}, [/\ ~~ abelian S, logn p #|S| = 3 & exponent S %| p] & exists C : {group gT}, [/\ S \* C = R, cyclic C & 'Ohm_1(C) = S^`(1)]]].
proof: Proof. move=> pR oddR ntR rR defRA p'A oddA. have [p_pr _ _] := pgroup_pdiv pR ntR; have p_gt1 := prime_gt1 p_pr. have nilR: nilpotent R := pgroup_nil pR. have nRA: A \subset 'N(R) by rewrite -commg_subl defRA. have p_gt3: p > 3; last split => //. have [Ab1 | [q q_pr q_dv_Ab]] := trivgVpdiv (A / 'C_A(R)). case/eqP: ntR; rewrite -defRA commGC; apply/commG1P. by rewrite -subsetIidl -quotient_sub1 ?Ab1 ?normsI ?norms_cent ?normG. have odd_q := dvdn_odd q_dv_Ab (quotient_odd _ oddA). have p'q := pgroupP (quotient_pgroup _ p'A) q q_pr q_dv_Ab. have q_gt1: q > 1 := prime_gt1 q_pr. have q_gt2: q > 2 by rewrite ltn_neqAle; case: eqP odd_q => // <-. apply: leq_ltn_trans q_gt2 _. rewrite /= -ker_conj_aut (card_isog (first_isog_loc _ _)) // in q_dv_Ab. have q_dv_A := dvdn_trans q_dv_Ab (cardSg (Aut_conj_aut R A)). by case/(pi_Aut_rank2_pgroup pR): (pgroupP (pgroup_pi _) q q_pr q_dv_A). pose S := 'Ohm_1(R); pose S' := S^`(1); pose C := 'C_R(S). have pS: p.-group S := pgroupS (Ohm_sub 1 _) pR. have nsSR: S <| R := gFnormal _ R. have nsS'R: S' <| R := gFnormal_trans _ nsSR. have [sSR nSR] := andP nsSR; have [_ nS'R] := andP nsS'R. have [Sle2 | Sgt2] := leqP (logn p #|S|) 2. have metaR: metacyclic R := p2_Ohm1_metacyclic pR p_gt3 Sle2. have [cRR _ _] := coprime_metacyclic_cent_sdprod pR oddR metaR p'A nRA. by left; rewrite -defRA. have{p_gt3} eS: exponent S %| p by apply: exponent_Ohm1_rank2. have{rR} rS: 'r(S) <= 2 by rewrite rank_Ohm1. have{Sgt2} dimS: logn p #|S| = 3. by apply/eqP; rewrite eqn_leq rank2_exponent_p_p3group. have{rS} not_cSS: ~~ abelian S. by apply: contraL rS => cSS; rewrite -ltnNge -dimS -rank_abelem ?abelem_Ohm1. have esS: extraspecial S by apply: (p3group_extraspecial pS); rewrite ?dimS. have defS': S' = 'Z(S) by case: esS; case. have oS': #|S'| = p by rewrite defS' (card_center_extraspecial pS esS). have dimS': logn p #|S'| = 1%N by rewrite oS' (pfactorK 1). have nsCR: C <| R := normalGI nSR (cent_normal _); have [sCR nCR] := andP nsCR. have [pC oddC]: p.-group C * odd #|C| := (pgroupS sCR pR, oddSg sCR oddR). have defC1: 'Ohm_1(C) = S'. apply/eqP; rewrite eqEsubset defS' subsetI OhmS ?(OhmE 1 pC) //= -/C. by rewrite gen_subG setIAC subsetIr sub_gen ?setSI // subsetI sSR sub_LdivT. have{pC oddC} cycC: cyclic C. rewrite (odd_pgroup_rank1_cyclic pC) //. by rewrite -p_rank_Ohm1 defC1 -dimS' p_rank_le_logn. pose T := [~: S, R]; have nsTR: T <| R by rewrite /normal commg_normr comm_subG. have [sTR nTR] := andP nsTR; have pT: p.-group T := pgroupS sTR pR. have [sTS' | not_sTS' {esS}] := boolP (T \subset S'). right; exists [group of S] => //; exists [group of C]. by rewrite (critical_extraspecial pR sSR esS sTS'). have ltTS: T \proper S by rewrite (nil_comm_properl nilR) ?Ohm1_eq1 ?subsetIidl. have sTS: T \subset S := proper_sub ltTS. have [sS'T ltS'T]: S' \subset T /\ S' \proper T by rewrite /proper commgS. have{ltS'T ltTS} dimT: logn p #|T| = 2. by apply/eqP; rewrite eqn_leq -ltnS -dimS -dimS' !properG_ltn_log. have{eS} eT: exponent T %| p := dvdn_trans (exponentS sTS) eS. have cTT: abelian T by rewrite (p2group_abelian pT) ?dimT. have abelT: p.-abelem T by apply/and3P. pose B := 'C_R(T); have sTB: T \subset B by rewrite subsetI sTR. have nsBR: B <| R := normalGI nTR (cent_normal _); have [sBR nBR] := andP nsBR. have not_sSB: ~~ (S \subset B). by rewrite defS' !subsetI sTS sSR centsC in not_sTS' *. have maxB: maximal B R. rewrite p_index_maximal // (_ : #|R : B| = p) //; apply/prime_nt_dvdP=> //. by apply: contra not_sSB; rewrite indexg_eq1; apply: subset_trans. rewrite -(part_pnat_id (pnat_dvd (dvdn_indexg _ _) pR)) p_part. by rewrite (@dvdn_exp2l _ _ 1) // logn_quotient_cent_abelem ?dimT //. have{maxB nsBR} defR: B * S = R := mulg_normal_maximal nsBR maxB sSR not_sSB. have cBbBb: abelian (B / C). rewrite sub_der1_abelian // subsetI comm_subG ?subsetIl //=; apply/commG1P. suff cB_SB: [~: S, B, B] = 1 by rewrite three_subgroup // [[~: _, S]]commGC. by apply/commG1P; rewrite centsC subIset // centS ?orbT // commgS. have{cBbBb} abelBb: p.-abelem (B / C). apply/abelemP=> //; split=> // Cg; case/morphimP=> x Nx Bx /= ->. have [Rx cTx] := setIP Bx; rewrite -morphX //= coset_id // inE groupX //=. apply/centP=> y Sy; symmetry; have Tyx : [~ y, x] \in T by apply: mem_commg. by apply/commgP; rewrite commgX ?(exponentP eT) //; apply: (centP cTx). have nsCB: C <| B by rewrite (normalS _ _ nsCR) ?setIS ?subsetIl // centS. have p'Ab: p^'.-group (A / C) by apply: quotient_pgroup. have sTbB: T / C \subset B / C by rewrite quotientS. have nSA: A \subset 'N(S) := gFnorm_trans _ nRA. have nTA: A \subset 'N(T) := normsR nSA nRA. have nTbA: A / C \subset 'N(T / C) := quotient_norms _ nTA. have nBbA: A / C \subset 'N(B / C). by rewrite quotient_norms ?normsI ?norms_cent. have{p'Ab sTbB nBbA abelBb nTbA} [Xb defBb nXbA] := Maschke_abelem abelBb p'Ab sTbB nBbA nTbA. have{defBb} [_] := dprodP defBb; rewrite /= -/T -/B => defBb _ tiTbX. have sXbB: Xb \subset B / C by rewrite -defBb mulG_subr. have{sXbB} [X] := inv_quotientS nsCB sXbB; rewrite /= -/C -/B => defXb sCX sXB. have sXR: X \subset R := subset_trans sXB sBR; have pX := pgroupS sXR pR. have nsCX: C <| X := normalS sCX sXR nsCR. have{tiTbX} ziTX: T :&: X \subset C. rewrite -quotient_sub1 ?subIset ?(subset_trans sTR) ?normal_norm //= -/C. by rewrite quotientIG -?defXb ?tiTbX. have{nXbA} nXA: A \subset 'N(X). have nCA: A \subset 'N(C) by rewrite normsI ?norms_cent. by rewrite -(quotientSGK nCA) ?normsG // quotient_normG -?defXb. have{abelT} defB1: 'Ohm_1(B) = T. apply/eqP; rewrite eq_sym eqEcard -{1}[T](Ohm1_id abelT) OhmS //. have pB1: p.-group 'Ohm_1(B) by apply: pgroupS pR; apply: gFsub_trans. rewrite (card_pgroup pT) (card_pgroup pB1) leq_exp2l //= -/T -/B. rewrite dimT -ltnS -dimS properG_ltn_log // properEneq OhmS ?subsetIl //= -/S. by case: eqP not_sSB => // <-; rewrite Ohm_sub. have{ziTX defB1} cycX: cyclic X; last have [x defX]:= cyclicP cycX. rewrite (odd_pgroup_rank1_cyclic pX (oddSg sXR oddR)) -p_rank_Ohm1. have:= cycC; rewrite abelian_rank1_cyclic ?cyclic_abelian //= -/C. apply: leq_trans (leq_trans (p_rank_le_rank p _) (rankS _)). by apply: subset_trans ziTX; rewrite subsetI Ohm_sub -defB1 OhmS. have{Xb defXb defBb nsCX} mulSX: S * X = R. have nCT: T \subset 'N(C) := subset_trans sTR nCR. rewrite -defR -(normC (subset_trans sSR nBR)) -[B](quotientGK nsCB) -defBb. rewrite cosetpreM quotientK // defXb quotientGK // -(normC nCT). by rewrite -mulgA (mulSGid sCX) mulgA (mulGSid sTS). have{mulSX} not_sXS_S': ~~ ([~: X, S] \subset S'). apply: contra not_sTS' => sXS_S'; rewrite /T -mulSX. by rewrite commGC commMG ?(subset_trans sXR) // mul_subG. have [oSb oTb] : #|S / T| = p /\ #|T / S'| = p. rewrite (card_pgroup (quotient_pgroup _ pS)) -divg_normal ?(normalS _ sSR) //. rewrite (card_pgroup (quotient_pgroup _ pT)) -divg_normal ?(normalS _ sTR) //. by rewrite !logn_div ?cardSg // dimS dimT dimS'. have [Ty defSb]: exists Ty, S / T = <[Ty]>. by apply/cyclicP; rewrite prime_cyclic ?oSb. have SbTy: Ty \in S / T by rewrite defSb cycle_id. have{SbTy} [y nTy Sy defTy] := morphimP SbTy. have [S'z defTb]: exists S'z, T / S' = <[S'z]>. apply/cyclicP; rewrite prime_cyclic ?oTb //. have TbS'z: S'z \in T / S' by rewrite defTb cycle_id. have{TbS'z} [z nS'z Tz defS'z] := morphimP TbS'z. have [Ta AbTa not_cSbTa]: exists2 Ta, Ta \in A / T & Ta \notin 'C(S / T). apply: subsetPn; rewrite quotient_cents2 ?commg_norml //= -/T commGC. apply: contra not_sSB => sSA_T; rewrite (subset_trans sSR) // -defRA -defR. rewrite -(normC (subset_trans sSR nBR)) commMG /= -/S -/B; last first. by rewrite cents_norm ?subIset ?centS ?orbT. by rewrite mul_subG ?commg_subl ?normsI ?norms_cent // (subset_trans sSA_T). have [a nTa Aa defTa] := morphimP AbTa. have nS'a: a \in 'N(S') := subsetP (gFnorm_trans _ nSA) a Aa. have [i xa]: exists i, x ^ a = x ^+ i. by apply/cycleP; rewrite -cycle_subG cycleJ /= -defX (normsP nXA). have [j Tya]: exists j, Ty ^ Ta = Ty ^+ j. apply/cycleP; rewrite -cycle_subG cycleJ /= -defSb. by rewrite (normsP (quotient_norms _ nSA)). suffices {oSb oddA not_cSbTa} j2_1: j ^ 2 == 1 %[mod p]. have Tya2: Ty ^ coset T (a ^+ 2) = Ty ^+ (j ^ 2). by rewrite morphX // conjgM -defTa Tya conjXg Tya expgM. have coA2: coprime #|A| 2 by rewrite coprime_sym prime_coprime // dvdn2 oddA. case/negP: not_cSbTa; rewrite defTa -(expgK coA2 Aa) morphX groupX //=. rewrite defSb cent_cycle inE conjg_set1 Tya2 sub1set inE. by rewrite (eq_expg_mod_order _ _ 1) orderE -defSb oSb. have {Tya Ta defTa AbTa} [u Tu yj]: exists2 u, u \in T & y ^+ j = u * y ^ a. apply: rcosetP; apply/rcoset_kercosetP; rewrite ?groupX ?groupJ //. by rewrite morphX ?morphJ -?defTy // -defTa. have{Ty defTy defSb} defS: T * <[y]> = S. rewrite -quotientK ?cycle_subG ?quotient_cycle // -defTy -defSb /= -/T. by rewrite quotientGK // /normal sTS /= commg_norml. have{nTA} [k S'zk]: exists k, S'z ^ coset S' a = S'z ^+ k. apply/cycleP; rewrite -cycle_subG cycleJ /= -defTb. by rewrite (normsP (quotient_norms _ nTA)) ?mem_quotient. have S'yz: [~ y, z] \in S' by rewrite mem_commg // (subsetP sTS). have [v Zv zk]: exists2 v, v \in 'Z(S) & z ^+ k = v * z ^ a. apply: rcosetP; rewrite -defS'. by apply/rcoset_kercosetP; rewrite ?groupX ?groupJ ?morphX ?morphJ -?defS'z. have defT: S' * <[z]> = T. rewrite -quotientK ?cycle_subG ?quotient_cycle // -defS'z -defTb /= -/S'. by rewrite quotientGK // (normalS _ sTR) // proper_sub. have nt_yz: [~ y, z] != 1. apply: contra not_cSS; rewrite (sameP commgP cent1P) => cyz. rewrite -defS abelianM cTT cycle_abelian /= -/T -defT centM /= -/S' defS'. by rewrite cent_cycle subsetI centsC subIset ?centS ?cycle_subG ?orbT. have sS'X1: S' \subset 'Ohm_1(X) by rewrite -defC1 OhmS. have i_neq0: i != 0 %[mod p]. have: 'Ohm_1(X) != 1 by rewrite (subG1_contra sS'X1) //= -cardG_gt1 oS'. rewrite defX in pX *; rewrite (Ohm_p_cycle 1 pX) subn1 trivg_card1 -orderE. rewrite -(orderJ _ a) conjXg xa order_eq1 -expgM -order_dvdn mod0n. apply: contra; case/dvdnP=> m ->; rewrite -mulnA -expnS dvdn_mull //. by rewrite {1}[#[x]](card_pgroup pX) dvdn_exp2l ?leqSpred. have Txy: [~ x, y] \in T by rewrite [T]commGC mem_commg // -cycle_subG -defX. have [Rx Ry]: x \in R /\ y \in R by rewrite -cycle_subG -defX (subsetP sSR). have [nS'x nS'y] := (subsetP nS'R x Rx, subsetP nS'R y Ry). have{not_sXS_S'} not_S'xy: [~ x, y] \notin S'. apply: contra not_sXS_S' => S'xy. rewrite -quotient_cents2 ?(subset_trans _ nS'R) //= -/S'. rewrite -defS quotientMl ?(subset_trans _ nS'R) // centM /= -/S' -/T. rewrite subsetI quotient_cents; last by rewrite (subset_trans sXB) ?subsetIr. rewrite defX !quotient_cycle // cent_cycle cycle_subG /= -/S'. by rewrite (sameP cent1P commgP) -morphR /= ?coset_id. have jk_eq_i: j * k = i %[mod p]. have Zyz: [~ y, z] \in 'Z(S) by rewrite -defS'. have Sz: z \in S := subsetP sTS z Tz. have yz_p: [~ y, z] ^+ p == 1 by rewrite -order_dvdn -oS' order_dvdG. have <-: #[[~ y, z]] = p by apply: nt_prime_order => //; apply: eqP. apply: eqP; rewrite -eq_expg_mod_order -commXXg; try exact: centerC Zyz. have cyv: [~ y ^+ j, v] = 1 by apply/eqP/commgP/(centerC (groupX j Sy) Zv). have cuz: [~ u, z ^ a] = 1. by apply/eqP/commgP/(centsP cTT); rewrite ?memJ_norm. rewrite zk commgMJ cyv yj commMgJ cuz !conj1g mulg1 mul1g -conjRg. suffices [m ->]: exists m, [~ y, z] = x ^+ m by rewrite conjXg xa expgAC. by apply/cycleP; rewrite -defX (subsetP (Ohm_sub 1 X)) ?(subsetP sS'X1). have ij_eq_k: i * j = k %[mod p]. have <-: #[coset S' [~ x, y]] = p. apply: nt_prime_order => //. by apply: eqP; rewrite -order_dvdn -oTb order_dvdG 1?mem_quotient. by apply: contraNneq not_S'xy; apply: coset_idr; rewrite groupR. have sTbZ: T / S' \subset 'Z(R / S'). rewrite prime_meetG ?oTb // (meet_center_nil (quotient_nil _ nilR)) //. by rewrite quotient_normal //; apply/andP. by rewrite -cardG_gt1 oTb. have ZRxyb: [~ coset S' x, coset S' y] \in 'Z(R / S'). by rewrite -morphR // (subsetP sTbZ) ?mem_quotient. apply: eqP; rewrite -eq_expg_mod_order {1}morphR //. rewrite -commXXg; try by apply: centerC ZRxyb; apply: mem_quotient. have [Ru nRa] := (subsetP sTR u Tu, subsetP nRA a Aa). rewrite -2?morphX // yj morphM ?(subsetP nS'R) ?memJ_norm //. have cxu_b: [~ coset S' (x ^+ i), coset S' u] = 1. apply: eqP; apply/commgP. by apply: centerC (subsetP sTbZ _ _); rewrite mem_quotient ?groupX. rewrite commgMJ cxu_b conj1g mulg1 -xa !morphJ // -conjRg -morphR //=. have: coset S' [~ x, y] \in <[S'z]> by rewrite -defTb mem_quotient. by case/cycleP=> m ->; rewrite conjXg S'zk expgAC. have j2_gt0: j ^ 2 > 0. rewrite expn_gt0 orbF lt0n; apply: contraNneq i_neq0 => j0. by rewrite -jk_eq_i j0. have{i_neq0} co_p_i: coprime p i by rewrite mod0n prime_coprime in i_neq0 *. rewrite eqn_mod_dvd // -(Gauss_dvdr _ co_p_i) mulnBr -eqn_mod_dvd ?leq_mul //. by rewrite muln1 mulnCA -modnMmr ij_eq_k modnMmr jk_eq_i. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)