proposition: Theorem der1_Aut_rank2_pgroup gT p (R : {group gT}) (A : {group {perm gT}}) : p.-group R -> odd #|R| -> 'r(R) <= 2 -> A \subset Aut R -> solvable A -> odd #|A| -> p.-group A^`(1).
proof: Proof. move=> pR oddR rR AutA solA oddA. without loss ntR: / R :!=: 1. case: eqP AutA => [-> | ntR _ -> //]; rewrite Aut1. by move/trivgP=> ->; rewrite derg1 commG1 pgroup1. have [p_pr _ _] := pgroup_pdiv pR ntR; have p_gt1 := prime_gt1 p_pr. have{ntR oddR} [H [charH _] _ eH pCH] := critical_odd pR oddR ntR. have sHR := char_sub charH; have pH := pgroupS sHR pR. have{rR} rH: 'r(H) <= 2 := leq_trans (rankS (char_sub charH)) rR. have dimH: logn p #|H| <= 3 by rewrite rank2_exponent_p_p3group ?eH. have{eH} ntH: H :!=: 1 by rewrite trivg_exponent eH gtnNdvd. have charP := Phi_char H; have [sPH nPH] := andP (Phi_normal H : 'Phi(H) <| H). have nHA: {acts A, on group H | [Aut R]} := gacts_char _ AutA charH. pose B := 'C(H | <[nHA]>); pose V := H / 'Phi(H); pose C := 'C(V | <[nHA]> / _). have{pCH} pB: p.-group B. by rewrite (pgroupS _ pCH) //= astab_actby setIid subsetIr. have s_p'C_B X: gval X \subset C -> p^'.-group X -> X \subset B. move=> sXC p'X; have [sDX _] := subsetIP sXC; have [sXA _] := subsetIP sDX. rewrite -gacentC //; apply/setIidPl; rewrite -[H :&: _]genGid //. apply: Phi_nongen; apply/eqP; rewrite eqEsubset join_subG sPH subsetIl. rewrite -quotientYK 1?subIset ?nPH //= -sub_quotient_pre //= -/V gacentIim. have pP := pgroupS sPH pH; have coPX := pnat_coprime pP p'X. rewrite -(setIid X) -(gacent_ract _ sXA). rewrite ext_coprime_quotient_cent ?(pgroup_sol pP) ?acts_char //. have domXb: X \subset qact_dom (<[nHA]> \ sXA) 'Phi(H). by rewrite qact_domE ?acts_char. rewrite gacentE // subsetIidl -/V; apply/subsetP=> v Vv; apply/afixP=> a Xa. have [cVa dom_a] := (subsetP sXC a Xa, subsetP domXb a Xa). have [x Nx Hx def_v] := morphimP Vv; rewrite {1}def_v qactE //=. by rewrite -qactE ?(astab_dom cVa) ?(astab_act cVa) -?def_v. have{B pB s_p'C_B} pC : p.-group C. apply/pgroupP=> q q_pr /Cauchy[] // a Ca oa; apply: wlog_neg => p'q. apply: (pgroupP pB) => //; rewrite -oa cardSg // s_p'C_B ?cycle_subG //. by rewrite /pgroup -orderE oa pnatE. have nVA: A \subset qact_dom <[nHA]> 'Phi(H) by rewrite qact_domE // acts_char. have nCA: A \subset 'N(C). by rewrite (subset_trans _ (astab_norm _ _)) // astabs_range. suffices{pC nCA}: p.-group (A / C)^`(1). by rewrite -quotient_der ?pquotient_pgroup // gFsub_trans. pose toAV := ((<[nHA]> / 'Phi(H)) \ nVA)%gact. have defC: C = 'C(V | toAV). by symmetry; rewrite astab_ract; apply/setIidPr; rewrite subIset ?subsetIl. have abelV: p.-abelem V := Phi_quotient_abelem pH. have ntV: V != 1 by rewrite -subG1 quotient_sub1 // proper_subn ?Phi_proper. have: 'r(V) \in iota 1 2. rewrite mem_iota rank_gt0 ntV (rank_abelem abelV). have [abelH | not_abelH] := boolP (p.-abelem H). by rewrite ltnS (leq_trans _ rH) // (rank_abelem abelH) logn_quotient. by rewrite (leq_trans _ dimH) // ltn_log_quotient // (trivg_Phi pH). rewrite !inE; case/pred2P=> dimV. have isoAb: A / C \isog actperm toAV @* A. by rewrite defC astab_range -ker_actperm first_isog. rewrite (derG1P _) ?pgroup1 // (isog_abelian isoAb). apply: abelianS (im_actperm_Aut _) (Aut_cyclic_abelian _). by rewrite (abelem_cyclic abelV) -rank_abelem ?dimV. pose Vb := sdpair1 toAV @* V; pose Ab := sdpair2 toAV @* A. have [injV injA] := (injm_sdpair1 toAV, injm_sdpair2 toAV). have abelVb: p.-abelem Vb := morphim_abelem _ abelV. have ntVb: Vb != 1 by rewrite morphim_injm_eq1. have nVbA: Ab \subset 'N(Vb) := im_sdpair_norm toAV. pose rV := morphim_repr (abelem_repr abelVb ntVb nVbA) (subxx A). have{defC} <-: rker rV = C; last move: rV. rewrite rker_morphim rker_abelem morphpreI morphimK //=. by rewrite (trivgP injA) mul1g -astabEsd // defC astab_ract 2!setIA !setIid. have ->: 'dim Vb = 2 by rewrite (dim_abelemE abelVb) // card_injm -?rank_abelem. move=> rV; rewrite -(eq_pgroup _ (GRing.charf_eq (char_Fp p_pr))). by apply: der1_odd_GL2_charf (kquo_mx_faithful rV); rewrite !morphim_odd. 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)