proposition: Theorem der1_odd_GL2_charf F gT (G : {group gT}) (rG : mx_representation F G 2) : odd #|G| -> mx_faithful rG -> [char F].-group G^`(1)%g.
proof: Proof. move=> oddG ffulG. without loss closF: F rG ffulG / group_closure_field F gT. move=> IH; apply: (@group_closure_field_exists gT F) => [[Fc f closFc]]. rewrite -(eq_pgroup _ (fmorph_char f)). by rewrite -(map_mx_faithful f) in ffulG; apply: IH ffulG closFc. elim: {G}_.+1 {-2}G (ltnSn #|G|) => // m IHm G le_g_m in rG oddG ffulG *. apply/pgroupP=> p p_pr pG'; rewrite !inE p_pr /=; apply: wlog_neg => p_nz. have [P sylP] := Sylow_exists p G. have nPG: G \subset 'N(P). apply/idPn=> ltNG; pose N := 'N_G(P); have sNG: N \subset G := subsetIl _ _. have{IHm ltNG} p'N': [char F].-group N^`(1)%g. apply: IHm (subg_mx_faithful sNG ffulG); last exact: oddSg oddG. rewrite -ltnS (leq_trans _ le_g_m) // ltnS proper_card //. by rewrite /proper sNG subsetI subxx. have{p'N'} tiPN': P :&: N^`(1)%g = 1%g. rewrite coprime_TIg ?(pnat_coprime (pHall_pgroup sylP)) //= -/N. apply: sub_in_pnat p'N' => q _; apply: contraL; move/eqnP->. by rewrite !inE p_pr. have sPN: P \subset N by rewrite subsetI normG (pHall_sub sylP). have{tiPN'} cPN: N \subset 'C(P). rewrite (sameP commG1P trivgP) -tiPN' subsetI commgS //. by rewrite commg_subr subsetIr. have /sdprodP[_ /= defG nKP _] := Burnside_normal_complement sylP cPN. set K := 'O_p^'(G) in defG nKP; have nKG: G \subset 'N(K) by apply: gFnorm. suffices p'G': p^'.-group G^`(1)%g by case/eqnP: (pgroupP p'G' p p_pr pG'). apply: pgroupS (pcore_pgroup p^' G); rewrite -quotient_cents2 //= -/K. by rewrite -defG quotientMidl /= -/K quotient_cents ?(subset_trans sPN). pose Q := G^`(1)%g :&: P; have sQG: Q \subset G by rewrite subIset ?der_subS. have nQG: G \subset 'N(Q) by rewrite normsI // normal_norm ?der_normalS. have pQ: (p %| #|Q|)%N. have sylQ: p.-Sylow(G^`(1)%g) Q. by apply: Sylow_setI_normal (der_normalS _ _) _. apply: contraLR pG'; rewrite -!p'natE // (card_Hall sylQ) -!partn_eq1 //. by rewrite part_pnat_id ?part_pnat. have{IHm} abelQ: abelian Q. apply/commG1P/eqP/idPn => ntQ'. have{IHm} p'Q': [char F].-group Q^`(1)%g. apply: IHm (subg_mx_faithful sQG ffulG); last exact: oddSg oddG. rewrite -ltnS (leq_trans _ le_g_m) // ltnS proper_card //. rewrite /proper sQG subsetI //= andbC subEproper. case: eqP => [-> /= | _]; last by rewrite /proper (pHall_sub sylP) andbF. have: nilpotent P by rewrite (pgroup_nil (pHall_pgroup sylP)). move/forallP/(_ P); apply: contraL; rewrite subsetI subxx => -> /=. apply: contra ntQ'; rewrite /Q => /eqP->. by rewrite (setIidPr _) ?sub1G // commG1. case/eqP: ntQ'; have{p'Q'}: P :&: Q^`(1)%g = 1%g. rewrite coprime_TIg ?(pnat_coprime (pHall_pgroup sylP)) //= -/Q. by rewrite (pi_p'nat p'Q') // !inE p_pr. by rewrite (setIidPr _) // comm_subG ?subsetIr. pose rQ := subg_repr rG sQG. wlog [U simU sU1]: / exists2 U, mxsimple rQ U & (U <= 1%:M)%MS. by apply: mxsimple_exists; rewrite ?mxmodule1 ?oner_eq0. have Uscal: \rank U = 1%N by apply: (mxsimple_abelian_linear (closF _)) simU. have{simU} [Umod _ _] := simU. have{sU1} [|V Vmod sumUV dxUV] := mx_Maschke _ _ Umod sU1. have: p.-group Q by apply: pgroupS (pHall_pgroup sylP); rewrite subsetIr. by apply: sub_in_pnat=> q _; move/eqnP->; rewrite !inE p_pr. have [u defU]: exists u : 'rV_2, (u :=: U)%MS. by move: (row_base U) (eq_row_base U); rewrite Uscal => u; exists u. have{dxUV Uscal} [v defV]: exists v : 'rV_2, (v :=: V)%MS. move/mxdirectP: dxUV; rewrite /= Uscal sumUV mxrank1 => [[Vscal]]. by move: (row_base V) (eq_row_base V); rewrite -Vscal => v; exists v. pose B : 'M_(1 + 1) := col_mx u v; have{sumUV} uB: B \in unitmx. rewrite -row_full_unit /row_full eqn_leq rank_leq_row {1}addn1. by rewrite -addsmxE -(mxrank1 F 2) -sumUV mxrankS // addsmxS ?defU ?defV. pose Qfix (w : 'rV_2) := {in Q, forall y, w *m rG y <= w}%MS. have{U defU Umod} u_fix: Qfix u. by move=> y Qy; rewrite /= (eqmxMr _ defU) defU (mxmoduleP Umod). have{V defV Vmod} v_fix: Qfix v. by move=> y Qy; rewrite /= (eqmxMr _ defV) defV (mxmoduleP Vmod). case/Cauchy: pQ => // x Qx oxp; have Gx := subsetP sQG x Qx. case/submxP: (u_fix x Qx) => a def_ux. case/submxP: (v_fix x Qx) => b def_vx. have def_x: rG x = B^-1 *m block_mx a 0 0 b *m B. rewrite -mulmxA -[2%N]/(1 + 1)%N mul_block_col !mul0mx addr0 add0r. by rewrite -def_ux -def_vx -mul_col_mx mulKmx. have ap1: a ^+ p = 1. suff: B^-1 *m block_mx (a ^+ p) 0 0 (b ^+ p) *m B = 1. move/(canRL (mulmxK uB))/(canRL (mulKVmx uB)); rewrite mul1mx. by rewrite mulmxV // scalar_mx_block; case/eq_block_mx. transitivity (rG x ^+ p); last first. by rewrite -(repr_mxX (subg_repr rG sQG)) // -oxp expg_order repr_mx1. elim: (p) => [|k IHk]; first by rewrite -scalar_mx_block mulmx1 mulVmx. rewrite !exprS -IHk def_x -!mulmxE !mulmxA mulmxK // -2!(mulmxA B^-1). by rewrite -[2%N]/(1 + 1)%N mulmx_block !mulmx0 !mul0mx !addr0 mulmxA add0r. have ab1: a * b = 1. have: Q \subset <<[set y in G | \det (rG y) == 1]>>. rewrite subIset // genS //; apply/subsetP=> yz; case/imset2P=> y z Gy Gz ->. rewrite inE !repr_mxM ?groupM ?groupV //= !detM (mulrCA _ (\det (rG y))). rewrite -!det_mulmx -!repr_mxM ?groupM ?groupV //. by rewrite mulKg mulVg repr_mx1 det1. rewrite gen_set_id; last first. apply/group_setP; split=> [|y z /setIdP[Gy /eqP y1] /setIdP[Gz /eqP z1]]. by rewrite inE group1 /= repr_mx1 det1. by rewrite inE groupM ?repr_mxM //= detM y1 z1 mulr1. case/subsetP/(_ x Qx)/setIdP=> _. rewrite def_x !detM mulrAC -!detM -mulrA mulKr // -!mulmxE. rewrite -[2%N]/(1 + 1)%N det_lblock // [a]mx11_scalar [b]mx11_scalar. by rewrite !det_scalar1 -scalar_mxM => /eqP->. have{ab1 ap1 def_x} ne_ab: a != b. apply/eqP=> defa; have defb: b = 1. rewrite -ap1 (divn_eq p 2) modn2. have ->: odd p by rewrite -oxp (oddSg _ oddG) // cycle_subG. by rewrite addn1 exprS mulnC exprM exprS {1 3}defa ab1 expr1n mulr1. suff x1: x \in [1] by rewrite -oxp (set1P x1) order1 in p_pr. rewrite (subsetP ffulG) // inE Gx def_x defa defb -scalar_mx_block mulmx1. by rewrite mul1mx mulVmx ?eqxx. have{a b ne_ab def_ux def_vx} nx_uv (w : 'rV_2): (w *m rG x <= w -> w <= u \/ w <= v)%MS. - case/submxP=> c; have:= mulmxKV uB w. rewrite -[_ *m invmx B]hsubmxK [lsubmx _]mx11_scalar [rsubmx _]mx11_scalar. move: (_ 0) (_ 0) => dv du; rewrite mul_row_col !mul_scalar_mx => <-{w}. rewrite mulmxDl -!scalemxAl def_ux def_vx mulmxDr -!scalemxAr. rewrite !scalemxAl -!mul_row_col; move/(can_inj (mulmxK uB)). case/eq_row_mx => eqac eqbc; apply/orP. have [-> | nz_dv] := eqVneq dv 0; first by rewrite scale0r addr0 scalemx_sub. have [-> | nz_du] := eqVneq du 0. by rewrite orbC scale0r add0r scalemx_sub. case/eqP: ne_ab; rewrite -[b]scale1r -(mulVf nz_dv) -[a]scale1r. by rewrite -(mulVf nz_du) -!scalerA eqac eqbc !scalerA !mulVf. have{x Gx Qx oxp nx_uv} redG y (A := rG y): y \in G -> (u *m A <= u /\ v *m A <= v)%MS. - move=> Gy; have uA: row_free A by rewrite row_free_unit repr_mx_unit. have Ainj (w t : 'rV_2): (w *m A <= w -> t *m A <= w -> t *m A <= t)%MS. case/sub_rVP=> [c ryww] /sub_rVP[d rytw]. rewrite -(submxMfree _ _ uA) rytw -scalemxAl ryww scalerA mulrC. by rewrite -scalerA scalemx_sub. have{Qx nx_uv} nAx w: Qfix w -> (w *m A <= u \/ w *m A <= v)%MS. move=> nwQ; apply: nx_uv; rewrite -mulmxA -repr_mxM // conjgCV. rewrite repr_mxM ?groupJ ?groupV // mulmxA submxMr // nwQ // -mem_conjg. by rewrite (normsP nQG). have [uAu | uAv] := nAx _ u_fix; have [vAu | vAv] := nAx _ v_fix; eauto. have [k ->]: exists k, A = A ^+ k.*2. exists #[y].+1./2; rewrite -mul2n -divn2 mulnC divnK. by rewrite -repr_mxX // expgS expg_order mulg1. by rewrite dvdn2 negbK; apply: oddSg oddG; rewrite cycle_subG. elim: k => [|k [IHu IHv]]; first by rewrite !mulmx1. case/sub_rVP: uAv => c uAc; case/sub_rVP: vAu => d vAd. rewrite doubleS !exprS !mulmxA; do 2!rewrite uAc vAd -!scalemxAl. by rewrite !scalemx_sub. suffices trivG': G^`(1)%g = 1%g. by rewrite /= trivG' cards1 gtnNdvd ?prime_gt1 in pG'. apply/trivgP; apply: subset_trans ffulG; rewrite gen_subG. apply/subsetP=> _ /imset2P[y z Gy Gz ->]; rewrite inE groupR //=. rewrite -(inj_eq (can_inj (mulKmx (repr_mx_unit rG (groupM Gz Gy))))). rewrite mul1mx mulmx1 -repr_mxM ?(groupR, groupM) // -commgC !repr_mxM //. rewrite -(inj_eq (can_inj (mulKmx uB))) !mulmxA !mul_col_mx. case/redG: Gy => /sub_rVP[a uya] /sub_rVP[b vyb]. case/redG: Gz => /sub_rVP[c uzc] /sub_rVP[d vzd]. by do 2!rewrite uya vyb uzc vzd -?scalemxAl; rewrite !scalerA mulrC (mulrC d). 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)