diff options
| author | Enrico Tassi | 2018-04-17 16:57:13 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-17 16:57:13 +0200 |
| commit | eaa90cf9520e43d0b05fc6431a479e6b9559ef0e (patch) | |
| tree | 8499953a468a8d8be510dd0d60232cbd8984c1ec /mathcomp/odd_order/BGsection14.v | |
| parent | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff) | |
move odd_order to its own repository
Diffstat (limited to 'mathcomp/odd_order/BGsection14.v')
| -rw-r--r-- | mathcomp/odd_order/BGsection14.v | 2520 |
1 files changed, 0 insertions, 2520 deletions
diff --git a/mathcomp/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v deleted file mode 100644 index bc6f9e2..0000000 --- a/mathcomp/odd_order/BGsection14.v +++ /dev/null @@ -1,2520 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype. -From mathcomp -Require Import bigop finset prime fingroup morphism perm automorphism quotient. -From mathcomp -Require Import action gproduct gfunctor pgroup cyclic center commutator. -From mathcomp -Require Import gseries nilpotent sylow abelian maximal hall frobenius. -From mathcomp -Require Import ssralg ssrnum ssrint rat. -From mathcomp -Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6. -From mathcomp -Require Import BGsection7 BGsection9 BGsection10 BGsection12 BGsection13. - -(******************************************************************************) -(* This file covers B & G, section 14, starting with the definition of the *) -(* sigma-decomposition of elements, sigma-supergroups, and basic categories *) -(* of maximal subgroups: *) -(* sigma_decomposition x == the set of nontrivial constituents x.`_\sigma(M), *) -(* with M ranging over maximal sugroups of G. *) -(* (x is the product of these). *) -(* \ell_\sigma[x] == #|sigma_decomposition x|. *) -(* 'M_\sigma(X) == the set of maximal subgroups M such that X is a *) -(* a subset of M`_\sigma. *) -(* 'M_\sigma[x] := 'M_\sigma(<[x]>) *) -(* \kappa(M) == the set of primes p in \tau1(M) or \tau3(M), such *) -(* that 'C_(M`_\sigma)(P) != 1 for some subgroup of *) -(* M of order p, i.e., the primes for which M fails *) -(* to be a Frobenius group. *) -(* kappa_complement M U K <-> U and K are respectively {kappa, sigma}'- and *) -(* kappa-Hall subgroups of M, whose product is a *) -(* sigma-complement of M. This corresponds to the *) -(* notation introduced at the start of section 15 in *) -(* B & G, but is needed here to capture the use of *) -(* bound variables of 14.2(a) in the statement of *) -(* Lemma 14.12. *) -(* 'M_'F == the set of maximal groups M for which \kappa(M) *) -(* is empty, i.e., the maximal groups of Frobenius *) -(* type (in the final classification, this becomes *) -(* Type I). *) -(* 'M_'P == the complement to 'M_'F in 'M, i.e., the set of M *) -(* for which at least E1 has a proper prime action *) -(* on M`_\sigma. *) -(* 'M_'P1 == the set of maximal subgroups M such that \pi(M) *) -(* is the disjoint union of \sigma(M) and \kappa(M), *) -(* i.e., for which the entire complement acts in a *) -(* prime manner (this troublesome subset of 'M_'P is *) -(* ultimately refined into Types III-V in the final *) -(* classification). *) -(* 'M_'P2 == the complement to 'M_'P1 in 'M_'P; this becomes *) -(* Type II in the final classification. *) -(* 'N[x] == if x != 1 and 'M_\sigma[x] > 1, the unique group *) -(* in 'M('C[x]) (see B & G, Theorem 14.4), and the *) -(* trivial group otherwise. *) -(* 'R[x] := 'C_('N[x]`_\sigma)[x]; if \ell_\sigma[x] == 1, *) -(* this is the normal Hall subgroup of 'C[x] that *) -(* acts sharply transitively by conjugagtion on *) -(* 'M`_\sigma[x] (again, by Theorem 14.4). *) -(* M^~~ == the union of all the cosets x *: 'R[x], with x *) -(* ranging over (M`_\sigma)^#. This will become the *) -(* support set for the Dade isometry for M in the *) -(* character theory part of the proof. *) -(* It seems 'R[x] and 'N[x]`_\sigma play a somewhat the role of a signalizer *) -(* functor in the FT proof; in particular 'R[x] will be used to construct the *) -(* Dade isometry in the character theory part of the proof. *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Local Open Scope ring_scope. -Local Open Scope nat_scope. -Import GRing.Theory Num.Theory GroupScope. - -Section Definitons. - -Variable gT : minSimpleOddGroupType. -Implicit Type x : gT. -Implicit Type M X : {set gT}. - -Definition sigma_decomposition x := - [set x.`_\sigma(M) | M : {group gT} in 'M]^#. -Definition sigma_length x := #|sigma_decomposition x|. - -Definition sigma_mmax_of X := [set M in 'M | X \subset M`_\sigma]. - -Definition FT_signalizer_base x := - if #|sigma_mmax_of <[x]>| > 1 then odflt 1%G (pick (mem 'M('C[x]))) else 1%G. - -Definition FT_signalizer x := 'C_((FT_signalizer_base x)`_\sigma)[x]. - -Definition sigma_cover M := \bigcup_(x in (M`_\sigma)^#) x *: FT_signalizer x. - -Definition tau13 M := [predU \tau1(M) & \tau3(M)]. - -Fact kappa_key : unit. Proof. by []. Qed. -Definition kappa_def M : nat_pred := - [pred p in tau13 M | [exists P in 'E_p^1(M), 'C_(M`_\sigma)(P) != 1]]. -Definition kappa := locked_with kappa_key kappa_def. -Canonical kappa_unlockable := [unlockable fun kappa]. - -Definition sigma_kappa M := [predU \sigma(M) & kappa M]. - -Definition kappa_complement (M U K : {set gT}) := - [/\ (sigma_kappa M)^'.-Hall(M) U, (kappa M).-Hall(M) K & group_set (U * K)]. - -Definition TypeF_maxgroups := [set M in 'M | (kappa M)^'.-group M]. - -Definition TypeP_maxgroups := 'M :\: TypeF_maxgroups. - -Definition TypeP1_maxgroups := - [set M in TypeP_maxgroups | (sigma_kappa M).-group M]. - -Definition TypeP2_maxgroups := TypeP_maxgroups :\: TypeP1_maxgroups. - -End Definitons. - -Notation "\ell_ \sigma ( x )" := (sigma_length x) - (at level 8, format "\ell_ \sigma ( x )") : group_scope. - -Notation "''M_' \sigma ( X )" := (sigma_mmax_of X) - (at level 8, format "''M_' \sigma ( X )") : group_scope. - -Notation "''M_' \sigma [ x ]" := (sigma_mmax_of <[x]>) - (at level 8, format "''M_' \sigma [ x ]") : group_scope. - -Notation "''N' [ x ]" := (FT_signalizer_base x) - (at level 8, format "''N' [ x ]") : group_scope. - -Notation "''R' [ x ]" := (FT_signalizer x) - (at level 8, format "''R' [ x ]") : group_scope. - -Notation "M ^~~" := (sigma_cover M) - (at level 2, format "M ^~~") : group_scope. - -Notation "\tau13 ( M )" := (tau13 M) - (at level 8, format "\tau13 ( M )") : group_scope. - -Notation "\kappa ( M )" := (kappa M) - (at level 8, format "\kappa ( M )") : group_scope. - -Notation "\sigma_kappa ( M )" := (sigma_kappa M) - (at level 8, format "\sigma_kappa ( M )") : group_scope. - -Notation "''M_' ''F'" := (TypeF_maxgroups _) - (at level 2, format "''M_' ''F'") : group_scope. - -Notation "''M_' ''P'" := (TypeP_maxgroups _) - (at level 2, format "''M_' ''P'") : group_scope. - -Notation "''M_' ''P1'" := (TypeP1_maxgroups _) - (at level 2, format "''M_' ''P1'") : group_scope. - -Notation "''M_' ''P2'" := (TypeP2_maxgroups _) - (at level 2, format "''M_' ''P2'") : group_scope. - -Section Section14. - -Variable gT : minSimpleOddGroupType. -Local Notation G := (TheMinSimpleOddGroup gT). -Implicit Types p q q_star r : nat. -Implicit Types x y z : gT. -Implicit Types A E H K L M Mstar N P Q Qstar R S T U V W X Y Z : {group gT}. - -(* Basic properties of the sigma decomposition. *) -Lemma mem_sigma_decomposition x M (xM := x.`_\sigma(M)) : - M \in 'M -> xM != 1 -> xM \in sigma_decomposition x. -Proof. by move=> maxM nt_xM; rewrite !inE nt_xM; apply: mem_imset. Qed. - -Lemma sigma_decompositionJ x z : - sigma_decomposition (x ^ z) = sigma_decomposition x :^ z. -Proof. -rewrite conjD1g -[_ :^ z]imset_comp; congr _^#. -by apply: eq_in_imset => M maxM; rewrite /= consttJ. -Qed. - -Lemma ell_sigmaJ x z : \ell_\sigma(x ^ z) = \ell_\sigma(x). -Proof. by rewrite /sigma_length sigma_decompositionJ cardJg. Qed. - -Lemma sigma_mmaxJ M (X : {set gT}) z : - ((M :^ z)%G \in 'M_\sigma(X :^ z)) = (M \in 'M_\sigma(X)). -Proof. by rewrite inE mmaxJ MsigmaJ conjSg !inE. Qed. - -Lemma card_sigma_mmaxJ (X : {set gT}) z : - #|'M_\sigma(X :^ z)| = #|'M_\sigma(X)|. -Proof. -rewrite -(card_setact 'JG _ z^-1) setactVin ?inE //. -by apply: eq_card => M; rewrite inE sigma_mmaxJ. -Qed. - -Lemma sigma_decomposition_constt' x M (sM := \sigma(M)) : - M \in 'M -> sigma_decomposition x.`_sM^' = sigma_decomposition x :\ x.`_sM. -Proof. -move=> maxM; apply/setP=> y; rewrite !inE andbCA; apply: andb_id2l => nty. -apply/imsetP/andP=> [ | [neq_y_xM /imsetP]] [L maxL def_y]. - have not_sMy: ~~ sM.-elt y. - apply: contra nty => sMy; rewrite -order_eq1 (pnat_1 sMy) // def_y. - by apply: p_eltX; apply: p_elt_constt. - split; first by apply: contraNneq not_sMy => ->; apply: p_elt_constt. - have notMGL: gval L \notin M :^: G. - apply: contra not_sMy; rewrite def_y; case/imsetP=> z _ ->. - by rewrite (eq_constt _ (sigmaJ M z)) p_elt_constt. - apply/imsetP; exists L; rewrite // def_y sub_in_constt // => p _ sLp. - by apply: contraFN (sigma_partition maxM maxL notMGL p) => sMp; apply/andP. -exists L; rewrite ?sub_in_constt // => p _ sLp. -suffices notMGL: gval L \notin M :^: G. - by apply: contraFN (sigma_partition maxM maxL notMGL p) => sMp; apply/andP. -apply: contra neq_y_xM; rewrite def_y => /imsetP[z _ ->]. -by rewrite (eq_constt _ (sigmaJ M z)). -Qed. - -(* General remarks about the sigma-decomposition, p. 105 of B & G. *) -Remark sigma_mmax_exists p : - p \in \pi(G) -> {M : {group gT} | M \in 'M & p \in \sigma(M)}. -Proof. -move=> piGp; have [P sylP] := Sylow_exists p [set: gT]. -have ntP: P :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylP) p_rank_gt0. -have ltPG: P \proper G := mFT_pgroup_proper (pHall_pgroup sylP). -have [M maxNM] := mmax_exists (mFT_norm_proper ntP ltPG). -have{maxNM} [maxM sNM] := setIdP maxNM; have sPM := subset_trans (normG P) sNM. -have{sylP} sylP := pHall_subl sPM (subsetT M) sylP. -by exists M => //; apply/exists_inP; exists P. -Qed. - -Lemma ell_sigma0P x : reflect (x = 1) (\ell_\sigma(x) == 0). -Proof. -rewrite cards_eq0 setD_eq0. -apply: (iffP idP) => [x1 | ->]; last first. - by apply/subsetP=> _ /imsetP[M _ ->]; rewrite constt1 inE. -rewrite -(prod_constt x) big1_seq //= => p _; apply: contraTeq x1 => nt_xp. -have piXp: p \in \pi(#[x]) by rewrite -p_part_gt1 -order_constt order_gt1. -have [M maxM sMp] := sigma_mmax_exists (piSg (subsetT _) piXp). -apply/subsetPn; exists (x.`_(\sigma(M))); first exact: mem_imset. -by rewrite (sameP set1P constt1P); apply: contraL sMp => /pnatPpi; apply. -Qed. - -Remark sigma_decomposition_subG x H : - x \in H -> sigma_decomposition x \subset H. -Proof. -by move=> Hx; apply/subsetP=> _ /setD1P[_ /imsetP[M _ ->]]; apply: groupX. -Qed. - -Remark prod_sigma_decomposition x : - \prod_(x_sM in sigma_decomposition x) x_sM = x. -Proof. -rewrite -big_filter filter_index_enum; set e := enum _. -have: uniq e := enum_uniq _; have: e =i sigma_decomposition x := mem_enum _. -elim: {x}e (x) => [|y e IHe] x def_e /= Ue. - by rewrite big_nil (ell_sigma0P x _) //; apply/pred0P; apply: fsym. -have{Ue} [not_e_y Ue] := andP Ue. -have [nty] := setD1P (etrans (fsym def_e y) (mem_head _ _)). -case/imsetP=> M maxM def_y; rewrite big_cons -(consttC \sigma(M) x) -def_y. -congr (y * _); apply: IHe Ue => z; rewrite sigma_decomposition_constt' //. -rewrite -def_y inE -def_e !inE andb_orr andNb andb_idl //. -by apply: contraTneq => ->. -Qed. - -Lemma ell1_decomposition x : - \ell_\sigma(x) == 1%N -> sigma_decomposition x = [set x]. -Proof. -case/cards1P=> y sdx_y. -by rewrite -{2}[x]prod_sigma_decomposition sdx_y big_set1. -Qed. - -Lemma Msigma_ell1 M x : - M \in 'M -> x \in (M`_\sigma)^# -> \ell_\sigma(x) == 1%N. -Proof. -move=> maxM /setD1P[ntx Ms_x]; apply/cards1P. -have sMx: \sigma(M).-elt x := mem_p_elt (pcore_pgroup _ _) Ms_x. -have def_xM: x.`_(\sigma(M)) = x := constt_p_elt sMx. -exists x; apply/eqP; rewrite eqEsubset sub1set !inE ntx -setD_eq0 /=. -rewrite -{2 3}def_xM -sigma_decomposition_constt' // (constt1P _) ?p_eltNK //. -by rewrite -cards_eq0 (sameP (ell_sigma0P 1) eqP) eqxx; apply: mem_imset. -Qed. - -Remark ell_sigma1P x : - reflect (x != 1 /\ 'M_\sigma[x] != set0) (\ell_\sigma(x) == 1%N). -Proof. -apply: (iffP idP) => [ell1x | [ntx]]; last first. - case/set0Pn=> M /setIdP[maxM]; rewrite cycle_subG => Ms_x. - by rewrite (Msigma_ell1 maxM) // in_setD1 ntx. -have sdx_x: x \in sigma_decomposition x by rewrite ell1_decomposition ?set11. -have{sdx_x} [ntx sdx_x] := setD1P sdx_x; split=> //; apply/set0Pn. -have{sdx_x} [M maxM def_x] := imsetP sdx_x; rewrite // -cycle_eq1 in ntx. -have sMx: \sigma(M).-elt x by rewrite def_x p_elt_constt. -have [[z sXzMs] _] := sigma_Jsub maxM sMx ntx. -by exists (M :^ z^-1)%G; rewrite inE mmaxJ maxM MsigmaJ -sub_conjg. -Qed. - -Remark ell_sigma_le1 x :(\ell_\sigma(x) <= 1) = ('M_\sigma[x] != set0). -Proof. -rewrite -[_ <= 1](mem_iota 0 2) !inE (sameP (ell_sigma0P x) eqP). -rewrite (sameP (ell_sigma1P x) andP); case: eqP => //= ->; symmetry. -have [M max1M] := mmax_exists (mFT_pgroup_proper (@pgroup1 gT 2)). -have [maxM _] := setIdP max1M; apply/set0Pn; exists M. -by rewrite inE maxM cycle1 sub1G. -Qed. - -(* Basic properties of \kappa and the maximal group subclasses. *) -Lemma kappaJ M x : \kappa(M :^ x) =i \kappa(M). -Proof. -move=> p; rewrite unlock 3!{1}inE /= tau1J tau3J; apply: andb_id2l => _. -apply/exists_inP/exists_inP=> [] [P EpP ntCMsP]. - rewrite -(conjsgK x M); exists (P :^ x^-1)%G; first by rewrite pnElemJ. - by rewrite MsigmaJ centJ -conjIg -subG1 sub_conjg conjs1g subG1. -exists (P :^ x)%G; first by rewrite pnElemJ. -by rewrite MsigmaJ centJ -conjIg -subG1 sub_conjg conjs1g subG1. -Qed. - -Lemma kappa_tau13 M p : p \in \kappa(M) -> (p \in \tau1(M)) || (p \in \tau3(M)). -Proof. by rewrite unlock => /andP[]. Qed. - -Lemma kappa_sigma' M : {subset \kappa(M) <= \sigma(M)^'}. -Proof. by move=> p /kappa_tau13/orP[] /andP[]. Qed. - -Remark rank_kappa M p : p \in \kappa(M) -> 'r_p(M) = 1%N. -Proof. by case/kappa_tau13/orP=> /and3P[_ /eqP]. Qed. - -Lemma kappa_pi M : {subset \kappa(M) <= \pi(M)}. -Proof. by move=> p kMp; rewrite -p_rank_gt0 rank_kappa. Qed. - -Remark kappa_nonregular M p P : - p \in \kappa(M) -> P \in 'E_p^1(M) -> 'C_(M`_\sigma)(P) != 1. -Proof. -move=> kMp EpP; have rpM := rank_kappa kMp. -have [sPM abelP oP] := pnElemPcard EpP; have [pP _] := andP abelP. -have [Q EpQ nregQ]: exists2 Q, Q \in 'E_p^1(M) & 'C_(M`_\sigma)(Q) != 1. - by apply/exists_inP; rewrite unlock in kMp; case/andP: kMp. -have [sQM abelQ oQ] := pnElemPcard EpQ; have [pQ _] := andP abelQ. -have [S sylS sQS] := Sylow_superset sQM pQ; have [_ pS _] := and3P sylS. -have [x Mx sPxS] := Sylow_Jsub sylS sPM pP. -rewrite -(inj_eq (@conjsg_inj _ x)) conjs1g conjIg -centJ. -rewrite (normsP (normal_norm (pcore_normal _ _))) // (subG1_contra _ nregQ) //. -rewrite setIS ?centS // -(cardSg_cyclic _ sPxS sQS) ?cardJg ?oP ?oQ //. -by rewrite (odd_pgroup_rank1_cyclic pS) ?mFT_odd // (p_rank_Sylow sylS) rpM. -Qed. - -Lemma ex_kappa_compl M K : - M \in 'M -> \kappa(M).-Hall(M) K -> - exists U : {group gT}, kappa_complement M U K. -Proof. -move=> maxM hallK; have [sKM kK _] := and3P hallK. -have s'K: \sigma(M)^'.-group K := sub_pgroup (@kappa_sigma' M) kK. -have [E hallE sKE] := Hall_superset (mmax_sol maxM) sKM s'K. -pose sk' := \sigma_kappa(M)^'. -have [U hallU] := Hall_exists sk' (sigma_compl_sol hallE). -exists U; split=> //. - by apply: subHall_Hall hallE _ hallU => p; case/norP. -suffices ->: U * K = E by apply: groupP. -have [[sUE sk'U _] [sEM s'E _]] := (and3P hallU, and3P hallE). -apply/eqP; rewrite eqEcard mulG_subG sUE sKE /= coprime_cardMg; last first. - by apply: p'nat_coprime (sub_pgroup _ sk'U) kK => p; case/norP. -rewrite -(partnC \kappa(M) (cardG_gt0 E)) -{2}(part_pnat_id s'E) mulnC. -rewrite -(card_Hall (pHall_subl sKE sEM hallK)) leq_mul // -partnI. -by rewrite -(@eq_partn sk') -?(card_Hall hallU) // => p; apply: negb_or. -Qed. - -Lemma FtypeP M : reflect (M \in 'M /\ \kappa(M) =i pred0) (M \in 'M_'F). -Proof. -do [apply: (iffP setIdP) => [] [maxM k'M]; split] => // [p|]. - by apply/idP=> /= kMp; case/negP: (pnatPpi k'M (kappa_pi kMp)). -by apply/pgroupP=> p _ _; rewrite inE /= k'M. -Qed. - -Lemma PtypeP M : reflect (M \in 'M /\ exists p, p \in \kappa(M)) (M \in 'M_'P). -Proof. -apply: (iffP setDP) => [[maxM kM] | [maxM [p kMp]]]; split => //. - rewrite inE maxM !negb_and cardG_gt0 /= all_predC negbK in kM. - by have [p _ kMp] := hasP kM; exists p. -by apply/FtypeP=> [[_ kM0]]; rewrite kM0 in kMp. -Qed. - -Lemma trivg_kappa M K : - M \in 'M -> \kappa(M).-Hall(M) K -> (K :==: 1) = (M \in 'M_'F). -Proof. -by move=> maxM hallK; rewrite inE maxM trivg_card1 (card_Hall hallK) partG_eq1. -Qed. - -(* Could go in Section 10. *) -Lemma not_sigma_mmax M : M \in 'M -> ~~ \sigma(M).-group M. -Proof. -move=> maxM; apply: contraL (mmax_sol maxM); rewrite negb_forall_in => sM. -apply/existsP; exists M; rewrite mmax_neq1 // subsetIidl andbT. -apply: subset_trans (Msigma_der1 maxM). -by rewrite (sub_Hall_pcore (Msigma_Hall maxM)). -Qed. - -Lemma trivg_kappa_compl M U K : - M \in 'M -> kappa_complement M U K -> (U :==: 1) = (M \in 'M_'P1). -Proof. -move=> maxM [hallU _ _]; symmetry. -rewrite 3!inE maxM /= trivg_card1 (card_Hall hallU) partG_eq1 pgroupNK andbT. -apply: andb_idl => skM; apply: contra (not_sigma_mmax maxM). -by apply: sub_in_pnat => p /(pnatPpi skM)/orP[] // kMp /negP. -Qed. - -Lemma FtypeJ M x : ((M :^ x)%G \in 'M_'F) = (M \in 'M_'F). -Proof. by rewrite inE mmaxJ pgroupJ (eq_p'group _ (kappaJ M x)) !inE. Qed. - -Lemma PtypeJ M x : ((M :^ x)%G \in 'M_'P) = (M \in 'M_'P). -Proof. by rewrite !in_setD mmaxJ FtypeJ. Qed. - -Lemma P1typeJ M x : ((M :^ x)%G \in 'M_'P1) = (M \in 'M_'P1). -Proof. -rewrite inE PtypeJ pgroupJ [M \in 'M_'P1]inE; congr (_ && _). -by apply: eq_pgroup => p; rewrite inE /= kappaJ sigmaJ. -Qed. - -Lemma P2typeJ M x : ((M :^ x)%G \in 'M_'P2) = (M \in 'M_'P2). -Proof. by rewrite in_setD PtypeJ P1typeJ -in_setD. Qed. - -(* This is B & G, Lemma 14.1. *) -Lemma sigma'_kappa'_facts M p S (A := 'Ohm_1(S)) (Ms := M`_\sigma) : - M \in 'M -> p.-Sylow(M) S -> - [&& p \in \pi(M), p \notin \sigma(M) & p \notin \kappa(M)] -> - [/\ M \in 'M_'F :|: 'M_'P2, logn p #|A| <= 2, 'C_Ms(A) = 1 & nilpotent Ms]. -Proof. -move=> maxM sylS /and3P[piMp sM'p kM'p]; have [sSM pS _] := and3P sylS. -rewrite 8!(maxM, inE) /= !andbT negb_and orb_andr orbN andbT negbK. -rewrite (contra (fun skM => pnatPpi skM piMp)) ?orbT; last exact/norP. -rewrite partition_pi_mmax // (negPf sM'p) orbF orbCA in piMp. -have{piMp} [t2p | t13p] := orP piMp. - rewrite (tau2_Msigma_nil maxM t2p); have [_ rpM] := andP t2p. - have{rpM} rS: 2 <= 'r_p(S) by rewrite (p_rank_Sylow sylS) (eqP rpM). - have [B EpB] := p_rank_geP rS; have{EpB} [sBS abelB dimB] := pnElemP EpB. - have EpB: B \in 'E_p^2(M) by rewrite !inE abelB dimB (subset_trans sBS). - have [defB _ regB _ _] := tau2_context maxM t2p EpB. - by rewrite /A -dimB; have [_ [|->]] := defB S sylS. -have [ntS cycS]: S :!=: 1 /\ cyclic S. - rewrite (odd_pgroup_rank1_cyclic pS) ?mFT_odd // (p_rank_Sylow sylS). - apply/andP; rewrite -rank_gt0 (rank_Sylow sylS) -eqn_leq eq_sym. - by rewrite -2!andb_orr orNb andbT inE /= sM'p in t13p. -have [p_pr _ _] := pgroup_pdiv pS ntS. -have oA: #|A| = p by rewrite (Ohm1_cyclic_pgroup_prime cycS pS). -have sAM: A \subset M by apply: gFsub_trans. -have regA: 'C_Ms(A) = 1. - apply: contraNeq kM'p => nregA; rewrite unlock; apply/andP; split=> //. - by apply/exists_inP; exists [group of A]; rewrite ?p1ElemE // !inE sAM oA /=. -have defMsA: Ms ><| A = Ms <*> A. - rewrite sdprodEY ?coprime_TIg ?(subset_trans sAM) ?gFnorm // oA. - by rewrite (pnat_coprime (pcore_pgroup _ _)) ?pnatE. -rewrite (prime_Frobenius_sol_kernel_nil defMsA) ?oA ?(pfactorK 1) //. -by rewrite (solvableS _ (mmax_sol maxM)) // join_subG pcore_sub. -Qed. - -Lemma notP1type_Msigma_nil M : - (M \in 'M_'F) || (M \in 'M_'P2) -> nilpotent M`_\sigma. -Proof. -move=> notP1maxM; suffices [maxM]: M \in 'M /\ ~~ \sigma_kappa(M).-group M. - rewrite negb_and cardG_gt0 => /allPn[p piMp /norP[s'p k'p]]. - by have [S /sigma'_kappa'_facts[] //] := Sylow_exists p M; apply/and3P. -have [/setIdP[maxM k'M] | /setDP[PmaxM]] := orP notP1maxM; last first. - by rewrite inE PmaxM; case/setDP: PmaxM. -split=> //; apply: contra (not_sigma_mmax maxM). -by apply: sub_in_pnat => p piMp /orP[] // /idPn[]; apply: (pnatPpi k'M). -Qed. - -(* This is B & G, Proposition 14.2. *) -Proposition Ptype_structure M K (Ms := M`_\sigma) (Kstar := 'C_Ms(K)) : - M \in 'M_'P -> \kappa(M).-Hall(M) K -> - [/\ (*a*) exists2 U : {group gT}, - kappa_complement M U K /\ Ms ><| (U ><| K) = M - & [/\ abelian U, semiprime Ms K & semiregular U K], - (*b*) (*1.2*) K \x Kstar = 'N_M(K) - /\ {in 'E^1(K), forall X, - (*1.1*) 'N_M(X) = 'N_M(K) - /\ (*2*) {in 'M('N(X)), forall Mstar, X \subset Mstar`_\sigma}}, - (*c*) Kstar != 1 /\ {in 'E^1(Kstar), forall X, 'M('C(X)) = [set M]}, - [/\ (*d*) {in ~: M, forall g, Kstar :&: M :^ g = 1} - /\ {in M :\: 'N_M(K), forall g, K :&: K :^ g = 1}, - (*e*) {in \pi(Kstar), forall p S, - p.-Sylow(M) S -> 'M(S) = [set M] /\ ~~ (S \subset Kstar)} - & (*f*) forall Y, \sigma(M).-group Y -> Y :&: Kstar != 1 -> Y \subset Ms] - & (*g*) M \in 'M_'P2 -> - [/\ \sigma(M) =i \beta(M), prime #|K|, nilpotent Ms - & normedTI Ms^# G M]]. -Proof. -move: @Kstar => Ks PmaxM hallK; have [maxM notFmaxM] := setDP PmaxM. -have sMs: \sigma(M).-group M`_\sigma := pcore_pgroup _ M. -have{notFmaxM} ntK: K :!=: 1 by rewrite (trivg_kappa maxM). -have [sKM kK _] := and3P hallK; have s'K := sub_pgroup (@kappa_sigma' M) kK. -have solM := mmax_sol maxM; have [E hallE sKE] := Hall_superset solM sKM s'K. -have [[sEM s'E _] [_ [E3 hallE3]]] := (and3P hallE, ex_tau13_compl hallE). -have [F1 hallF1] := Hall_exists \tau1(M) (solvableS sKM solM). -have [[sF1K t1F1 _] solE] := (and3P hallF1, sigma_compl_sol hallE). -have [E1 hallE1 sFE1] := Hall_superset solE (subset_trans sF1K sKE) t1F1. -have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. -have [[_ nsE3E] _ [cycE1 _] [defEl defE] _] := sigma_compl_context maxM complEi. -have [sE1E t1E1 _] := and3P hallE1; have sE1M := subset_trans sE1E sEM. -have [sE3E t3E3 _] := and3P hallE3; have sE3M := subset_trans sE3E sEM. -set part_a := exists2 U, _ & _; pose b1_hyp := {in 'E^1(K), forall X, X <| K}. -have [have_a nK1K ntE1 sE1K]: [/\ part_a, b1_hyp, E1 :!=: 1 & E1 \subset K]. - have [t1K | not_t1K] := boolP (\tau1(M).-group K). - have sKE1: K \subset E1 by rewrite (sub_pHall hallF1 t1K). - have prE1 := tau1_primact_Msigma maxM hallE hallE1. - have st1k: {subset \tau1(M) <= \kappa(M)}. - move=> p t1p; rewrite unlock 3!inE /= t1p /=. - have [X]: exists X, X \in 'E_p^1(E1). - apply/p_rank_geP; rewrite p_rank_gt0 /= (card_Hall hallE1). - by rewrite pi_of_part // inE /= (partition_pi_sigma_compl maxM) ?t1p. - rewrite -(setIidPr sE1M) pnElemI -setIdE => /setIdP[EpX sXE1]. - pose q := pdiv #|K|; have piKq: q \in \pi(K) by rewrite pi_pdiv cardG_gt1. - have /p_rank_geP[Y]: 0 < 'r_q(K) by rewrite p_rank_gt0. - rewrite -(setIidPr sKM) pnElemI -setIdE => /setIdP[EqY sYK]. - have ntCMsY := kappa_nonregular (pnatPpi kK piKq) EqY. - have [ntY sYE1] := (nt_pnElem EqY isT, subset_trans sYK sKE1). - apply/exists_inP; exists X; rewrite ?(subG1_contra _ ntCMsY) //=. - by rewrite (cent_semiprime prE1 sYE1 ntY) ?setIS ?centS. - have defK := sub_pHall hallK (sub_pgroup st1k t1E1) sKE1 sE1M. - split=> [|X||]; rewrite ?defK //; last first. - rewrite -defK; case/nElemP=> p /pnElemP[sXE1 _ _]. - by rewrite char_normal // sub_cyclic_char. - have [[U _ defU _] _ _ _] := sdprodP defE; rewrite defU in defE. - have [nsUE _ mulUE1 nUE1 _] := sdprod_context defE. - have [[_ V _ defV] _] := sdprodP defEl; rewrite defV. - have [_ <- nE21 _] := sdprodP defV => /mulGsubP[nE32 nE31] _. - have regUK: semiregular U K. - move=> y /setD1P[]; rewrite -cycle_subG -cent_cycle -order_gt1. - rewrite -pi_pdiv; move: (pdiv _) => p pi_y_p Ky. - have piKp := piSg Ky pi_y_p; have t1p := pnatPpi t1K piKp. - move: pi_y_p; rewrite -p_rank_gt0 => /p_rank_geP[Y] /=. - rewrite -{1}(setIidPr (subset_trans Ky sKE)) pnElemI -setIdE. - case/setIdP=> EpY sYy; have EpMY := subsetP (pnElemS _ _ sEM) Y EpY. - apply: contraNeq (kappa_nonregular (pnatPpi kK piKp) EpMY). - move/(subG1_contra (setIS U (centS sYy))). - have{y sYy Ky} sYE1 := subset_trans sYy (subset_trans Ky sKE1). - have ntY: Y :!=: 1 by apply: (nt_pnElem EpY). - rewrite -subG1 /=; have [_ <- _ tiE32] := sdprodP defU. - rewrite -subcent_TImulg ?subsetI ?(subset_trans sYE1) // mulG_subG. - rewrite !subG1 /= => /nandP[nregE3Y | nregE2Y]. - have pr13 := cent_semiprime (tau13_primact_Msigma maxM complEi _). - rewrite pr13 ?(subset_trans sYE1) ?joing_subr //; last first. - by move/cent_semiregular=> regE31; rewrite regE31 ?eqxx in nregE3Y. - pose q := pdiv #|'C_E3(Y)|. - have piE3q: q \in \pi(E3). - by rewrite (piSg (subsetIl E3 'C(Y))) // pi_pdiv cardG_gt1. - have /p_rank_geP[X]: 0 < 'r_q(M :&: E3). - by rewrite (setIidPr sE3M) p_rank_gt0. - rewrite pnElemI -setIdE => /setIdP[EqX sXE3]. - rewrite -subG1 -(_ : 'C_Ms(X) = 1) ?setIS ?centS //. - by rewrite (subset_trans sXE3) ?joing_subl. - apply: contraTeq (pnatPpi t3E3 piE3q) => nregMsX; apply: tau3'1. - suffices kq: q \in \kappa(M). - rewrite (pnatPpi t1K) //= (card_Hall hallK) pi_of_part //. - by rewrite inE /= kappa_pi. - rewrite unlock 3!inE /= (pnatPpi t3E3 piE3q) orbT /=. - by apply/exists_inP; exists X. - pose q := pdiv #|'C_E2(Y)|; have [sE2E t2E2 _] := and3P hallE2. - have piCE2Yq: q \in \pi('C_E2(Y)) by rewrite pi_pdiv cardG_gt1. - have [X]: exists X, X \in 'E_q^1(E :&: 'C_E2(Y)). - by apply/p_rank_geP; rewrite /= setIA (setIidPr sE2E) p_rank_gt0. - rewrite pnElemI -setIdE => /setIdP[EqX sXcE2Y]. - have t2q:= pnatPpi t2E2 (piSg (subsetIl _ _) piCE2Yq). - have [A Eq2A _] := ex_tau2Elem hallE t2q. - have [[_ defEq1] _ _ _] := tau2_compl_context maxM hallE t2q Eq2A. - rewrite (tau12_regular maxM hallE t1p EpY t2q Eq2A) //. - rewrite (subG1_contra _ (nt_pnElem EqX _)) // subsetI. - rewrite defEq1 in EqX; case/pnElemP: EqX => -> _ _. - by rewrite (subset_trans sXcE2Y) ?subsetIr. - have [defM [sUE _]] := (sdprod_sigma maxM hallE, andP nsUE). - have hallU: \sigma_kappa(M)^'.-Hall(M) U. - suffices: [predI \sigma(M)^' & \kappa(M)^'].-Hall(M) U. - by apply: etrans; apply: eq_pHall=> p; rewrite inE /= negb_or. - apply: subHall_Hall hallE _ _ => [p|]; first by case/andP. - rewrite pHallE partnI (part_pnat_id s'E) -pHallE. - have hallK_E: \kappa(M).-Hall(E) K := pHall_subl sKE sEM hallK. - by apply/(sdprod_normal_pHallP nsUE hallK_E); rewrite -defK. - exists U; [rewrite -{2}defK defE | rewrite -{1}defK]; split=> //. - by split; rewrite // -defK mulUE1 groupP. - apply: abelianS (der_mmax_compl_abelian maxM hallE). - rewrite -(coprime_cent_prod nUE1) ?(solvableS sUE) //. - by rewrite {2}defK (cent_semiregular regUK) // mulg1 commgSS. - by rewrite (coprime_sdprod_Hall_r defE); apply: pHall_Hall hallE1. - move: not_t1K; rewrite negb_and cardG_gt0 => /allPn[p piKp t1'p]. - have kp := pnatPpi kK piKp; have t3p := kappa_tau13 kp. - rewrite [p \in _](negPf t1'p) /= in t3p. - have [X]: exists X, X \in 'E_p^1(K) by apply/p_rank_geP; rewrite p_rank_gt0. - rewrite -{1}(setIidPr sKM) pnElemI -setIdE => /setIdP[EpX sXK]. - have sXE3: X \subset E3. - rewrite (sub_normal_Hall hallE3) ?(subset_trans sXK) ?(pi_pgroup _ t3p) //. - by case/pnElemP: EpX => _ /andP[]. - have [nregX ntX] := (kappa_nonregular kp EpX, nt_pnElem EpX isT). - have [regE3|ntE1 {defE}defE prE nE1_E] := tau13_nonregular maxM complEi. - by case/eqP: nregX; rewrite (cent_semiregular regE3). - have defK: E :=: K. - apply: (sub_pHall hallK _ sKE sEM); apply/pgroupP=> q q_pr q_dv_E. - have{q_dv_E} piEq: q \in \pi(E) by rewrite mem_primes q_pr cardG_gt0. - rewrite unlock; apply/andP; split=> /=. - apply: pnatPpi piEq; rewrite -pgroupE -(sdprodW defE). - rewrite pgroupM (sub_pgroup _ t3E3) => [|r t3r]; last by apply/orP; right. - by rewrite (sub_pgroup _ t1E1) // => r t1r; apply/orP; left. - have:= piEq; rewrite -p_rank_gt0 => /p_rank_geP[Y]. - rewrite -{1}(setIidPr sEM) pnElemI -setIdE => /setIdP[EqY sYE]. - rewrite (cent_semiprime prE) ?(subset_trans sXK) // in nregX. - apply/exists_inP; exists Y => //; apply: subG1_contra nregX. - by rewrite setIS ?centS. - have defM := sdprod_sigma maxM hallE. - rewrite /b1_hyp -defK; split=> //; exists 1%G; last first. - by split; [apply: abelian1 | rewrite -defK | apply: semiregular1l]. - rewrite sdprod1g; do 2?split=> //; rewrite ?mul1g ?groupP -?defK //. - rewrite pHallE sub1G cards1 eq_sym partG_eq1 pgroupNK /=. - have{defM} [_ defM _ _] := sdprodP defM; rewrite -{2}defM defK pgroupM. - rewrite (sub_pgroup _ sMs) => [|r sr]; last by apply/orP; left. - by rewrite (sub_pgroup _ kK) // => r kr; apply/orP; right. -set part_b := _ /\ _; set part_c := _ /\ _; set part_d := _ /\ _. -have [U [complUK defM] [cUU prMsK regUK]] := have_a. -have [hallU _ _] := complUK; have [sUM sk'U _] := and3P hallU. -have have_b: part_b. - have coMsU: coprime #|Ms| #|U|. - by rewrite (pnat_coprime sMs (sub_pgroup _ sk'U)) // => p; case/norP. - have{defM} [[_ F _ defF]] := sdprodP defM; rewrite defF. - have [_ <- nUK _] := sdprodP defF; rewrite mulgA mulG_subG => defM. - case/andP=> nMsU nMsK _. - have coMsU_K: coprime #|Ms <*> U| #|K|. - rewrite norm_joinEr // (p'nat_coprime _ kK) // -pgroupE. - rewrite pgroupM // (sub_pgroup _ sMs) => [|r]; last first. - by apply: contraL; apply: kappa_sigma'. - by apply: sub_pgroup _ sk'U => r /norP[]. - have defNK X: X <| K -> X :!=: 1 -> 'N_M(X) = Ks * K. - case/andP=> sXK nXK ntX; rewrite -defM -(norm_joinEr nMsU). - rewrite setIC -group_modr // setIC. - rewrite coprime_norm_cent ?(subset_trans sXK) ?normsY //; last first. - by rewrite (coprimegS sXK). - rewrite /= norm_joinEr -?subcent_TImulg ?(coprime_TIg coMsU) //; last first. - by rewrite subsetI !(subset_trans sXK). - by rewrite (cent_semiregular regUK) // mulg1 (cent_semiprime prMsK). - rewrite /part_b dprodE ?subsetIr //; last first. - rewrite setICA setIA (coprime_TIg (coprimeSg _ coMsU_K)) ?setI1g //. - by rewrite joing_subl. - rewrite -centC ?subsetIr // defNK //; split=> // X Eq1X. - have [q EqX] := nElemP Eq1X; have ntX := nt_pnElem EqX isT. - have:= EqX; rewrite -{1}(setIidPr sKE) pnElemI -setIdE. - case/setIdP=> EqEX sXK; split; first by rewrite defNK ?nK1K. - have [_ abelX dimX] := pnElemP EqX; have [qX _] := andP abelX. - have kq: q \in \kappa(M). - by rewrite (pnatPpi kK (piSg sXK _)) // -p_rank_gt0 p_rank_abelem ?dimX. - have nregX := kappa_nonregular kq (subsetP (pnElemS _ _ sEM) _ EqEX). - have sq := tau13_nonregular_sigma maxM hallE EqEX (kappa_tau13 kq) nregX. - move=> H maxNH; have [maxH sNXH] := setIdP maxNH. - rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(subset_trans (normG X)) //. - exact: pi_pgroup qX (sq H maxNH). -have have_c: part_c. - pose p := pdiv #|E1|; have piE1p: p \in \pi(E1) by rewrite pi_pdiv cardG_gt1. - have:= piE1p; rewrite -p_rank_gt0 => /p_rank_geP[Y]. - rewrite -(setIidPr sE1M) pnElemI -setIdE => /setIdP[EpY sYE1]. - have [sYK ntY] := (subset_trans sYE1 sE1K, nt_pnElem EpY isT). - split=> [|X /nElemP[q]]. - rewrite /Ks -(cent_semiprime prMsK sYK) //. - exact: kappa_nonregular (pnatPpi kK (piSg sE1K piE1p)) EpY. - rewrite /= -(cent_semiprime prMsK sYK) // => EqX. - by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sYE1 ntY EqX. -have [[defNK defK1] [_ uniqKs]] := (have_b, have_c). -have have_d: part_d. - split=> g. - rewrite inE; apply: contraNeq; rewrite -rank_gt0. - case/rank_geP=> X; rewrite nElemI -setIdE -groupV => /setIdP[EpX sXMg]. - have [_ sCXMs] := mem_uniq_mmax (uniqKs _ EpX). - case/nElemP: EpX => p /pnElemP[/subsetIP[sXMs _] abelX dimX]. - have [[pX _] sXM] := (andP abelX, subset_trans sXMs (pcore_sub _ _)). - have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. - have sp := pnatPpi sMs (piSg sXMs piXp). - have [def_g _ _] := sigma_group_trans maxM sp pX. - have [|c cXc [m Mm ->]] := def_g g^-1 sXM; first by rewrite sub_conjgV. - by rewrite groupM // (subsetP sCXMs). - case/setDP=> Mg; apply: contraNeq; rewrite -rank_gt0 /=. - case/rank_geP=> X; rewrite nElemI -setIdE => /setIdP[EpX sXKg]. - have [<- _] := defK1 X EpX; rewrite 2!inE Mg /=. - have{EpX} [p EpX] := nElemP EpX; have [_ abelX dimX] := pnElemP EpX. - have defKp1: {in 'E_p^1(K), forall Y, 'Ohm_1('O_p(K)) = Y}. - move=> Y EpY; have E1K_Y: Y \in 'E^1(K) by apply/nElemP; exists p. - have piKp: p \in \pi(K) by rewrite -p_rank_gt0; apply/p_rank_geP; exists Y. - have [pKp sKpK] := (pcore_pgroup p K, pcore_sub p K). - have cycKp: cyclic 'O_p(K). - rewrite (odd_pgroup_rank1_cyclic pKp) ?mFT_odd //. - by rewrite -(rank_kappa (pnatPpi kK piKp)) p_rankS ?(subset_trans sKpK). - have [sYK abelY oY] := pnElemPcard EpY; have [pY _] := andP abelY. - have sYKp: Y \subset 'O_p(K) by rewrite pcore_max ?nK1K. - apply/eqP; rewrite eq_sym eqEcard -{1}(Ohm1_id abelY) OhmS //= oY. - rewrite (Ohm1_cyclic_pgroup_prime cycKp pKp) ?(subG1_contra sYKp) //=. - exact: nt_pnElem EpY _. - rewrite sub_conjg -[X :^ _]defKp1 ?(defKp1 X) //. - by rewrite !inE sub_conjgV sXKg abelemJ abelX cardJg dimX. -split=> {part_a part_b part_c have_a have_b have_c}//; first split=> //. -- move=> q; rewrite /Ks -(cent_semiprime prMsK sE1K ntE1) => picMsE1q. - have sq := pnatPpi (pcore_pgroup _ M) (piSg (subsetIl _ _) picMsE1q). - move: picMsE1q; rewrite -p_rank_gt0; case/p_rank_geP=> y EqY S sylS. - have [sSM qS _] := and3P sylS. - have sSMs: S \subset M`_\sigma. - by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup qS). - have sylS_Ms: q.-Sylow(M`_\sigma) S := pHall_subl sSMs (pcore_sub _ M) sylS. - have [_]:= cent_cent_Msigma_tau1_uniq maxM hallE hallE1 (subxx _) ntE1 EqY. - move/(_ S sylS_Ms) => uniqS; split=> //; rewrite subsetI sSMs /=. - pose p := pdiv #|E1|; have piE1p: p \in \pi(E1) by rewrite pi_pdiv cardG_gt1. - have [s'p _] := andP (pnatPpi t1E1 piE1p). - have [P sylP] := Sylow_exists p E1; have [sPE1 pP _] := and3P sylP. - apply: contra (s'p) => cE1S; apply/exists_inP; exists P. - exact: subHall_Sylow s'p (subHall_Sylow hallE1 (pnatPpi t1E1 piE1p) sylP). - apply: (sub_uniq_mmax uniqS); first by rewrite cents_norm // (centsS sPE1). - apply: mFT_norm_proper (mFT_pgroup_proper pP). - by rewrite -rank_gt0 (rank_Sylow sylP) p_rank_gt0. -- move=> Y sY ntYKs; have ntY: Y :!=:1 := subG1_contra (subsetIl _ _) ntYKs. - have [[x sYxMs] _] := sigma_Jsub maxM sY ntY; rewrite sub_conjg in sYxMs. - suffices Mx': x^-1 \in M by rewrite (normsP _ _ Mx') ?gFnorm in sYxMs. - rewrite -(setCK M) inE; apply: contra ntYKs => M'x'. - rewrite setIC -(setIidPr sYxMs) -/Ms -[Ms](setIidPr (pcore_sub _ _)). - by rewrite conjIg !setIA; have [-> // _] := have_d; rewrite !setI1g. -rewrite inE PmaxM andbT -(trivg_kappa_compl maxM complUK) => ntU. -have [regMsU nilMs]: 'C_Ms(U) = 1 /\ nilpotent Ms. - pose p := pdiv #|U|; have piUp: p \in \pi(U) by rewrite pi_pdiv cardG_gt1. - have sk'p := pnatPpi sk'U piUp. - have [S sylS] := Sylow_exists p U; have [sSU _] := andP sylS. - have sylS_M := subHall_Sylow hallU sk'p sylS. - have [|_ _ regMsS1 nilMs] := sigma'_kappa'_facts maxM sylS_M. - by rewrite -negb_or (piSg sUM). - by split=> //; apply/trivgP; rewrite -regMsS1 setIS ?centS ?gFsub_trans. -have [[_ F _ defF] _ _ _] := sdprodP defM; rewrite defF in defM. -have hallMs: \sigma(M).-Hall(M) Ms by apply: Msigma_Hall. -have hallF: \sigma(M)^'.-Hall(M) F by apply/(sdprod_Hall_pcoreP hallMs). -have frF: [Frobenius F = U ><| K] by apply/Frobenius_semiregularP. -have ntMs: Ms != 1 by apply: Msigma_neq1. -have prK: prime #|K|. - have [solF [_ _ nMsF _]] := (sigma_compl_sol hallF, sdprodP defM). - have solMs: solvable Ms := solvableS (pcore_sub _ _) (mmax_sol maxM). - have coMsF: coprime #|Ms| #|F|. - by rewrite (coprime_sdprod_Hall_r defM) (pHall_Hall hallF). - by have [] := Frobenius_primact frF solF nMsF solMs ntMs coMsF prMsK. -have eq_sb: \sigma(M) =i \beta(M). - suffices bMs: \beta(M).-group Ms. - move=> p; apply/idP/idP=> [sp|]; last exact: beta_sub_sigma. - rewrite (pnatPpi bMs) //= (card_Hall (Msigma_Hall maxM)) pi_of_part //. - by rewrite inE /= sigma_sub_pi. - have [H hallH cHF'] := der_compl_cent_beta' maxM hallF. - rewrite -pgroupNK -partG_eq1 -(card_Hall hallH) -trivg_card1 -subG1. - rewrite -regMsU subsetI (pHall_sub hallH) centsC (subset_trans _ cHF') //. - have [solU [_ mulUK nUK _]] := (abelian_sol cUU, sdprodP defF). - have coUK: coprime #|U| #|K|. - rewrite (p'nat_coprime (sub_pgroup _ (pHall_pgroup hallU)) kK) // => p. - by case/norP. - rewrite -(coprime_cent_prod nUK) // (cent_semiregular regUK) // mulg1. - by rewrite -mulUK commgSS ?mulG_subl ?mulG_subr. -split=> //; apply/normedTI_P; rewrite setD_eq0 subG1 setTI normD1 gFnorm. -split=> // g _; rewrite -setI_eq0 conjD1g -setDIl setD_eq0 subG1 /= -/Ms. -have [_ _ b'MsMg] := sigma_compl_embedding maxM hallE. -apply: contraR => notMg; have{b'MsMg notMg} [_ b'MsMg _] := b'MsMg g notMg. -rewrite -{2}(setIidPr (pHall_sub hallMs)) conjIg setIA coprime_TIg // cardJg. -by apply: p'nat_coprime b'MsMg _; rewrite -(eq_pnat _ eq_sb). -Qed. - -(* This is essentially the skolemized form of 14.2(a). *) -Lemma kappa_compl_context M U K : - M \in 'M -> kappa_complement M U K -> - [/\ \sigma(M)^'.-Hall(M) (U <*> K), - M`_\sigma ><| (U ><| K) = M, - semiprime M`_\sigma K, - semiregular U K - & K :!=: 1 -> abelian U]. -Proof. -move=> maxM [hallU hallK gsetUK]; set E := U <*> K. -have mulUK: U * K = E by rewrite -(gen_set_id gsetUK) genM_join. -have [[sKM kK _] [sUM sk'U _]] := (and3P hallK, and3P hallU). -have tiUK: U :&: K = 1. - by apply: coprime_TIg (p'nat_coprime (sub_pgroup _ sk'U) kK) => p; case/norP. -have hallE: \sigma(M)^'.-Hall(M) E. - rewrite pHallE /= -/E -mulUK mul_subG //= TI_cardMg //. - rewrite -(partnC \kappa(M) (part_gt0 _ _)) (partn_part _ (@kappa_sigma' M)). - apply/eqP; rewrite -partnI -(card_Hall hallK) mulnC; congr (_ * _)%N. - by rewrite (card_Hall hallU); apply: eq_partn => p; apply: negb_or. -have [K1 | ntK] := altP (K :=P: 1). - rewrite K1 sdprodg1 -{1}(mulg1 U) -{1}K1 mulUK sdprod_sigma //. - by split=> //; first apply: semiregular_prime; apply: semiregular1r. -have PmaxM: M \in 'M_'P by rewrite inE maxM -(trivg_kappa maxM hallK) andbT. -have [[V [complV defM] [cVV prK regK]] _ _ _ _] := Ptype_structure PmaxM hallK. -have [[_ F _ defF] _ _ _] := sdprodP defM; rewrite defF in defM. -have hallF: \sigma(M)^'.-Hall(M) F. - exact/(sdprod_Hall_pcoreP (Msigma_Hall maxM)). -have [a Ma /= defFa] := Hall_trans (mmax_sol maxM) hallE hallF. -have [hallV _ _] := complV; set sk' := \sigma_kappa(M)^' in hallU hallV sk'U. -have [nsVF sKF _ _ _] := sdprod_context defF. -have [[[sVF _] [sFM _]] [sEM _]] := (andP nsVF, andP hallF, andP hallE). -have hallV_F: sk'.-Hall(F) V := pHall_subl sVF sFM hallV. -have hallU_E: sk'.-Hall(E) U := pHall_subl (joing_subl _ _) sEM hallU. -have defV: 'O_sk'(F) = V := normal_Hall_pcore hallV_F nsVF. -have hallEsk': sk'.-Hall(E) 'O_sk'(E). - by rewrite [E]defFa pcoreJ pHallJ2 /= defV. -have defU: 'O_sk'(E) = U by rewrite (eq_Hall_pcore hallEsk' hallU_E). -have nUE: E \subset 'N(U) by rewrite -defU gFnorm. -have hallK_E: \kappa(M).-Hall(E) K := pHall_subl (joing_subr _ _) sEM hallK. -have hallK_F: \kappa(M).-Hall(F) K := pHall_subl sKF sFM hallK. -have hallKa_E: \kappa(M).-Hall(E) (K :^ a) by rewrite [E]defFa pHallJ2. -have [b Eb /= defKab] := Hall_trans (sigma_compl_sol hallE) hallK_E hallKa_E. -have defVa: V :^ a = U by rewrite -defV -pcoreJ -defFa defU. -split=> // [| x Kx | _]; last by rewrite -defVa abelianJ. - by rewrite [U ><| K]sdprodEY ?sdprod_sigma //; case/joing_subP: nUE. -rewrite -(conjgKV (a * b) x) -(normsP nUE b Eb) -defVa -conjsgM. -rewrite -cent_cycle cycleJ centJ -conjIg cent_cycle regK ?conjs1g //. -by rewrite -mem_conjg conjD1g conjsgM -defKab. -Qed. - -(* This is B & G, Corollary 14.3. *) -Corollary pi_of_cent_sigma M x x' : - M \in 'M -> x \in (M`_\sigma)^# -> - x' \in ('C_M[x])^# -> \sigma(M)^'.-elt x' -> - (*1*) \kappa(M).-elt x' /\ 'C[x] \subset M - \/ (*2*) [/\ \tau2(M).-elt x', \ell_\sigma(x') == 1%N & 'M('C[x']) = [set M]]. -Proof. -move: x' => y maxM /setD1P[ntx Ms_x] /setD1P[nty cMxy] s'y. -have [My cxy] := setIP cMxy. -have [t2y | not_t2y] := boolP (\tau2(M).-elt y); [right | left]. - have uniqCy: 'M('C[y]) = [set M]; last split=> //. - apply: cent1_nreg_sigma_uniq; rewrite // ?inE ?nty //. - by apply/trivgPn; exists x; rewrite // inE Ms_x cent1C. - pose p := pdiv #[y]; have piYp: p \in \pi(#[y]) by rewrite pi_pdiv order_gt1. - have t2p := pnatPpi t2y piYp; have [E hallE] := ex_sigma_compl maxM. - have [A Ep2A _] := ex_tau2Elem hallE t2p. - have pA: p.-group A by case/pnElemP: Ep2A => _ /andP[]. - have ntA: A :!=: 1 by rewrite (nt_pnElem Ep2A). - have [H maxNH] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper pA)). - have [st2MsH _ _] := primes_norm_tau2Elem maxM hallE t2p Ep2A maxNH. - have [maxH _] := setIdP maxNH. - have sHy: \sigma(H).-elt y by apply: sub_p_elt t2y => q /st2MsH/andP[]. - rewrite /sigma_length (cardsD1 y.`_(\sigma(H))). - rewrite mem_sigma_decomposition //; last by rewrite constt_p_elt. - rewrite eqSS -sigma_decomposition_constt' //. - by apply/ell_sigma0P; rewrite (constt1P _) ?p_eltNK. -have{not_t2y} [p piYp t2'p]: exists2 p, p \in \pi(#[y]) & p \notin \tau2(M). - by apply/allPn; rewrite negb_and cardG_gt0 in not_t2y. -have sYM: <[y]> \subset M by rewrite cycle_subG. -have piMp: p \in \pi(M) := piSg sYM piYp. -have t13p: p \in [predU \tau1(M) & \tau3(M)]. - move: piMp; rewrite partition_pi_mmax // (negPf t2'p) /= orbA. - by case/orP=> // sMy; case/negP: (pnatPpi s'y piYp). -have [X]: exists X, X \in 'E_p^1(<[y]>) by apply/p_rank_geP; rewrite p_rank_gt0. -rewrite -(setIidPr sYM) pnElemI -setIdE => /setIdP[EpX sXy]. -have kp: p \in \kappa(M). - rewrite unlock; apply/andP; split=> //; apply/exists_inP; exists X => //. - apply/trivgPn; exists x; rewrite // inE Ms_x (subsetP (centS sXy)) //. - by rewrite cent_cycle cent1C. -have [sXM abelX dimX] := pnElemP EpX; have [pX _] := andP abelX. -have [K hallK sXK] := Hall_superset (mmax_sol maxM) sXM (pi_pgroup pX kp). -have PmaxM: M \in 'M_'P. - by rewrite 2!inE maxM andbT; apply: contraL kp => k'M; apply: (pnatPpi k'M). -have [_ [defNK defNX] [_ uniqCKs] _ _] := Ptype_structure PmaxM hallK. -have{defNX} sCMy_nMK: 'C_M[y] \subset 'N_M(K). - have [|<- _] := defNX X. - by apply/nElemP; exists p; rewrite !inE sXK abelX dimX. - by rewrite setIS // cents_norm // -cent_cycle centS. -have [[sMK kK _] [_ mulKKs cKKs _]] := (and3P hallK, dprodP defNK). -have s'K: \sigma(M)^'.-group K := sub_pgroup (@kappa_sigma' M) kK. -have sMs: \sigma(M).-group M`_\sigma := pcore_pgroup _ M. -have sKs: \sigma(M).-group 'C_(M`_\sigma)(K) := pgroupS (subsetIl _ _) sMs. -have{s'K sKs} [hallK_N hallKs] := coprime_mulGp_Hall mulKKs s'K sKs. -split. - rewrite (mem_p_elt kK) // (mem_normal_Hall hallK_N) ?normal_subnorm //. - by rewrite (subsetP sCMy_nMK) // inE My cent1id. -have Mx: x \in M := subsetP (pcore_sub _ _) x Ms_x. -have sxKs: <[x]> \subset 'C_(M`_\sigma)(K). - rewrite cycle_subG (mem_normal_Hall hallKs) ?(mem_p_elt sMs) //=. - by rewrite -mulKKs /normal mulG_subr mulG_subG normG cents_norm // centsC. - by rewrite (subsetP sCMy_nMK) // inE Mx cent1C. -have /rank_geP[Z]: 0 < 'r(<[x]>) by rewrite rank_gt0 cycle_eq1. -rewrite /= -(setIidPr sxKs) nElemI -setIdE => /setIdP[E1KsZ sZx]. -have [_ sCZM] := mem_uniq_mmax (uniqCKs Z E1KsZ). -by rewrite (subset_trans _ sCZM) // -cent_cycle centS. -Qed. - -(* This is B & G, Theorem 14.4. *) -(* We are omitting the first half of part (a), since we have taken it as our *) -(* definition of 'R[x]. *) -Theorem FT_signalizer_context x (N := 'N[x]) (R := 'R[x]) : - \ell_\sigma(x) == 1%N -> - [/\ [/\ [transitive R, on 'M_\sigma[x] | 'JG], - #|R| = #|'M_\sigma[x]|, - R <| 'C[x] - & Hall 'C[x] R] - & #|'M_\sigma[x]| > 1 -> - [/\ 'M('C[x]) = [set N], - (*a*) R :!=: 1, - (*c1*) \tau2(N).-elt x, - (*f*) N \in 'M_'F :|: 'M_'P2 - & {in 'M_\sigma[x], forall M, - [/\ (*b*) R ><| 'C_(M :&: N)[x] = 'C[x], - (*c2*) {subset \tau2(N) <= \sigma(M)}, - (*d*) {subset [predI \pi(M) & \sigma(N)] <= \beta(N)} - & (*e*) \sigma(N)^'.-Hall(N) (M :&: N)]}]]. -Proof. -rewrite {}/N {}/R => ell1x; have [ntx ntMSx] := ell_sigma1P x ell1x. -have [M MSxM] := set0Pn _ ntMSx; have [maxM Ms_x] := setIdP MSxM. -rewrite cycle_subG in Ms_x; have sMx := mem_p_elt (pcore_pgroup _ M) Ms_x. -have Mx: x \in M := subsetP (pcore_sub _ _) x Ms_x. -have [MSx_le1 | MSx_gt1] := leqP _ 1. - rewrite /'R[x] /'N[x] ltnNge MSx_le1 (trivgP (pcore_sub _ _)) setI1g normal1. - have <-: [set M] = 'M_\sigma[x]. - by apply/eqP; rewrite eqEcard sub1set MSxM cards1. - by rewrite /Hall atrans_acts_card ?imset_set1 ?cards1 ?sub1G ?coprime1n. -have [q pi_x_q]: exists q, q \in \pi(#[x]). - by exists (pdiv #[x]); rewrite pi_pdiv order_gt1. -have{sMx} sMq: q \in \sigma(M) := pnatPpi sMx pi_x_q. -have [X EqX]: exists X, X \in 'E_q^1(<[x]>). - by apply/p_rank_geP; rewrite p_rank_gt0. -have [sXx abelX dimX] := pnElemP EqX; have [qX cXX _] := and3P abelX. -have ntX: X :!=: 1 := nt_pnElem EqX isT. -have sXM: X \subset M by rewrite (subset_trans sXx) ?cycle_subG. -have [N maxNX_N] := mmax_exists (mFT_norm_proper ntX (mFT_pgroup_proper qX)). -have [maxN sNX_N] := setIdP maxNX_N; pose R := 'C_(N`_\sigma)[x]%G. -have sCX_N: 'C(X) \subset N := subset_trans (cent_sub X) sNX_N. -have sCx_N: 'C[x] \subset N by rewrite -cent_cycle (subset_trans (centS sXx)). -have sMSx_MSX: 'M_\sigma[x] \subset 'M_\sigma(X). - apply/subsetP=> M1 /setIdP[maxM1 sxM1]. - by rewrite inE maxM1 (subset_trans sXx). -have nsRCx: R <| 'C[x] by rewrite /= setIC (normalGI sCx_N) ?pcore_normal. -have hallR: \sigma(N).-Hall('C[x]) R. - exact: setI_normal_Hall (pcore_normal _ _) (Msigma_Hall maxN) sCx_N. -have transCX: [transitive 'C(X), on 'M_\sigma(X) | 'JG]. - have [_ trCX _ ] := sigma_group_trans maxM sMq qX. - case/imsetP: trCX => _ /setIdP[/imsetP[y _ ->] sXMy] trCX. - have maxMy: (M :^ y)%G \in 'M by rewrite mmaxJ. - have sXMys: X \subset (M :^ y)`_\sigma. - by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup qX) ?sigmaJ. - apply/imsetP; exists (M :^ y)%G; first exact/setIdP. - apply/setP=> Mz; apply/setIdP/imsetP=> [[maxMz sXMzs] | [z cXz -> /=]]. - suffices: gval Mz \in orbit 'Js 'C(X) (M :^ y). - by case/imsetP=> z CXz /group_inj->; exists z. - rewrite -trCX inE andbC (subset_trans sXMzs) ?pcore_sub //=. - apply/idPn => /(sigma_partition maxM maxMz)/=/(_ q)/idP[]. - rewrite inE /= sMq (pnatPpi (pgroupS sXMzs (pcore_pgroup _ _))) //. - by rewrite -p_rank_gt0 p_rank_abelem ?dimX. - by rewrite mmaxJ -(normP (subsetP (cent_sub X) z cXz)) MsigmaJ conjSg. -have MSX_M: M \in 'M_\sigma(X) := subsetP sMSx_MSX M MSxM. -have not_sCX_M: ~~ ('C(X) \subset M). - apply: contraL MSx_gt1 => sCX_M. - rewrite -leqNgt (leq_trans (subset_leq_card sMSx_MSX)) //. - rewrite -(atransP transCX _ MSX_M) card_orbit astab1JG. - by rewrite (setIidPl (normsG sCX_M)) indexgg. -have neqNM: N :!=: M by apply: contraNneq not_sCX_M => <-. -have maxNX'_N: N \in 'M('N(X)) :\ M by rewrite 2!inE neqNM. -have [notMGN _] := sigma_subgroup_embedding maxM sMq sXM qX ntX maxNX'_N. -have sN'q: q \notin \sigma(N). - by apply: contraFN (sigma_partition maxM maxN notMGN q) => sNq; apply/andP. -rewrite (negPf sN'q) => [[t2Nq s_piM_bN hallMN]]. -have defN: N`_\sigma ><| (M :&: N) = N. - exact/(sdprod_Hall_pcoreP (Msigma_Hall maxN)). -have Nx: x \in N by rewrite (subsetP sCx_N) ?cent1id. -have MNx: x \in M :&: N by rewrite inE Mx. -have sN'x: \sigma(N)^'.-elt x by rewrite (mem_p_elt (pHall_pgroup hallMN)). -have /andP[sNsN nNsN]: N`_\sigma <| N := pcore_normal _ _. -have nNs_x: x \in 'N(N`_\sigma) := subsetP nNsN x Nx. -have defCx: R ><| 'C_(M :&: N)[x] = 'C[x]. - rewrite -{2}(setIidPr sCx_N) /= -cent_cycle (subcent_sdprod defN) //. - by rewrite subsetI andbC normsG ?cycle_subG. -have transR: [transitive R, on 'M_\sigma[x] | 'JG]. - apply/imsetP; exists M => //; apply/setP=> L. - apply/idP/imsetP=> [MSxL | [u Ru ->{L}]]; last first. - have [_ cxu] := setIP Ru; rewrite /= -cent_cycle in cxu. - by rewrite -(normsP (cent_sub _) u cxu) sigma_mmaxJ. - have [u cXu defL] := atransP2 transCX MSX_M (subsetP sMSx_MSX _ MSxL). - have [_ mulMN nNsMN tiNsMN] := sdprodP defN. - have:= subsetP sCX_N u cXu; rewrite -mulMN -normC //. - case/imset2P=> v w /setIP[Mv _] Ns_w def_u; exists w => /=; last first. - by apply: group_inj; rewrite defL /= def_u conjsgM (conjGid Mv). - rewrite inE Ns_w -groupV (sameP cent1P commgP) -in_set1 -set1gE -tiNsMN. - rewrite setICA setIC (setIidPl sNsN) inE groupMl ?groupV //. - rewrite memJ_norm // groupV Ns_w /= -(norm_mmax maxM) inE sub_conjg. - rewrite invg_comm -(conjSg _ _ w) -{2}(conjGid Mx) -!conjsgM -conjg_Rmul. - rewrite -conjgC conjsgM -(conjGid Mv) -(conjsgM M) -def_u. - rewrite -[M :^ u](congr_group defL) conjGid // -cycle_subG. - by have [_ Ls_x] := setIdP MSxL; rewrite (subset_trans Ls_x) ?pcore_sub. -have oR: #|R| = #|'M_\sigma[x]|. - rewrite -(atransP transR _ MSxM) card_orbit astab1JG (norm_mmax maxM). - rewrite -setIAC /= -{3}(setIidPl sNsN) -(setIA _ N) -(setIC M). - by have [_ _ _ ->] := sdprodP defN; rewrite setI1g indexg1. -have ntR: R :!=: 1 by rewrite -cardG_gt1 oR. -have [y Ns_y CNy_x]: exists2 y, y \in (N`_\sigma)^# & x \in ('C_N[y])^#. - have [y Ry nty] := trivgPn _ ntR; have [Ns_y cxy] := setIP Ry. - by exists y; rewrite 2!inE ?nty // inE Nx cent1C ntx. -have kN'q: q \notin \kappa(N). - rewrite (contra (@kappa_tau13 N q)) // negb_or (contraL (@tau2'1 _ _ _)) //. - exact: tau3'2. -have [[kNx _] | [t2Nx _ uniqN]] := pi_of_cent_sigma maxN Ns_y CNy_x sN'x. - by case/idPn: (pnatPpi kNx pi_x_q). -have defNx: 'N[x] = N. - apply/set1P; rewrite -uniqN /'N[x] MSx_gt1. - by case: pickP => // /(_ N); rewrite uniqN /= set11. -rewrite /'R[x] {}defNx -(erefl (gval R)) (pHall_Hall hallR). -split=> // _; split=> // [|L MSxL]. - rewrite !(maxN, inE) /=; case: (pgroup _ _) => //=; rewrite andbT. - apply: contra kN'q => skN_N; have:= pnatPpi (mem_p_elt skN_N Nx) pi_x_q. - by case/orP=> //=; rewrite (negPf sN'q). -have [u Ru ->{L MSxL}] := atransP2 transR MSxM MSxL; rewrite /= cardJg. -have [Ns_u cxu] := setIP Ru; have Nu := subsetP sNsN u Ns_u. -rewrite -{1}(conjGid Ru) -(conjGid cxu) -{1 6 7}(conjGid Nu) -!conjIg pHallJ2. -split=> // [|p t2Np]. - rewrite /= -(setTI 'C[x]) -!(setICA setT) -!morphim_conj. - exact: injm_sdprod (subsetT _) (injm_conj _ _) defCx. -have [A Ep2A _] := ex_tau2Elem hallMN t2Np. -have [[nsAMN _] _ _ _] := tau2_compl_context maxN hallMN t2Np Ep2A. -have{Ep2A} Ep2A: A \in 'E_p^2(M) by move: Ep2A; rewrite pnElemI; case/setIP. -have rpM: 'r_p(M) > 1 by apply/p_rank_geP; exists A. -have: p \in \pi(M) by rewrite -p_rank_gt0 ltnW. -rewrite sigmaJ partition_pi_mmax // !orbA; case/orP=> //. -rewrite orbAC -2!andb_orr -(subnKC rpM) andbF /= => t2Mp. -case/negP: ntX; rewrite -subG1 (subset_trans sXx) //. -have [_ _ <- _ _] := tau2_context maxM t2Mp Ep2A. -have [[sAM abelA _] [_ nAMN]] := (pnElemP Ep2A, andP nsAMN). -rewrite -coprime_norm_cent ?(subset_trans sAM) ?gFnorm //. - by rewrite cycle_subG inE Ms_x (subsetP nAMN). -have [[sM'p _] [pA _]] := (andP t2Mp, andP abelA). -exact: pnat_coprime (pcore_pgroup _ _) (pi_pgroup pA sM'p). -Qed. - -(* A useful supplement to Theorem 14.4. *) -Lemma cent1_sub_uniq_sigma_mmax x M : - #|'M_\sigma[x]| == 1%N -> M \in 'M_\sigma[x] -> 'C[x] \subset M. -Proof. -move: M => M0 /cards1P[M defMSx] MS_M0; move: MS_M0 (MS_M0). -rewrite {1}defMSx => /set1P->{M0} MSxM; have [maxM _] := setIdP MSxM. -rewrite -(norm_mmax maxM); apply/normsP=> y cxy; apply: congr_group. -by apply/set1P; rewrite -defMSx -(mulKg y x) (cent1P cxy) cycleJ sigma_mmaxJ. -Qed. - -Remark cent_FT_signalizer x : x \in 'C('R[x]). -Proof. by rewrite -sub_cent1 subsetIr. Qed. - -(* Because the definition of 'N[x] uses choice, we can only prove it commutes *) -(* with conjugation now that we have established that the choice is unique. *) -Lemma FT_signalizer_baseJ x z : 'N[x ^ z] :=: 'N[x] :^ z. -Proof. -case MSx_gt1: (#|'M_\sigma[x]| > 1); last first. - by rewrite /'N[x] /'N[_] cycleJ card_sigma_mmaxJ MSx_gt1 conjs1g. -have [x1 | ntx] := eqVneq x 1. - rewrite x1 conj1g /'N[1] /= norm1. - case: pickP => [M maxTM | _]; last by rewrite if_same conjs1g. - by have [maxM] := setIdP maxTM; case/idPn; rewrite proper_subn ?mmax_proper. -apply: congr_group; apply/eqP; rewrite eq_sym -in_set1. -have ell1xz: \ell_\sigma(x ^ z) == 1%N. - by rewrite ell_sigmaJ; apply/ell_sigma1P; rewrite -cards_eq0 -lt0n ltnW. -have [_ [|<- _ _ _ _]] := FT_signalizer_context ell1xz. - by rewrite cycleJ card_sigma_mmaxJ. -rewrite -conjg_set1 normJ mmax_ofJ; rewrite ell_sigmaJ in ell1xz. -by have [_ [//|-> _ _ _ _]] := FT_signalizer_context ell1xz; apply: set11. -Qed. - -Lemma FT_signalizerJ x z : 'R[x ^ z] :=: 'R[x] :^ z. -Proof. -by rewrite /'R[x] /'R[_] FT_signalizer_baseJ MsigmaJ -conjg_set1 normJ conjIg. -Qed. - -Lemma sigma_coverJ x z : x ^ z *: 'R[x ^ z] = (x *: 'R[x]) :^ z. -Proof. by rewrite FT_signalizerJ conjsMg conjg_set1. Qed. - -Lemma sigma_supportJ M z : (M :^ z)^~~ = M^~~ :^ z. -Proof. -rewrite -bigcupJ /_^~~ MsigmaJ -conjD1g (big_imset _ (in2W (act_inj 'J z))) /=. -by apply: eq_bigr => x _; rewrite sigma_coverJ. -Qed. - -(* This is the remark imediately above B & G, Lemma 14.5; note the adjustment *) -(* allowing for the case x' = 1. *) -Remark sigma_cover_decomposition x x' : - \ell_\sigma(x) == 1%N -> x' \in 'R[x] -> - sigma_decomposition (x * x') = x |: [set x']^#. -Proof. -move=> ell1x Rx'; have [-> | ntx'] := eqVneq x' 1. - by rewrite mulg1 setDv setU0 ell1_decomposition. -rewrite setDE (setIidPl _) ?sub1set ?inE // setUC. -have ntR: #|'R[x]| > 1 by rewrite cardG_gt1; apply/trivgPn; exists x'. -have [Ns_x' cxx'] := setIP Rx'; move/cent1P in cxx'. -have [[_ <- _ _] [//| maxN _ t2Nx _ _]] := FT_signalizer_context ell1x. -have{maxN} [maxN _] := mem_uniq_mmax maxN. -have sNx' := mem_p_elt (pcore_pgroup _ _) Ns_x'. -have sN'x: \sigma('N[x])^'.-elt x by apply: sub_p_elt t2Nx => p /andP[]. -have defx': (x * x').`_\sigma('N[x]) = x'. - by rewrite consttM // (constt1P sN'x) mul1g constt_p_elt. -have sd_xx'_x': x' \in sigma_decomposition (x * x'). - by rewrite 2!inE ntx' -{1}defx'; apply: mem_imset. -rewrite -(setD1K sd_xx'_x') -{3}defx' -sigma_decomposition_constt' ?consttM //. -by rewrite constt_p_elt // (constt1P _) ?p_eltNK ?mulg1 // ell1_decomposition. -Qed. - -(* This is the simplified form of remark imediately above B & G, Lemma 14.5. *) -Remark nt_sigma_cover_decomposition x x' : - \ell_\sigma(x) == 1%N -> x' \in 'R[x]^# -> - sigma_decomposition (x * x') = [set x; x']. -Proof. -move=> ell1x /setD1P[ntx' Rx']; rewrite sigma_cover_decomposition //. -by rewrite setDE (setIidPl _) ?sub1set ?inE // setUC. -Qed. - -Remark mem_sigma_cover_decomposition x g : - \ell_\sigma(x) == 1%N -> g \in x *: 'R[x] -> x \in sigma_decomposition g. -Proof. -by move=> ell1x /lcosetP[x' Rx' ->]; rewrite sigma_cover_decomposition ?setU11. -Qed. - -Remark ell_sigma_cover x g : - \ell_\sigma(x) == 1%N -> g \in x *: 'R[x] -> \ell_\sigma(g) <= 2. -Proof. -move=> ell1x /lcosetP[x' Rx' ->]. -rewrite /(\ell_\sigma(_)) sigma_cover_decomposition // cardsU1. -by rewrite (leq_add (leq_b1 _)) // -(cards1 x') subset_leq_card ?subsetDl. -Qed. - -Remark ell_sigma_support M g : M \in 'M -> g \in M^~~ -> \ell_\sigma(g) <= 2. -Proof. -by move=> maxM /bigcupP[x Msx]; apply: ell_sigma_cover; apply: Msigma_ell1 Msx. -Qed. - -(* This is B & G, Lemma 14.5(a). *) -Lemma sigma_cover_disjoint x y : - \ell_\sigma(x) == 1%N -> \ell_\sigma(y) == 1%N -> x != y -> - [disjoint x *: 'R[x] & y *: 'R[y]]. -Proof. -move=> ell1x ell1y neq_xy; apply/pred0P=> g /=. -have [[ntx _] [nty _]] := (ell_sigma1P x ell1x, ell_sigma1P y ell1y). -apply: contraNF (ntx) => /andP[/lcosetP[x' Rxx' ->{g}] /= yRy_xx']. -have def_y: y = x'. - apply: contraTeq (mem_sigma_cover_decomposition ell1y yRy_xx') => neq_yx'. - by rewrite sigma_cover_decomposition // !inE negb_or nty eq_sym neq_xy. -have [[_ <- _ _] [|uniqCx _ _ _ _]] := FT_signalizer_context ell1x. - by rewrite cardG_gt1; apply/trivgPn; exists x'; rewrite // -def_y. -have{uniqCx} [maxNx sCxNx] := mem_uniq_mmax uniqCx. -have Rx_y: y \in 'R[x] by [rewrite def_y]; have [Nxs_y cxy] := setIP Rx_y. -have Ry_x: x \in 'R[y]. - by rewrite -def_y -(cent1P cxy) mem_lcoset mulKg in yRy_xx'. -have MSyNx: 'N[x] \in 'M_\sigma[y] by rewrite inE maxNx cycle_subG. -have [[_ <- _ _] [|uniqCy _ _ _]] := FT_signalizer_context ell1y. - by rewrite cardG_gt1; apply/trivgPn; exists x. -have{uniqCy} [_ sCyNy] := mem_uniq_mmax uniqCy. -case/(_ 'N[x] MSyNx)=> /sdprodP[_ _ _ tiRyNx] _ _ _. -rewrite -in_set1 -set1gE -tiRyNx -setIA (setIidPr sCyNy) inE Ry_x /=. -by rewrite inE cent1C cxy (subsetP sCxNx) ?cent1id. -Qed. - -(* This is B & G, Lemma 14.5(b). *) -Lemma sigma_support_disjoint M1 M2 : - M1 \in 'M -> M2 \in 'M -> gval M2 \notin M1 :^: G -> [disjoint M1^~~ & M2^~~]. -Proof. -move=> maxM1 maxM2 notM1GM2; rewrite -setI_eq0 -subset0 big_distrl. -apply/bigcupsP=> x M1s_x; rewrite big_distrr; apply/bigcupsP=> y M2s_y /=. -have [ell1x ell1y] := (Msigma_ell1 maxM1 M1s_x, Msigma_ell1 maxM2 M2s_y). -rewrite subset0 setI_eq0 sigma_cover_disjoint //. -have{M1s_x M2s_y}[[ntx M1s_x] [_ M2s_y]] := (setD1P M1s_x, setD1P M2s_y). -pose p := pdiv #[x]; have pixp: p \in \pi(#[x]) by rewrite pi_pdiv order_gt1. -apply: contraFN (sigma_partition maxM1 maxM2 notM1GM2 p) => eq_xy. -rewrite inE /= (pnatPpi (mem_p_elt (pcore_pgroup _ _) M1s_x)) //=. -by rewrite (pnatPpi (mem_p_elt (pcore_pgroup _ _) M2s_y)) -?(eqP eq_xy). -Qed. - -(* This is B & G, Lemma 14.5(c). *) -Lemma card_class_support_sigma M : - M \in 'M -> #|class_support M^~~ G| = (#|M`_\sigma|.-1 * #|G : M|)%N. -Proof. -move=> maxM; rewrite [#|M`_\sigma|](cardsD1 1) group1 /=. -set MsG := class_support (M`_\sigma)^# G; pose P := [set x *: 'R[x] | x in MsG]. -have ellMsG x: x \in MsG -> \ell_\sigma(x) == 1%N. - by case/imset2P=> y z My _ ->; rewrite ell_sigmaJ (Msigma_ell1 maxM). -have tiP: trivIset P. - apply/trivIsetP=> _ _ /imsetP[x MsGx ->] /imsetP[y MsGy ->] neq_xRyR. - by rewrite sigma_cover_disjoint ?ellMsG //; apply: contraNneq neq_xRyR => ->. -have->: class_support M^~~ G = cover P. - apply/setP=> az; apply/imset2P/bigcupP=> [[a z] | [xRz]]. - case/bigcupP=> x Ms_x xRa Gz ->; exists (x ^ z *: 'R[x ^ z]). - by apply: mem_imset; apply: mem_imset2. - by rewrite sigma_coverJ memJ_conjg. - case/imsetP=> _ /imset2P[x z Ms_x Gz ->] ->; rewrite sigma_coverJ. - by case/imsetP=> a xRa ->; exists a z => //; apply/bigcupP; exists x. -rewrite -(eqnP tiP) big_imset /= => [|x y MsGx MsGy eq_xyR]; last first. - have: x *: 'R[x] != set0 by rewrite -cards_eq0 -lt0n card_lcoset cardG_gt0. - rewrite -[x *: _]setIid {2}eq_xyR setI_eq0. - by apply: contraNeq => neq_xy; rewrite sigma_cover_disjoint ?ellMsG. -rewrite -{2}(norm_mmax maxM) -astab1JG -indexgI -card_orbit. -set MG := orbit _ G M; rewrite mulnC -sum_nat_const. -transitivity (\sum_(Mz in MG) \sum_(x in (Mz`_\sigma)^#) 1); last first. - apply: eq_bigr => _ /imsetP[z _ ->]; rewrite sum1_card MsigmaJ. - by rewrite -conjD1g cardJg. -rewrite (exchange_big_dep (mem MsG)) /= => [|Mz xz]; last first. - case/imsetP=> z Gz ->; rewrite MsigmaJ -conjD1g => /imsetP[x Ms_x ->{xz}]. - exact: mem_imset2. -apply: eq_bigr => x MsGx; rewrite card_lcoset sum1dep_card. -have ell1x := ellMsG x MsGx; have [ntx _] := ell_sigma1P x ell1x. -have [[transRx -> _ _] _] := FT_signalizer_context ell1x. -apply: eq_card => Mz; rewrite 2!inE cycle_subG in_setD1 ntx /=. -apply: andb_id2r => Mzs_x. -apply/idP/imsetP=> [maxMz | [z _ ->]]; last by rewrite mmaxJ. -have [y t Ms_y _ def_x] := imset2P MsGx; have{Ms_y} [_ Ms_y] := setD1P Ms_y. -have [MSxMz MSxMt]: Mz \in 'M_\sigma[x] /\ (M :^ t)%G \in 'M_\sigma[x]. - by rewrite {2}def_x cycleJ sigma_mmaxJ inE maxMz inE maxM !cycle_subG. -have [z _ ->] := atransP2 transRx MSxMt MSxMz. -by exists (t * z); rewrite ?inE ?actM. -Qed. - -(* This is B & G, Lemma 14.6. *) -Lemma sigma_decomposition_dichotomy (g : gT) : - g != 1 -> - [exists (x | \ell_\sigma(x) == 1%N), x^-1 * g \in 'R[x]] - (+) [exists (y | \ell_\sigma(y) == 1%N), - let y' := y^-1 * g in - [exists M in 'M_\sigma[y], (y' \in ('C_M[y])^#) && \kappa(M).-elt y']]. -Proof. -move=> ntg; have [[x ell1x Rx'] | ] := altP exists_inP. - rewrite /= negb_exists_in; apply/forall_inP=> y ell1y. - set y' := y^-1 * g; set x' := x^-1 * g in Rx'. - apply/existsP=> -[M /and3P[MSyM CMy_y' kMy']]. - have [maxM Ms_y] := setIdP MSyM; rewrite cycle_subG in Ms_y. - have [nty'] := setD1P CMy_y'; case/setIP=> My'; move/cent1P=> cyy'. - have [[nty _] sMy]:= (ell_sigma1P y ell1y, mem_p_elt (pcore_pgroup _ _) Ms_y). - have sM'y': \sigma(M)^'.-elt y' := sub_p_elt (@kappa_sigma' M) kMy'. - have t2M'y': \tau2(M)^'.-elt y'. - apply: sub_p_elt kMy' => p; move/kappa_tau13. - by case/orP; [apply: tau2'1 | apply: contraL; apply: tau3'2]. - have xx'_y: y \in pred2 x x'. - suffices: y \in x |: [set x']^# by rewrite !inE nty. - rewrite -sigma_cover_decomposition // mulKVg 2!inE nty /=. - apply/imsetP; exists M => //; rewrite -(mulKVg y g) -/y' consttM //. - by rewrite (constt_p_elt sMy) (constt1P sM'y') mulg1. - have nt_x': x' != 1 by case/pred2P: xx'_y; rewrite /x' => <-. - have maxCY_M: M \in 'M('C[y]). - have Ms1_y: y \in (M`_\sigma)^# by apply/setD1P. - rewrite inE maxM; case/pi_of_cent_sigma: CMy_y' => // [[//] | [t2y']]. - by rewrite -order_eq1 (pnat_1 t2y' t2M'y') in nty'. - have [[_ <- _ _] [|uniqNx _ t2Nx _ _]] := FT_signalizer_context ell1x. - by rewrite cardG_gt1; apply/trivgPn; exists x'. - rewrite -order_gt1 (pnat_1 sMy _) // -/(_.-elt _) in nty. - have{xx'_y} [eq_yx | eq_yx']: y = x \/ y = x' := pred2P xx'_y. - rewrite eq_yx uniqNx in maxCY_M *; rewrite (set1P maxCY_M). - by apply: sub_p_elt t2Nx => p; case/andP. - have eq_xy': x = y' by apply: (mulIg y); rewrite cyy' {1}eq_yx' !mulKVg. - have [[z _ defM] | notMGNx] := altP (@orbitP _ _ _ 'Js G 'N[x] M). - rewrite -order_eq1 (pnat_1 _ t2M'y') // in nty'. - by rewrite -defM (eq_pnat _ (tau2J _ _)) -eq_xy'. - have Ns_y: y \in 'N[x]`_\sigma by rewrite eq_yx'; case/setIP: Rx'. - apply: sub_p_elt (mem_p_elt (pcore_pgroup _ _) Ns_y) => p sNp. - have [maxN _] := mem_uniq_mmax uniqNx. - by apply: contraFN (sigma_partition _ _ notMGNx p) => // sMp; apply/andP. -rewrite negb_exists_in => /forall_inP not_sign_g. -apply: wlog_neg; rewrite negb_exists_in => /forall_inP not_kappa_g. -have s'g M: M \in 'M -> g \in M -> g.`_\sigma(M) = 1. - move=> maxM; set x := g.`_\sigma(M); pose x' := g.`_(\sigma(M))^'. - have def_x': x^-1 * g = x' by rewrite -(consttC \sigma(M) g) mulKg. - apply: contraTeq => ntx. - have ell1x: \ell_\sigma(x) == 1%N. - rewrite /sigma_length (cardsD1 x.`_\sigma(M)). - rewrite -sigma_decomposition_constt' // mem_sigma_decomposition //. - by apply/ell_sigma0P; apply/constt1P; rewrite p_eltNK p_elt_constt. - by rewrite sub_in_constt // => ?. - apply: contra (not_sign_g _ ell1x) => Mg; rewrite def_x'. - have [-> | ntx'] := eqVneq x' 1; first exact: group1. - have cxx': x \in 'C[x'] by apply/cent1P; apply: commuteX2. - have cMx_x': x' \in ('C_M[x])^# by rewrite 3!inE ntx' cent1C cxx' groupX. - have Ms_x: x \in M`_\sigma. - by rewrite (mem_Hall_pcore (Msigma_Hall maxM)) ?p_elt_constt ?groupX. - have Ms1x: x \in (M`_\sigma)^# by apply/setD1P. - have sM'x': (\sigma(M))^'.-elt x' := p_elt_constt _ _. - have [[kMx' _] | [_ ell1x' uniqM]] := pi_of_cent_sigma maxM Ms1x cMx_x' sM'x'. - case/existsP: (not_kappa_g _ ell1x); exists M; rewrite def_x' cMx_x' /=. - by rewrite inE maxM cycle_subG Ms_x. - have MSx'_gt1: #|'M_\sigma[x']| > 1. - have [_ ntMSx'] := ell_sigma1P _ ell1x'. - rewrite ltn_neqAle lt0n cards_eq0 ntMSx' andbT eq_sym. - apply: contra ntx' => MSx'_eq1; rewrite -order_eq1 (pnat_1 _ sM'x') //. - have [N MSx'N] := set0Pn _ ntMSx'; have [maxN Ns_x'] := setIdP MSx'N. - rewrite -(eq_uniq_mmax uniqM maxN) ?cent1_sub_uniq_sigma_mmax //. - exact: pgroupS Ns_x' (pcore_pgroup _ _). - have defNx': 'N[x'] = M. - by apply: set1_inj; case/FT_signalizer_context: ell1x' => _ [|<-]. - case/negP: (not_sign_g _ ell1x'). - by rewrite -(consttC \sigma(M)^' g) mulKg consttNK inE defNx' Ms_x. -have [x sg_x]: exists x, x \in sigma_decomposition g. - by apply/set0Pn; rewrite -cards_eq0 (sameP (ell_sigma0P g) eqP). -have{sg_x} [ntx /imsetP[M maxM def_x]] := setD1P sg_x. -wlog MSxM: M maxM def_x / M \in 'M_\sigma[x]. - have sMx: \sigma(M).-elt x by rewrite def_x p_elt_constt. - have [|[z Ms_xz] _] := sigma_Jsub maxM sMx; first by rewrite cycle_eq1. - move/(_ (M :^ z^-1)%G)->; rewrite ?mmaxJ ?(eq_constt _ (sigmaJ M _)) //. - by rewrite inE mmaxJ maxM MsigmaJ -sub_conjg. -have ell1x: \ell_\sigma(x) == 1%N. - by apply/ell_sigma1P; split=> //; apply/set0Pn; exists M. -have notMg: g \notin M by apply: contra ntx; rewrite def_x; move/s'g->. -have cxg: g \in 'C[x] by rewrite cent1C def_x groupX ?cent1id. -have MSx_gt1: #|'M_\sigma[x]| > 1. - rewrite ltnNge; apply: contra notMg => MSx_le1; apply: subsetP cxg. - have [_ ntMSx] := ell_sigma1P _ ell1x. - by rewrite cent1_sub_uniq_sigma_mmax // eqn_leq MSx_le1 lt0n cards_eq0. -have [_ [//|defNx _ _ _]] := FT_signalizer_context ell1x. -case/(_ M)=> // _ _ _ hallMN; have [maxN sCxN] := mem_uniq_mmax defNx. -have Ng: <[g]> \subset 'N[x] by rewrite cycle_subG (subsetP sCxN). -have sN'g: \sigma('N[x])^'.-elt g by apply/constt1P; rewrite s'g // -cycle_subG. -have [z _ MNgz] := Hall_subJ (mmax_sol maxN) hallMN Ng sN'g. -case/eqP: ntx; rewrite def_x -(eq_constt _ (sigmaJ M z)) s'g ?mmaxJ //. -by move: MNgz; rewrite conjIg cycle_subG => /setIP[]. -Qed. - -Section PTypeEmbedding. -Implicit Types Mi Mj : {group gT}. -Implicit Type Ks : {set gT}. - -(* This is B & G, Theorem 14.7. *) -(* This theorem provides the basis for the maximal subgroup classification, *) -(* the main output of the local analysis. Note that we handle differently the *) -(* two separate instances of non-structural proof (by analogy) that occur in *) -(* the textbook, p. 112, l. 7 and p. 113, l. 22. For the latter we simply use *) -(* global induction on the size of the class support of the TI-set \hat{Z} *) -(* (for this reason we have kept the assertion that this is greater than half *) -(* of the size of G, even though this is not used later in the proof; we did *) -(* drop the more precise lower bound). For the former we prove a preliminary *) -(* lemma that summarizes the four results of the beginning of the proof that *) -(* used after p. 112, l. 7 -- note that this also gets rid of a third non *) -(* structural argument (on p. 112, l. 5). *) -(* Also, note that the direct product decomposition of Z and the K_i, and *) -(* its direct relation with the sigma-decomposition of elements of Z (p. 112, *) -(* l. 13-19) is NOT materially used in the rest of the argument, though it *) -(* does obviously help a human reader forge a mental picture of the situation *) -(* at hand. Only the first remark, l. 13, is used to prove the alternative *) -(* definition of T implicit in the remarks l. 22-23. Accordingly, we have *) -(* suppressed most of these intermediate results: we have only kept the proof *) -(* that Z is the direct product of the K_i^*, though we discard this result *) -(* immediately (its 24-line proof just nudges the whole proof size slightyly *) -(* over the 600-line bar). *) -Theorem Ptype_embedding M K : - M \in 'M_'P -> \kappa(M).-Hall(M) K -> - exists2 Mstar, Mstar \in 'M_'P /\ gval Mstar \notin M :^: G - & let Kstar := 'C_(M`_\sigma)(K) in - let Z := K <*> Kstar in let Zhat := Z :\: (K :|: Kstar) in - [/\ (*a*) {in 'E^1(K), forall X, 'M('C(X)) = [set Mstar]}, - (*b*) \kappa(Mstar).-Hall(Mstar) Kstar /\ \sigma(M).-Hall(Mstar) Kstar, - (*c*) 'C_(Mstar`_\sigma)(Kstar) = K /\ \kappa(M) =i \tau1(M), - (*d*) [/\ cyclic Z, M :&: Mstar = Z, - {in K^#, forall x, 'C_M[x] = Z}, - {in Kstar^#, forall y, 'C_Mstar[y] = Z} - & {in K^# & Kstar^#, forall x y, 'C[x * y] = Z}] -& [/\ (*e*) [/\ normedTI Zhat G Z, {in ~: M, forall g, [disjoint Zhat & M :^ g]} - & (#|G|%:R / 2%:R < #|class_support Zhat G|%:R :> rat)%R ], - (*f*) M \in 'M_'P2 /\ prime #|K| \/ Mstar \in 'M_'P2 /\ prime #|Kstar|, - (*g*) {in 'M_'P, forall H, gval H \in M :^: G :|: Mstar :^: G} - & (*h*) M^`(1) ><| K = M]]. -Proof. -pose isKi Ks M K := [&& M \in 'M_'P, \kappa(M).-Hall(M) K & Ks \subset K]. -move: M K; have Pmax_sym M K X (Ks := 'C_(M`_\sigma)(K)) (Z := K <*> Ks) Mi : - M \in 'M_'P -> \kappa(M).-Hall(M) K -> X \in 'E^1(K) -> Mi \in 'M('N(X)) -> - [/\ Z \subset Mi, gval Mi \notin M :^: G, exists Ki, isKi Ks Mi Ki - & {in 'E^1(Ks), forall Xs, Z \subset 'N_Mi(gval Xs)}]. -- move=> PmaxM hallK E1X maxNMi. - have [[_ maxM] [maxMi sNXMi]] := (setIdP PmaxM, setIdP maxNMi). - have [_ [defNK defNX] [ntKs uniqCKs] _ _] := Ptype_structure PmaxM hallK. - rewrite -/Ks in defNK ntKs uniqCKs; have [_ mulKKs cKKs _] := dprodP defNK. - have{mulKKs} defZ: 'N_M(K) = Z by rewrite -mulKKs -cent_joinEr. - have sZMi: Z \subset Mi. - by rewrite -defZ; have [<- _] := defNX X E1X; rewrite setIC subIset ?sNXMi. - have [sKMi sKsMi] := joing_subP sZMi. - have sXMis: X \subset Mi`_\sigma by have [_ ->] := defNX X E1X. - have sMiX: \sigma(Mi).-group X := pgroupS sXMis (pcore_pgroup _ _). - have [q EqX] := nElemP E1X; have [sXK abelX dimX] := pnElemP EqX. - have piXq: q \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. - have notMGMi: gval Mi \notin M :^: G. - apply: contraL (pnatPpi sMiX piXq); case/imsetP=> a _ ->; rewrite sigmaJ. - exact: kappa_sigma' (pnatPpi (pHall_pgroup hallK) (piSg sXK piXq)). - have kMiKs: \kappa(Mi).-group Ks. - apply/pgroupP=> p p_pr /Cauchy[] // xs Ks_xs oxs. - pose Xs := <[xs]>%G; have sXsKs: Xs \subset Ks by rewrite cycle_subG. - have EpXs: Xs \in 'E_p^1(Ks) by rewrite p1ElemE // !inE sXsKs -oxs /=. - have sMi'Xs: \sigma(Mi)^'.-group Xs. - rewrite /pgroup /= -orderE oxs pnatE //=. - apply: contraFN (sigma_partition maxM maxMi notMGMi p) => /= sMi_p. - rewrite inE /= sMi_p -pnatE // -oxs andbT. - exact: pgroupS sXsKs (pgroupS (subsetIl _ _) (pcore_pgroup _ _)). - have uniqM: 'M('C(Xs)) = [set M] by apply: uniqCKs; apply/nElemP; exists p. - have [x Xx ntx] := trivgPn _ (nt_pnElem EqX isT). - have Mis_x: x \in (Mi`_\sigma)^# by rewrite !inE ntx (subsetP sXMis). - have CMix_xs: xs \in ('C_Mi[x])^#. - rewrite 2!inE -order_gt1 oxs prime_gt1 // inE -!cycle_subG. - rewrite (subset_trans sXsKs) //= sub_cent1 (subsetP _ x Xx) //. - by rewrite centsC (centSS sXsKs sXK). - have{sMi'Xs} [|[_ _]] := pi_of_cent_sigma maxMi Mis_x CMix_xs sMi'Xs. - by case; rewrite /p_elt oxs pnatE. - case/mem_uniq_mmax=> _ sCxsMi; case/negP: notMGMi. - by rewrite -(eq_uniq_mmax uniqM maxMi) ?orbit_refl //= cent_cycle. - have{kMiKs} [Ki hallKi sKsKi] := Hall_superset (mmax_sol maxMi) sKsMi kMiKs. - have{ntKs} PmaxMi: Mi \in 'M_'P. - rewrite !(maxMi, inE) andbT /= -partG_eq1 -(card_Hall hallKi) -trivg_card1. - exact: subG1_contra sKsKi ntKs. - have [_ [defNKi defNXs] _ _ _] := Ptype_structure PmaxMi hallKi. - split=> //= [|Xs]; first by exists Ki; apply/and3P. - rewrite -{1}[Ks](setIidPr sKsKi) nElemI -setIdE => /setIdP[E1Xs sXsKs]. - have{defNXs} [defNXs _] := defNXs _ E1Xs; rewrite join_subG /= {2}defNXs. - by rewrite !subsetI sKMi sKsMi cents_norm ?normsG ?(centsS sXsKs) // centsC. -move=> M K PmaxM hallK /=; set Ks := 'C_(M`_\sigma)(K); set Z := K <*> Ks. -move: {2}_.+1 (ltnSn #|class_support (Z :\: (K :|: Ks)) G|) => nTG. -elim: nTG => // nTG IHn in M K PmaxM hallK Ks Z *; rewrite ltnS => leTGn. -have [maxM notFmaxM]: M \in 'M /\ M \notin 'M_'F := setDP PmaxM. -have{notFmaxM} ntK: K :!=: 1 by rewrite (trivg_kappa maxM). -have [_ [defNK defNX] [ntKs uniqCKs] _ _] := Ptype_structure PmaxM hallK. -rewrite -/Ks in defNK ntKs uniqCKs; have [_ mulKKs cKKs _] := dprodP defNK. -have{mulKKs} defZ: 'N_M(K) = Z by rewrite -mulKKs -cent_joinEr. -pose MNX := \bigcup_(X in 'E^1(K)) 'M('N(X)); pose MX := M |: MNX. -have notMG_MNX: {in MNX, forall Mi, gval Mi \notin M :^: G}. - by move=> Mi /bigcupP[X E1X /(Pmax_sym M K)[]]. -have MX0: M \in MX := setU11 M MNX. -have notMNX0: M \notin MNX by apply/negP=> /notMG_MNX; rewrite orbit_refl. -pose K_ Mi := odflt K [pick Ki | isKi Ks Mi Ki]. -pose Ks_ Mi := 'C_(Mi`_\sigma)(K_ Mi). -have K0: K_ M = K. - rewrite /K_; case: pickP => // K1 /and3P[_ /and3P[_ kK1 _] sKsK1]. - have sM_Ks: \sigma(M).-group Ks := pgroupS (subsetIl _ _) (pcore_pgroup _ _). - rewrite -(setIid Ks) coprime_TIg ?eqxx ?(pnat_coprime sM_Ks) // in ntKs. - exact: sub_pgroup (@kappa_sigma' M) (pgroupS sKsK1 kK1). -have Ks0: Ks_ M = Ks by rewrite /Ks_ K0. -have K_spec: {in MNX, forall Mi, isKi Ks Mi (K_ Mi)}. - move=> Mi /bigcupP[X _ /(Pmax_sym M K)[] // _ _ [Ki Ki_ok] _]. - by rewrite /K_; case: pickP => // /(_ Ki)/idP. -have PmaxMX: {in MX, forall Mi, Mi \in 'M_'P /\ \kappa(Mi).-Hall(Mi)(K_ Mi)}. - by move=> Mi /setU1P[-> | /K_spec/and3P[]//]; rewrite K0. -have ntKsX: {in MX, forall Mi, Ks_ Mi != 1}. - by move=> Mi /PmaxMX[MX_Mi /Ptype_structure[] // _ _ []]. -pose co_sHallK Mi Zi := - let sMi := \sigma(Mi) in sMi^'.-Hall(Zi) (K_ Mi) /\ sMi.-Hall(Zi) (Ks_ Mi). -have hallK_Zi: {in MX, forall Mi, co_sHallK Mi (K_ Mi \x Ks_ Mi)}. - move=> Mi MXi; have [PmaxMi hallKi] := PmaxMX _ MXi. - have [_ [defNKs _] _ _ _] := Ptype_structure PmaxMi hallKi. - have [_ mulKKs _ _] := dprodP defNKs; rewrite defNKs. - have sMi_Kis: _.-group (Ks_ Mi) := pgroupS (subsetIl _ _) (pcore_pgroup _ _). - have sMi'Ki := sub_pgroup (@kappa_sigma' _) (pHall_pgroup hallKi). - exact: coprime_mulGp_Hall mulKKs sMi'Ki sMi_Kis. -have{K_spec} defZX: {in MX, forall Mi, K_ Mi \x Ks_ Mi = Z}. - move=> Mi MXi; have [-> | MNXi] := setU1P MXi; first by rewrite K0 Ks0 defNK. - have /and3P[PmaxMi hallKi sKsKi] := K_spec _ MNXi. - have [X E1X maxNMi] := bigcupP MNXi. - have{defNX} [defNX /(_ Mi maxNMi) sXMis] := defNX X E1X. - have /rank_geP[Xs E1Xs]: 0 < 'r(Ks) by rewrite rank_gt0. - have [_ [defNi defNXi] _ _ _] := Ptype_structure PmaxMi hallKi. - have [defNXs _] := defNXi _ (subsetP (nElemS 1 sKsKi) _ E1Xs). - have [_ hallKis] := hallK_Zi _ MXi; rewrite defNi in hallKis. - have sZNXs: Z \subset 'N_Mi(Xs) by case/(Pmax_sym M K): maxNMi => // _ _ _ ->. - apply/eqP; rewrite eqEsubset andbC {1}defNi -defNXs sZNXs. - have [_ _ cKiKis tiKiKis] := dprodP defNi; rewrite dprodEY // -defZ -defNX. - have E1KiXs: Xs \in 'E^1(K_ Mi) := subsetP (nElemS 1 sKsKi) Xs E1Xs. - have [|_ _ _ -> //] := Pmax_sym Mi _ Xs M PmaxMi hallKi E1KiXs. - have [p EpXs] := nElemP E1Xs; have [_] := pnElemP EpXs; case/andP=> pXs _ _. - rewrite inE maxM (sub_uniq_mmax (uniqCKs _ E1Xs)) ?cent_sub //=. - exact: mFT_norm_proper (nt_pnElem EpXs isT) (mFT_pgroup_proper pXs). - have [q /pnElemP[sXK abelX dimX]] := nElemP E1X. - apply/nElemP; exists q; apply/pnElemP; split=> //. - have nKisZi: Ks_ Mi <| 'N_Mi(K_ Mi) by case/dprod_normal2: defNi. - rewrite (sub_normal_Hall hallKis) ?(pgroupS sXMis (pcore_pgroup _ _)) //=. - by rewrite -defNXs (subset_trans sXK) // (subset_trans (joing_subl _ Ks)). -have{hallK_Zi} hallK_Z: {in MX, forall Mi, co_sHallK Mi Z}. - by move=> Mi MXi; rewrite -(defZX _ MXi); apply: hallK_Zi. -have nsK_Z: {in MX, forall Mi, K_ Mi <| Z /\ Ks_ Mi <| Z}. - by move=> Mi /defZX; apply: dprod_normal2. -have tiKs: {in MX &, forall Mi Mj, gval Mi != gval Mj -> Ks_ Mi :&: Ks_ Mj = 1}. - move=> Mi Mj MXi MXj; apply: contraNeq; rewrite -rank_gt0. - case/rank_geP=> X E1X; move: E1X (E1X); rewrite /= {1}setIC {1}nElemI. - case/setIP=> E1jX _; rewrite nElemI => /setIP[E1iX _]. - have [[maxKi hallKi] [maxKj hallKj]] := (PmaxMX _ MXi, PmaxMX _ MXj). - have [_ _ [_ uniqMi] _ _] := Ptype_structure maxKi hallKi. - have [_ _ [_ uniqMj] _ _] := Ptype_structure maxKj hallKj. - by rewrite val_eqE -in_set1 -(uniqMj _ E1jX) (uniqMi _ E1iX) set11. -have sKsKX: {in MX &, forall Mi Mj, Mj != Mi -> Ks_ Mj \subset K_ Mi}. - move=> Mi Mj MXi MXj /= neqMji; have [hallKi hallKsi] := hallK_Z _ MXi. - have [[_ nsKsjZ] [nsKiZ _]] := (nsK_Z _ MXj, nsK_Z _ MXi). - rewrite (sub_normal_Hall hallKi) ?(normal_sub nsKsjZ) // -partG_eq1. - by rewrite -(card_Hall (Hall_setI_normal _ hallKsi)) //= setIC tiKs ?cards1. -have exMNX X: X \in 'E^1(K) -> exists2 Mi, Mi \in MNX & X \subset Mi`_\sigma. - move=> E1X; have [p EpX] := nElemP E1X; have [_ abelX _] := pnElemP EpX. - have ltXG: X \proper G := mFT_pgroup_proper (abelem_pgroup abelX). - have [Mi maxNMi] := mmax_exists (mFT_norm_proper (nt_pnElem EpX isT) ltXG). - have MNXi: Mi \in MNX by apply/bigcupP; exists X. - by exists Mi => //; have [_ ->] := defNX X E1X. -have dprodKs_eqZ: \big[dprod/1]_(Mi in MX) Ks_ Mi = Z; last clear dprodKs_eqZ. - have sYKs_KX Mi: - Mi \in MX -> <<\bigcup_(Mj in MX | Mj != Mi) Ks_ Mj>> \subset K_ Mi. - - move=> MXi; rewrite gen_subG. - by apply/bigcupsP=> Mj /= /andP[]; apply: sKsKX. - transitivity <<\bigcup_(Mi in MX) Ks_ Mi>>; apply/eqP. - rewrite -bigprodGE; apply/bigdprodYP => Mi MXi; rewrite bigprodGE. - apply: subset_trans (sYKs_KX _ MXi) _; apply/dprodYP. - have [_ defZi cKiKs tiKiKs] := dprodP (defZX _ MXi). - by rewrite dprodC joingC dprodEY. - rewrite eqEsubset {1}(bigD1 M) //= Ks0 setUC -joingE -joing_idl. - rewrite genS ?setSU ?big_setU1 //=; last by rewrite -K0 sYKs_KX. - rewrite setUC -joingE -joing_idl Ks0 genS ?setSU // -(Sylow_gen K) gen_subG. - apply/bigcupsP=> P; case/SylowP=> p p_pr /=; case/and3P=> sPK pP _. - have [-> | ] := eqsVneq P 1; first exact: sub1G. - rewrite -rank_gt0 (rank_pgroup pP); case/p_rank_geP=> X EpX. - have EpKX: X \in 'E_p^1(K) := subsetP (pnElemS p 1 sPK) X EpX. - have{EpKX} E1X: X \in 'E^1(K) by apply/nElemP; exists p. - have [Mi MNXi sXMis] := exMNX X E1X; have MXi: Mi \in MX by rewrite setU1r. - have [[_ nsKsi] [_ hallKsi]] := (nsK_Z _ MXi, hallK_Z _ MXi). - have sPZ: P \subset Z := subset_trans sPK (joing_subl _ _). - rewrite sub_gen ?(bigcup_max Mi) // (sub_normal_Hall hallKsi) //. - rewrite (pi_pgroup pP) // (pnatPpi (pcore_pgroup _ _) (piSg sXMis _)) //. - by have [_ ? dimX] := pnElemP EpX; rewrite -p_rank_gt0 p_rank_abelem ?dimX. -pose PZ := [set (Ks_ Mi)^# | Mi in MX]; pose T := Z^# :\: cover PZ. -have defT: \bigcup_(Mi in MX) (Ks_ Mi)^# * (K_ Mi)^# = T. - apply/setP=> x; apply/bigcupP/setDP=> [[Mi MXi] | [Zx notZXx]]. - case/mulsgP=> y y' /setD1P[nty Ks_y] /setD1P[nty' Ky'] defx. - have [_ defZi cKsKi tiKsKi] := dprodP (defZX _ MXi). - rewrite 2!inE -[Z]defZi -(centC cKsKi) andbC {1}defx mem_mulg //=. - have notKx: x \notin K_ Mi. - by rewrite -in_set1 -set1gE -tiKsKi inE Ks_y andbT defx groupMr in nty *. - split; first exact: group1_contra notKx. - rewrite cover_imset; apply/bigcupP=> [[Mj MXj /setD1P[_ Ksj_x]]]. - rewrite (subsetP (sKsKX Mi Mj _ _ _)) // in notKx. - apply: contraNneq nty' => eqMji; rewrite -in_set1 -set1gE -tiKsKi inE Ky'. - by rewrite -(groupMl _ Ks_y) -defx -eqMji. - have{Zx} [ntx Zx] := setD1P Zx. - have [Mi MXi notKi_x]: exists2 Mi, Mi \in MX & x \notin K_ Mi. - have [Kx | notKx] := boolP (x \in K); last by exists M; rewrite ?K0. - pose p := pdiv #[x]; have xp: p \in \pi(#[x]) by rewrite pi_pdiv order_gt1. - have /p_rank_geP[X EpX]: 0 < 'r_p(<[x]>) by rewrite p_rank_gt0. - have [sXx abelX dimX] := pnElemP EpX. - have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. - have sXK: X \subset K by rewrite (subset_trans sXx) ?cycle_subG. - have E1X: X \in 'E^1(K) by apply/nElemP; exists p; apply/pnElemP. - have [Mi MNXi sXMis] := exMNX X E1X; have MXi: Mi \in MX := setU1r M MNXi. - have sXZ: X \subset Z := subset_trans sXK (joing_subl _ _). - have sMip: p \in \sigma(Mi) := pnatPpi (pcore_pgroup _ _) (piSg sXMis piXp). - have [hallKi _] := hallK_Z _ MXi. - exists Mi => //; apply: contraL sMip => Ki_x. - exact: pnatPpi (mem_p_elt (pHall_pgroup hallKi) Ki_x) xp. - have [_ defZi cKisKi _] := dprodP (defZX _ MXi). - rewrite -[Z]defZi -(centC cKisKi) in Zx. - have [y y' Kis_y Ki_y' defx] := mulsgP Zx. - have Kis1y: y \in (Ks_ Mi)^#. - rewrite 2!inE Kis_y andbT; apply: contraNneq notKi_x => y1. - by rewrite defx y1 mul1g. - exists Mi; rewrite // defx mem_mulg // 2!inE Ki_y' andbT. - apply: contraNneq notZXx => y'1; rewrite cover_imset. - by apply/bigcupP; exists Mi; rewrite // defx y'1 mulg1. -have oT: #|T| = #|Z| + #|MNX| - (\sum_(Mi in MX) #|Ks_ Mi|). - have tiTPZ Kis: Kis \in PZ -> [disjoint T & Kis]. - move=> Z_Kis; rewrite -setI_eq0 setIDAC setD_eq0. - by rewrite (bigcup_max Kis) ?subsetIr. - have notPZset0: set0 \notin PZ. - apply/imsetP=> [[Mi MXi]]; apply/eqP; rewrite /= eq_sym setD_eq0 subG1. - exact: ntKsX. - have [| tiPZ injKs] := trivIimset _ notPZset0. - move=> Mi Mj MXi MXj /= neqMji. - by rewrite -setI_eq0 -setDIl setD_eq0 setIC tiKs. - have{tiPZ} [tiPZ notPZ_T] := trivIsetU1 tiTPZ tiPZ notPZset0. - rewrite (eq_bigr (fun Mi : {group gT} => 1 + #|(Ks_ Mi)^#|)%N); last first. - by move=> Mi _; rewrite (cardsD1 1) group1. - rewrite big_split sum1_card cardsU1 notMNX0 (cardsD1 1 Z) group1 /=. - have ->: Z^# = cover (T |: PZ). - rewrite -(setID Z^# (cover PZ)) setUC (setIidPr _) /cover ?big_setU1 //=. - apply/bigcupsP=> _ /imsetP[Mi MXi ->]; apply: setSD. - by case/nsK_Z: MXi => _ /andP[]. - by rewrite addnAC subnDl -(eqnP tiPZ) big_setU1 // big_imset //= addnK. -have tiTscov: {in 'M, forall H, [disjoint T & H^~~]}. - move=> H maxH; apply/pred0P=> t; apply/andP=> [[/= Tt scovHt]]. - have ntt: t != 1 by have [/setD1P[]] := setDP Tt. - have [x Hs_x xR_y] := bigcupP scovHt; have ell1x := Msigma_ell1 maxH Hs_x. - have:= sigma_decomposition_dichotomy ntt. - rewrite (introT existsP) /=; last by exists x; rewrite ell1x -mem_lcoset. - rewrite -defT in Tt; have [Mi MXi Zi_t] := bigcupP Tt. - case/mulsgP: Zi_t => y y' /setD1P[nty Ks_y] /setD1P[nty' Ky'] ->. - case/existsP; exists y; rewrite mulKg. - have [[Mis_y cKy] [PmaxMi hallKi]] := (setIP Ks_y, PmaxMX _ MXi). - have [[maxMi _] [sKiMi kMiKi _]] := (setDP PmaxMi, and3P hallKi). - rewrite (Msigma_ell1 maxMi) ?inE ?nty //=; apply/existsP; exists Mi. - rewrite inE maxMi cycle_subG Mis_y 3!inE nty' (subsetP sKiMi) //=. - by rewrite (subsetP _ _ Ky') ?sub_cent1 // (mem_p_elt kMiKi). -have nzT: T != set0. - have [[y Ksy nty] [y' Ky' nty']] := (trivgPn _ ntKs, trivgPn _ ntK). - apply/set0Pn; exists (y * y'); rewrite -defT; apply/bigcupP. - by exists M; rewrite ?MX0 // K0 Ks0 mem_mulg 2?inE ?nty ?nty'. -have ntiT: normedTI T G Z. - have sTZ: {subset T <= Z} by apply/subsetP; rewrite 2!subDset setUA subsetUr. - have nTZ: Z \subset 'N(T). - rewrite normsD ?norms_bigcup ?normD1 ?normG //. - apply/bigcapsP=> _ /imsetP[Mi MXi ->]; rewrite normD1. - by case/nsK_Z: MXi => _ /andP[]. - apply/normedTI_P; rewrite setTI /= -/Z. - split=> // a _ /pred0Pn[t /andP[/= Tt]]; rewrite mem_conjg => Tta. - have{Tta} [Zt Zta] := (sTZ t Tt, sTZ _ Tta). - move: Tt; rewrite -defT => /bigcupP[Mi MXi]. - case/mulsgP=> y y' /setD1P[nty Kisy] /setD1P[nty' Kiy'] def_yy'. - have [[hallKi hallKis] [nsKiZ _]] := (hallK_Z _ MXi, nsK_Z _ MXi). - have [[PmaxMi hallKiMi] defZi] := (PmaxMX _ MXi, defZX _ MXi). - have [_ [defNKi _] _ [[]]] := Ptype_structure PmaxMi hallKiMi. - rewrite -defNKi defZi -/(Ks_ _) => tiKsi tiKi _ _ _. - have [defy defy']: y = t.`_\sigma(Mi) /\ y' = t.`_\sigma(Mi)^'. - have [_ cKiy] := setIP Kisy; have cy'y := centP cKiy _ Kiy'. - have sMi_y := mem_p_elt (pHall_pgroup hallKis) Kisy. - have sMi'y' := mem_p_elt (pHall_pgroup hallKi) Kiy'. - rewrite def_yy' !consttM // constt_p_elt // 2?(constt1P _) ?p_eltNK //. - by rewrite mulg1 mul1g constt_p_elt. - have: a \in Mi. - apply: contraR nty; rewrite -in_setC -in_set1 -set1gE; move/tiKsi <-. - rewrite inE Kisy mem_conjg defy -consttJ groupX ?(subsetP _ _ Zta) //. - by rewrite -defZi defNKi subsetIl. - apply/implyP; apply: contraR nty'; rewrite negb_imply andbC -in_setD. - rewrite -in_set1 -set1gE => /tiKi <-; rewrite inE Kiy' defy' mem_conjg. - by rewrite -consttJ (mem_normal_Hall hallKi nsKiZ) ?p_elt_constt ?groupX. -have [_ tiT /eqP defNT] := and3P ntiT; rewrite setTI in defNT. -pose n : rat := #|MNX|%:R; pose g : rat := #|G|%:R. -pose z : rat := #|Z|%:R; have nz_z: z != 0%R := natrG_neq0 _ _. -pose k_ Mi : rat := #|K_ Mi|%:R. -have nz_ks: #|Ks_ _|%:R != 0%R :> rat := natrG_neq0 _ _. -pose TG := class_support T G. -have oTG: (#|TG|%:R = (1 + n / z - \sum_(Mi in MX) (k_ Mi)^-1) * g)%R. - rewrite /TG class_supportEr -cover_imset -(eqnP tiT). - rewrite (eq_bigr (fun _ => #|T|)) => [|_ /imsetP[x _ ->]]; last first. - by rewrite cardJg. - rewrite sum_nat_const card_conjugates setTI defNT. - rewrite natrM natf_indexg ?subsetT //= -/z -mulrA mulrC; congr (_ * _)%R. - rewrite oT natrB; last by rewrite ltnW // -subn_gt0 lt0n -oT cards_eq0. - rewrite mulrC natrD -/n -/z natr_sum /=. - rewrite mulrBl mulrDl big_distrl divff //=; congr (_ - _)%R. - apply: eq_bigr => Mi MXi; have defZi := defZX _ MXi. - by rewrite /z -(dprod_card defZi) natrM invfM mulrC divfK. -have neMNX: MNX != set0. - move: ntK; rewrite -rank_gt0 => /rank_geP[X /exMNX[Mi MNXi _]]. - by apply/set0Pn; exists Mi. -have [Mi MXi P2maxMi]: exists2 Mi, Mi \in MX & Mi \in 'M_'P2. - apply/exists_inP; apply: negbNE; rewrite negb_exists_in. - apply/forall_inP=> allP1; pose ssup Mi := class_support (gval Mi)^~~ G. - have{allP1} min_ssupMX Mi: - Mi \in MX -> (#|ssup Mi|%:R >= ((k_ Mi)^-1 - (z *+ 2)^-1) * g)%R. - - move=> MXi; have [PmaxMi hallKi] := PmaxMX _ MXi. - have [[U [complU defMi] _]] := Ptype_structure PmaxMi hallKi. - case=> defZi _ _ _ _; have [maxMi _] := setDP PmaxMi. - have{complU} U1: U :==: 1; last rewrite {U U1}(eqP U1) sdprod1g in defMi. - rewrite (trivg_kappa_compl maxMi complU). - by apply: contraR (allP1 _ MXi) => ?; apply/setDP. - rewrite card_class_support_sigma // natrM natf_indexg ?subsetT // -/g. - rewrite mulrCA mulrC ler_wpmul2r ?ler0n // -subn1 natrB ?cardG_gt0 //. - rewrite mulr1n mulrBl -{1}(sdprod_card defMi) natrM invfM. - rewrite mulVKf ?natrG_neq0 // ler_add2l ler_opp2 -(mulr_natr _ 2) invfM. - rewrite ler_pdivr_mulr ?natrG_gt0 // mulrC mulrA. - have sZM: Z \subset M by rewrite -defZ subsetIl. - have sZMi: Z \subset Mi by rewrite -(defZX _ MXi) defZi subsetIl. - rewrite -natf_indexg //= -/Z ler_pdivl_mulr ?(ltr0Sn _ 1) // mul1r ler_nat. - rewrite indexg_gt1 /= -/Z subEproper /proper sZMi andbF orbF. - apply: contraNneq notMNX0 => defMiZ; have [Mj MNXj] := set0Pn _ neMNX. - have maxZ: [group of Z] \in 'M by rewrite !inE defMiZ in maxMi *. - have eqZ := group_inj (eq_mmax maxZ _ _); rewrite -(eqZ M) //. - have [Xj E1Xj maxNMj] := bigcupP MNXj; have [maxMj _] := setIdP maxNMj. - by rewrite (eqZ Mj) //; case/(Pmax_sym M K): maxNMj. - pose MXsup := [set ssup Mi | Mi in MX]. - have notMXsup0: set0 \notin MXsup. - apply/imsetP=> [[Mi /PmaxMX[/setDP[maxMi _] _] /esym/eqP/set0Pn[]]]. - have [x Mis_x ntx] := trivgPn _ (Msigma_neq1 maxMi). - exists (x ^ 1); apply: mem_imset2; rewrite ?inE //. - by apply/bigcupP; exists x; rewrite ?inE ?ntx // lcoset_refl. - have [Mi Mj MXi MXj /= neqMij | tiMXsup inj_ssup] := trivIimset _ notMXsup0. - apply/pred0Pn=> [[_ /andP[/imset2P[x y1 signMi_x _ ->]]]] /=. - rewrite /ssup class_supportEr /= => /bigcupP[y2 _]. - rewrite -mem_conjgV -conjsgM -sigma_supportJ; set H := Mj :^ _ => Hx. - suffices: [disjoint Mi^~~ & H^~~]. - by case/pred0Pn; exists x; rewrite /= {1}signMi_x Hx. - have [[PmaxMi _] [PmaxMj _]] := (PmaxMX _ MXi, PmaxMX _ MXj). - have [[maxMi _] [maxMj _]] := (setDP PmaxMi, setDP PmaxMj). - apply: sigma_support_disjoint; rewrite ?mmaxJ //. - rewrite (orbit_transl _ (mem_orbit _ _ _)) ?inE //=. - apply: contra (ntKsX _ MXi); case/imsetP=> y _ /= defMj; rewrite -/(Ks_ _). - have sKisKj: Ks_ Mi \subset K_ Mj by rewrite sKsKX // eq_sym. - rewrite -(setIidPl sKisKj) coprime_TIg //. - have [[_ hallKis] [hallKj _]] := (hallK_Z _ MXi, hallK_Z _ MXj). - apply: pnat_coprime (pHall_pgroup hallKj). - by rewrite defMj -pgroupE (eq_pgroup _ (sigmaJ _ _)) (pHall_pgroup hallKis). - have [|tiPG notMXsupTG]: _ /\ TG \notin _ := trivIsetU1 _ tiMXsup notMXsup0. - move=> _ /imsetP[Mi /PmaxMX[/setDP[maxMi _] _] ->]. - apply/pred0Pn=> [[_ /andP[/imset2P[x y1 Tx _ ->]]]] /=. - rewrite /ssup class_supportEr => /bigcupP[y2 _]. - rewrite -mem_conjgV -conjsgM -sigma_supportJ; set H := Mi :^ _ => Hx. - have maxH: [group of H] \in 'M by rewrite mmaxJ. - by case/andP: (pred0P (tiTscov _ maxH) x). - suffices: (g <= #|cover (TG |: MXsup)|%:R)%R. - rewrite ler_nat (cardsD1 1 G) group1 ltnNge subset_leq_card //. - apply/bigcupsP=> _ /setU1P[|/imsetP[Mi /PmaxMX[/setDP[maxMi _] _]]] ->. - rewrite /TG class_supportEr; apply/bigcupsP=> x _. - rewrite sub_conjg (normP _) ?normD1 ?(subsetP (normG _)) ?inE //. - by rewrite subDset setUC subsetU // setSD ?subsetT. - rewrite /ssup class_supportEr; apply/bigcupsP=> x _. - rewrite subsetD1 subsetT mem_conjg conj1g {x}/=. - move/ell_sigma0P: (@erefl gT 1); rewrite cards_eq0. - apply: contraL => /bigcupP[x Mis_x xR1]; apply/set0Pn; exists x. - exact: mem_sigma_cover_decomposition (Msigma_ell1 maxMi Mis_x) xR1. - rewrite -(eqnP tiPG) big_setU1 ?big_imset //= natrD natr_sum. - suffices: (g <= #|TG|%:R + \sum_(i in MX) ((k_ i)^-1 - (z *+ 2)^-1) * g)%R. - by move/ler_trans->; rewrite // ler_add2l ler_sum. - rewrite -big_distrl /= oTG -/g -mulrDl big_split /= sumr_const. - rewrite addrA subrK -(mulr_natl _ 2) -[_ *+ _]mulr_natl invfM mulrN. - rewrite mulrA -addrA -mulrBl -{1}(mul1r g) ler_wpmul2r ?ler0n //. - rewrite ler_addl -(mul0r z^-1)%R ler_wpmul2r ?invr_ge0 ?ler0n //. - rewrite subr_ge0 ler_pdivr_mulr ?(ltr0Sn _ 1) // -natrM ler_nat. - by rewrite muln2 -addnn cardsU1 leq_add2r notMNX0 lt0n cards_eq0. -have [prKi nilMis]: prime #|K_ Mi| /\ nilpotent Mi`_\sigma. - by have [PmaxMi /Ptype_structure[] // _ _ _ _ []] := PmaxMX _ MXi. -have [Mj MXj neqMji]: exists2 Mj, Mj \in MX & Mj :!=: Mi. - have [Mj |] := pickP (mem ((MX) :\ Mi)); first by case/setD1P; exists Mj. - move/eq_card0/eqP; rewrite -(eqn_add2l true) -{1}MXi -cardsD1 cardsU1. - by rewrite notMNX0 eqSS cards_eq0 (negPf neMNX). -have defKjs: Ks_ Mj = K_ Mi. - have sKjsKi: Ks_ Mj \subset K_ Mi by rewrite sKsKX. - apply/eqP; rewrite eqEcard sKjsKi (prime_nt_dvdP _ _ (cardSg sKjsKi)) //=. - by rewrite -trivg_card1 ntKsX. -have defMXij: MX = [set Mi; Mj]. - symmetry; rewrite -(setD1K MXi); congr (_ |: _); apply/eqP. - rewrite eqEcard sub1set cards1 (cardsD1 Mj) 2!inE neqMji MXj /= ltnS leqn0. - apply/pred0Pn=> [[Mk /setD1P[neMkj /setD1P[neMki MXk]]]]. - have sKskKsj: Ks_ Mk \subset Ks_ Mj by rewrite defKjs sKsKX. - by case/negP: (ntKsX _ MXk); rewrite -(setIidPl sKskKsj) tiKs. -have defKsi: Ks_ Mi = K_ Mj. - apply/eqP; rewrite eqEcard sKsKX 1?eq_sym //=. - rewrite -(@leq_pmul2r #|Ks_ Mj|) ?cardG_gt0 // (dprod_card (defZX _ MXj)). - by rewrite defKjs mulnC (dprod_card (defZX _ MXi)). -have{nilMis} cycZ: cyclic Z. - have cycKi := prime_cyclic prKi. - apply: nil_Zgroup_cyclic. - apply/forall_inP=> S /SylowP[p _ /and3P[sSZ pS _]]. - have [[hallKi hallKis] [nsKi nsKis]] := (hallK_Z _ MXi, nsK_Z _ MXi). - have [sMi_p | sMi'p] := boolP (p \in \sigma(Mi)); last first. - by rewrite (cyclicS _ cycKi) // (sub_normal_Hall hallKi) ?(pi_pgroup pS). - have sSKj: S \subset K_ Mj. - by rewrite -defKsi (sub_normal_Hall hallKis) ?(pi_pgroup pS). - rewrite (odd_pgroup_rank1_cyclic pS) ?mFT_odd //. - apply: wlog_neg; rewrite -ltnNge ltn_neqAle p_rank_gt0 => /andP[_ piSp]. - have [_ /and3P[sKjMj kKj _]] := PmaxMX _ MXj. - rewrite -(rank_kappa (pnatPpi kKj (piSg sSKj piSp))) p_rankS //. - exact: subset_trans sSKj sKjMj. - rewrite (dprod_nil (defZX _ MXi)) abelian_nil ?cyclic_abelian //=. - exact: (nilpotentS (subsetIl _ _)) nilMis. -have cycK: cyclic K := cyclicS (joing_subl _ _) cycZ. -have defM: M^`(1) ><| K = M. - have [U complU] := ex_kappa_compl maxM hallK; have [hallU _ _] := complU. - have [_ defM _ regUK _] := kappa_compl_context maxM complU. - have{hallU} [[sUM _] [sKM kK _]] := (andP hallU, and3P hallK). - case/sdprodP: defM => [[_ E _ defE]]; rewrite defE. - case/sdprodP: defE => _ <-{E} nUK _ defM /mulGsubP[nMsU nMsK] tiMsUK. - pose MsU := M`_\sigma <*> U; have nMsUK: K \subset 'N(MsU) by rewrite normsY. - have defMl: MsU * K = M by rewrite [MsU]norm_joinEr // -mulgA. - have coUK := regular_norm_coprime nUK regUK. - have ->: M^`(1) = MsU. - apply/eqP; rewrite eqEsubset; apply/andP; split; last first. - have solU := solvableS sUM (mmax_sol maxM). - rewrite join_subG Msigma_der1 //= -(coprime_cent_prod nUK coUK solU). - by rewrite (cent_semiregular regUK) // mulg1 commgSS. - apply: der1_min; first by rewrite -{1}defMl mulG_subG normG. - by rewrite -{2}defMl quotientMidl quotient_abelian ?cyclic_abelian. - rewrite sdprodE ?coprime_TIg //= norm_joinEr //. - rewrite (coprime_dvdl (dvdn_cardMg _ _)) // coprime_mull coUK. - rewrite (pnat_coprime (pcore_pgroup _ _) (sub_pgroup _ kK)) //. - exact: kappa_sigma'. -have{neMNX} [Mstar MNX'star] := set0Pn _ neMNX. -have defMNX: MNX = [set Mstar]. - apply/eqP; rewrite eq_sym eqEcard sub1set MNX'star /= -(leq_add2l true). - by rewrite -{1}notMNX0 -cardsU1 -/MX defMXij setUC cards2 neqMji !cards1. -have MXstar: Mstar \in MX by rewrite setU1r. -have [[PmaxMstar hallKstar] defZstar] := (PmaxMX _ MXstar, defZX _ MXstar). -have [maxMstar _] := setDP PmaxMstar. -have notMGMstar := notMG_MNX _ MNX'star; exists Mstar => //. -have [defKs defKs_star]: Ks = K_ Mstar /\ Ks_ Mstar = K. - rewrite /Ks /Ks_ -K0; rewrite /MX defMNX 3!inE val_eqE in neqMji MXj MXi. - by case/set2P: MXi (negPf neqMji) MXj => <- ->; rewrite ?orbF /= => /eqP <-. -have hallKs: \sigma(M).-Hall(Mstar) Ks. - have sKsMstar: Ks \subset Mstar by rewrite defKs (pHall_sub hallKstar). - have sM_Ks: \sigma(M).-group Ks := pgroupS (subsetIl _ _) (pcore_pgroup _ _). - have [Y hallY sKsY] := Hall_superset (mmax_sol maxMstar) sKsMstar sM_Ks. - have [sYMstar sM_Y _] := and3P hallY; apply: etrans hallY; congr pHall. - have sYMs: Y \subset M`_\sigma. - case/Ptype_structure: hallK => // _ _ _ [_ _ -> //]. - by rewrite (setIidPr sKsY). - apply/eqP; rewrite eqEsubset sKsY subsetI sYMs (sameP commG1P trivgP) /=. - have <-: M`_\sigma :&: Mstar`_\sigma = 1. - rewrite coprime_TIg // (pnat_coprime (pcore_pgroup _ _)) //. - apply: sub_pgroup (pcore_pgroup _ _) => q sM1q. - apply: contraFN (sigma_partition maxM maxMstar notMGMstar q) => sMq. - exact/andP. - rewrite commg_subI //. - by rewrite subsetI sYMs (subset_trans sYMstar) ?gFnorm. - rewrite subsetI -{1}defKs_star subsetIl. - by rewrite (subset_trans (pHall_sub hallK)) ?gFnorm. -have oTGgt_g2: (g / 2%:R < #|TG|%:R)%R. - rewrite oTG big_setU1 //= /n defMNX big_set1 cards1 mulrC mul1r. - rewrite ltr_pmul2r ?(ltr_nat _ 0) ?cardG_gt0 // /k_ K0 -defKs. - rewrite /z -defZ -(dprod_card defNK) natrM invfM opprD. - pose hm u : rat := (1 - u%:R^-1)%R; set lhs := (_^-1)%R. - suffices: (lhs < hm #|K| * hm #|Ks|)%R. - by rewrite mulrBl !mulrBr !mul1r mulr1 opprB addrAC !addrA. - have hm_inc u v: 0 < u <= v -> (hm u <= hm v)%R. - case/andP=> u_gt0 le_uv; rewrite ler_add2l ler_opp2. - have v_gt0 := leq_trans u_gt0 le_uv. - rewrite -(mul1r _^-1)%R ler_pdivr_mulr ?ltr0n //. - by rewrite ler_pdivl_mull ?ltr0n // mulr1 ler_nat. - have le_pdiv H: 0 < pdiv #|H| <= #|H| by rewrite pdiv_gt0 dvdn_leq ?pdiv_dvd. - have{le_pdiv} hm_pdiv := hm_inc _ _ (le_pdiv _). - have hm_ge0 u: (0 <= hm u)%R. - by case: u => // u; rewrite subr_ge0 invf_le1 ?ltr0Sn ?(ler_nat _ 1). - do 2![rewrite mulrC (ltr_le_trans _ (ler_wpmul2r (hm_ge0 _) (hm_pdiv _))) //]. - set p := pdiv #|K|; set q := pdiv #|Ks|. - have [odd_p odd_q]: odd p /\ odd q. - by split; apply: dvdn_odd (pdiv_dvd _) (mFT_odd _). - without loss [lt1p ltpq]: p q odd_p odd_q / 1 < p /\ p < q. - have [p_pr q_pr]: prime p /\ prime q by rewrite !pdiv_prime ?cardG_gt1. - have [ltpq | ltqp | eqpq] := ltngtP p q. - - by apply; rewrite ?prime_gt1. - - by rewrite mulrC; apply; rewrite ?prime_gt1. - have [] := hallK_Z _ MX0. - rewrite K0 Ks0 => /and3P[_ sM'K _] /and3P[_ sMKs _]. - case/negP: (pgroupP sM'K _ p_pr (pdiv_dvd _)); rewrite eqpq. - exact: pgroupP sMKs _ q_pr (pdiv_dvd _). - have p_gt2: 2 < p by rewrite odd_geq. - apply: ltr_le_trans (isT : lhs < hm 3 * hm 5)%R _. - by rewrite ler_pmul ?hm_inc ?hm_ge0 //= odd_geq ?(leq_trans _ ltpq). -have defZhat: Z :\: (K :|: Ks) = T. - rewrite /T cover_imset big_setU1 //= defMNX big_set1 defKs_star Ks0. - by rewrite -setDUl setDDl setUC setD1K // inE group1. -rewrite defZhat {1}defKs; split; first 2 [by split]. -- by rewrite -defKs_star; case/Ptype_structure: hallKstar => // _ _ []. -- split=> [|p]; first by rewrite -defKs_star defKs. - apply/idP/idP=> [kMp | t1p]. - have /orP[// | /and3P[_ _ p_dv_M']] := kappa_tau13 kMp. - have hallM': \kappa(M)^'.-Hall(M) M^`(1). - exact/(sdprod_normal_pHallP (der_normal 1 M) hallK). - have piMp: p \in \pi(M) by rewrite kappa_pi. - case/idPn: kMp; apply: (pnatPpi (pHall_pgroup hallM')). - by move: piMp; rewrite !mem_primes !cardG_gt0 /= => /andP[->]. - apply: (pnatPpi (pHall_pgroup hallK)); have [_ _ not_p_dv_M'] := and3P t1p. - have: p \in \pi(M) by rewrite (partition_pi_mmax maxM) t1p ?orbT. - rewrite !mem_primes !cardG_gt0 /= => /andP[p_pr]. - by rewrite p_pr -(sdprod_card defM) Euclid_dvdM // (negPf not_p_dv_M'). -- split=> // [| x | y | x y K1_x Ks1_y]. - + have defMsMstar: M`_\sigma :&: Mstar = Ks. - apply: sub_pHall hallKs _ _ (subsetIr _ _). - exact: pgroupS (subsetIl _ _) (pcore_pgroup _ _). - by rewrite subsetI subsetIl /= -/Ks defKs (pHall_sub hallKstar). - have nKsMMstar: M :&: Mstar \subset 'N(Ks). - by rewrite -defMsMstar normsIG ?gFnorm. - have [_ [defNKs _] _ _ _] := Ptype_structure PmaxMstar hallKstar. - rewrite -(setIidPl nKsMMstar) -setIA defKs -defNKs defZstar. - by rewrite -defZ setIA setIid. - + case/setD1P; rewrite -cycle_eq1 -cycle_subG -cent_cycle => ntx sxK. - apply/eqP; rewrite eqEsubset andbC subsetI -{1}defZ subsetIl. - rewrite sub_abelian_cent ?cyclic_abelian //=; last first. - by rewrite (subset_trans sxK) ?joing_subl. - move: ntx; rewrite -rank_gt0 /= -{1}(setIidPr sxK) => /rank_geP[X]. - rewrite nElemI -setIdE -defZ => /setIdP[E1X sXx]. - by have [<- _] := defNX _ E1X; rewrite setIS ?cents_norm ?centS. - + case/setD1P; rewrite -cycle_eq1 -cycle_subG -cent_cycle => nty syKs. - have [_ [defNKs defNY] _ _ _] := Ptype_structure PmaxMstar hallKstar. - rewrite defZstar -defKs in defNKs defNY. - apply/eqP; rewrite eqEsubset andbC subsetI {1}defNKs subsetIl. - rewrite sub_abelian_cent ?cyclic_abelian //=; last first. - by rewrite (subset_trans syKs) ?joing_subr. - move: nty; rewrite -rank_gt0 /= -{1}(setIidPr syKs) => /rank_geP[Y]. - rewrite nElemI -setIdE defNKs => /setIdP[E1Y sYy]. - by have [<- _] := defNY _ E1Y; rewrite setIS ?cents_norm ?centS. - have [[_ K_x] [_ Ks_y]] := (setD1P K1_x, setD1P Ks1_y). - apply/eqP; rewrite eqEsubset sub_cent1 -(centsP cKKs) //. - have Tyx: y * x \in T by rewrite -defT big_setU1 //= inE Ks0 K0 mem_mulg. - rewrite (subset_trans _ (cent1_normedTI ntiT Tyx)) ?setTI //. - rewrite (subsetP _ _ Tyx) // -defZhat setDE subIset //. - by rewrite -abelianE cyclic_abelian. -split=> // [||H PmaxH]. -- split=> // a notMa. - have{tiKs} [_ _ _ [[tiKs _] _ _] _] := Ptype_structure PmaxM hallK. - rewrite -defT big_setU1 //= defMNX big_set1 -defKs defKs_star Ks0 K0. - rewrite centC ?(centSS _ _ cKKs) ?subsetDl // setUid. - apply/pred0Pn=> [[_ /andP[/mulsgP[x y K1_x Ks1_y ->] /= Ma_xy]]]. - have [[_ K_x] [nty Ks_y]] := (setD1P K1_x, setD1P Ks1_y); case/negP: nty. - rewrite -in_set1 -set1gE -(tiKs a notMa) inE Ks_y. - suffices ->: y = (x * y).`_\sigma(M) by rewrite groupX. - rewrite consttM; last by red; rewrite -(centsP cKKs). - have sM'K := sub_pgroup (@kappa_sigma' M) (pHall_pgroup hallK). - rewrite (constt1P (mem_p_elt sM'K K_x)) mul1g constt_p_elt //. - exact: mem_p_elt (pHall_pgroup hallKs) Ks_y. -- have:= set21 Mi Mj; rewrite -defMXij /MX defMNX defKs -K0. - by case/set2P=> <-; [left | right]. -have [maxH _] := setDP PmaxH. -have{maxH}[L hallL] := Hall_exists \kappa(H) (mmax_sol maxH). -pose Ls := 'C_(H`_\sigma)(L); pose S := (L <*> Ls) :\: (L :|: Ls). -have{IHn} oSGgt_g2: (g / 2%:R < #|class_support S G|%:R)%R. - have [|nTG_leS] := ltnP #|class_support S G| nTG. - by case/IHn=> // Sstar _ [_ _ _ _ [[_ _ -> //]]]. - apply: ltr_le_trans oTGgt_g2 _; rewrite ler_nat /TG -defZhat. - exact: leq_trans leTGn nTG_leS. -have{oSGgt_g2 oTGgt_g2} meetST: ~~ [disjoint TG & class_support S G]. - rewrite -leq_card_setU; apply: contraTneq (leqnn #|G|) => tiTGS. - rewrite -ltnNge -(ltr_nat [realFieldType of rat]) -/g. - rewrite -{1}[g](@divfK _ 2%:R) // mulr_natr. - apply: ltr_le_trans (ltr_add oTGgt_g2 oSGgt_g2) _. - by rewrite -natrD -tiTGS ler_nat cardsT max_card. -have{meetST} [x Tx [a Sx]]: exists2 x, x \in T & exists a, x \in S :^ a. - have [_ /andP[/imset2P[x a1 Tx _ ->]]] := pred0Pn meetST. - rewrite class_supportEr => /bigcupP[a2 _ Sa2_xa1]. - by exists x => //; exists (a2 * a1^-1); rewrite conjsgM mem_conjgV. -rewrite {}/S {}/Ls in Sx; without loss a1: a H L PmaxH hallL Sx / a = 1. - move/(_ 1 (H :^ a)%G (L :^ a)%G); rewrite conjsg1 PtypeJ PmaxH pHallJ2. - rewrite (eq_pHall _ _ (kappaJ H a)) hallL MsigmaJ centJ. - rewrite -conjIg -conjYg -conjUg -conjDg Sx !inE. - by rewrite !(orbit_transl _ (mem_orbit _ _ _)) ?inE //; apply. -have [_ [defNL _] [_ uniqH] _ _] := Ptype_structure PmaxH hallL. -do [rewrite {a}a1 conjsg1; set Ls := 'C_(_)(L)] in Sx defNL. -have{x Sx Tx} [Mk MXk ntLsMks]: exists2 Mk, Mk \in MX & Ls :&: Ks_ Mk != 1. - have [_ _ cLLs tiLLs] := dprodP defNL. - pose W := L <*> Ls; pose y := x.`_\sigma(H); pose ys := y.`_\sigma(Mi). - have Zy: y \in Z by apply: groupX; case/setDP: Tx; case/setD1P=> _ ->. - have{hallL} [hallL hallLs]: \sigma(H)^'.-Hall(W) L /\ \sigma(H).-Hall(W) Ls. - apply: coprime_mulGp_Hall; first by rewrite /= cent_joinEr. - exact: sub_pgroup (@kappa_sigma' H) (pHall_pgroup hallL). - exact: pgroupS (subsetIl _ _) (pcore_pgroup _ _). - have [nsLW nsLsW]: L <| W /\ Ls <| W := cprod_normal2 (cprodEY cLLs). - have{Sx} [Ls_y nty]: y \in Ls /\ y != 1. - move: Sx; rewrite 2!inE negb_or -andbA -/W; case/and3P=> notLx _ Wx. - split; first by rewrite (mem_normal_Hall hallLs) ?p_elt_constt ?groupX. - by rewrite (sameP eqP constt1P) -(mem_normal_Hall hallL). - have [[hallKi hallKis] [nsKi nsKis]] := (hallK_Z _ MXi, nsK_Z _ MXi). - have [/constt1P sM'y | ntys] := altP (ys =P 1). - exists Mj; rewrite // defKjs. - by apply/trivgPn; exists y; rewrite // inE Ls_y (mem_normal_Hall hallKi). - exists Mi => //; apply/trivgPn; exists ys; rewrite // inE groupX //=. - by rewrite (mem_normal_Hall hallKis) ?p_elt_constt // groupX. -suffices ->: H = Mk. - by move: MXk; rewrite /MX defMNX => /set2P[]->; rewrite inE orbit_refl ?orbT. -move: ntLsMks; rewrite -rank_gt0 => /rank_geP[Y E1Y]. -have:= E1Y; rewrite nElemI => /setIP[E1LsY _]. -apply: set1_inj; rewrite -(uniqH _ E1LsY). -have [PmaxMk hallKk] := PmaxMX _ MXk. -have [_ _ [_ -> //]] := Ptype_structure PmaxMk hallKk. -by rewrite /= setIC nElemI in E1Y; case/setIP: E1Y. -Qed. - -End PTypeEmbedding. - -(* This is the first part of B & G, Corollary 14.8. *) -Corollary P1type_trans : {in 'M_'P1 &, forall M H, gval H \in M :^: G}. -Proof. -move=> M H P1maxM P1maxH; have [PmaxM _] := setIdP P1maxM. -have [[maxM _] [PmaxH _]] := (setDP PmaxM, setIdP P1maxH). -have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). -have [Mstar _ [_ _ _ _ [_ [|]]]] := Ptype_embedding PmaxM hallK. - by case; rewrite inE P1maxM. -case=> /setDP[_ /negP notP1maxMstar] _. -case/(_ H PmaxH)/setUP=> // /imsetP[a _ /group_inj defH]. -by rewrite defH P1typeJ in P1maxH. -Qed. - -(* This is the second part of B & G, Corollary 14.8. *) -Corollary Ptype_trans : {in 'M_'P, forall M, - exists2 Mstar, Mstar \in 'M_'P /\ gval Mstar \notin M :^: G - & {in 'M_'P, forall H, gval H \in M :^: G :|: Mstar :^: G}}. -Proof. -move=> M PmaxM; have [maxM _] := setDP PmaxM. -have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). -have [Mstar PmaxMstar [_ _ _ _ [_ _ inMMs _]]] := Ptype_embedding PmaxM hallK. -by exists Mstar. -Qed. - -(* This is B & G, Corollary 14.9. *) -Corollary mFT_partition : - let Pcover := [set class_support M^~~ G | M : {group gT} in 'M] in - [/\ (*1*) 'M_'P == set0 :> {set {group gT}} -> partition Pcover G^# - & (*2*) forall M K, M \in 'M_'P -> \kappa(M).-Hall(M) K -> - let Ks := 'C_(M `_\sigma)(K) in let Z := K <*> Ks in - let Zhat := Z :\: (K :|: Ks) in - let ClZhat := class_support Zhat G in - partition (ClZhat |: Pcover) G^# /\ ClZhat \notin Pcover]. -Proof. -move=> Pcover; have notPcover0: set0 \notin Pcover. - apply/imsetP=> [[M maxM]]; apply/eqP; rewrite eq_sym; apply/set0Pn. - have [x Ms_x ntx] := trivgPn _ (Msigma_neq1 maxM); exists x. - rewrite class_supportEl; apply/bigcupP; exists x; last exact: class_refl. - by apply/bigcupP; exists x; [apply/setD1P | apply: lcoset_refl]. -have tiPcover: trivIset Pcover. - apply/trivIsetP=> _ _ /imsetP[M maxM ->] /imsetP[H maxH ->] notMGH. - rewrite -setI_eq0 !{1}class_supportEr big_distrr big1 //= => a Ga. - rewrite big_distrl big1 //= => b Gb; apply/eqP. - rewrite -!{1}sigma_supportJ setI_eq0 sigma_support_disjoint ?mmaxJ //. - apply: contra notMGH; rewrite {a Ga}(orbit_transl _ (mem_orbit _ _ Ga)). - rewrite {b Gb}(orbit_eqP (mem_orbit _ _ Gb))=> /imsetP[c Gc ->] /=. - by rewrite sigma_supportJ class_supportGidl. -have ntPcover: cover Pcover \subset G^#. - apply/bigcupsP=> _ /imsetP[M maxM ->]; rewrite class_supportEr. - apply/bigcupsP=> a _; rewrite subsetD1 subsetT mem_conjg conj1g {a}//=. - move/ell_sigma0P: (@erefl gT 1); rewrite cards_eq0; apply: contraL. - case/bigcupP=> x Ms_x xR1; apply/set0Pn; exists x. - exact: mem_sigma_cover_decomposition (Msigma_ell1 maxM Ms_x) xR1. -split=> [MP0 | M K PmaxM hallK Ks Z Zhat ClZhat]. - rewrite /partition eqEsubset ntPcover tiPcover notPcover0 !andbT /=. - apply/subsetP=> x; rewrite !inE andbT => ntx. - have:= sigma_decomposition_dichotomy ntx. - have [[y ell1y yRx] _ | _] := exists_inP. - have [nty /set0Pn[M /setIdP[maxM Ms_y]]] := ell_sigma1P _ ell1y. - apply/bigcupP; exists (class_support M^~~ G); first exact: mem_imset. - rewrite -(conjg1 x) mem_imset2 ?inE //. - apply/bigcupP; exists y; last by rewrite mem_lcoset. - by rewrite !inE nty -cycle_subG. - case/exists_inP=> y _; move: (_ * x) => y' /existsP[M]. - case/and3P => /setIdP[maxM _] /setD1P[nty' /setIP[My' _]] kMy' {y}. - case/set0Pn: MP0; exists M; rewrite 2!inE maxM andbT. - apply: contra nty' => kM'M; rewrite -order_eq1 (pnat_1 kMy') //. - exact: mem_p_elt kM'M My'. -have [_ [defNK _] [ntKs _] _ _] := Ptype_structure PmaxM hallK. -have [Mst [PmaxMst _] [_ [hallKst _] [defK _]]] := Ptype_embedding PmaxM hallK. -rewrite -/Ks -/Z -/Zhat in ntKs hallKst * => _ [_ _ conjMMst _]. -have [_ _ [ntK _] _ _] := Ptype_structure PmaxMst hallKst. -have [maxM _] := setDP PmaxM; rewrite defK in ntK. -have [|//|tiZPcover notPcovZ]: _ /\ ClZhat \notin _ := trivIsetU1 _ tiPcover _. - move=> HcovG; case/imsetP=> H maxH ->{HcovG}. - rewrite -setI_eq0 /ClZhat !class_supportEr big_distrr big1 //= => a _. - rewrite big_distrl big1 //= => b _; apply/eqP; rewrite -cards_eq0. - rewrite -(cardJg _ b^-1) conjIg conjsgK -conjsgM -sigma_supportJ cards_eq0. - wlog ->: a b H maxH / H :^ (a * b^-1) = H. - by move/(_ a a (H :^ (a * b^-1))%G); rewrite mmaxJ mulgV act1 => ->. - rewrite setIC big_distrl big1 //= => y Hs_y; apply/setP=> x; rewrite in_set0. - rewrite 3!inE mem_lcoset negb_or -andbA; apply/and4P=> [[yRx notKx notKs_x]]. - rewrite /Z cent_joinEr ?subsetIr //; case/mulsgP=> z z' Kz Ks_z' defx. - have:= sigma_decomposition_dichotomy (group1_contra notKx). - rewrite (introT exists_inP) /=; last first. - by exists y; rewrite // (Msigma_ell1 maxH). - have [Ms_z' cKz'] := setIP Ks_z'; case/exists_inP; exists z'. - rewrite (Msigma_ell1 maxM) ?inE // Ms_z' andbT. - by apply: contraNneq notKx => z'1; rewrite defx z'1 mulg1. - apply/existsP; exists M; rewrite inE maxM cycle_subG Ms_z'. - rewrite defx -(centP cKz') // mulKg (mem_p_elt (pHall_pgroup hallK)) //=. - rewrite 3!inE (subsetP (pHall_sub hallK)) //= cent1C !andbT. - rewrite andbC cent1C (subsetP _ _ Kz) ?sub_cent1 //=. - by apply: contraNneq notKs_x => z1; rewrite defx z1 mul1g. -split=> //; rewrite /partition eqEsubset 2!inE {}tiZPcover negb_or notPcover0. -rewrite /cover big_setU1 {notPcovZ}//= subUset ntPcover subsetD1 subsetT. -rewrite {}/ClZhat {}/Zhat !andbT /= andbC; apply/and3P; split. -- have [[y Ks_y nty] [y' Ky' nty']] := (trivgPn _ ntKs, trivgPn _ ntK). - rewrite eq_sym; apply/set0Pn; exists ((y' * y) ^ 1). - apply: mem_imset2; rewrite 2?inE // groupMl // groupMr // -/Ks negb_or. - have [_ _ _ tiKKs] := dprodP defNK. - rewrite -[Z]genM_join ?mem_gen ?mem_mulg //= andbT; apply/andP; split. - by apply: contra nty => Ky; rewrite -in_set1 -set1gE -tiKKs inE Ky. - by apply: contra nty' => Ks_y'; rewrite -in_set1 -set1gE -tiKKs inE Ky'. -- rewrite class_supportEr; apply/bigcupP=> [[a _]]. - by rewrite mem_conjg conj1g 2!inE !group1. -apply/subsetP=> x; case/setD1P=> ntx _; apply/setUP. -case: exists_inP (sigma_decomposition_dichotomy ntx) => [[y ell1y yRx] _ | _]. - have [nty] := ell_sigma1P _ ell1y; case/set0Pn=> H; case/setIdP=> maxH Hs_y. - right; apply/bigcupP; exists (class_support H^~~ G); first exact: mem_imset. - rewrite -[x]conjg1 mem_imset2 ?inE //; apply/bigcupP. - by exists y; rewrite ?mem_lcoset // !inE nty -cycle_subG. -case/exists_inP=> y ell1y /existsP[H]; set y' := y^-1 * x. -case/and3P=> /setIdP[maxH Hs_y] /setD1P[nty' /setIP[Hy' cyy']] kHy'. -rewrite {ntK ntKs maxM defNK}/Z /Ks; left. -wlog{Ks Mst PmaxMst hallKst conjMMst defK maxH} defH: M K PmaxM hallK / H :=: M. - move=> IH; have PmaxH: H \in 'M_'P. - apply/PtypeP; split=> //; exists (pdiv #[y']). - by rewrite (pnatPpi kHy') // pi_pdiv order_gt1. - have [|] := setUP (conjMMst H PmaxH); case/imsetP=> a Ga defH. - have:= IH _ (K :^ a)%G _ _ defH. - rewrite (eq_pHall _ _ (kappaJ _ _)) pHallJ2 PtypeJ MsigmaJ centJ. - by rewrite -conjIg -conjUg -conjYg -conjDg class_supportGidl //; apply. - have:= IH _ [group of Ks :^ a] _ _ defH. - rewrite (eq_pHall _ _ (kappaJ _ _)) pHallJ2 PtypeJ MsigmaJ centJ. - rewrite -conjIg -conjUg -conjYg -conjDg setUC joingC defK. - by rewrite class_supportGidl //; apply. -have /andP[sMsM nMsM]: M`_\sigma <| M := pcore_normal _ M. -have{Hs_y} Ms_y: y \in M`_\sigma by rewrite -defH -cycle_subG. -wlog{H defH Hy' kHy'} Ky': K hallK / y' \in K. - have [maxM _] := setDP PmaxM; rewrite -cycle_subG defH in Hy' kHy'. - have [a Ma Ka_y'] := Hall_subJ (mmax_sol maxM) hallK Hy' kHy'. - move/(_ (K :^ a)%G); rewrite pHallJ // -cycle_subG. - rewrite -{1 2}(normsP nMsM a Ma) centJ -conjIg -conjYg -conjUg -conjDg. - by rewrite class_supportGidl ?inE //; apply. -rewrite -[x]conjg1 mem_imset2 ?group1 //. -have [Mst _ [_ _ _ [cycZ _ defZ _ _] _]] := Ptype_embedding PmaxM hallK. -rewrite -(mulKVg y x) -/y' 2!inE negb_or andbC. -do [set Ks := 'C_(_)(K); set Z := K <*> _] in cycZ defZ *. -have Ks_y: y \in Ks. - have cKZ := sub_abelian_cent (cyclic_abelian cycZ) (joing_subl K Ks). - rewrite inE Ms_y (subsetP cKZ) // -(defZ y'); last by rewrite !inE nty'. - by rewrite inE cent1C (subsetP sMsM). -have [_ [defNK _] _ _ _] := Ptype_structure PmaxM hallK. -have{defNK} [_ _ cKKs tiKKs] := dprodP defNK. -rewrite [Z]joingC cent_joinEl // mem_mulg // groupMr // groupMl //= -/Ks. -apply/andP; split. - have [nty _] := ell_sigma1P _ ell1y. - by apply: contra nty => Ky; rewrite -in_set1 -set1gE -tiKKs inE Ky. -by apply: contra nty' => Ks_y'; rewrite -in_set1 -set1gE -tiKKs inE Ky'. -Qed. - -(* This is B & G, Corollary 14.10. *) -Corollary ell_sigma_leq_2 x : \ell_\sigma(x) <= 2. -Proof. -have [/ell_sigma0P/eqP-> // | ntx] := eqVneq x 1. -case sigma_x: (x \in cover [set class_support M^~~ G | M : {group gT} in 'M]). - case/bigcupP: sigma_x => _ /imsetP[M maxM ->]. - case/imset2P=> x0 a /bigcupP[y Ms_y yRx0] _ ->; rewrite ell_sigmaJ. - exact: ell_sigma_cover (Msigma_ell1 maxM Ms_y) yRx0. -have G1x: x \in G^# by rewrite !inE andbT. -have [FpartG1 PpartG1] := mFT_partition. -have [/eqP/FpartG1 partG1 | [M PmaxM]] := set_0Vmem ('M_'P : {set {group gT}}). - by rewrite -(cover_partition partG1) sigma_x in G1x. -have [maxM _] := setDP PmaxM. -have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). -have{PpartG1} [/cover_partition defG1 notZsigma] := PpartG1 M K PmaxM hallK. -rewrite -{}defG1 /cover big_setU1 {notZsigma}// inE {}sigma_x orbF in G1x. -case/imset2P: G1x => x0 a /setDP[]. -have [Mst [PmaxMst _] [_ _ [defK _] _ _]] := Ptype_embedding PmaxM hallK. -rewrite cent_joinEr ?subsetIr // => /mulsgP[y' y Ky' /= Ks_y ->]. -rewrite inE; have [-> | nty] := eqVneq y 1; first by rewrite mulg1 Ky'. -have [-> | nty' _ _ ->] := eqVneq y' 1; first by rewrite mul1g Ks_y orbT. -have [Ms_y cKy] := setIP Ks_y; set Ks := 'C_(_)(_) in Ks_y defK. -have Msts_y': y' \in Mst`_\sigma by move: Ky'; rewrite -defK => /setIP[]. -have kMy': \kappa(M).-elt y' := mem_p_elt (pHall_pgroup hallK) Ky'. -have{kMy'} sM'y': \sigma(M)^'.-elt y' := sub_pgroup (@kappa_sigma' _) kMy'. -rewrite ell_sigmaJ /sigma_length (cardsD1 (y' * y).`_\sigma(M)). -rewrite (leq_add (leq_b1 _)) // -sigma_decomposition_constt' //. -rewrite consttM /commute ?(centP cKy) // constt_p_elt //. -rewrite (constt1P _) ?p_eltNK ?(mem_p_elt (pcore_pgroup _ _) Ms_y) // mulg1. -have [maxMst _] := setDP PmaxMst; rewrite leq_eqVlt (Msigma_ell1 maxMst) //. -by rewrite !inE nty' Msts_y'. -Qed. - -(* This is B & G, Lemma 14.11. *) -Lemma primes_non_Fitting_Ftype M E q Q : - M \in 'M_'F -> \sigma(M)^'.-Hall(M) E -> - Q \in 'E_q^1(E) -> ~~ (Q \subset 'F(E)) -> - exists2 Mstar, Mstar \in 'M & - [\/ (*1*) q \in \tau2(Mstar) /\ 'M('C(Q)) = [set Mstar] - | (*2*) q \in \kappa(Mstar) /\ Mstar \in 'M_'P1 ]. -Proof. -move=> FmaxM hallE EqQ notsFE_Q; have [maxM k'M] := FtypeP _ FmaxM. -have [sQE abelQ dimQ] := pnElemP EqQ; have [qQ _] := andP abelQ. -have [q_pr oQ] := (pnElem_prime EqQ, card_pnElem EqQ : #|Q| = q). -have t1Mq: q \in \tau1(M). - have: q \in \pi(E) by rewrite -p_rank_gt0; apply/p_rank_geP; exists Q. - rewrite (partition_pi_sigma_compl maxM hallE) => /or3P[// | t2q | t3q]. - have [A EqA _] := ex_tau2Elem hallE t2q. - have [[nsAE defA1] _ _ _] := tau2_compl_context maxM hallE t2q EqA. - have sQA: Q \subset A by move: EqQ; rewrite defA1 => /pnElemP[]. - rewrite (subset_trans sQA) ?Fitting_max // ?abelian_nil // in notsFE_Q. - by have [_ abelA _] := pnElemP EqA; apply: abelem_abelian abelA. - have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. - have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. - have [[_ nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi. - have sQE3: Q \subset E3 by rewrite (sub_normal_Hall hallE3) ?(pi_pgroup qQ). - rewrite (subset_trans sQE3) ?Fitting_max ?abelian_nil // in notsFE_Q. - exact: cyclic_abelian cycE3. -have q'FE: q^'.-group 'F(E). - have [R sylR sQR] := Sylow_superset sQE qQ; have [sRE qR _] := and3P sylR. - have cycR: cyclic R. - rewrite (odd_pgroup_rank1_cyclic qR) ?mFT_odd // (p_rank_Sylow sylR) //. - by move: t1Mq; rewrite (tau1E maxM hallE) eqn_leq; case/and4P. - rewrite -partG_eq1 -(card_Hall (Hall_setI_normal (Fitting_normal E) sylR)). - have sRFER: R :&: 'F(E) \subset R := subsetIl _ _. - apply: contraR notsFE_Q; rewrite -trivg_card1 => ntRFE. - rewrite (subset_trans _ (subsetIr R _)) // -(cardSg_cyclic cycR) // oQ. - by have [] := pgroup_pdiv (pgroupS sRFER qR) ntRFE. -have cE'E': abelian E^`(1) := der_mmax_compl_abelian maxM hallE. -pose K := [~: E, Q]; have cKK: abelian K by rewrite (abelianS (commgS E sQE)). -have nsKE: K <| E by rewrite /normal commg_norml comm_subG. -have q'K: q^'.-group K by rewrite (pgroupS _ q'FE) // Fitting_max ?abelian_nil. -have [sKE nKE] := andP nsKE; have nKQ := subset_trans sQE nKE. -have defKQ: [~: K, Q] = K. - have nsKQ_E: K <*> Q <| E. - rewrite -(quotientGK nsKE) -(quotientYK nKQ) cosetpre_normal /= -/K. - by rewrite /normal quotientS // cents_norm // quotient_cents2r. - have [_ sylQ] := coprime_mulGp_Hall (esym (norm_joinEr nKQ)) q'K qQ. - have defE: K * 'N_E(Q) = E. - rewrite -{2}(Frattini_arg nsKQ_E sylQ) /= norm_joinEr //= -/K -mulgA. - by congr (K * _); rewrite mulSGid // subsetI sQE normG. - have cQ_NEQ: [~: 'N_E(Q), Q] = 1. - apply/trivgP; rewrite -(coprime_TIg (pnat_coprime qQ q'K)) subsetI. - by rewrite commg_subr subsetIr commSg ?subsetIl. - by rewrite {2}/K -defE commMG ?cQ_NEQ ?mulg1 1?normsR ?subsetIr ?subIset ?nKE. -have [sEM s'E _] := and3P hallE; have sQM := subset_trans sQE sEM. -have [sKM s'K] := (subset_trans sKE sEM, pgroupS sKE s'E). -have regQ: 'C_(M`_\sigma)(Q) = 1. - apply/eqP; apply: contraFT (k'M q) => nregQ. - have EqQ_M: Q \in 'E_q^1(M) by apply/pnElemP. - by rewrite unlock 3!inE /= t1Mq; apply/exists_inP; exists Q. -have nsKM: K <| M. - have [s'q _] := andP t1Mq. - have EqQ_NK: Q \in 'E_q^1('N_M(K)) by apply/pnElemP; rewrite subsetI sQM. - have:= commG_sigma'_1Elem_cyclic maxM sKM s'K s'q EqQ_NK regQ q'K cKK. - by rewrite defKQ; case. -have ntK: K != 1. - apply: contraNneq notsFE_Q => /commG1P cQE. - by rewrite Fitting_max ?(pgroup_nil qQ) // /normal sQE cents_norm. -pose p := pdiv #|K|; have p_pr: prime p by rewrite pdiv_prime ?cardG_gt1. -have piKp: p \in \pi(K) by rewrite pi_pdiv cardG_gt1. -have t2Mp: p \in \tau2(M). - have s'p := pnatPpi s'K piKp. - have sylKp: p.-Sylow(K) 'O_p(K) := nilpotent_pcore_Hall p (abelian_nil cKK). - have ntKp: 'O_p(K) != 1 by rewrite -rank_gt0 (rank_Sylow sylKp) p_rank_gt0. - rewrite inE /= s'p ?(sigma'_norm_mmax_rank2 maxM s'p (pHall_pgroup sylKp)) //. - by rewrite (mmax_normal maxM) ?gFnormal_trans. -have [A EpA _] := ex_tau2Elem hallE t2Mp. -have [sAE /andP[pA _] dimA] := pnElemP EpA. -have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp EpA. -have nAQ := subset_trans sQE (normal_norm nsAE). -have [S sylS sAS]:= Sylow_superset (subsetT A) pA. -have not_cSS: ~~ abelian S. - apply: contra notsFE_Q => cSS; rewrite Fitting_max ?(pgroup_nil qQ) //. - have solE := sigma_compl_sol hallE. - have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pgroup qQ t1Mq). - have [_ [E3 hallE3]] := ex_tau13_compl hallE. - have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. - have [_ _ _ sQZ] := abelian_tau2 maxM complEi t2Mp EpA sylS sAS cSS. - by rewrite sub_center_normal ?{}sQZ //; apply/nElemP; exists q; apply/pnElemP. -have [] := nonabelian_tau2 maxM hallE t2Mp EpA (pHall_pgroup sylS) not_cSS. -set A0 := 'C_A(M`_\sigma)%G => _ [oA0 defFM] _ _. -have defA0: A0 :=: K. - have sA0E: A0 \subset E by rewrite subIset ?sAE. - have sKA0: K \subset A0. - have [_ _ _ tiMsE] := sdprodP (sdprod_sigma maxM hallE). - rewrite -(mul1g A0) -tiMsE setIC group_modr // subsetI sKE. - by have [_ -> _ _] := dprodP defFM; rewrite Fitting_max ?abelian_nil. - by apply/eqP; rewrite eqEsubset prime_meetG ?(setIidPr sKA0) ?oA0. -have ntA: A :!=: 1 := nt_pnElem EpA isT. -have [H maxNH] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper pA)). -have [maxH sNH] := setIdP maxNH; have sQH := subset_trans nAQ sNH. -exists H => //. -have: p \in [predD \sigma(H) & \beta(H)] /\ q \in [predU \tau1(H) & \tau2(H)]. - have [-> // piAb _] := primes_norm_tau2Elem maxM hallE t2Mp EpA maxNH. - rewrite (pnatPpi piAb) // (piSg (quotientS _ sQE)) //=. - have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 p_rank_abelem ?dimQ. - rewrite /= card_quotient ?normsI ?norms_cent // ?normsG //. - rewrite -indexgI setIA (setIidPl sQE) prime_TIg ?indexg1 // ?oQ //. - rewrite (sameP commG1P eqP) (subG1_contra _ ntK) //= -/K -defKQ commGC. - by rewrite -defA0 commgS ?subsetIl. -case=> /andP[/= b'Hp sHP] t12Hq. -have nregQHs: 'C_(H`_\sigma)(Q) != 1. - apply: subG1_contra (setSI _ _) (_ : 'C_A(Q) != 1). - rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(pi_pgroup pA) //. - exact: subset_trans (normG A) sNH. - apply: contraTneq (leqnn 1) => regQA; rewrite -ltnNge -dimA. - rewrite -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup // -oA0 defA0. - have coAQ := pnat_coprime (pi_pnat pA t2Mp) (pi_pnat qQ (tau2'1 t1Mq)). - rewrite subset_leq_card // -(coprime_cent_prod nAQ) ?(pgroup_sol pA) //. - by rewrite regQA mulg1 commSg. -have{t12Hq} [/= t1Hq | /= t2Hq] := orP t12Hq. - have EqQ_H: Q \in 'E_q^1(H) by apply/pnElemP. - have kHq: q \in \kappa(H). - by rewrite unlock 3!inE /= t1Hq; apply/exists_inP; exists Q. - right; split=> //; apply: contraR b'Hp => notP1maxH. - have PmaxH: H \in 'M_'P by apply/PtypeP; split=> //; exists q. - have [L hallL] := Hall_exists \kappa(H) (mmax_sol maxH). - by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxH hallL; apply/setDP. -left; split=> //. -have [x defQ]: exists x, Q :=: <[x]> by apply/cyclicP; rewrite prime_cyclic ?oQ. -rewrite defQ cent_cycle in nregQHs *; rewrite (cent1_nreg_sigma_uniq maxH) //. - by rewrite 2!inE -cycle_eq1 -cycle_subG -defQ (nt_pnElem EqQ). -by rewrite /p_elt /order -defQ oQ pnatE. -Qed. - -(* This is B & G, Lemma 14.12. *) -(* Note that the assumption M \in 'M_'P2 could be weakened to M \in 'M_'P, *) -(* since the assumption H \in 'M('N(R)) implies H != 1, and hence U != 1. *) -Lemma P2type_signalizer M Mstar U K r R H : - M \in 'M_'P2 -> kappa_complement M U K -> Mstar \in 'M('C(K)) -> - r.-Sylow(U) R -> H \in 'M('N(R)) -> - [/\ H \in 'M_'F, U \subset H`_\sigma, U <*> K = M :&: H - & [/\ ~~ ('N_H(U) \subset M), K \subset 'F(H :&: Mstar) - & \sigma(H)^'.-Hall(H) (H :&: Mstar)]]. -Proof. -move=> P2maxM complU maxCMstar sylR maxNH; have [hallU hallK _] := complU. -have [PmaxM notP1maxM] := setDP P2maxM; have [maxM notFmaxM] := setDP PmaxM. -have [[sUM sk'M_U _] [sKM kK _]] := (and3P hallU, and3P hallK). -have{notFmaxM} ntK: K :!=: 1 by rewrite (trivg_kappa maxM). -have [hallE defM _ regK /(_ ntK)cUU] := kappa_compl_context maxM complU. -case/sdprodP: defM => [[_ E _ defE] _ _ _]. -have [nsUE sKE mulUK nUK tiUK] := sdprod_context defE. -rewrite (norm_joinEr nUK) mulUK in hallE *. -have [Mst [PmaxMst notMGMst] [uniqMst []]] := Ptype_embedding PmaxM hallK. -set Ks := 'C_(_)(K) => hallKs; case/and3P=> sKsMst sM_Ks _ [defK _]. -case=> cycZ ziMMst _ _ _ [_ _ defPmax _]. -have [_ [defNK _] [ntKs _] _ [//|_ q_pr _ _]] := Ptype_structure PmaxM hallK. -set q := #|K| in q_pr. -have{uniqMst} uniqMst: 'M('C(K)) = [set Mst]. - by apply: uniqMst; apply/nElemP; exists q; rewrite p1ElemE // !inE subxx /=. -have{maxCMstar} ->: Mstar = Mst by [apply/set1P; rewrite -uniqMst] => {Mstar}. -have [maxH sNRH] := setIdP maxNH. -have ntR: R :!=: 1. - by apply: contraTneq sNRH => ->; rewrite norm1 proper_subn ?mmax_proper. -have piUr: r \in \pi(U) by rewrite -p_rank_gt0 -(rank_Sylow sylR) rank_gt0. -have r_pr: prime r by move: piUr; rewrite mem_primes; case/andP. -have sylR_M := subHall_Sylow hallU (pnatPpi sk'M_U piUr) sylR. -have [/= s'Mr k'Mr] := norP (pnatPpi sk'M_U piUr). -have [sRH [sRM rR _]] := (subset_trans (normG R) sNRH, and3P sylR_M). -have notMGH: gval H \notin M :^: G. - apply: contra s'Mr; case/imsetP=> a _ defH. - rewrite -(sigmaJ _ a) -defH; apply/exists_inP; exists R => //. - by rewrite pHallE sRH /= (card_Hall sylR_M) defH cardJg. -have sK_uniqMst a: K \subset Mst :^ a -> a \in Mst. - move=> sKMa; apply: contraR ntK; rewrite -in_setC => Mst'a. - have [_ _ _ [[tiK_MstG _] _ _] _] := Ptype_structure PmaxMst hallKs. - by rewrite -(tiK_MstG a) // defK (setIidPl sKMa). -have [_ _] := dprodP defNK; rewrite -/Ks => cKKs tiKKs. -have snK_sMst L: K <|<| L -> L \subset Mst. - elim: {L}_.+1 {-2}L (ltnSn #|L|) => // n IHn A leAn. - case/subnormalEr=> [<- | [L [snKL nsLA ltLA]]]. - by rewrite -defK subIset // pcore_sub. - have [sKL sLMst]: K \subset L /\ L \subset Mst. - by rewrite subnormal_sub // IHn // (leq_trans (proper_card ltLA)). - apply/subsetP=> a Aa; rewrite -groupV sK_uniqMst // (subset_trans sKL) //. - by rewrite -sub_conjg (normsP (normal_norm nsLA)). -have sEH: E \subset H. - have defR: R :=: 'O_r(U) := nilpotent_Hall_pcore (abelian_nil cUU) sylR. - by apply: subset_trans sNRH; rewrite defR gFnorm_trans ?normal_norm. -have [sUH sKH]: U \subset H /\ K \subset H by apply/mulGsubP; rewrite mulUK. -have notMstGH: gval H \notin Mst :^: G. - apply: contra ntR => /imsetP[a _ defH]. - have{a defH} defH: H :=: Mst by rewrite -(conjGid (sK_uniqMst a _)) -?defH. - rewrite -(setIidPl sRH) -(setIidPl sRM) -setIA defH ziMMst coprime_TIg //=. - rewrite cent_joinEr // TI_cardMg //= coprime_mulr -/Ks. - rewrite (p'nat_coprime (pi_pnat rR _) kK) //=. - exact: p'nat_coprime (pi_pnat rR _) sM_Ks. -have FmaxH: H \in 'M_'F. - suffices: H \notin 'M_'P by rewrite inE maxH andbT negbK. - by apply: (contra (defPmax H)); rewrite inE; apply/norP. -have sKMsts: K \subset Mst`_\sigma by rewrite -defK subsetIl. -have s'H_K: \sigma(H)^'.-group K. - apply/pgroupP=> p p_pr p_dv_K; have [maxMst _] := setDP PmaxMst. - apply: contraFN (sigma_partition maxMst maxH notMstGH p) => /= sHp. - by rewrite inE /= (pgroupP (pgroupS sKMsts _)) ?pcore_pgroup. -have [D hallD sKD] := Hall_superset (mmax_sol maxH) sKH s'H_K. -have piKq: q \in \pi(K) by rewrite pi_of_prime ?inE. -have sK_FD: K \subset 'F(D). - have EqK: K \in 'E_q^1(D) by rewrite p1ElemE // !inE sKD /=. - have sMst_q: q \in \sigma(Mst). - by rewrite (pnatPpi (pcore_pgroup _ _) (piSg sKMsts _)). - apply: contraR notP1maxM => not_sKFD. - have [L _ ] := primes_non_Fitting_Ftype FmaxH hallD EqK not_sKFD. - case=> [[t2Lq ]|[kLq P1maxL]]. - rewrite uniqMst => /set1_inj defL. - by rewrite -defL 3!inE sMst_q in t2Lq. - have [PmaxL _] := setIdP P1maxL. - case/setUP: (defPmax L PmaxL) => /imsetP[a _ defL]. - by rewrite (group_inj defL) P1typeJ in P1maxL. - move: kLq; rewrite defL kappaJ unlock 3!inE /=. - by rewrite -andb_orr inE /= sMst_q. -have sDMst: D \subset Mst. - apply: snK_sMst (subnormal_trans _ (normal_subnormal (Fitting_normal D))). - exact: nilpotent_subnormal (Fitting_nil D) sK_FD. -have defUK: [~: U, K] = U. - rewrite -{2}(coprime_cent_prod nUK) ?abelian_sol //; last first. - by apply: p'nat_coprime (sub_pgroup _ sk'M_U) kK => ? /norP[]. - by rewrite (cent_semiregular regK) ?mulg1. -have qK: q.-group K := pnat_id q_pr. -have sUHs: U \subset H`_\sigma. - have [nsHsH _ mulHsD nHsD _] := sdprod_context (sdprod_sigma maxH hallD). - have nHsDq: 'O_q(D) \subset 'N(H`_\sigma) by apply: gFsub_trans. - pose HsDq := H`_\sigma <*> 'O_q(D). - have defHsDq: H`_\sigma * 'O_q(D) = HsDq by rewrite -norm_joinEr. - have hallHs_HsDq: q^'.-Hall(HsDq) H`_\sigma. - have [|//] := coprime_mulGp_Hall defHsDq _ (pcore_pgroup _ _). - rewrite p'groupEpi; apply: (contra (pnatPpi (pcore_pgroup _ _))). - exact: pnatPpi s'H_K piKq. - have sK_HsDq: K \subset HsDq. - rewrite sub_gen ?subsetU // orbC -p_core_Fitting. - by rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ (Fitting_nil _))) ?qK. - have [|sHsDq_H nHsDq_H] := andP (_ : HsDq <| H). - rewrite -(quotientGK nsHsH) -[HsDq]quotientYK //= cosetpre_normal //. - by rewrite -{3}mulHsD quotientMidl quotient_normal // pcore_normal. - have sU_HsDq: U \subset HsDq. - by rewrite -defUK (subset_trans (commgSS sUH sK_HsDq)) // commg_subr. - rewrite (sub_normal_Hall hallHs_HsDq) ?normalYl // p'groupEpi. - by apply: contraL (pnatPpi sk'M_U) _; rewrite !inE /= orbC (pnatPpi kK). -have defNMU: 'N_M(U) = E. - have [_ mulHsE nHsE _] := sdprodP (sdprod_sigma maxM hallE). - have [sUE nUE] := andP nsUE; rewrite -mulHsE -normC // -group_modl //=. - rewrite coprime_norm_cent ?(subset_trans sUE) //; last first. - exact: coprimegS sUE (coprime_sigma_compl hallE). - have sR1U: 'Ohm_1(R) \subset U := gFsub_trans _ (pHall_sub sylR). - rewrite (trivgP (subset_trans (setIS _ (centS sR1U)) _)) ?mulg1 //. - have [|_ _ -> //] := sigma'_kappa'_facts maxM sylR_M. - by rewrite s'Mr (piSg sUM). -have sHsFH: H`_\sigma \subset 'F(H). - rewrite Fitting_max ?pcore_normal //. - have [S] := Sylow_exists q H; case/sigma'_kappa'_facts=> {S}//. - have [_ k'H] := setIdP FmaxH. - rewrite [~~ _](pnatPpi (pHall_pgroup hallD) (piSg sKD _)) //=. - by rewrite [~~ _](pnatPpi k'H) (piSg sKH). -suffices ->: H :&: Mst = D. - set sk' := _^' in sk'M_U hallU; pose Fu := 'O_sk'('F(H)). - have [sUFH nilFH] := (subset_trans sUHs sHsFH, Fitting_nil H). - have hallFu: sk'.-Hall('F(H)) Fu := nilpotent_pcore_Hall sk' nilFH. - have sUFu: U \subset Fu by rewrite (sub_Hall_pcore hallFu). - have nsFuH: Fu <| H by rewrite !gFnormal_trans. - have [[sFuFH sk'Fu _] [sFuH nFuH]] := (and3P hallFu, andP nsFuH). - have defU: M :&: Fu = U. - have sk'MFu: sk'.-group(M :&: Fu) := pgroupS (subsetIr M _) sk'Fu. - by rewrite (sub_pHall hallU sk'MFu) ?subsetIl // subsetI sUM. - do 2?split=> //. - apply/eqP; rewrite eqEsubset subsetI (pHall_sub hallE) sEH /=. - by rewrite -defNMU subsetI subsetIl -defU normsGI. - apply: contra (contra_orbit _ _ notMGH) => sNHU_M. - rewrite (eq_mmax maxH maxM (subset_trans _ sNHU_M)) // subsetIidl. - rewrite -(nilpotent_sub_norm (nilpotentS sFuFH nilFH) sUFu) //= -/Fu. - by rewrite -{2}defU subsetI subsetIl (subset_trans (setSI _ sFuH)). -have [maxMst _] := setDP PmaxMst. -have [_ <- _ _] := sdprodP (sdprod_sigma maxH hallD). -rewrite -{2}(mul1g D) setIC -group_modr // setIC; congr (_ * _). -apply/eqP; apply: wlog_neg => ntHsMst. -have nregHsK: 'C_(H`_\sigma)(K) != 1. - rewrite (subG1_contra _ ntHsMst) // subsetI subsetIl (sameP commG1P trivgP). - have <-: H`_\sigma :&: Mst`_\sigma = 1. - apply: card_le1_trivg; rewrite leqNgt -pi_pdiv; set p := pdiv _. - apply: contraFN (sigma_partition maxMst maxH notMstGH p) => piIp. - rewrite inE /= (pnatPpi (pcore_pgroup _ _) (piSg (subsetIl _ _) piIp)). - by rewrite (pnatPpi (pcore_pgroup _ _) (piSg (subsetIr _ _) piIp)). - rewrite commg_subI ?setIS ?gFnorm // subsetI sKMsts. - by rewrite (subset_trans sKH) ?gFnorm. -have t2Hq: q \in \tau2(H). - have: q \in \pi(D) := piSg sKD piKq. - rewrite (partition_pi_sigma_compl maxH hallD) orbCA; case/orP=> // t13Hq. - case/FtypeP: FmaxH => _ /(_ q)/idP[]; rewrite unlock 3!inE /= t13Hq. - by apply/exists_inP; exists K => //; rewrite p1ElemE // !inE sKH /=. -have [A EqA_D EqA] := ex_tau2Elem hallD t2Hq. -have [_ _ _ -> //] := tau2_context maxH t2Hq EqA. -rewrite 3!inE -val_eqE /= eq_sym (contra_orbit _ _ notMstGH) maxMst. -by have [sAD _ _] := pnElemP EqA_D; apply: subset_trans sAD sDMst. -Qed. - -(* This is B & G, Lemma 14.13(a). *) -(* Part (b) is not needed for the Peterfalvi revision of the character theory *) -(* part of the proof. *) -Lemma non_disjoint_signalizer_Frobenius x M : - \ell_\sigma(x) == 1%N -> #|'M_\sigma[x]| > 1 -> - M \in 'M_\sigma[x] -> ~~ (\sigma('N[x])^'.-group M) -> - M \in 'M_'F /\ \tau2(M)^'.-group M. -Proof. -move=> ell1x ntR SMxM; have [maxM Ms_x] := setIdP SMxM. -rewrite negb_and cardG_gt0 all_predC negbK => /hasP[q /= piMq sNq]. -have [Q EqQ]: exists Q, Q \in 'E_q^1(M) by apply/p_rank_geP; rewrite p_rank_gt0. -have [ntQ [sQM abelQ dimQ]] := (nt_pnElem EqQ isT, pnElemP EqQ). -have [[qQ _] q_pr] := (andP abelQ, pnElem_prime EqQ). -have [_ [//| uniqN _ t2Nx _]] := FT_signalizer_context ell1x. -case/(_ M SMxM)=> _ st2NsM spM_sbN _; have [maxN sCxN] := mem_uniq_mmax uniqN. -have bNq: q \in \beta('N[x]) by rewrite spM_sbN //= 4!inE /= piMq. -have bGq: q \in \beta(G) by move: bNq; rewrite -predI_sigma_beta // inE /= sNq. -set p := pdiv #[x]; have pi_p: p \in \pi(#[x]). - by rewrite pi_pdiv order_gt1 (sameP eqP (ell_sigma0P _)) (eqP ell1x). -have sMp: p \in \sigma(M) := pnatPpi (pcore_pgroup _ _) (piSg Ms_x pi_p). -have t2Np: p \in \tau2('N[x]) := pnatPpi t2Nx pi_p. -have notMGN: gval 'N[x] \notin M :^: G. - apply: contraL t2Np => /imsetP[a _ ->]. - by rewrite negb_and negbK /= sigmaJ sMp. -have sM'q: q \in \sigma(M)^'. - by apply: contraFN (sigma_partition maxM maxN notMGN q) => sMq; apply/andP. -have [g sQNg]: exists g, Q \subset 'N[x] :^ g. - have [Q1 sylQ1] := Sylow_exists q 'N[x]. - have [g _ sQQ1g] := Sylow_subJ (sigma_Sylow_G maxN sNq sylQ1) (subsetT Q) qQ. - by exists g; rewrite (subset_trans sQQ1g) // conjSg (pHall_sub sylQ1). -have EqNQ: Q \in 'E_q^1('N[x] :^ g) by apply/pnElemP. -have uniqNg: 'M('C(Q)) = [set 'N[x] :^ g]%G. - by case/cent_der_sigma_uniq: EqNQ; rewrite ?mmaxJ 1?betaJ ?bNq. -have b'Mp: p \notin \beta(M). - by rewrite -predI_sigma_beta // inE /= sMp /=; case/tau2_not_beta: t2Np. -have{p pi_p sMp t2Np b'Mp} FmaxM: M \in 'M_'F. - have [P1maxM | notP1maxM] := boolP (M \in 'M_'P1); last first. - have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). - apply: contraR b'Mp => notFmaxM; have PmaxM: M \in 'M_'P by apply/setDP. - by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxM hallK; apply/setDP. - have [PmaxM skM] := setIdP P1maxM. - have kMq: q \in \kappa(M). - by case/orP: (pnatPpi skM piMq) => //= sMq; case/negP: sM'q. - have [K hallK sQK] := Hall_superset (mmax_sol maxM) sQM (pi_pnat qQ kMq). - have EqKQ: Q \in 'E_q^1(K) by apply/pnElemP. - have [L _ [uniqL [kLhallKs sMhallKs] _ _ _]] := Ptype_embedding PmaxM hallK. - set Ks := 'C_(_)(K) in kLhallKs sMhallKs. - have{uniqL} defL: 'N[x] :^ g = L. - apply: congr_group; apply: set1_inj; rewrite -uniqNg uniqL //. - by apply/nElemP; exists q. - have rpL: 'r_p(L) = 2. - by apply/eqP; case/andP: t2Np => _; rewrite -defL p_rankJ. - suffices piKs_p: p \in \pi(Ks). - by rewrite rank_kappa // (pnatPpi (pHall_pgroup kLhallKs)) in rpL. - have [P sylP] := Sylow_exists p [group of Ks]. - have sylP_L: p.-Sylow(L) P := subHall_Sylow sMhallKs sMp sylP. - by rewrite -p_rank_gt0 -(rank_Sylow sylP) (rank_Sylow sylP_L) ?rpL. -split=> //; apply: sub_pgroup (pgroup_pi _) => p piMp; apply/negP=> /= t2Mp. -have rpN: 'r_p('N[x]) <= 1. - have: p \notin \beta('N[x]). - rewrite -(predI_sigma_beta maxN) negb_and /= orbC. - by have [-> _] := tau2_not_beta maxM t2Mp. - apply: contraR; rewrite -ltnNge => rpN; rewrite spM_sbN // inE /= piMp. - have: p \in \pi('N[x]) by rewrite -p_rank_gt0 ltnW. - rewrite (partition_pi_mmax maxN) orbCA => /orP[t2Np | ]. - by case/andP: t2Mp => /negP[]; apply: st2NsM. - by rewrite orbA -!andb_orr eqn_leq leqNgt rpN andbF. -have [E hallE sQE] := Hall_superset (mmax_sol maxM) sQM (pi_pgroup qQ sM'q). -have [A Ep2A _] := ex_tau2Elem hallE t2Mp; have [_ abelA dimA] := pnElemP Ep2A. -pose A0 := [~: A, Q]%G; pose A1 := 'C_A(Q)%G. -have sCQNg: 'C(Q) \subset 'N[x] :^ g by have [] := mem_uniq_mmax uniqNg. -have ntA0: A0 :!=: 1. - rewrite (sameP eqP commG1P); apply: contraL rpN => cQA. - rewrite -ltnNge -(p_rankJ p _ g); apply/p_rank_geP. - by exists A; apply/pnElemP; rewrite (subset_trans cQA). -have t1Mq: q \in \tau1(M). - have [_ nsCEA_E t1Eb] := tau1_cent_tau2Elem_factor maxM hallE t2Mp Ep2A. - rewrite (pnatPpi t1Eb) // (piSg (quotientS _ sQE)) // -p_rank_gt0. - rewrite -rank_pgroup ?quotient_pgroup // rank_gt0 -subG1. - rewrite quotient_sub1 ?(subset_trans _ (normal_norm nsCEA_E)) //. - by rewrite subsetI sQE centsC (sameP commG1P eqP). -have EqEQ: Q \in 'E_q^1(E) by apply/pnElemP. -have regMsQ: 'C_(M`_\sigma)(Q) = 1. - apply: contraTeq FmaxM => nregMsQ; apply/FtypeP=> [[_]]; move/(_ q). - by rewrite unlock 3!inE /= t1Mq; case/exists_inP; exists Q. -have [[]] := tau1_act_tau2 maxM hallE t2Mp Ep2A t1Mq EqEQ regMsQ ntA0. -rewrite -/A0 -/A1 => EpA0 cMsA0 _ notA1GA0 [EpA1 _]. -have [sA0A abelA0 oA0] := pnElemPcard EpA0; have [pA0 _] := andP abelA0. -have [sA1A abelA1 oA1] := pnElemPcard EpA1; have [pA1 _] := andP abelA1. -have sA0N: A0 \subset 'N[x]. - rewrite -cMsA0 (subset_trans _ sCxN) //= -cent_cycle (centsS Ms_x) //. - exact: subsetIr. -have [P sylP sA0P] := Sylow_superset sA0N pA0; have [_ pP _] := and3P sylP. -have cycP: cyclic P. - by rewrite (odd_pgroup_rank1_cyclic pP) ?mFT_odd ?(p_rank_Sylow sylP). -have sA1gN: A1 :^ g^-1 \subset 'N[x] by rewrite sub_conjgV subIset ?sCQNg ?orbT. -have [|z _ sA1gzP] := Sylow_Jsub sylP sA1gN; first by rewrite pgroupJ. -case/imsetP: notA1GA0; exists (g^-1 * z); rewrite ?inE // conjsgM. -by apply/eqP; rewrite (eq_subG_cyclic cycP) // !cardJg oA0 oA1. -Qed. - -End Section14. - - |