proposition: Lemma regular_pq_group_cyclic gT p q (H R : {group gT}) : [/\ prime p, prime q & p != q] -> #|R| = (p * q)%N -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R -> cyclic R.
proof: Proof. case=> pr_p pr_q q'p oR ntH nHR regHR. without loss{q'p} ltpq: p q pr_p pr_q oR / p < q. by move=> IH; case: ltngtP q'p => // /IH-> //; rewrite mulnC. have [p_gt0 q_gt0]: 0 < p /\ 0 < q by rewrite !prime_gt0. have [[P sylP] [Q sylQ]] := (Sylow_exists p R, Sylow_exists q R). have [sPR sQR] := (pHall_sub sylP, pHall_sub sylQ). have [oP oQ]: #|P| = p /\ #|Q| = q. rewrite (card_Hall sylQ) (card_Hall sylP) oR !p_part !lognM ?logn_prime //. by rewrite !eqxx eq_sym gtn_eqF. have [ntP ntQ]: P :!=: 1 /\ Q :!=: 1 by rewrite -!cardG_gt1 oP oQ !prime_gt1. have nQR: R \subset 'N(Q). rewrite -subsetIidl -indexg_eq1 -(card_Syl_mod R pr_q) (card_Syl sylQ) /=. rewrite modn_small // -divgS ?subsetIl ?ltn_divLR // mulnC oR ltn_pmul2r //. by rewrite (leq_trans ltpq) // -oQ subset_leq_card // subsetI sQR normG. have coQP: coprime #|Q| #|P|. by rewrite oP oQ prime_coprime ?dvdn_prime2 ?gtn_eqF. have defR: Q ><| P = R. rewrite sdprodE ?coprime_TIg ?(subset_trans sPR) //. by apply/eqP; rewrite eqEcard mul_subG //= oR coprime_cardMg // oP oQ mulnC. have [cycP cycQ]: cyclic P /\ cyclic Q by rewrite !prime_cyclic ?oP ?oQ. suffices cQP: P \subset 'C(Q) by rewrite (@cyclic_dprod _ Q P) ?dprodEsd. without loss /is_abelemP[r pr_r abelH]: H ntH nHR regHR / is_abelem H. move=> IH; have [r _ rH] := rank_witness H. have solR: solvable R. apply/metacyclic_sol/metacyclicP; exists Q. by rewrite /(Q <| R) sQR -(isog_cyclic (sdprod_isog defR)). have coHR: coprime #|H| #|R| := regular_norm_coprime nHR regHR. have [H1 sylH1 nH1R] := sol_coprime_Sylow_exists r solR nHR coHR. have ntH1: H1 :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylH1) -rH rank_gt0. have [H2 minH2 sH21] := minnormal_exists ntH1 nH1R. have [sH1H rH1 _] := and3P sylH1; have sH2H := subset_trans sH21 sH1H. have [nH2R ntH2 abelH2] := minnormal_solvable minH2 sH21 (pgroup_sol rH1). by apply: IH abelH2 => //; apply: semiregularS regHR. have: rfix_mx (abelem_repr abelH ntH nHR) P == 0. rewrite -mxrank_eq0 rfix_abelem // mxrank_eq0 rowg_mx_eq0 /=. by rewrite (cent_semiregular regHR) ?morphim1. apply: contraLR => not_cQP; have{not_cQP} frobR: [Frobenius R = Q ><| P]. by apply/prime_FrobeniusP; rewrite ?prime_TIg ?oP ?oQ // centsC. apply: (Frobenius_rfix_compl frobR). rewrite (eq_p'group _ (charf_eq (char_Fp pr_r))). rewrite (coprime_p'group _ (abelem_pgroup abelH)) //. by rewrite coprime_sym (coprimegS sQR) ?regular_norm_coprime. rewrite rker_abelem subsetI sQR centsC. by rewrite -subsetIidl (cent_semiregular regHR) ?subG1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)