proposition: Theorem Frobenius_prime_rfix1 F gT (G K R : {group gT}) n (rG : mx_representation F G n) : K ><| R = G -> solvable G -> prime #|R| -> 'C_K(R) = 1 -> [char F]^'.-group G -> \rank (rfix_mx rG R) = 1%N -> K^`(1) \subset rker rG.
proof: Proof. move=> defG solG p_pr regR F'G fixRlin. wlog closF: F rG F'G fixRlin / group_closure_field F gT. move=> IH; apply: (@group_closure_field_exists gT F) => [[Fc f closFc]]. rewrite -(rker_map f) IH //; last by rewrite -map_rfix_mx mxrank_map. by rewrite (eq_p'group _ (fmorph_char f)). move: {2}_.+1 (ltnSn #|K|) => m. elim: m => // m IHm in gT G K R rG solG p_pr regR F'G closF fixRlin defG *. rewrite ltnS => leKm. have [nsKG sRG defKR nKR tiKR] := sdprod_context defG. have [sKG nKG] := andP nsKG; have solK := solvableS sKG solG. have cycR := prime_cyclic p_pr. case: (eqsVneq K 1) => [-> | ntK]; first by rewrite derg1 commG1 sub1G. have defR x: x \in R^# -> <[x]> = R. case/setD1P; rewrite -cycle_subG -cycle_eq1 => ntX sXR. apply/eqP; rewrite eqEsubset sXR; apply: contraR ntX => /(prime_TIg p_pr). by rewrite /= (setIidPr sXR) => ->. have ntR: R :!=: 1 by rewrite -cardG_gt1 prime_gt1. have frobG: [Frobenius G = K ><| R]. by apply/Frobenius_semiregularP=> // x Rx; rewrite -cent_cycle defR. case: (eqVneq (rker rG) 1) => [ffulG | ntC]; last first. set C := rker rG in ntC *; have nsCG: C <| G := rker_normal rG. have [sCG nCG] := andP nsCG. have nCK := subset_trans sKG nCG; have nCR := subset_trans sRG nCG. case sKC: (K \subset C); first exact: gFsub_trans. have sCK: C \subset K. by rewrite proper_sub // (Frobenius_normal_proper_ker frobG) ?sKC. have frobGq: [Frobenius G / C = (K / C) ><| (R / C)]. by apply: Frobenius_quotient; rewrite ?sKC. have [defGq _ ntRq _ _] := Frobenius_context frobGq. rewrite -quotient_sub1 ?comm_subG ?quotient_der //= -/C. apply: subset_trans (kquo_mx_faithful rG). apply: IHm defGq _; rewrite 1?(quotient_sol, quotient_pgroup, rfix_quo) //. - rewrite card_quotient // -indexgI /= -/C setIC. by rewrite -(setIidPl sCK) -setIA tiKR (setIidPr (sub1G _)) indexg1. - have: cyclic (R / C) by [rewrite quotient_cyclic]; case/cyclicP=> Cx defRq. rewrite /= defRq cent_cycle (Frobenius_reg_ker frobGq) //= !inE defRq. by rewrite cycle_id -cycle_eq1 -defRq ntRq. - move=> Hq; rewrite -(group_inj (cosetpreK Hq)). by apply: quotient_splitting_field; rewrite ?subsetIl. by apply: leq_trans leKm; apply: ltn_quotient. have ltK_abelian (N : {group gT}): R \subset 'N(N) -> N \proper K -> abelian N. move=> nNR ltNK; have [sNK _] := andP ltNK; apply/commG1P/trivgP. rewrite -(setIidPr (sub1G (N <*> R))) /= -ffulG; set G1 := N <*> R. have sG1: G1 \subset G by rewrite join_subG (subset_trans sNK). have defG1: N ><| R = G1. by rewrite sdprodEY //; apply/trivgP; rewrite -tiKR setSI. rewrite -(rker_subg _ sG1). apply: IHm defG1 _; rewrite ?(solvableS sG1) ?(pgroupS sG1) //. by apply/trivgP; rewrite -regR setSI. by apply: leq_trans leKm; apply: proper_card. have cK'K': abelian K^`(1). exact: ltK_abelian (gFnorm_trans _ nKR) (sol_der1_proper solK _ ntK). pose fixG := rfix_mx rG; pose NRmod N (U : 'M_n) := N <*> R \subset rstabs rG U. have dx_modK_rfix (N : {group gT}) U V: N \subset K -> R \subset 'N(N) -> NRmod N U -> NRmod N V -> mxdirect (U + V) -> (U <= fixG N)%MS || (V <= fixG N)%MS. - move=> sNK nNR nUNR nVNR dxUV. have [-> | ntN] := eqsVneq N 1; first by rewrite -rfix_mx_rstabC sub1G. have sNRG: N <*> R \subset G by rewrite join_subG (subset_trans sNK). pose rNR := subg_repr rG sNRG. have nfixU W: NRmod N W -> ~~ (W <= fixG N)%MS -> (fixG R <= W)%MS. move=> nWN not_cWN; rewrite (sameP capmx_idPr eqmxP). rewrite -(geq_leqif (mxrank_leqif_eq (capmxSr _ _))) fixRlin lt0n. rewrite mxrank_eq0 -(in_submodK (capmxSl _ _)) val_submod_eq0. have modW: mxmodule rNR W by rewrite /mxmodule rstabs_subg subsetI subxx. rewrite -(eqmx_eq0 (rfix_submod modW _)) ?joing_subr //. apply: Frobenius_rfix_compl (pgroupS (subset_trans sNK sKG) F'G) _. apply/Frobenius_semiregularP=> // [|x Rx]. by rewrite sdprodEY //; apply/trivgP; rewrite -tiKR setSI. by apply/trivgP; rewrite -regR /= -cent_cycle defR ?setSI. by rewrite rker_submod rfix_mx_rstabC ?joing_subl. have: fixG R != 0 by rewrite -mxrank_eq0 fixRlin. apply: contraR; case/norP=> not_fixU not_fixW. by rewrite -submx0 -(mxdirect_addsP dxUV) sub_capmx !nfixU. have redG := mx_Maschke rG F'G. wlog [U simU nfixU]: / exists2 U, mxsimple rG U & ~~ (U <= fixG K)%MS. move=> IH; wlog [I U /= simU sumU _]: / mxsemisimple rG 1%:M. exact: (mx_reducible_semisimple (mxmodule1 _) redG). have [i nfixU | fixK] := pickP (fun i => ~~ (U i <= fixG K)%MS). by apply: IH; exists (U i). rewrite gFsub_trans // rfix_mx_rstabC // -sumU. by apply/sumsmx_subP=> i _; apply/idPn; rewrite fixK. have [modU ntU minU] := simU; pose rU := submod_repr modU. have irrU: mx_irreducible rU by apply/submod_mx_irr. have [W modW sumUW dxUW] := redG U modU (submx1 U). have cWK: (W <= fixG K)%MS. have:= dx_modK_rfix _ _ _ (subxx _) nKR _ _ dxUW. by rewrite /NRmod /= norm_joinEr // defKR (negPf nfixU); apply. have nsK'G: K^`(1) <| G by rewrite gFnormal_trans. have [sK'G nK'G] := andP nsK'G. suffices nregK'U: (rfix_mx rU K^`(1))%MS != 0. rewrite rfix_mx_rstabC ?normal_sub // -sumUW addsmx_sub andbC. rewrite (submx_trans cWK) ?rfix_mxS ?der_sub //= (sameP capmx_idPl eqmxP). rewrite minU ?capmxSl ?capmx_module ?normal_rfix_mx_module //. apply: contra nregK'U => cUK'; rewrite (eqmx_eq0 (rfix_submod _ _)) //. by rewrite (eqP cUK') linear0. pose rK := subg_repr rU (normal_sub nsKG); set p := #|R| in p_pr. wlog sK: / socleType rK by apply: socle_exists. have [i _ def_sK]: exists2 i, i \in setT & [set: sK] = orbit 'Cl G i. exact/imsetP/Clifford_atrans. have card_sK: #|[set: sK]| = #|G : 'C[i | 'Cl]|. by rewrite def_sK card_orbit_in ?indexgI. have ciK: K \subset 'C[i | 'Cl]. apply: subset_trans (astabS _ (subsetT _)). by apply: subset_trans (Clifford_astab _); apply: joing_subl. pose M := socle_base i; have simM: mxsimple rK M := socle_simple i. have [sKp | sK1 {ciK card_sK}]: #|[set: sK]| = p \/ #|[set: sK]| = 1%N. - apply/pred2P; rewrite orbC card_sK; case/primeP: p_pr => _; apply. by rewrite (_ : p = #|G : K|) ?indexgS // -divgS // -(sdprod_card defG) mulKn. - have{} def_sK: [set: sK] = orbit 'Cl R i. apply/eqP; rewrite eq_sym -subTset def_sK -[G in orbit _ G i]defKR. apply/subsetP=> _ /imsetP[_ /imset2P[y z /(subsetP ciK)ciy Rz ->] ->]. rewrite !(inE, sub1set) in ciy; have{ciy}[Gy /eqP-ciy]:= andP ciy. by rewrite actMin ?(subsetP sRG z Rz) // ciy mem_orbit. have inj_i: {in R &, injective ('Cl%act i)}. apply/dinjectiveP/card_uniqP; rewrite size_map -cardE -/p. by rewrite -sKp def_sK /orbit [in _ @: _]unlock cardsE. pose sM := (\sum_(y in R) M *m rU y)%MS. have dxM: mxdirect sM. apply/mxdirect_sumsP=> y Ry; have Gy := subsetP sRG y Ry. pose j := 'Cl%act i y. apply/eqP; rewrite -submx0 -{2}(mxdirect_sumsP (Socle_direct sK) j) //. rewrite capmxS ?val_Clifford_act // ?submxMr ?component_mx_id //. apply/sumsmx_subP => z; case/andP=> Rz ne_z_y; have Gz := subsetP sRG z Rz. rewrite (sumsmx_sup ('Cl%act i z)) ?(inj_in_eq inj_i) //. by rewrite val_Clifford_act // ?submxMr // ?component_mx_id. pose inCR := \sum_(x in R) rU x. have im_inCR: (inCR <= rfix_mx rU R)%MS. apply/rfix_mxP=> x Rx; have Gx := subsetP sRG x Rx. rewrite {2}[inCR](reindex_astabs 'R x) ?astabsR //= mulmx_suml. by apply: eq_bigr => y; move/(subsetP sRG)=> Gy; rewrite repr_mxM. pose inM := proj_mx M (\sum_(x in R | x != 1) M *m rU x)%MS. have dxM1 := mxdirect_sumsP dxM _ (group1 R). rewrite repr_mx1 mulmx1 in dxM1. have inCR_K: M *m inCR *m inM = M. rewrite mulmx_sumr (bigD1 1) //= repr_mx1 mulmx1 mulmxDl proj_mx_id //. by rewrite proj_mx_0 ?addr0 // summx_sub_sums. have [modM ntM _] := simM. have linM: \rank M = 1%N. apply/eqP; rewrite eqn_leq lt0n mxrank_eq0 ntM andbT. rewrite -inCR_K; apply: leq_trans (mxrankM_maxl _ _) _. apply: leq_trans (mxrankS (mulmx_sub _ im_inCR)) _. rewrite rfix_submod //; apply: leq_trans (mxrankM_maxl _ _) _. by rewrite -fixRlin mxrankS ?capmxSr. apply: contra (ntM); move/eqP; rewrite -submx0 => <-. by rewrite -(rfix_mx_rstabC rK) ?der_sub // -(rker_submod modM) rker_linear. have{sK i M simM sK1 def_sK} irrK: mx_irreducible rK. have cycGq: cyclic (G / K) by rewrite -defKR quotientMidl quotient_cyclic. apply: (mx_irr_prime_index closF irrU cycGq simM) => x Gx /=. apply: (component_mx_iso simM); first exact: Clifford_simple. have jP: component_mx rK (M *m rU x) \in socle_enum sK. exact/component_socle/Clifford_simple. pose j := PackSocle jP; apply: submx_trans (_ : j <= _)%MS. by rewrite PackSocleK component_mx_id //; apply: Clifford_simple. have def_i: [set i] == [set: sK] by rewrite eqEcard subsetT cards1 sK1. by rewrite ((j =P i) _) // -in_set1 (eqP def_i) inE. pose G' := K^`(1) <*> R. have sG'G: G' \subset G by rewrite join_subG sK'G. pose rG' := subg_repr rU sG'G. wlog irrG': / mx_irreducible rG'. move=> IH; wlog [M simM sM1]: / exists2 M, mxsimple rG' M & (M <= 1%:M)%MS. by apply: mxsimple_exists; rewrite ?mxmodule1; case: irrK. have [modM ntM _] := simM. have [M' modM' sumM dxM] := mx_Maschke rG' (pgroupS sG'G F'G) modM sM1. wlog{IH} ntM': / M' != 0. case: eqP sumM => [-> M1 _ | _ _ -> //]; apply: IH. by apply: mx_iso_simple simM; apply: eqmx_iso; rewrite addsmx0_id in M1. suffices: (K^`(1) \subset rstab rG' M) || (K^`(1) \subset rstab rG' M'). rewrite !rfix_mx_rstabC ?joing_subl //; rewrite -!submx0 in ntM ntM' *. by case/orP; move/submx_trans=> sM; apply: (contra (sM _ _)). rewrite !rstab_subg !rstab_submod !subsetI joing_subl !rfix_mx_rstabC //. rewrite /mxmodule !rstabs_subg !rstabs_submod !subsetI !subxx in modM modM'. do 2!rewrite orbC -genmxE. rewrite dx_modK_rfix // /NRmod ?(eqmx_rstabs _ (genmxE _)) ?der_sub //. exact: subset_trans sRG nK'G. apply/mxdirect_addsP; apply/eqP; rewrite -genmx_cap (eqmx_eq0 (genmxE _)). rewrite -(in_submodK (submx_trans (capmxSl _ _) (val_submodP _))). rewrite val_submod_eq0 in_submodE -submx0 (submx_trans (capmxMr _ _ _)) //. by rewrite -!in_submodE !val_submodK (mxdirect_addsP dxM). have nsK'K: K^`(1) <| K by apply: der_normal. pose rK'K := subg_repr rK (normal_sub nsK'K). have irrK'K: mx_absolutely_irreducible rK'K. wlog sK'K: / socleType rK'K by apply: socle_exists. have sK'_dv_K: #|[set: sK'K]| %| #|K|. exact: atrans_dvd_in (Clifford_atrans _ _). have nsK'G': K^`(1) <| G' := normalS (joing_subl _ _) sG'G nsK'G. pose rK'G' := subg_repr rG' (normal_sub nsK'G'). wlog sK'G': / socleType rK'G' by apply: socle_exists. have coKp: coprime #|K| p := Frobenius_coprime frobG. have nK'R := subset_trans sRG nK'G. have sK'_dv_p: #|[set: sK'G']| %| p. suffices: #|G' : 'C([set: sK'G'] | 'Cl)| %| #|G' : K^`(1)|. rewrite -(divgS (joing_subl _ _)) /= {2}norm_joinEr //. rewrite coprime_cardMg ?(coprimeSg (normal_sub nsK'K)) //. rewrite mulKn ?cardG_gt0 // -indexgI; apply: dvdn_trans. exact: atrans_dvd_index_in (Clifford_atrans _ _). rewrite indexgS //; apply: subset_trans (Clifford_astab sK'G'). exact: joing_subl. have eq_sK': #|[set: sK'K]| = #|[set: sK'G']|. rewrite !cardsT !cardE -!(size_map (fun i => socle_val i)). apply: perm_size. rewrite uniq_perm 1?(map_inj_uniq val_inj) 1?enum_uniq // => V. apply/mapP/mapP=> [] [i _ ->{V}]. exists (PackSocle (component_socle sK'G' (socle_simple i))). by rewrite mem_enum. by rewrite PackSocleK. exists (PackSocle (component_socle sK'K (socle_simple i))). by rewrite mem_enum. by rewrite PackSocleK. have [i def_i]: exists i, [set: sK'G'] = [set i]. apply/cards1P; rewrite -dvdn1 -[X in _ %| X](eqnP coKp) dvdn_gcd. by rewrite -{1}eq_sK' sK'_dv_K sK'_dv_p. pose M := socle_base i; have simM : mxsimple rK'G' M := socle_simple i. have cycGq: cyclic (G' / K^`(1)). by rewrite /G' joingC quotientYidr ?quotient_cyclic. apply closF; apply: (mx_irr_prime_index closF irrG' cycGq simM) => x K'x /=. apply: (component_mx_iso simM); first exact: Clifford_simple. have jP: component_mx rK'G' (M *m rG' x) \in socle_enum sK'G'. exact/component_socle/Clifford_simple. pose j := PackSocle jP; apply: submx_trans (_ : j <= _)%MS. by rewrite PackSocleK component_mx_id //; apply: Clifford_simple. by rewrite ((j =P i) _) // -in_set1 -def_i inE. have linU: \rank U = 1%N by apply/eqP; rewrite abelian_abs_irr in irrK'K. case: irrU => _ nz1 _; apply: contra nz1; move/eqP=> fix0. by rewrite -submx0 -fix0 -(rfix_mx_rstabC rK) ?der_sub // rker_linear. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)