proposition: Theorem coprime_metacyclic_cent_sdprod gT p (R A : {group gT}) : p.-group R -> odd #|R| -> metacyclic R -> p^'.-group A -> A \subset 'N(R) -> let T := [~: R, A] in let C := 'C_R(A) in [/\ abelian T, T ><| C = R & ~~ abelian R -> T != 1 -> [/\ C != 1, cyclic T, cyclic C & R^`(1) \subset T]].
proof: Proof. move=> pR oddR metaR p'A nRA T C. suffices{C T} cTT: abelian [~: R, A]. have sTR: T \subset R by rewrite commg_subl. have nTR: R \subset 'N(T) by rewrite commg_norml. have coRA: coprime #|R| #|A| := pnat_coprime pR p'A. have solR: solvable R := pgroup_sol pR. have defR: T * C = R by rewrite coprime_cent_prod. have sCR: C \subset R := subsetIl _ _; have nTC := subset_trans sCR nTR. have tiTC: T :&: C = 1. have defTA: [~: T, A] = T by rewrite coprime_commGid. have coTA: coprime #|T| #|A| := coprimeSg sTR coRA. by rewrite setIA (setIidPl sTR) -defTA coprime_abel_cent_TI ?commg_normr. split=> // [|not_cRR ntT]; first by rewrite sdprodE. have ntC: C != 1 by apply: contraNneq not_cRR => C1; rewrite -defR C1 mulg1. suffices [cycT cycC]: cyclic T /\ cyclic C. split=> //; rewrite der1_min //= -/T -defR quotientMidl. by rewrite cyclic_abelian ?quotient_cyclic. have [pT pC]: p.-group T /\ p.-group C by rewrite !(pgroupS _ pR). apply/andP; rewrite (odd_pgroup_rank1_cyclic pC (oddSg sCR oddR)). rewrite abelian_rank1_cyclic // -rank_pgroup //. rewrite -(geq_leqif (leqif_add (leqif_geq _) (leqif_geq _))) ?rank_gt0 //. have le_rTC_dimTC1: 'r(T) + 'r(C) <= logn p #|'Ohm_1(T) * 'Ohm_1(C)|. rewrite (rank_pgroup pC) -p_rank_Ohm1 (rank_abelian_pgroup pT cTT). rewrite TI_cardMg; last by apply/trivgP; rewrite -tiTC setISS ?Ohm_sub. by rewrite lognM ?cardG_gt0 // leq_add2l p_rank_le_logn. apply: leq_trans le_rTC_dimTC1 _; rewrite add1n. have ncycR: ~~ cyclic R by apply: contra not_cRR; apply: cyclic_abelian. have: 'Ohm_1(R)%G \in 'E_p^2(R) by apply: Ohm1_metacyclic_p2Elem. have nT1C1: 'Ohm_1(C) \subset 'N('Ohm_1(T)). by rewrite gFsub_trans ?gFnorm_trans. by case/pnElemP=> _ _ <-; rewrite -norm_joinEr ?lognSg // join_subG !OhmS. without loss defR: R pR oddR metaR nRA / [~: R, A] = R. set T := [~: R, A] => IH; have sTR: T \subset R by rewrite commg_subl. have defTA: [~: T, A] = T. by rewrite coprime_commGid ?(pgroup_sol pR) ?(pnat_coprime pR). rewrite -defTA IH ?(pgroupS sTR) ?(oddSg sTR) ?(metacyclicS sTR) //. exact: commg_normr. rewrite defR; apply: wlog_neg => not_cRR. have ncycR: ~~ cyclic R := contra (@cyclic_abelian _ R) not_cRR. pose cycR_nA S := [&& cyclic S, S \subset R & A \subset 'N(S)]. have [S maxS sR'S] : {S | [max S | cycR_nA S] & R^`(1) \subset S}. apply: maxgroup_exists; rewrite {}/cycR_nA der_sub /= gFnorm_trans // andbT. have [K [cycK nsKR cycKR]] := metacyclicP metaR. by rewrite (cyclicS _ cycK) // der1_min ?normal_norm // cyclic_abelian. have{maxS} [/and3P[cycS sSR nSA] maxS] := maxgroupP maxS. have ntS: S :!=: 1 by rewrite (subG1_contra sR'S) // (sameP eqP derG1P). have nSR: R \subset 'N(S) := sub_der1_norm sR'S sSR. have nsSR: S <| R by apply/andP. have sSZ: S \subset 'Z(R). have sR_NS': R \subset 'N(S)^`(1) by rewrite -{1}defR commgSS. rewrite subsetI sSR centsC (subset_trans sR_NS') // der1_min ?cent_norm //=. rewrite -ker_conj_aut (isog_abelian (first_isog _)). by rewrite (abelianS (Aut_conj_aut _ _)) ?Aut_cyclic_abelian. have cRbRb: abelian (R / S) by rewrite sub_der1_abelian. have pRb: p.-group (R / S) := quotient_pgroup S pR. pose R1 := 'Ohm_1(R); pose Rb1 := 'Ohm_1(R / S). have [Xb]: exists2 Xb, R1 / S \x gval Xb = Rb1 & A / S \subset 'N(Xb). have MaschkeRb1 := Maschke_abelem (Ohm1_abelem pRb cRbRb). pose normOhm1 := (morphim_Ohm, gFnorm_trans, quotient_norms S). by apply: MaschkeRb1; rewrite ?quotient_pgroup ?normOhm1. case/dprodP=> _ defRb1 _ tiR1bX nXbA. have sXbR: Xb \subset R / S. by apply: subset_trans (Ohm_sub 1 _); rewrite -defRb1 mulG_subr. have{sXbR} [X defXb sSX sXR] := inv_quotientS nsSR sXbR. have{nXbA nsSR} nXA: A \subset 'N(X). rewrite (subset_trans (mulG_subr S A)) // -quotientK //. by rewrite -(quotientGK (normalS sSX sXR nsSR)) -defXb morphpre_norms. have{tiR1bX} cycX: cyclic X. have sX1_XR1: 'Ohm_1(X) \subset X :&: R1 by rewrite subsetI Ohm_sub OhmS. have cyc_sR := odd_pgroup_rank1_cyclic (pgroupS _ pR) (oddSg _ oddR). have:= cycS; rewrite !{}cyc_sR //; apply: leq_trans. rewrite -p_rank_Ohm1 p_rankS // (subset_trans sX1_XR1) //. rewrite -quotient_sub1 ?subIset ?(subset_trans sXR) //. by rewrite quotientGI // setIC -defXb tiR1bX. rewrite (cyclic_factor_abelian sSZ) // abelian_rank1_cyclic //. rewrite (rank_abelian_pgroup pRb cRbRb) -defRb1 defXb. rewrite (maxS X) ?trivg_quotient ?mulg1 //; last exact/and3P. have EpR1: 'Ohm_1(R)%G \in 'E_p^2(R) by apply: Ohm1_metacyclic_p2Elem. have [sR1R _ dimR1] := pnElemP EpR1; have pR1 := pgroupS sR1R pR. rewrite -(card_isog (second_isog _)) ?(subset_trans sR1R) // -ltnS -dimR1. by rewrite (ltn_log_quotient pR1) ?subsetIr //= meet_Ohm1 // (setIidPl sSR). 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)