proposition: Theorem Aut_narrow (A : {group {perm gT}}) : p.-narrow R -> solvable A -> A \subset Aut R -> odd #|A| -> [/\ p^'.-group (A / 'O_p(A)), abelian (A / 'O_p(A)) & 2 < 'r(R) -> forall x, x \in A -> p^'.-elt x -> #[x] %| p.-1].
proof: Proof. move=> nnR solA AutA oddA; have nilR := pgroup_nil pR. have [rR | rR] := leqP 'r(R) 2. have pA' := der1_Aut_rank2_pgroup pR oddR rR AutA solA oddA. have sA'Ap: A^`(1) \subset 'O_p(A) by rewrite pcore_max ?der_normal. have cAbAb: abelian (A / 'O_p(A)) by rewrite sub_der1_abelian. split; rewrite // -(nilpotent_pcoreC p (abelian_nil cAbAb)). by rewrite trivg_pcore_quotient dprod1g pcore_pgroup. have ntR: R :!=: 1 by rewrite -rank_gt0 2?ltnW. rewrite (rank_pgroup pR) in rR. have [H [charH sHRZ] _ eH pCH] := critical_odd pR oddR ntR. have{ntR} [[p_pr _ _] sHR] := (pgroup_pdiv pR ntR, char_sub charH). have ntH: H :!=: 1 by rewrite trivg_exponent eH -prime_coprime ?coprimen1. have{nnR} [S C sSR sCR oS cycC defSC] := narrow_structureP rR nnR. have [_ mulSC cSC tiSC] := dprodP defSC. have abelS: p.-abelem S := prime_abelem p_pr oS; have [pS cSS _] := and3P abelS. have cycS: cyclic S by rewrite prime_cyclic ?oS. have tiHS: H :&: S = 1. have rCRS: 'r_p('C_R(S)) <= 2. rewrite -(p_rank_dprod p defSC) -addn1 -!rank_pgroup ?(pgroupS _ pR) //. by rewrite leq_add -?abelian_rank1_cyclic ?cyclic_abelian. rewrite setIC prime_TIg ?oS //; apply: contraL (rCRS) => sSH; rewrite -ltnNge. have cZHS: S \subset 'C('Z(H)) by rewrite centsC (centsS sSH) ?subsetIr. pose U := S <*> 'Z(H). have sUH: U \subset H by rewrite join_subG sSH subsetIl. have cUU: abelian U by rewrite abelianY cSS center_abelian centsC. have abelU: p.-abelem U by rewrite abelemE // cUU -eH exponentS. have sUR: U \subset R := subset_trans sUH sHR. have rU: 'r_p(U) <= 'r_p('C_R(S)). by rewrite p_rankS //= subsetI sUR (centsS (joing_subl S 'Z(H))). have nsUR: U <| R. rewrite /normal sUR -commg_subl (subset_trans (commSg _ sUH)) //= -/U. by rewrite (subset_trans sHRZ) // joing_subr. have{rU}:= leq_trans rU rCRS; rewrite leq_eqVlt => /predU1P[] rU. have Ep2U: [group of U] \in 'E_p^2(R). by rewrite !inE /= sUR abelU -(p_rank_abelem abelU) rU. have [F scn3F sUF] := normal_p2Elem_SCN3 rR Ep2U nsUR. have [scnF rF] := setIdP scn3F; have [_ scF] := SCN_P scnF. rewrite (leq_trans rF) // -scF -rank_pgroup ?(pgroupS (subsetIl _ _)) //. by rewrite rankS ?setIS ?centS // (subset_trans _ sUF) ?joing_subl. have defU: S :=: U. apply/eqP; rewrite eqEcard oS joing_subl (card_pgroup (pgroupS sUR pR)). by rewrite -p_rank_abelem // (leq_exp2l _ 1) // prime_gt1. have ntS: S :!=: 1 by rewrite -cardG_gt1 oS prime_gt1. have sSZ: S \subset 'Z(R) by rewrite prime_meetG ?oS ?meet_center_nil // defU. by rewrite (setIidPl _) // centsC (subset_trans sSZ) ?subsetIr. have{tiHS eH} oCHS: #|'C_H(S)| = p. have ntCHS: 'C_H(S) != 1. have: H :&: 'Z(R) != 1 by rewrite meet_center_nil ?char_normal. by apply: subG1_contra; rewrite setIS // (centsS sSR) ?subsetIr. have cycCHS: cyclic 'C_H(S). have tiS_CHS: S :&: 'C_H(S) = 1 by rewrite setICA setIA tiHS setI1g. rewrite (isog_cyclic (quotient_isog _ tiS_CHS)) ?subIset ?cent_sub ?orbT //. rewrite (cyclicS _ (quotient_cyclic S cycC)) //= -(quotientMidl S C). by rewrite mulSC quotientS // setSI // char_sub. have abelCHS: p.-abelem 'C_H(S). by rewrite abelemE ?cyclic_abelian // -eH exponentS ?subsetIl. rewrite -(Ohm1_id abelCHS). by rewrite (Ohm1_cyclic_pgroup_prime _ (abelem_pgroup abelCHS)). pose B := A^`(1) <*> [set a ^+ p.-1 | a in A]. have sBA: B \subset A. rewrite join_subG (der_sub 1 A) /=. by apply/subsetP=> _ /imsetP[a Aa ->]; rewrite groupX. have AutB: B \subset Aut R := subset_trans sBA AutA. suffices pB (X : {group {perm gT}}): X \subset B -> p^'.-group X -> X :=: 1. have cAbAb: abelian (A / 'O_p(A)). rewrite sub_der1_abelian // pcore_max ?der_normal //. apply/pgroupP=> q q_pr; apply: contraLR => p'q; rewrite -p'natE //. have [X sylX] := Sylow_exists q A^`(1); have [sXA' qX _] := and3P sylX. rewrite -partn_eq1 ?cardG_gt0 // -(card_Hall sylX). by rewrite (pB X) ?cards1 ?(pi_pgroup qX) ?(subset_trans sXA') ?joing_subl. rewrite cAbAb -(nilpotent_pcoreC p (abelian_nil cAbAb)) trivg_pcore_quotient. rewrite dprod1g pcore_pgroup; split=> //_ a Aa p'a. rewrite order_dvdn -cycle_eq1 [<[_]>]pB ?(pgroupS (cycleX _ _) p'a) //. by rewrite genS // sub1set inE orbC (imset_f (expgn^~ _)). move=> sXB p'X; have AutX := subset_trans sXB AutB. pose toX := ([Aut R] \ AutX)%gact; pose CX := 'C_(H | toX)(X). suffices sHCX: H \subset CX. rewrite -(setIid X) coprime_TIg ?(pnat_coprime (pgroupS _ pCH)) //. by rewrite subsetIidl gacent_ract setIid gacentC in sHCX. elim: _.+1 {1 2 4 6}H (charH) (subxx H) (ltnSn #|H|) => // n IHn L charL sLH. rewrite ltnS => leLn; have sLR := char_sub charL; pose K := [~: L, R]. wlog ntL: / L :!=: 1 by case: eqP => [-> | _ -> //]; rewrite sub1G. have charK: K \char R by rewrite charR ?char_refl. have ltKL: K \proper L. have nLR: R \subset 'N_R(L) by rewrite subsetIidl char_norm. exact: nil_comm_properl nilR sLR ntL nLR. have [sKL sKR] := (proper_sub ltKL, char_sub charK). have [sKH pK] := (subset_trans sKL sLH, pgroupS sKR pR : p.-group K). have nsKH: K <| H := normalS sKH sHR (char_normal charK). have sKCX: K \subset CX by rewrite IHn ?(leq_trans (proper_card ltKL)) ?leLn. have pL := pgroupS sLR pR; have nKL: L \subset 'N(K) := commg_norml _ _. have{pS cSS} oLb: #|L / K| = p. have [v defS] := cyclicP cycS; rewrite defS cycle_subG in sSR. have ntLb: L / K != 1 by rewrite -subG1 quotient_sub1 ?proper_subn. have [_ p_dv_Lb _] := pgroup_pdiv (quotient_pgroup _ pL) ntLb. apply/eqP; rewrite eqn_leq {p_dv_Lb}(dvdn_leq _ p_dv_Lb) // andbT. rewrite -divg_normal ?(normalS sKL sLH nsKH) // leq_divLR ?cardSg //= -/K. rewrite -(card_lcoset K v) -(LagrangeI L 'C(S)) -indexgI /= -oCHS /K commGC. rewrite {2}defS cent_cycle index_cent1 leq_mul ?subset_leq_card ?setSI //. by apply/subsetP=> vx; case/imsetP=> x Lx ->; rewrite mem_lcoset mem_commg. have cycLb: cyclic (L / K) by rewrite prime_cyclic ?oLb. rewrite -(quotientSGK _ sKCX) // quotientGI // subsetI quotientS //= -/K. have actsXK: [acts X, on K | toX] by rewrite acts_ract subxx acts_char. rewrite ext_coprime_quotient_cent ?(pnat_coprime pK p'X) ?(pgroup_sol pK) //. have actsAL : {acts A, on group L | [Aut R]} by apply: gacts_char. have sAD: A \subset qact_dom <[actsAL]> [~: L, R]. by rewrite qact_domE // acts_actby subxx (setIidPr sKL) acts_char. suffices cLbX: X \subset 'C(L / K | <[actsAL]> / _). rewrite gacentE ?qact_domE // subsetI quotientS //=. apply/subsetP=> Ku LbKu; rewrite inE; apply/subsetP=> x Xx; rewrite inE. have [Dx cLx] := setIdP (subsetP cLbX x Xx); have [Ax _] := setIdP Dx. rewrite inE in cLx; have:= subsetP cLx Ku LbKu; rewrite inE /=. have [u Nu Lu ->] := morphimP LbKu. by rewrite !{1}qactE // ?actbyE // qact_domE ?(subsetP actsXK). rewrite (subset_trans sXB) // astab_range -ker_actperm gen_subG. rewrite -sub_morphim_pre; last by rewrite -gen_subG ?(subset_trans sBA). rewrite morphimU subUset morphim_der // (sameP trivgP derG1P). rewrite (abelianS _ (Aut_cyclic_abelian cycLb)); last first. exact: subset_trans (morphim_sub _ _) (im_actperm_Aut _). apply/subsetP=> _ /morphimP[_ _ /imsetP[x Ax ->] ->]. have Dx := subsetP sAD x Ax; rewrite inE morphX //= -order_dvdn. apply: dvdn_trans (order_dvdG (actperm_Aut _ Dx)) _. by rewrite card_Aut_cyclic // oLb (@totient_pfactor p 1) ?muln1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)