proposition: Theorem nonabelian_Uniqueness p P : p.-group P -> ~~ abelian P -> P \in 'U.
proof: Proof. move=> pP not_cPP; have [M maxP_M] := mmax_exists (mFT_pgroup_proper pP). have sigma_p L: L \in 'M(P) -> p \in \sigma(L). case/setIdP=> maxL sPL; apply: contraR not_cPP => sL'p. exact: sigma'_nil_abelian maxL sPL (pi_pnat pP _) (pgroup_nil pP). have{maxP_M} [[maxM sPM] sMp] := (setIdP maxP_M, sigma_p M maxP_M). rewrite (uniq_mmax_subset1 maxM sPM); apply/subsetP=> H maxP_H; rewrite inE. have{sigma_p maxP_H} [[maxH sPH] sHp] := (setIdP maxP_H, sigma_p H maxP_H). without loss{pP sPH sPM} sylP: P not_cPP / p.-Sylow(M :&: H) P. move=> IH; have sP_MH: P \subset M :&: H by rewrite subsetI sPM. have [S sylS sPS] := Sylow_superset sP_MH pP. exact: IH (contra (abelianS sPS) not_cPP) sylS. have [sP_MH pP _] := and3P sylP; have [sPM sPH] := subsetIP sP_MH. have ncycP := contra (@cyclic_abelian _ _) not_cPP. have{sHp} sNMH: 'N(P) \subset M :&: H. by rewrite subsetI !(@norm_noncyclic_sigma _ p). have{sylP} sylP_M: p.-Sylow(M) P. have [S sylS sPS] := Sylow_superset sPM pP; have pS := pHall_pgroup sylS. have [-> // | ltPS] := eqVproper sPS. have /andP[sNP] := nilpotent_proper_norm (pgroup_nil pS) ltPS. rewrite (sub_pHall sylP _ sNP) ?subxx ?(pgroupS (subsetIl _ _)) //. by rewrite subIset // orbC sNMH. have{sMp} sylP_G: p.-Sylow(G) P := sigma_Sylow_G maxM sMp sylP_M. have sylP_H: p.-Sylow(H) P := pHall_subl sPH (subsetT H) sylP_G. have [rPgt2 | rPle2] := ltnP 2 'r(P). have uniqP: P \in 'U by rewrite rank3_Uniqueness ?(mFT_pgroup_proper pP). have defMP: 'M(P) = [set M] := def_uniq_mmax uniqP maxM sPM. by rewrite -val_eqE /= (eq_uniq_mmax defMP maxH). have rpP: 'r_p(P) = 2. apply/eqP; rewrite eqn_leq -{1}rank_pgroup // rPle2 ltnNge. by rewrite -odd_pgroup_rank1_cyclic ?mFT_odd. have:= mFT_rank2_Sylow_cprod sylP_G rPle2 not_cPP. case=> Q [not_cQQ dimQ eQ] [R cycR [defP defR1]]. have sQP: Q \subset P by have /mulG_sub[] := cprodW defP. have pQ: p.-group Q := pgroupS sQP pP. have oQ: #|Q| = (p ^ 3)%N by rewrite (card_pgroup pQ) dimQ. have esQ: extraspecial Q by apply: (p3group_extraspecial pQ); rewrite ?dimQ. have p_pr := extraspecial_prime pQ esQ; have p_gt1 := prime_gt1 p_pr. pose Z := 'Z(Q)%G; have oZ: #|Z| = p := card_center_extraspecial pQ esQ. have nsZQ: Z <| Q := center_normal Q; have [sZQ nZQ] := andP nsZQ. have [[defPhiQ defQ'] _]: ('Phi(Q) = Z /\ Q^`(1) = Z) /\ _ := esQ. have defZ: 'Ohm_1 ('Z(P)) = Z. have [_ <- _] := cprodP (center_cprod defP). by rewrite (center_idP (cyclic_abelian cycR)) -defR1 mulSGid ?Ohm_sub. have ncycQ: ~~ cyclic Q := contra (@cyclic_abelian _ Q) not_cQQ. have rQgt1: 'r_p(Q) > 1. by rewrite ltnNge -(odd_pgroup_rank1_cyclic pQ) ?mFT_odd. have [A Ep2A]: exists A, A \in 'E_p^2(Q) by apply/p_rank_geP. wlog uniqNEpA: M H maxM maxH sP_MH sNMH sPM sPH sylP_M sylP_H / ~~ [exists A0 in 'E_p^1(A) :\ Z, 'M('N(A0)) == [set M]]. - move=> IH; case: exists_inP (IH M H) => [[A0 EpA0 defMA0] _ | _ -> //]. case: exists_inP {IH}(IH H M) => [[A1 EpA1 defMA1] _ | _]; last first. by rewrite setIC eq_sym => ->. have [sAQ abelA dimA] := pnElemP Ep2A; have sAP := subset_trans sAQ sQP. have transNP: [transitive 'N_P(A), on 'E_p^1(A) :\ Z | 'JG]. have [|_ _] := basic_p2maxElem_structure _ pP sAP not_cPP. have Ep2A_G := subsetP (pnElemS p 2 (subsetT Q)) A Ep2A. rewrite inE Ep2A_G (subsetP (p_rankElem_max p G)) //. by rewrite -(p_rank_Sylow sylP_G) rpP. by rewrite (group_inj defZ). have [x NPx defA1] := atransP2 transNP EpA0 EpA1. have Mx: x \in M by rewrite (subsetP sPM) //; case/setIP: NPx. rewrite eq_sym -in_set1 -(group_inj (conjGid Mx)). by rewrite -(eqP defMA1) defA1 /= normJ mmax_ofJ (eqP defMA0) set11. apply: contraR uniqNEpA => neqHM; have sQM := subset_trans sQP sPM. suffices{A Ep2A} [ntMa nonuniqNZ]: M`_\alpha != 1 /\ 'M('N(Z)) != [set M]. have [A0 EpA0 defMNA0]: exists2 A0, A0 \in 'E_p^1(A) & 'M('N(A0)) == [set M]. apply/exists_inP; apply: contraR ntMa; rewrite negb_exists_in => uniqNA1. have{} Ep2A: A \in 'E_p^2(M) := subsetP (pnElemS p 2 sQM) A Ep2A. by have [_ [//|_ ->]] := p2Elem_mmax maxM Ep2A. apply/exists_inP; exists A0; rewrite // 2!inE EpA0 andbT. by apply: contraNneq nonuniqNZ => <-. have coMaQ: coprime #|M`_\alpha| #|Q|. apply: pnat_coprime (pcore_pgroup _ _) (pi_pnat pQ _). by rewrite !inE -(p_rank_Sylow sylP_M) rpP. have nMaQ: Q \subset 'N(M`_\alpha) by rewrite (subset_trans sQM) ?gFnorm. have [coMaZ nMaZ] := (coprimegS sZQ coMaQ, subset_trans sZQ nMaQ). pose K := 'N_(M`_\alpha)(Z). have defKC: 'C_(M`_\alpha)(Z) = K by rewrite -coprime_norm_cent. have coKQ: coprime #|K| #|Q| := coprimeSg (subsetIl _ _) coMaQ. have nKQ: Q \subset 'N(K) by rewrite normsI ?norms_norm. have [coKZ nKZ] := (coprimegS sZQ coKQ, subset_trans sZQ nKQ). have sKH: K \subset H. have sZH := subset_trans sZQ (subset_trans sQP sPH). rewrite -(quotientSGK (subsetIr _ _) sZH) /= -/Z -/K. have cQQb: abelian (Q / Z) by rewrite -defQ' sub_der1_abelian. rewrite -(coprime_abelian_gen_cent cQQb) ?coprime_morph ?quotient_norms //. rewrite gen_subG /= -/K -/Z; apply/bigcupsP=> Ab; rewrite andbC; case/andP. case/(inv_quotientN nsZQ)=> A -> sZA nsAQ; have sAQ := normal_sub nsAQ. rewrite (isog_cyclic (third_isog _ _ _)) // -/Z => cycQA. have pA: p.-group A := pgroupS sAQ pQ. have rAgt1: 'r_p(A) > 1. have [-> // | ltAQ] := eqVproper sAQ. rewrite ltnNge -(odd_pgroup_rank1_cyclic pA) ?mFT_odd //. apply: contraL cycQA => cycA /=; have cAA := cyclic_abelian cycA. suff <-: Z :=: A by rewrite -defPhiQ (contra (@Phi_quotient_cyclic _ Q)). apply/eqP; rewrite eqEcard sZA /= oZ (card_pgroup pA) (leq_exp2l _ 1) //. by rewrite -abelem_cyclic // /abelem pA cAA (dvdn_trans (exponentS sAQ)). have [A1 EpA1] := p_rank_geP rAgt1. rewrite -(setIidPr (subset_trans sAQ (subset_trans sQP sPH))) pnElemI in EpA1. have{EpA1} [Ep2A1 sA1A]:= setIdP EpA1; rewrite inE in sA1A. have [sCA1_H _]: 'C(A1) \subset H /\ _ := p2Elem_mmax maxH Ep2A1. rewrite -quotient_TI_subcent ?(subset_trans sAQ) ?(coprime_TIg coKZ) //= -/K. by rewrite quotientS // subIset // orbC (subset_trans (centS sA1A)). have defM: M`_\alpha * (M :&: H) = M. rewrite setIC in sNMH *. have [defM eq_aM_bM] := nonuniq_norm_Sylow_pprod maxM maxH neqHM sylP_G sNMH. by rewrite [M`_\alpha](eq_pcore M eq_aM_bM). do [split; apply: contraNneq neqHM] => [Ma1 | uniqNZ]. by rewrite -val_eqE /= (eq_mmax maxM maxH) // -defM Ma1 mul1g subsetIr. have [_ sNZM]: _ /\ 'N(Z) \subset M := mem_uniq_mmax uniqNZ. rewrite -val_eqE /= (eq_uniq_mmax uniqNZ maxH) //= -(setIidPr sNZM). have sZ_MH: Z \subset M :&: H := subset_trans sZQ (subset_trans sQP sP_MH). rewrite -(pprod_norm_coprime_prod defM) ?pcore_normal ?mmax_sol //. by rewrite mulG_subG /= defKC sKH setIAC subsetIr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)