proposition: Theorem repr_extraspecial_prime_sdprod_cycle p n gT (G P H : {group gT}) : p.-group P -> extraspecial P -> P ><| H = G -> cyclic H -> let h := #|H| in #|P| = (p ^ n.*2.+1)%N -> coprime p h -> {in H^#, forall x, 'C_P[x] = 'Z(P)} -> (h %| p ^ n + 1) || (h %| p ^ n - 1) /\ ((h != p ^ n + 1)%N -> forall F q (rG : mx_representation F G q), [char F]^'.-group G -> mx_faithful rG -> rfix_mx rG H != 0).
proof: Proof. move=> pP esP sdPH_G cycH h oPpn co_p_h primeHP. set dvd_h_pn := _ || _; set neq_h_pn := h != _. suffices IH F q (rG : mx_representation F G q): [char F]^'.-group G -> mx_faithful rG -> dvd_h_pn && (neq_h_pn ==> (rfix_mx rG H != 0)). - split=> [|ne_h F q rG F'G ffulG]; last first. by case/andP: (IH F q rG F'G ffulG) => _; rewrite ne_h. pose r := pdiv #|G|.+1. have r_pr: prime r by rewrite pdiv_prime // ltnS cardG_gt0. have F'G: [char 'F_r]^'.-group G. rewrite /pgroup (eq_pnat _ (eq_negn (charf_eq (char_Fp r_pr)))). rewrite p'natE // -prime_coprime // (coprime_dvdl (pdiv_dvd _)) //. by rewrite /coprime -addn1 gcdnC gcdnDl gcdn1. by case/andP: (IH _ _ _ F'G (regular_mx_faithful _ _)). move=> F'G ffulG. without loss closF: F rG F'G ffulG / group_closure_field F gT. move=> IH; apply: (@group_closure_field_exists gT F) => [[Fs f clFs]]. rewrite -(map_mx_eq0 f) map_rfix_mx {}IH ?map_mx_faithful //. by rewrite (eq_p'group _ (fmorph_char f)). have p_pr := extraspecial_prime pP esP; have p_gt1 := prime_gt1 p_pr. have oZp := card_center_extraspecial pP esP; have[_ prZ] := esP. have{sdPH_G} [nsPG sHG defG nPH tiPH] := sdprod_context sdPH_G. have sPG := normal_sub nsPG. have coPH: coprime #|P| #|H| by rewrite oPpn coprime_pexpl. have nsZG: 'Z(P) <| G := gFnormal_trans _ nsPG. have defCP: 'C_G(P) = 'Z(P). apply/eqP; rewrite eqEsubset andbC setSI //=. rewrite -(coprime_mulG_setI_norm defG) ?norms_cent ?normal_norm //=. rewrite mul_subG // -(setD1K (group1 H)). apply/subsetP=> x; case/setIP; case/setU1P=> [-> // | H'x]. rewrite -sub_cent1; move/setIidPl; rewrite primeHP // => defP. by have:= min_card_extraspecial pP esP; rewrite -defP oZp (leq_exp2l 3 1). have F'P: [char F]^'.-group P by apply: pgroupS sPG F'G. have F'H: [char F]^'.-group H by apply: pgroupS sHG F'G. wlog{ffulG F'G} [irrG regZ]: q rG / mx_irreducible rG /\ rfix_mx rG 'Z(P) = 0. move=> IH; wlog [I W /= simW defV _]: / mxsemisimple rG 1%:M. exact: (mx_reducible_semisimple (mxmodule1 _) (mx_Maschke rG F'G)). have [z Zz ntz]: exists2 z, z \in 'Z(P) & z != 1%g. by apply/trivgPn; rewrite -cardG_gt1 oZp prime_gt1. have Gz := subsetP sPG z (subsetP (center_sub P) z Zz). case: (pickP (fun i => z \notin rstab rG (W i))) => [i ffZ | z1]; last first. case/negP: ntz; rewrite -in_set1 (subsetP ffulG) // inE Gz /=. apply/eqP; move/eqmxP: defV; case/andP=> _; case/sub_sumsmxP=> w ->. rewrite mulmx_suml; apply: eq_bigr => i _. by move/negbFE: (z1 i) => /rstab_act-> //; rewrite submxMl. have [modW _ _] := simW i; pose rW := submod_repr modW. rewrite -(eqmx_rstab _ (val_submod1 (W i))) -(rstab_submod modW) in ffZ. have irrW: mx_irreducible rW by apply/submod_mx_irr. have regZ: rfix_mx rW 'Z(P)%g = 0. apply/eqP; apply: contraR ffZ; case/mx_irrP: irrW => _ minW /minW. by rewrite normal_rfix_mx_module // -sub1mx inE Gz /= => /implyP/rfix_mxP->. have ffulP: P :&: rker rW = 1%g. apply: (TI_center_nil (pgroup_nil pP)). by rewrite /normal subsetIl normsI ?normG ?(subset_trans _ (rker_norm _)). rewrite /= setIC setIA (setIidPl (center_sub _)); apply: prime_TIg=> //. by apply: contra ffZ => /subsetP->. have cPker: rker rW \subset 'C_G(P). rewrite subsetI rstab_sub (sameP commG1P trivgP) /= -ffulP subsetI. rewrite commg_subl commg_subr (subset_trans sPG) ?rker_norm //. by rewrite (subset_trans (rstab_sub _ _)) ?normal_norm. have [->] := andP (IH _ _ (conj irrW regZ)); case: (neq_h_pn) => //. apply: contra; rewrite (eqmx_eq0 (rfix_submod modW sHG)) => /eqP->. by rewrite capmx0 linear0. pose rP := subg_repr rG sPG; pose rH := subg_repr rG sHG. wlog [M simM _]: / exists2 M, mxsimple rP M & (M <= 1%:M)%MS. by apply: (mxsimple_exists (mxmodule1 _)); last case irrG. have{M simM irrG regZ F'P} [irrP def_q]: mx_irreducible rP /\ q = (p ^ n)%N. have [modM nzM _]:= simM. have [] := faithful_repr_extraspecial _ _ oPpn _ _ simM => // [|<- isoM]. apply/eqP; apply: (TI_center_nil (pgroup_nil pP)). rewrite /= -(eqmx_rstab _ (val_submod1 M)) -(rstab_submod modM). exact: rker_normal. rewrite setIC prime_TIg //=; apply: contra nzM => cMZ. rewrite -submx0 -regZ; apply/rfix_mxP=> z; move/(subsetP cMZ)=> cMz. by rewrite (rstab_act cMz). suffices irrP: mx_irreducible rP. by split=> //; apply/eqP; rewrite eq_sym; case/mx_irrP: irrP => _; apply. apply: (@mx_irr_prime_index F _ G P _ M nsPG) => // [|x Gx]. by rewrite -defG quotientMidl quotient_cyclic. rewrite (bool_irrelevance (normal_sub nsPG) sPG). apply: isoM; first exact: (@Clifford_simple _ _ _ _ nsPG). have cZx: x \in 'C_G('Z(P)). rewrite (setIidPl _) // -defG mulG_subG centsC subsetIr. rewrite -(setD1K (group1 H)) subUset sub1G /=. by apply/subsetP=> y H'y; rewrite -sub_cent1 -(primeHP y H'y) subsetIr. by have [f] := Clifford_iso nsZG rG M cZx; exists f. pose E_P := enveloping_algebra_mx rP; have{irrP} absP := closF P _ _ irrP. have [q_gt0 EPfull]: q > 0 /\ (1%:M <= E_P)%MS by apply/andP; rewrite sub1mx. pose Z := 'Z(P); have [sZP nZP] := andP (center_normal P : Z <| P). have nHZ: H \subset 'N(Z) := subset_trans sHG (normal_norm nsZG). pose clPqH := [set Zx ^: (H / Z) | Zx in P / Z]%g. pose b (ZxH : {set coset_of Z}) := repr (repr ZxH). have Pb ZxH: ZxH \in clPqH -> b ZxH \in P. case/imsetP=> Zx P_Zx ->{ZxH}. rewrite -(quotientGK (center_normal P)) /= -/Z inE repr_coset_norm /=. rewrite inE coset_reprK; apply: subsetP (mem_repr _ (class_refl _ _)). rewrite -class_support_set1l class_support_sub_norm ?sub1set //. by rewrite quotient_norms. have{primeHP coPH} card_clPqH ZxH: ZxH \in clPqH^# -> #|ZxH| = #|H|. case/setD1P=> ntZxH P_ZxH. case/imsetP: P_ZxH ntZxH => Zx P_Zx ->{ZxH}; rewrite classG_eq1 => ntZx. rewrite -index_cent1 ['C__[_]](trivgP _). rewrite indexg1 card_quotient // -indexgI setICA setIA tiPH. by rewrite (setIidPl (sub1G _)) indexg1. apply/subsetP=> Zy => /setIP[/morphimP[y Ny]]; rewrite -(setD1K (group1 H)). case/setU1P=> [-> | Hy] ->{Zy} cZxy; first by rewrite morph1 set11. have: Zx \in 'C_(P / Z)(<[y]> / Z). by rewrite inE P_Zx quotient_cycle // cent_cycle cent1C. case/idPn; rewrite -coprime_quotient_cent ?cycle_subG ?(pgroup_sol pP) //. by rewrite /= cent_cycle primeHP // trivg_quotient inE. by apply: coprimegS coPH; rewrite cycle_subG; case/setD1P: Hy. pose B x := \matrix_(i < #|H|) mxvec (rP (x ^ enum_val i)%g). have{E_P EPfull absP} sumB: (\sum_(ZxH in clPqH) <<B (b ZxH)>> :=: 1%:M)%MS. apply/eqmxP; rewrite submx1 (submx_trans EPfull) //. apply/row_subP=> ix; set x := enum_val ix; pose ZxH := coset Z x ^: (H / Z)%g. have Px: x \in P by [rewrite enum_valP]; have nZx := subsetP nZP _ Px. have P_ZxH: ZxH \in clPqH by apply: imset_f; rewrite mem_quotient. have Pbx := Pb _ P_ZxH; have nZbx := subsetP nZP _ Pbx. rewrite rowK (sumsmx_sup ZxH) {P_ZxH}// genmxE -/x. have: coset Z x \in coset Z (b ZxH) ^: (H / Z)%g. by rewrite class_sym coset_reprK (mem_repr _ (class_refl _ _)). case/imsetP=> _ /morphimP[y Ny Hy ->]. rewrite -morphJ //; case/kercoset_rcoset; rewrite ?groupJ // => z Zz ->. have [Pz cPz] := setIP Zz; rewrite repr_mxM ?memJ_norm ?(subsetP nPH) //. have [a ->]: exists a, rP z = a%:M. apply/is_scalar_mxP; apply: (mx_abs_irr_cent_scalar absP). by apply/centgmxP=> t Pt; rewrite -!repr_mxM ?(centP cPz). rewrite mul_scalar_mx linearZ scalemx_sub //. by rewrite (eq_row_sub (gring_index H y)) // rowK gring_indexK. have{card_clPqH} Bfree_if ZxH: ZxH \in clPqH^# -> \rank <<B (b ZxH)>> <= #|ZxH| ?= iff row_free (B (b ZxH)). - by move=> P_ZxH; rewrite genmxE card_clPqH // /leqif rank_leq_row. have B1_if: \rank <<B (b 1%g)>> <= 1 ?= iff (<<B (b 1%g)>> == mxvec 1%:M)%MS. have r1: \rank (mxvec 1%:M : 'rV[F]_(q ^ 2)) = 1%N. by rewrite rank_rV mxvec_eq0 -mxrank_eq0 mxrank1 -lt0n q_gt0. rewrite -{1}r1; apply: mxrank_leqif_eq; rewrite genmxE. have ->: b 1%g = 1%g by rewrite /b repr_set1 repr_coset1. by apply/row_subP=> i; rewrite rowK conj1g repr_mx1. have rankEP: \rank (1%:M : 'A[F]_q) = (\sum_(ZxH in clPqH) #|ZxH|)%N. rewrite acts_sum_card_orbit ?astabsJ ?quotient_norms // card_quotient //. rewrite mxrank1 -divgS // -mulnn oPpn oZp expnS -muln2 expnM -def_q. by rewrite mulKn // ltnW. have cl1: 1%g \in clPqH by apply/imsetP; exists 1%g; rewrite ?group1 ?class1G. have{B1_if Bfree_if}:= leqif_add B1_if (leqif_sum Bfree_if). case/(leqif_trans (mxrank_sum_leqif _)) => _ /=. rewrite -{1}(big_setD1 _ cl1) sumB {}rankEP (big_setD1 1%g) // cards1 eqxx. case/esym/and3P=> dxB /eqmxP defB1 /forall_inP/= Bfree. have [yg defH] := cyclicP cycH; pose g := rG yg. have Hxg: yg \in H by [rewrite defH cycle_id]; have Gyg := subsetP sHG _ Hxg. pose gE : 'A_q := lin_mx (mulmx (invmx g) \o mulmxr g). pose yr := regular_repr F H yg. have mulBg x: x \in P -> B x *m gE = yr *m B x. move/(subsetP sPG)=> Gx. apply/row_matrixP=> i; have Hi := enum_valP i; have Gi := subsetP sHG _ Hi. rewrite 2!row_mul !rowK mul_vec_lin /= -rowE rowK gring_indexK ?groupM //. by rewrite conjgM -repr_mxV // -!repr_mxM // ?(groupJ, groupM, groupV). wlog sH: / irrType F H by apply: socle_exists. have{cycH} linH: irr_degree (_ : sH) = 1%N. exact: irr_degree_abelian (cyclic_abelian cycH). have baseH := linear_irr_comp F'H (closF H) (linH _). have{} linH (W : sH): \rank W = 1%N by rewrite baseH; apply: linH. have [w] := cycle_repr_structure sH defH F'H (closF H). rewrite -/h => prim_w [Wi [bijWi _ _ Wi_yg]]. have{Wi_yg baseH} Wi_yr i: Wi i *m yr = w ^+ i *: (Wi i : 'M_h). have /submxP[u ->]: (Wi i <= val_submod (irr_repr (Wi i) 1%g))%MS. by rewrite repr_mx1 val_submod1 -baseH. rewrite repr_mx1 -mulmxA -2!linearZ; congr (u *m _). by rewrite -mul_mx_scalar -Wi_yg /= val_submodJ. pose E_ m := eigenspace gE (w ^+ m). have dxE: mxdirect (\sum_(m < h) E_ m)%MS. apply: mxdirect_sum_eigenspace => m1 m2 _ _ eq_m12; apply/eqP. by move/eqP: eq_m12; rewrite (eq_prim_root_expr prim_w) !modn_small. pose B2 ZxH i : 'A_q := <<Wi i *m B (b ZxH)>>%MS. pose B1 i : 'A_q := (\sum_(ZxH in clPqH^#) B2 ZxH i)%MS. pose SB := (<<B (b 1%g)>> + \sum_i B1 i)%MS. have{yr Wi_yr Pb mulBg} sB1E i: (B1 i <= E_ i)%MS. apply/sumsmx_subP=> ZxH /setIdP[_]; rewrite genmxE => P_ZxH. by apply/eigenspaceP; rewrite -mulmxA mulBg ?Pb // mulmxA Wi_yr scalemxAl. have{bijWi sumB cl1 F'H} defSB: (SB :=: 1%:M)%MS. apply/eqmxP; rewrite submx1 -sumB (big_setD1 _ cl1) addsmxS //=. rewrite exchange_big sumsmxS // => ZxH _; rewrite genmxE /= -sumsmxMr_gen. rewrite -((reindex Wi) xpredT val) /=; last by apply: onW_bij. by rewrite -/(Socle _) (reducible_Socle1 sH (mx_Maschke _ F'H)) mul1mx. rewrite mxdirect_addsE /= in dxB; case/and3P: dxB => _ dxB dxB1. have{linH Bfree dxB} rankB1 i: \rank (B1 i) = #|clPqH^#|. rewrite -sum1_card (mxdirectP _) /=. by apply: eq_bigr => ZxH P_ZxH; rewrite genmxE mxrankMfree ?Bfree. apply/mxdirect_sumsP=> ZxH P_ZxH. apply/eqP; rewrite -submx0 -{2}(mxdirect_sumsP dxB _ P_ZxH) capmxS //. by rewrite !genmxE submxMl. by rewrite sumsmxS // => ZyH _; rewrite !genmxE submxMl. have rankEi (i : 'I_h) : i != 0%N :> nat -> \rank (E_ i) = #|clPqH^#|. move=> i_gt0; apply/eqP; rewrite -(rankB1 i) (mxrank_leqif_sup _) ?sB1E //. rewrite -[E_ i]cap1mx -(cap_eqmx defSB (eqmx_refl _)) /SB. rewrite (bigD1 i) //= (addsmxC (B1 i)) addsmxA addsmxC -matrix_modl //. rewrite -(addsmx0 (q ^ 2) (B1 i)) addsmxS //. rewrite capmxC -{2}(mxdirect_sumsP dxE i) // capmxS // addsmx_sub // . rewrite (sumsmx_sup (Ordinal (cardG_gt0 H))) ?sumsmxS 1?eq_sym //. rewrite defB1; apply/eigenspaceP; rewrite mul_vec_lin scale1r /=. by rewrite mul1mx mulVmx ?repr_mx_unit. have{b B defB1 rP rH sH Wi rankB1 dxB1 defSB sB1E B1 B2 dxE SB} rankE0 i: (i : 'I_h) == 0%N :> nat -> \rank (E_ i) = #|clPqH^#|.+1. - move=> i_eq0; rewrite -[E_ i]cap1mx -(cap_eqmx defSB (eqmx_refl _)) /SB. rewrite (bigD1 i) // addsmxA -matrix_modl; last first. rewrite addsmx_sub // sB1E andbT defB1; apply/eigenspaceP. by rewrite mul_vec_lin (eqP i_eq0) scale1r /= mul1mx mulVmx ?repr_mx_unit. rewrite (((_ :&: _)%MS =P 0) _). rewrite addsmx0 mxrank_disjoint_sum /=. by rewrite defB1 rank_rV rankB1 mxvec_eq0 -mxrank_eq0 mxrank1 -lt0n q_gt0. apply/eqP; rewrite -submx0 -(eqP dxB1) capmxS // sumsmxS // => ZxH _. by rewrite !genmxE ?submxMl. by rewrite -submx0 capmxC /= -{2}(mxdirect_sumsP dxE i) // capmxS ?sumsmxS. have{clPqH rankE0 rankEi} (m): m != 0 %[mod h] -> \rank (E_ 0%N) = (\rank (E_ m)).+1. - move=> nz_m; rewrite (rankE0 (Ordinal (cardG_gt0 H))) //. rewrite /E_ -(prim_expr_mod prim_w); rewrite mod0n in nz_m. have lt_m: m %% h < h by rewrite ltn_mod ?cardG_gt0. by rewrite (rankEi (Ordinal lt_m)). have: q > 1. rewrite def_q (ltn_exp2l 0) // lt0n. apply: contraL (min_card_extraspecial pP esP). by rewrite oPpn; move/eqP->; rewrite leq_exp2l. rewrite {}/E_ {}/gE {}/dvd_h_pn {}/neq_h_pn -{n oPpn}def_q subn1 addn1 /=. case: q q_gt0 => // q' _ in rG g * => q_gt1 rankE. have gh1: g ^+ h = 1 by rewrite -repr_mxX // /h defH expg_order repr_mx1. apply/andP; split. have [n' def_q _]:= rank_eigenspaces_quasi_homocyclic gh1 prim_w rankE. move/eqP: def_q; rewrite distn_eq1 eqSS. by case: ifP => _ /eqP->; rewrite dvdn_mulr ?orbT. apply/implyP; apply: contra => regH. have [|-> //]:= rank_eigenspaces_free_quasi_homocyclic gh1 prim_w rankE q_gt1. apply/eqP; rewrite mxrank_eq0 -submx0 -(eqP regH). apply/rV_subP=> v /eigenspaceP; rewrite scale1r => cvg. apply/rfix_mxP=> y Hy; apply: rstab_act (submx_refl v); apply: subsetP y Hy. by rewrite defH cycle_subG !inE Gyg /= cvg. 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)