proposition: Theorem odd_p_stable gT p (G : {group gT}) : odd #|G| -> p.-stable G.
proof: Proof. move: gT G. pose p_xp gT (E : {group gT}) x := p.-elt x && (x \in 'C([~: E, [set x]])). suffices IH gT (E : {group gT}) x y (G := <<[set x; y]>>) : [&& odd #|G|, p.-group E & G \subset 'N(E)] -> p_xp gT E x && p_xp gT E y -> p.-group (G / 'C(E)). - move=> gT G oddG P A pP /andP[/mulGsubP[_ sPG] _] /andP[sANG pA] cRA. apply/subsetP=> _ /morphimP[x Nx Ax ->]; have NGx := subsetP sANG x Ax. apply: Baer_Suzuki => [|_ /morphimP[y Ny NGy ->]]; first exact: mem_quotient. rewrite -morphJ // -!morphim_set1 -?[<<_>>]morphimY ?sub1set ?groupJ //. set G1 := _ <*> _; rewrite /pgroup -(card_isog (second_isog _)); last first. by rewrite join_subG !sub1set Nx groupJ. have{Nx NGx Ny NGy} [[Gx Nx] [Gy Ny]] := (setIP NGx, setIP NGy). have sG1G: G1 \subset G by rewrite join_subG !sub1set groupJ ?andbT. have nPG1: G1 \subset 'N(P) by rewrite join_subG !sub1set groupJ ?andbT. rewrite -setIA setICA (setIidPr sG1G). rewrite (card_isog (second_isog _)) ?norms_cent //. apply: IH => //; first by rewrite pP nPG1 (oddSg sG1G). rewrite /p_xp -{2}(normP Ny) -conjg_set1 -conjsRg centJ memJ_conjg. rewrite p_eltJ andbb (mem_p_elt pA) // -sub1set centsC (sameP commG1P trivgP). by rewrite -cRA !commgSS ?sub1set. move: {2}_.+1 (ltnSn #|E|) => n; elim: n => // n IHn in gT E x y G *. rewrite ltnS => leEn /and3P[oddG pE nEG] /and3P[/andP[p_x cRx] p_y cRy]. have [Gx Gy]: x \in G /\ y \in G by apply/andP; rewrite -!sub1set -join_subG. apply: wlog_neg => p'Gc; apply/pgroupP=> q q_pr qGc; apply/idPn => p'q. have [Q sylQ] := Sylow_exists q [group of G]. have [sQG qQ]: Q \subset G /\ q.-group Q by case/and3P: sylQ. have{qQ p'q} p'Q: p^'.-group Q by apply: sub_in_pnat qQ => q' _ /eqnP->. have{q q_pr sylQ qGc} ncEQ: ~~ (Q \subset 'C(E)). apply: contraL qGc => cEQ; rewrite -p'natE // -partn_eq1 //. have nCQ: Q \subset 'N('C(E)) by apply: subset_trans (normG _). have sylQc: q.-Sylow(G / 'C(E)) (Q / 'C(E)) by rewrite morphim_pSylow. by rewrite -(card_Hall sylQc) -trivg_card1 (sameP eqP trivgP) quotient_sub1. have solE: solvable E := pgroup_sol pE. have ntE: E :!=: 1 by apply: contra ncEQ; move/eqP->; rewrite cents1. have{Q ncEQ p'Q sQG} minE_EG: minnormal E (E <*> G). apply/mingroupP; split=> [|D]; rewrite join_subG ?ntE ?normG //. case/and3P=> ntD nDE nDG sDE; have nDGi := subsetP nDG. apply/eqP; rewrite eqEcard sDE leqNgt; apply: contra ncEQ => ltDE. have nDQ: Q \subset 'N(D) by rewrite (subset_trans sQG). have cDQ: Q \subset 'C(D). rewrite -quotient_sub1 ?norms_cent // ?[_ / _]card1_trivg //. apply: pnat_1 (morphim_pgroup _ p'Q); apply: pgroupS (quotientS _ sQG) _. apply: IHn (leq_trans ltDE leEn) _ _; first by rewrite oddG (pgroupS sDE). rewrite /p_xp p_x p_y /=; apply/andP. by split; [move: cRx | move: cRy]; apply: subsetP; rewrite centS ?commSg. apply: (stable_factor_cent cDQ) solE; rewrite ?(pnat_coprime pE) //. apply/and3P; split; rewrite // -quotient_cents2 // centsC. rewrite -quotient_sub1 ?norms_cent ?quotient_norms ?(subset_trans sQG) //=. rewrite [(_ / _) / _]card1_trivg //=. apply: pnat_1 (morphim_pgroup _ (morphim_pgroup _ p'Q)). apply: pgroupS (quotientS _ (quotientS _ sQG)) _. have defGq: G / D = <<[set coset D x; coset D y]>>. by rewrite quotient_gen -1?gen_subG ?quotientU ?quotient_set1 ?nDGi. rewrite /= defGq IHn ?(leq_trans _ leEn) ?ltn_quotient // -?defGq. by rewrite quotient_odd // quotient_pgroup // quotient_norms. rewrite /p_xp -!sub1set !morph_p_elt -?quotient_set1 ?nDGi //=. by rewrite -!quotientR ?quotient_cents ?sub1set ?nDGi. have abelE: p.-abelem E. by rewrite -is_abelem_pgroup //; case: (minnormal_solvable minE_EG _ solE). have cEE: abelian E by case/and3P: abelE. have{minE_EG} minE: minnormal E G. case/mingroupP: minE_EG => _ minE; apply/mingroupP; rewrite ntE. split=> // D ntD sDE; apply: minE => //; rewrite join_subG cents_norm //. by rewrite centsC (subset_trans sDE). have nCG: G \subset 'N('C_G(E)) by rewrite normsI ?normG ?norms_cent. suffices{p'Gc} pG'c: p.-group (G / 'C_G(E))^`(1). have [Pc sylPc sGc'Pc]:= Sylow_superset (der_subS _ _) pG'c. have nsPc: Pc <| G / 'C_G(E) by rewrite sub_der1_normal ?(pHall_sub sylPc). case/negP: p'Gc; rewrite /pgroup -(card_isog (second_isog _)) ?norms_cent //. rewrite setIC; apply: pgroupS (pHall_pgroup sylPc) => /=. rewrite sub_quotient_pre // join_subG !sub1set !(subsetP nCG, inE) //=. by rewrite !(mem_normal_Hall sylPc) ?mem_quotient ?morph_p_elt ?(subsetP nCG). have defC := rker_abelem abelE ntE nEG; rewrite /= -/G in defC. set rG := abelem_repr abelE ntE nEG in defC. case ncxy: (rG x *m rG y == rG y *m rG x). have Cxy: [~ x, y] \in 'C_G(E). rewrite -defC inE groupR //= !repr_mxM ?groupM ?groupV // mul1mx -/rG. by rewrite (eqP ncxy) -!repr_mxM ?groupM ?groupV // mulKg mulVg repr_mx1. rewrite [_^`(1)](commG1P _) ?pgroup1 //= quotient_gen -gen_subG //= -/G. rewrite !gen_subG centsC gen_subG quotient_cents2r ?gen_subG //= -/G. rewrite /commg_set imset2Ul !imset2_set1l !imsetU !imset_set1. by rewrite !subUset andbC !sub1set !commgg group1 /= -invg_comm groupV Cxy. pose Ax : 'M(E) := rG x - 1; pose Ay : 'M(E) := rG y - 1. have Ax2: Ax *m Ax = 0. apply/row_matrixP=> i; apply/eqP; rewrite row_mul mulmxBr mulmx1. rewrite row0 subr_eq0 -(can_eq (rVabelemK abelE ntE)) rVabelemJ //. rewrite conjgE -(centP cRx) ?mulKg //. rewrite linearB /= addrC row1 rowE rVabelemD rVabelemN rVabelemJ //=. by rewrite mem_commg ?set11 ?mem_rVabelem. have Ay2: Ay *m Ay = 0. apply/row_matrixP=> i; apply/eqP; rewrite row_mul mulmxBr mulmx1. rewrite row0 subr_eq0 -(inj_eq (@rVabelem_inj _ _ _ abelE ntE)). rewrite rVabelemJ // conjgE -(centP cRy) ?mulKg //. rewrite linearB /= addrC row1 rowE rVabelemD rVabelemN rVabelemJ //=. by rewrite mem_commg ?set11 ?mem_rVabelem. pose A := Ax *m Ay + Ay *m Ax. have cAG: centgmx rG A. rewrite /centgmx gen_subG subUset !sub1set !inE Gx Gy /=; apply/andP. rewrite -[rG x](subrK 1%R) -[rG y](subrK 1%R) -/Ax -/Ay. rewrite 2!(mulmxDl _ 1 A) 2!(mulmxDr A _ 1) !mulmx1 !mul1mx. rewrite !(inj_eq (addIr A)) ![_ *m A]mulmxDr ![A *m _]mulmxDl. by rewrite -!mulmxA Ax2 Ay2 !mulmx0 !mulmxA Ax2 Ay2 !mul0mx !addr0 !add0r. have irrG: mx_irreducible rG by apply/abelem_mx_irrP. pose FA := gen_of irrG cAG; pose dA := gen_dim A. pose rAG : mx_representation FA G dA := gen_repr irrG cAG. pose inFA m W : 'M[FA]_(m, dA) := in_gen irrG cAG W. pose valFA m (W : 'M[FA]_(m, dA)) := val_gen W. rewrite -(rker_abelem abelE ntE nEG) -/rG -(rker_gen irrG cAG) -/rAG. have dA_gt0: dA > 0 by rewrite (gen_dim_gt0 irrG cAG). have irrAG: mx_irreducible rAG by apply: gen_mx_irr. have: dA <= 2. case Ax0: (Ax == 0). by rewrite subr_eq0 in Ax0; case/eqP: ncxy; rewrite (eqP Ax0) mulmx1 mul1mx. case/rowV0Pn: Ax0 => v /submxP[u def_v nzv]. pose U := col_mx v (v *m Ay); pose UA := <<inFA (1 + 1)%N U>>%MS. pose rvalFA m (W : 'M[FA]_(m, dA)) := rowval_gen W. have Umod: mxmodule rAG UA. rewrite /mxmodule gen_subG subUset !sub1set !inE Gx Gy /= andbC. apply/andP; split; rewrite (eqmxMr _ (genmxE _)) -in_genJ // genmxE. rewrite submx_in_gen // -[rG y](subrK 1%R) -/Ay mulmxDr mulmx1. rewrite addmx_sub // mul_col_mx -mulmxA Ay2 mulmx0. by rewrite -!addsmxE addsmx0 addsmxSr. rewrite -[rG x](subrK 1%R) -/Ax mulmxDr mulmx1 in_genD mul_col_mx. rewrite -mulmxA -[Ay *m Ax](addKr (Ax *m Ay)) (mulmxDr v _ A) -mulmxN. rewrite mulmxA {1 2}def_v -(mulmxA u) Ax2 mulmx0 mul0mx add0r. pose B := A; rewrite -(mul0mx _ B) -mul_col_mx -[B](mxval_groot irrG cAG). rewrite {B} -[_ 0 v](in_genK irrG cAG) -val_genZ val_genK. rewrite addmx_sub ?scalemx_sub ?submx_in_gen //. by rewrite -!addsmxE adds0mx addsmxSl. have nzU: UA != 0. rewrite -mxrank_eq0 genmxE mxrank_eq0 -(can_eq (fun W => val_genK W)). by rewrite in_genK val_gen0 -submx0 col_mx_sub submx0 negb_and nzv. case/mx_irrP: irrAG => _ /(_ UA Umod nzU)/eqnP <-. by rewrite genmxE rank_leq_row. rewrite leq_eqVlt ltnS leq_eqVlt ltnNge dA_gt0 orbF orbC; case/pred2P=> def_dA. rewrite [_^`(1)](commG1P _) ?pgroup1 // quotient_cents2r // gen_subG. apply/subsetP=> zt; case/imset2P=> z t Gz Gt ->{zt}. rewrite !inE groupR //= mul1mx; have Gtz := groupM Gt Gz. rewrite -(inj_eq (can_inj (mulKmx (repr_mx_unit rAG Gtz)))) mulmx1. rewrite [eq_op]lock -repr_mxM ?groupR ?groupM // -commgC !repr_mxM // -lock. apply/eqP; move: (rAG z) (rAG t); rewrite /= -/dA def_dA => Az At. by rewrite [Az]mx11_scalar scalar_mxC. move: (kquo_repr _) (kquo_mx_faithful rAG) => /=; set K := rker _. rewrite def_dA => r2G; move/der1_odd_GL2_charf; move/implyP. rewrite quotient_odd //= -/G; apply: etrans; apply: eq_pgroup => p'. have [p_pr _ _] := pgroup_pdiv pE ntE. by rewrite (fmorph_char (gen _ _)) (charf_eq (char_Fp _)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)