proposition: Lemma regular_abelem2_on_abelem2 p q gT (P Q : {group gT}) : p.-abelem P -> q.-abelem Q -> 'r_p(P) = 2%N ->'r_q(Q) = 2%N -> Q \subset 'N(P) -> 'C_Q(P) = 1%g -> (q %| p.-1)%N /\ (exists2 a, a \in Q^# & exists r, [/\ {in P, forall x, x ^ a = x ^+ r}%g, r ^ q = 1 %[mod p] & r != 1 %[mod p]]).
proof: Proof. move=> abelP abelQ; rewrite !p_rank_abelem // => logP logQ nPQ regQ. have ntP: P :!=: 1%g by case: eqP logP => // ->; rewrite cards1 logn1. have [p_pr _ _]:= pgroup_pdiv (abelem_pgroup abelP) ntP. have ntQ: Q :!=: 1%g by case: eqP logQ => // ->; rewrite cards1 logn1. have [q_pr _ _]:= pgroup_pdiv (abelem_pgroup abelQ) ntQ. pose rQ := abelem_repr abelP ntP nPQ. have [|P1 simP1 _] := dec_mxsimple_exists (mxmodule1 rQ). by rewrite oner_eq0. have [modP1 nzP1 _] := simP1. have ffulQ: mx_faithful rQ by apply: abelem_mx_faithful. have linP1: \rank P1 = 1%N. apply/eqP; have:= abelem_cyclic abelQ; rewrite logQ; apply: contraFT. rewrite neq_ltn ltnNge lt0n mxrank_eq0 nzP1 => P1full. have irrQ: mx_irreducible rQ. apply: mx_iso_simple simP1; apply: eqmx_iso; apply/eqmxP. by rewrite submx1 sub1mx -col_leq_rank {1}(dim_abelemE abelP ntP) logP. exact: mx_faithful_irr_abelian_cyclic irrQ (abelem_abelian abelQ). have ne_qp: q != p. move/implyP: (logn_quotient_cent_abelem nPQ abelP). by rewrite logP regQ indexg1 /=; case: eqP => // <-; rewrite logQ. have redQ: mx_completely_reducible rQ 1%:M. apply: mx_Maschke; apply: pi_pnat (abelem_pgroup abelQ) _. by rewrite inE /= (charf_eq (char_Fp p_pr)). have [P2 modP2 sumP12 dxP12] := redQ _ modP1 (submx1 _). have{dxP12} linP2: \rank P2 = 1%N. apply: (@addnI 1%N); rewrite -{1}linP1 -(mxdirectP dxP12) /= sumP12. by rewrite mxrank1 (dim_abelemE abelP ntP) logP. have{sumP12} [u def1]: exists u, 1%:M = u.1 *m P1 + u.2 *m P2. by apply/sub_addsmxP; rewrite sumP12. pose lam (Pi : 'M(P)) b := (nz_row Pi *m rQ b *m pinvmx (nz_row Pi)) 0 0. have rQ_lam Pi b: mxmodule rQ Pi -> \rank Pi = 1%N -> b \in Q -> Pi *m rQ b = lam Pi b *: Pi. - rewrite /lam => modPi linPi Qb; set v := nz_row Pi; set a := _ 0. have nz_v: v != 0 by rewrite nz_row_eq0 -mxrank_eq0 linPi. have sPi_v: (Pi <= v)%MS. by rewrite -mxrank_leqif_sup ?nz_row_sub // rank_rV nz_v linPi. have [v' defPi] := submxP sPi_v; rewrite {2}defPi scalemxAr -mul_scalar_mx. rewrite -mx11_scalar !(mulmxA v') -defPi mulmxKpV ?(submx_trans _ sPi_v) //. exact: (mxmoduleP modPi). have lam_q Pi b: mxmodule rQ Pi -> \rank Pi = 1%N -> b \in Q -> lam Pi b ^+ q = 1. - move=> modPi linPi Qb; apply/eqP; rewrite eq_sym -subr_eq0. have: \rank Pi != 0%N by rewrite linPi. apply: contraR; move/eqmx_scale=> <-. rewrite mxrank_eq0 scalerBl subr_eq0 -mul_mx_scalar -(repr_mx1 rQ). have <-: (b ^+ q = 1)%g by case/and3P: abelQ => _ _; move/exponentP->. apply/eqP; rewrite repr_mxX //. elim: (q) => [|k IHk]; first by rewrite scale1r mulmx1. by rewrite !exprS mulmxA rQ_lam // -scalemxAl IHk scalerA. pose f b := (lam P1 b, lam P2 b). have inj_f: {in Q &, injective f}. move=> b c Qb Qc /= [eq_bc1 eq_bc2]; apply: (mx_faithful_inj ffulQ) => //. rewrite -[rQ b]mul1mx -[rQ c]mul1mx {}def1 !mulmxDl -!mulmxA. by rewrite !{1}rQ_lam ?eq_bc1 ?eq_bc2. pose rs := [set x : 'F_p | x ^+ q == 1]. have s_fQ_rs: f @: Q \subset setX rs rs. apply/subsetP=> _ /imsetP[b Qb ->]. by rewrite !{1}inE /= !{1}lam_q ?eqxx. have le_rs_q: #|rs| <= q ?= iff (#|rs| == q). split; rewrite // cardE max_unity_roots ?enum_uniq ?prime_gt0 //. by apply/allP=> x; rewrite mem_enum inE unity_rootE. have:= subset_leqif_card s_fQ_rs. rewrite card_in_imset // (card_pgroup (abelem_pgroup abelQ)) logQ. case/(leqif_trans (leqif_mul le_rs_q le_rs_q))=> _; move/esym. rewrite cardsX eqxx andbb muln_eq0 orbb eqn0Ngt prime_gt0 //= => /andP[rs_q]. rewrite subEproper /proper {}s_fQ_rs andbF orbF => /eqP rs2_Q. have: ~~ (rs \subset [set 1 : 'F_p]). apply: contraL (prime_gt1 q_pr); move/subset_leq_card. by rewrite cards1 (eqnP rs_q) leqNgt. case/subsetPn => r rs_r; rewrite inE => ne_r_1. have rq1: r ^+ q = 1 by apply/eqP; rewrite inE in rs_r. split. have Ur: r \in GRing.unit. by rewrite -(unitrX_pos _ (prime_gt0 q_pr)) rq1 unitr1. pose u_r : {unit 'F_p} := Sub r Ur; have:= order_dvdG (in_setT u_r). rewrite card_units_Zp ?pdiv_gt0 // [X in totient X]/pdiv primes_prime //=. rewrite (@totient_pfactor p 1) // muln1; apply: dvdn_trans. have: (u_r ^+ q == 1)%g. by rewrite -val_eqE unit_Zp_expg -Zp_nat natrX natr_Zp rq1. case/primeP: q_pr => _ q_min; rewrite -order_dvdn; move/q_min. by rewrite order_eq1 -val_eqE (negPf ne_r_1) /=; move/eqnP->. have /imsetP[a Qa [def_a1 def_a2]]: (r, r) \in f @: Q. by rewrite -rs2_Q inE andbb. have rQa: rQ a = r%:M. rewrite -[rQ a]mul1mx def1 mulmxDl -!mulmxA !rQ_lam //. by rewrite -def_a1 -def_a2 !linearZ -scalerDr -def1 /= scalemx1. exists a. rewrite !inE Qa andbT; apply: contra ne_r_1 => a1. by rewrite (eqP a1) repr_mx1 in rQa; rewrite (fmorph_inj _ rQa). exists r; rewrite -!val_Fp_nat // natrX natr_Zp rq1. split=> // x Px; apply: (@abelem_rV_inj _ _ _ abelP ntP); rewrite ?groupX //. by rewrite memJ_norm ?(subsetP nPQ). by rewrite abelem_rV_X // -mul_mx_scalar natr_Zp -rQa -abelem_rV_J. 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)