proposition: Proposition ext_odd_regular_pgroup_cyclic (aT rT : finGroupType) p (D R : {group aT}) (K H : {group rT}) (to : groupAction D K) : p.-group R -> odd #|R| -> H :!=: 1 -> {acts R, on group H | to} -> {in R^#, forall x, 'C_(H | to)[x] = 1} -> cyclic R.
proof: Proof. move: R H => R0 H0 pR0 oddR0 ntH0 actsR0 regR0. pose gT := sdprod_groupType <[actsR0]>. pose H : {group gT} := (sdpair1 <[actsR0]> @* H0)%G. pose R : {group gT} := (sdpair2 <[actsR0]> @* R0)%G. pose G : {group gT} := [set: gT]%G. have{pR0} pR: p.-group R by rewrite morphim_pgroup. have{oddR0} oddR: odd #|R| by rewrite morphim_odd. have [R1 | ntR] := eqsVneq R 1. by rewrite -(im_invm (injm_sdpair2 <[actsR0]>)) {2}R1 morphim1 cyclic1. have{ntH0} ntH: H :!=: 1. apply: contraNneq ntH0 => H1. by rewrite -(im_invm (injm_sdpair1 <[actsR0]>)) {2}H1 morphim1. have{regR0 ntR} frobG: [Frobenius G = H ><| R]. apply/Frobenius_semiregularP => // [|x]; first exact: sdprod_sdpair. case/setD1P=> nt_x; case/morphimP=> x2 _ Rx2 def_x. apply/trivgP; rewrite -(morphpreSK _ (subsetIl _ _)) morphpreI. rewrite /= -cent_cycle def_x -morphim_cycle // -gacentEsd. rewrite injmK ?injm_sdpair1 // (trivgP (injm_sdpair1 _)). rewrite -(regR0 x2) ?inE ?Rx2 ?andbT; last first. by apply: contra nt_x; rewrite def_x; move/eqP->; rewrite morph1. have [sRD sHK]: R0 \subset D /\ H0 \subset K by case actsR0; move/acts_dom. have sx2R: <[x2]> \subset R0 by rewrite cycle_subG. rewrite gacent_actby setIA setIid (setIidPr sx2R). rewrite !gacentE ?cycle_subG ?sub1set ?(subsetP sRD) //. by rewrite !setIS ?afixS ?sub_gen. suffices: cyclic R by rewrite (injm_cyclic (injm_sdpair2 _)). move: gT H R G => {aT rT to D K H0 R0 actsR0} gT H R G in ntH pR oddR frobG *. have [defG _ _ _ _] := Frobenius_context frobG; case/sdprodP: defG => _ _ nHR _. have coHR := Frobenius_coprime frobG. rewrite (odd_pgroup_rank1_cyclic pR oddR) leqNgt. apply: contra ntH => /p_rank_geP[E /pnElemP[sER abelE dimE2]]. have ncycE: ~~ cyclic E by rewrite (abelem_cyclic abelE) dimE2. have nHE := subset_trans sER nHR; have coHE := coprimegS sER coHR. rewrite -subG1 -(coprime_abelian_gen_cent1 _ _ nHE) ?(abelem_abelian abelE) //. rewrite -bigprodGE big1 // => x /setD1P[nt_x Ex]; apply: val_inj => /=. by apply: (Frobenius_reg_ker frobG); rewrite !inE nt_x (subsetP sER). 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)