proposition: Theorem odd_prime_sdprod_rfix0 F gT (G K R : {group gT}) n (rG : mx_representation F G n) : K ><| R = G -> solvable G -> odd #|G| -> coprime #|K| #|R| -> prime #|R| -> [char F]^'.-group G -> rfix_mx rG R = 0 -> [~: R, K] \subset rker rG.
proof: Proof. move: {2}_.+1 (ltnSn #|G|) => m; elim: m => // m IHm in gT G K R n rG *. rewrite ltnS; set p := #|R| => leGm defG solG oddG coKR p_pr F'G regR. have [nsKG sRG defKR nKR tiKR] := sdprod_context defG. have [sKG nKG] := andP nsKG; have solK := solvableS sKG solG. have [-> | ntK] := eqsVneq K 1; first by rewrite commG1 sub1G. have ker_ltK (H : {group gT}): H \proper K -> R \subset 'N(H) -> [~: R, H] \subset rker rG. - move=> ltKH nHR; have sHK := proper_sub ltKH; set G1 := H <*> R. have sG1G: G1 \subset G by rewrite join_subG (subset_trans sHK). have coHR := coprimeSg sHK coKR. have defG1: H ><| R = G1 by rewrite sdprodEY // coprime_TIg. apply: subset_trans (subsetIr G1 _); rewrite -(rker_subg _ sG1G). apply: IHm; rewrite ?(solvableS sG1G) ?(oddSg sG1G) ?(pgroupS sG1G) //. apply: leq_trans leGm; rewrite /= norm_joinEr // -defKR !coprime_cardMg //. by rewrite ltn_pmul2r ?proper_card. without loss [q q_pr qK]: / exists2 q, prime q & q.-group K. move=> IH; set q := pdiv #|K|. have q_pr: prime q by rewrite pdiv_prime ?cardG_gt1. have exHall := coprime_Hall_exists _ nKR coKR solK. have [Q sylQ nQR] := exHall q; have [Q' hallQ' nQ'R] := exHall q^'. have [sQK qQ _] := and3P sylQ; have [sQ'K q'Q' _] := and3P hallQ'. without loss{IH} ltQK: / Q \proper K. by rewrite properEneq; case: eqP IH => [<- -> | _ _ ->] //; exists q. have ltQ'K: Q' \proper K. rewrite properEneq; case: eqP (pgroupP q'Q' q q_pr) => //= ->. by rewrite !inE pdiv_dvd eqxx; apply. have nkerG := subset_trans _ (rker_norm rG). rewrite -quotient_cents2 ?nkerG //. have <-: Q * Q' = K. apply/eqP; rewrite eqEcard mulG_subG sQK sQ'K. rewrite coprime_cardMg ?(pnat_coprime qQ) //=. by rewrite (card_Hall sylQ) (card_Hall hallQ') partnC. rewrite quotientMl ?nkerG ?(subset_trans sQK) // centM subsetI. by rewrite !quotient_cents2r ?ker_ltK. without loss{m IHm leGm} [ffulG cycZ]: / rker rG = 1 /\ cyclic 'Z(G). move=> IH; wlog [I M /= simM sumM _]: / mxsemisimple rG 1%:M. exact: (mx_reducible_semisimple (mxmodule1 _) (mx_Maschke _ F'G)). pose not_cRK_M i := ~~ ([~: R, K] \subset rstab rG (M i)). case: (pickP not_cRK_M) => [i | cRK_M]; last first. rewrite rfix_mx_rstabC ?comm_subG // -sumM. apply/sumsmx_subP=> i _; move/negbFE: (cRK_M i). by rewrite rfix_mx_rstabC ?comm_subG. have [modM ntM _] := simM i; pose rM := kquo_repr (submod_repr modM). do [rewrite {+}/not_cRK_M -(rker_submod modM) /=; set N := rker _] in rM *. have [N1 _ | ntN] := eqVneq N 1. apply: IH; split. by apply/trivgP; rewrite -N1 /N rker_submod rstabS ?submx1. have: mx_irreducible (submod_repr modM) by apply/submod_mx_irr. by apply: mx_faithful_irr_center_cyclic; apply/trivgP. have tiRN: R :&: N = 1. by apply: prime_TIg; rewrite //= rker_submod rfix_mx_rstabC // regR submx0. have nsNG: N <| G := rker_normal _; have [sNG nNG] := andP nsNG. have nNR := subset_trans sRG nNG. have sNK: N \subset K. have [pi hallK]: exists pi, pi.-Hall(G) K. by apply: HallP; rewrite -(coprime_sdprod_Hall_l defG). rewrite (sub_normal_Hall hallK) //=. apply: pnat_dvd (pHall_pgroup hallK). rewrite -(dvdn_pmul2r (prime_gt0 p_pr)) -!TI_cardMg // 1?setIC // defKR. by rewrite -norm_joinEr // cardSg // join_subG sNG. have defGq: (K / N) ><| (R / N) = G / N. rewrite sdprodE ?quotient_norms -?quotientMr ?defKR //. by rewrite -quotientGI // tiKR quotient1. case/negP; rewrite -quotient_cents2 ?(subset_trans _ nNG) //= -/N. rewrite (sameP commG1P trivgP). apply: subset_trans (kquo_mx_faithful (submod_repr modM)). rewrite IHm ?quotient_sol ?coprime_morph ?morphim_odd ?quotient_pgroup //. - by apply: leq_trans leGm; apply: ltn_quotient. - by rewrite card_quotient // -indexgI tiRN indexg1. apply/eqP; rewrite -submx0 rfix_quo // rfix_submod //. by rewrite regR capmx0 linear0 sub0mx. without loss perfectK: / [~: K, R] = K. move=> IH; have: [~: K, R] \subset K by rewrite commg_subl. rewrite subEproper; case/predU1P=> //; move/ker_ltK. by rewrite commGC commg_normr coprime_commGid // commGC => ->. have primeR: {in R^#, forall x, 'C_K[x] = 'C_K(R)}. move=> x; case/setD1P=> nt_x Rx; rewrite -cent_cycle ((<[x]> =P R) _) //. rewrite eqEsubset cycle_subG Rx; apply: contraR nt_x; move/prime_TIg. by rewrite -cycle_eq1 (setIidPr _) ?cycle_subG // => ->. case cKK: (abelian K). rewrite commGC perfectK; move/eqP: regR; apply: contraLR. apply: Frobenius_rfix_compl => //; last exact: pgroupS F'G. rewrite -{2 4}perfectK coprime_abel_cent_TI // in primeR. by apply/Frobenius_semiregularP; rewrite // -cardG_gt1 prime_gt1. have [spK defZK]: special K /\ 'C_K(R) = 'Z(K). apply: (abelian_charsimple_special qK) => //. apply/bigcupsP=> H /andP[chHK cHH]. have:= char_sub chHK; rewrite subEproper. case/predU1P=> [eqHK | ltHK]; first by rewrite eqHK cKK in cHH. have nHR: R \subset 'N(H) := char_norm_trans chHK nKR. by rewrite (sameP commG1P trivgP) /= commGC -ffulG ker_ltK. have{spK} esK: extraspecial K. have abelZK := center_special_abelem qK spK; have [qZK _] := andP abelZK. have /(pgroup_pdiv qZK)[_ _ []]: 'Z(K) != 1. by case: spK => _ <-; rewrite (sameP eqP commG1P) -abelianE cKK. case=> [|e] oK; first by split; rewrite ?oK. suffices: cyclic 'Z(K) by rewrite (abelem_cyclic abelZK) oK pfactorK. rewrite (cyclicS _ cycZ) // subsetI subIset ?sKG //=. by rewrite -defKR centM subsetI -{2}defZK !subsetIr. have [e e_gt0 oKqe] := card_extraspecial qK esK. have cycR: cyclic R := prime_cyclic p_pr. have co_q_p: coprime q p by rewrite oKqe coprime_pexpl in coKR. move/eqP: regR; case/idPn. rewrite defZK in primeR. case: (repr_extraspecial_prime_sdprod_cycle _ _ defG _ oKqe) => // _. apply=> //; last exact/trivgP. apply: contraL (oddSg sRG oddG); move/eqP->; have:= oddSg sKG oddG. by rewrite oKqe addn1 /= !oddX /= orbC => ->. 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)