proposition: Theorem charf_GL2_der_subS_abelian_Sylow p F gT (G : {group gT}) (rG : mx_representation F G 2) : odd #|G| -> mx_faithful rG -> p \in [char F] -> exists P : {group gT}, [/\ p.-Sylow(G) P, abelian P & G^`(1)%g \subset P].
proof: Proof. move=> oddG ffG charFp. have{oddG} pG': p.-group G^`(1)%g. rewrite /pgroup -(eq_pnat _ (charf_eq charFp)). exact: der1_odd_GL2_charf ffG. have{pG'} [P SylP sG'P]:= Sylow_superset (der_sub _ _) pG'. exists P; split=> {sG'P}//; case/and3P: SylP => sPG pP _. apply/commG1P/trivgP; apply: subset_trans ffG; rewrite gen_subG. apply/subsetP=> _ /imset2P[y z Py Pz ->]; rewrite inE (subsetP sPG) ?groupR //=. pose rP := subg_repr rG sPG; pose U := rfix_mx rP P. rewrite -(inj_eq (can_inj (mulKmx (repr_mx_unit rP (groupM Pz Py))))). rewrite mul1mx mulmx1 -repr_mxM ?(groupR, groupM) // -commgC !repr_mxM //. have: U != 0 by apply: (rfix_pgroup_char charFp). rewrite -mxrank_eq0 -lt0n 2!leq_eqVlt ltnNge rank_leq_row orbF orbC eq_sym. case/orP=> [Ufull | Uscal]. suffices{y z Py Pz} rP1 y: y \in P -> rP y = 1%:M by rewrite !rP1 ?mulmx1. move=> Py; apply/row_matrixP=> i. by rewrite rowE -row1 (rfix_mxP P _) ?submx_full. have [u defU]: exists u : 'rV_2, (u :=: U)%MS. by move: (row_base U) (eq_row_base U); rewrite -(eqP Uscal) => u; exists u. have fix_u: {in P, forall x, u *m rP x = u}. by move/eqmxP: defU; case/andP; move/rfix_mxP. have [v defUc]: exists u : 'rV_2, (u :=: U^C)%MS. have UCscal: \rank U^C = 1%N by rewrite mxrank_compl -(eqP Uscal). by move: (row_base _)%MS (eq_row_base U^C)%MS; rewrite UCscal => v; exists v. pose B := col_mx u v; have uB: B \in unitmx. rewrite -row_full_unit -sub1mx -(eqmxMfull _ (addsmx_compl_full U)). by rewrite mulmx1 -addsmxE addsmxS ?defU ?defUc. have Umod: mxmodule rP U by apply: rfix_mx_module. pose W := rfix_mx (factmod_repr Umod) P. have ntW: W != 0. apply: (rfix_pgroup_char charFp) => //. rewrite eqmxMfull ?row_full_unit ?unitmx_inv ?row_ebase_unit //. by rewrite rank_copid_mx -(eqP Uscal). have{ntW} Wfull: row_full W. by rewrite -col_leq_rank {1}mxrank_coker -(eqP Uscal) lt0n mxrank_eq0. have svW: (in_factmod U v <= W)%MS by rewrite submx_full. have fix_v: {in P, forall x, v *m rG x - v <= u}%MS. move=> x Px /=; rewrite -[v *m _](add_sub_fact_mod U) (in_factmodJ Umod) //. move/rfix_mxP: svW => -> //; rewrite in_factmodK ?defUc // addrK. by rewrite defU val_submodP. have fixB: {in P, forall x, exists2 a, u *m rG x = u & v *m rG x = v + a *: u}. move=> x Px; case/submxP: (fix_v x Px) => a def_vx. exists (a 0 0); first exact: fix_u. by rewrite addrC -mul_scalar_mx -mx11_scalar -def_vx subrK. rewrite -(inj_eq (can_inj (mulKmx uB))) // !mulmxA !mul_col_mx. case/fixB: Py => a uy vy; case/fixB: Pz => b uz vz. by rewrite uy uz vy vz !mulmxDl -!scalemxAl uy uz vy vz addrAC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)