proposition: Theorem SCN_Fitting_Uniqueness p M P A : M \in 'M -> p.-group ('F(M)) -> p.-Sylow(M) P -> 'r_p('F(M)) >= 3 -> A \in 'SCN_3(P) -> [/\ p.-Sylow(G) P, A \subset 'F(M) & A \in 'U].
proof: Proof. set F := 'F(M) => maxM pF sylP dimFp3 scn3_A. have [scnA dimA3] := setIdP scn3_A; have [nsAP defCA] := SCN_P scnA. have cAA := SCN_abelian scnA; have sAP := normal_sub nsAP. have [sPM pP _] := and3P sylP; have sAM := subset_trans sAP sPM. have{dimA3} ntA: A :!=: 1 by case: eqP dimA3 => // ->; rewrite rank1. have prM := mmax_proper maxM; have solM := mFT_sol prM. have{pF} Mp'1: 'O_p^'(M) = 1. apply/eqP; rewrite -trivg_Fitting ?(solvableS (pcore_sub _ _)) //. rewrite Fitting_pcore -(setIidPr (pcore_sub _ _)) coprime_TIg //. exact: pnat_coprime (pcore_pgroup _ _). have defF: F = M`p := Fitting_eq_pcore Mp'1. have sFP: F \subset P by rewrite defF (pcore_sub_Hall sylP). have sAF: A \subset F. rewrite defF -(pseries_pop2 _ Mp'1). exact: (odd_p_abelian_constrained (mFT_odd _) solM sylP cAA nsAP). have sZA: 'Z(F) \subset A. by rewrite -defCA setISS ?centS // defF pcore_sub_Hall. have sCAM: 'C(A) \subset M. have nsZM: 'Z(F) <| M by rewrite !gFnormal_trans. rewrite -(mmax_normal maxM nsZM); last first. rewrite /= -(setIidPr (center_sub _)) meet_center_nil ?Fitting_nil //. by rewrite -proper1G (proper_sub_trans _ sAF) ?proper1G. by rewrite (subset_trans _ (cent_sub _)) ?centS. have nsZL_M: 'Z('L(P)) <| M. by rewrite (Puig_center_normal (mFT_odd _) solM sylP). have sNPM: 'N(P) \subset M. rewrite -(mmax_normal maxM nsZL_M) ?gFnorm_trans //. apply/eqP => /(trivg_center_Puig_pgroup (pHall_pgroup sylP))-P1. by rewrite -subG1 -P1 sAP in ntA. have sylPG: p.-Sylow(G) P := mmax_sigma_Sylow maxM sylP sNPM. split; rewrite // (uniq_mmax_subset1 maxM sAM). have{} scn3_A: A \in 'SCN_3[p] by apply/bigcupP; exists P; rewrite // inE. pose K := 'O_p^'('C(A)); have sKF: K \subset F. have sKM: K \subset M := gFsub_trans _ sCAM. apply: subset_trans (cent_sub_Fitting solM). rewrite subsetI sKM coprime_nil_faithful_cent_stab ?Fitting_nil //. - by rewrite gFsub_trans ?(subset_trans sCAM) ?gFnorm. - by rewrite /= -/F defF coprime_pcoreC. have sACK: A \subset 'C_F(K) by rewrite subsetI sAF centsC pcore_sub. by rewrite /= -/F -/K (subset_trans _ sACK) //= -defCA setISS ?centS. have{sKF} K1: K = 1 by rewrite -(setIidPr sKF) defF TI_pcoreC. have p'nbyA_1 q: q != p -> |/|*(A; q) = [set 1%G]. move=> p'q. have: [transitive K, on |/|*(A; q) | 'JG] by apply: Thompson_transitivity. case/imsetP=> Q maxQ; rewrite K1 /orbit imset_set1 act1 => defAmax. have nQNA: 'N(A) \subset 'N(Q). apply/normsP=> x Nx; apply: congr_group; apply/set1P; rewrite -defAmax. by rewrite (acts_act (norm_acts_max_norm _ _)). have{nQNA} nQF: F \subset 'N(Q). exact: subset_trans (subset_trans (normal_norm nsAP) nQNA). have defFmax: |/|*(F; q) = [set Q] := max_normed_uniq defAmax sAF nQF. have nQM: M \subset 'N(Q). apply/normsP=> x Mx; apply: congr_group; apply/set1P; rewrite -defFmax. rewrite (acts_act (norm_acts_max_norm _ _)) ?defFmax ?set11 //. by rewrite (subsetP (gFnorm _ _)). have [<- // | ntQ] := eqVneq Q 1%G. rewrite inE in maxQ; have [qQ _] := andP (maxgroupp maxQ). have{nQM} defNQ: 'N(Q) = M. by rewrite (mmax_norm maxM) // (mFT_pgroup_proper qQ). case/negP: ntQ; rewrite -[_ == _]subG1 -Mp'1 -defNQ pcore_max ?normalG //. exact: pi_pnat qQ _. have{} p'nbyA_1 X: X \proper G -> p^'.-group X -> A \subset 'N(X) -> X :=: 1. - move=> prX p'X nXA; have solX := mFT_sol prX. apply/eqP; rewrite -trivg_Fitting // -subG1 /= FittingEgen gen_subG. apply/bigcupsP=> [[q /= _] _]; have [-> | p'q] := eqVneq q p. rewrite -(setIidPl (pcore_sub _ _)) coprime_TIg //. by rewrite (pnat_coprime (pcore_pgroup _ _)). have [R] := max_normed_exists (pcore_pgroup q X) (gFnorm_trans _ nXA). by rewrite p'nbyA_1 // => /set1P->. apply/subsetPn=> -[H0 MA_H0 neH0M]. pose H := [arg max_(H > H0 | (H \in 'M(A)) && (H != M)) #|H :&: M|`_p]. case: arg_maxnP @H => [|H {H0 MA_H0 neH0M}]; first by rewrite MA_H0 -in_set1. rewrite /= inE -andbA => /and3P[maxH sAH neHM] maxHM. have prH: H \proper G by rewrite inE in maxH; apply: maxgroupp maxH. have sAHM: A \subset H :&: M by rewrite subsetI sAH. have [R sylR_HM sAR]:= Sylow_superset sAHM (pgroupS sAP pP). have [/subsetIP[sRH sRM] pR _] := and3P sylR_HM. have{sylR_HM} sylR_H: p.-Sylow(H) R. have [Q sylQ] := Sylow_superset sRM pR; have [sQM pQ _] := and3P sylQ. case/eqVproper=> [defR | /(nilpotent_proper_norm (pgroup_nil pQ)) sRN]. apply: (pHall_subl sRH (subsetT _)); rewrite pHallE subsetT /=. by rewrite -(card_Hall sylPG) (card_Hall sylP) defR (card_Hall sylQ). case/maximal_exists: (subsetT 'N(R)) => [nRG | [D maxD sND]]. case/negP: (proper_irrefl (mem G)); rewrite -{1}nRG. rewrite mFT_norm_proper ?(mFT_pgroup_proper pR) //. by rewrite -proper1G (proper_sub_trans _ sAR) ?proper1G. move/implyP: (maxHM D); rewrite 2!inE {}maxD leqNgt. case: eqP sND => [->{D} sNM _ | _ sND]. rewrite -Sylow_subnorm (pHall_subl _ _ sylR_HM) ?setIS //. by rewrite subsetI sRH normG. rewrite (subset_trans (subset_trans sAR (normG R)) sND); case/negP. rewrite -(card_Hall sylR_HM) (leq_trans (proper_card sRN)) //. rewrite -(part_pnat_id (pgroupS (subsetIl _ _) pQ)) dvdn_leq //. by rewrite partn_dvd ?cardG_gt0 // cardSg //= setIC setISS. have Hp'1: 'O_p^'(H) = 1. apply: p'nbyA_1 (pcore_pgroup _ _) (subset_trans sAH (gFnorm _ _)). exact: sub_proper_trans (pcore_sub _ _) prH. have nsZLR_H: 'Z('L(R)) <| H. exact: Puig_center_normal (mFT_odd _) (mFT_sol prH) sylR_H _. have ntZLR: 'Z('L(R)) != 1. apply/eqP=> /(trivg_center_Puig_pgroup pR) R1. by rewrite -subG1 -R1 sAR in ntA. have defH: 'N('Z('L(R))) = H := mmax_normal maxH nsZLR_H ntZLR. have{sylR_H} sylR: p.-Sylow(G) R. rewrite -Sylow_subnorm setTI (pHall_subl _ _ sylR_H) ?normG //=. by rewrite -defH !gFnorm_trans. have nsZLR_M: 'Z('L(R)) <| M. have sylR_M := pHall_subl sRM (subsetT _) sylR. exact: Puig_center_normal (mFT_odd _) solM sylR_M _. case/eqP: neHM; apply: group_inj. by rewrite -defH (mmax_normal maxM nsZLR_M). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup automorphism action gproduct gfunctor) mathcomp(center commutator pgroup gseries nilpotent sylow abelian maximal) odd_order(BGsection1 BGsection5 BGsection6 BGsection7)