proposition: Theorem extraspecial_repr_structure (sS : irrType F S) : [/\ #|linear_irr sS| = (p ^ n.*2)%N, exists iphi : 'I_p.-1 -> sS, let phi i := irr_repr (iphi i) in [/\ injective iphi, codom iphi =i ~: linear_irr sS, forall i, mx_faithful (phi i), forall z, z \in 'Z(S)^# -> exists2 w, primitive_root_of_unity p w & forall i, phi i z = (w ^+ i.+1)%:M & forall i, irr_degree (iphi i) = (p ^ n)%N] & #|sS| = (p ^ n.*2 + p.-1)%N].
proof: Proof. have [[defPhiS defS'] prZ] := esS; set linS := linear_irr sS. have nb_lin: #|linS| = (p ^ n.*2)%N. rewrite card_linear_irr // -divgS ?der_sub //=. by rewrite oSpn defS' oZp expnS mulKn. have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N. pose Zcl := classes S ::&: 'Z(S). have cardZcl: #|Zcl| = p. transitivity #|[set [set z] | z in 'Z(S)]|; last first. by rewrite card_imset //; apply: set1_inj. apply: eq_card => zS; apply/setIdP/imsetP=> [[] | [z]]. case/imsetP=> z Sz ->{zS} szSZ. have Zz: z \in 'Z(S) by rewrite (subsetP szSZ) ?class_refl. exists z => //; rewrite inE Sz in Zz. apply/eqP; rewrite eq_sym eqEcard sub1set class_refl cards1. by rewrite -index_cent1 (setIidPl _) ?indexgg // sub_cent1. case/setIP=> Sz cSz ->{zS}; rewrite sub1set inE Sz; split=> //. apply/imsetP; exists z; rewrite //. apply/eqP; rewrite eqEcard sub1set class_refl cards1. by rewrite -index_cent1 (setIidPl _) ?indexgg // sub_cent1. move/eqP: (class_formula S); rewrite (bigID [in Zcl]) /=. rewrite (eq_bigr (fun _ => 1)) => [|zS]; last first. case/andP=> _ /setIdP[/imsetP[z Sz ->{zS}] /subsetIP[_ cSzS]]. rewrite (setIidPl _) ?indexgg // sub_cent1 (subsetP cSzS) //. exact: mem_repr (class_refl S z). rewrite sum1dep_card setIdE (setIidPr _) 1?cardsE ?cardZcl; last first. by apply/subsetP=> zS /[!inE] /andP[]. have pn_gt0: p ^ n.*2 > 0 by rewrite expn_gt0 p_gt0. rewrite card_irr // oSpn expnS -(prednK pn_gt0) mulnS eqn_add2l. rewrite (eq_bigr (fun _ => p)) => [|xS]; last first. case/andP=> SxS; rewrite inE SxS; case/imsetP: SxS => x Sx ->{xS} notZxS. have [y Sy ->] := repr_class S x; apply: p_maximal_index => //. apply: cent1_extraspecial_maximal => //; first exact: groupJ. apply: contra notZxS => Zxy; rewrite -{1}(lcoset_id Sy) class_lcoset. rewrite ((_ ^: _ =P [set x ^ y])%g _) ?sub1set // eq_sym eqEcard. rewrite sub1set class_refl cards1 -index_cent1 (setIidPl _) ?indexgg //. by rewrite sub_cent1; apply: subsetP Zxy; apply: subsetIr. rewrite sum_nat_cond_const mulnC eqn_pmul2l //; move/eqP <-. rewrite addSnnS prednK // -cardZcl -[card _](cardsID Zcl) /= addnC. by congr (_ + _)%N; apply: eq_card => t; rewrite !inE andbC // andbAC andbb. have fful_nlin i: i \in ~: linS -> mx_faithful (irr_repr i). rewrite !inE => nlin_phi. apply/trivgP; apply: (TI_center_nil (pgroup_nil pS) (rker_normal _)). rewrite setIC; apply: (prime_TIg prZ); rewrite /= -defS' der1_sub_rker //. exact: socle_irr. have [i0 nlin_i0]: exists i0, i0 \in ~: linS. by apply/card_gt0P; rewrite cardsCs setCK nb_irr nb_lin addKn -subn1 subn_gt0. have [z defZ]: exists z, 'Z(S) = <[z]> by apply/cyclicP; rewrite prime_cyclic. have Zz: z \in 'Z(S) by [rewrite defZ cycle_id]; have [Sz cSz] := setIP Zz. have ozp: #[z] = p by rewrite -oZp defZ. have ntz: z != 1%g by rewrite -order_gt1 ozp. pose phi := irr_repr i0; have irr_phi: mx_irreducible phi := socle_irr i0. pose w := irr_mode i0 z. have phi_z: phi z = w%:M by rewrite /phi irr_center_scalar. have phi_ze e: phi (z ^+ e)%g = (w ^+ e)%:M. by rewrite /phi irr_center_scalar ?groupX ?irr_modeX. have wp1: w ^+ p = 1 by rewrite -irr_modeX // -ozp expg_order irr_mode1. have injw: {in 'Z(S) &, injective (irr_mode i0)}. move=> x y Zx Zy /= eq_xy; have [[Sx _] [Sy _]] := (setIP Zx, setIP Zy). apply: mx_faithful_inj (fful_nlin _ nlin_i0) _ _ Sx Sy _. by rewrite !{1}irr_center_scalar ?eq_xy; first by split. have prim_w e: 0 < e < p -> p.-primitive_root (w ^+ e). case/andP=> e_gt0 lt_e_p; apply/andP; split=> //. apply/eqfunP=> -[d ltdp] /=; rewrite unity_rootE -exprM. rewrite -(irr_mode1 i0) -irr_modeX // (inj_in_eq injw) ?groupX ?group1 //. rewrite -order_dvdn ozp Euclid_dvdM // gtnNdvd //=. move: ltdp; rewrite leq_eqVlt. by case: eqP => [-> _ | _ ltd1p]; rewrite (dvdnn, gtnNdvd). have /cyclicP[a defAutZ]: cyclic (Aut 'Z(S)) by rewrite Aut_prime_cyclic ?ozp. have phi_unitP (i : 'I_p.-1): (i.+1%:R : 'Z_#[z]) \in GRing.unit. by rewrite unitZpE ?order_gt1 // ozp prime_coprime // -lt0n !modIp'. pose ephi i := invm (injm_Zpm a) (Zp_unitm (FinRing.Unit (phi_unitP i))). pose j : 'Z_#[z] := val (invm (injm_Zp_unitm z) a). have co_j_p: coprime j p. rewrite coprime_sym /j; case: (invm _ a) => /=. by rewrite ozp /GRing.unit /= Zp_cast. have [alpha Aut_alpha alphaZ] := center_aut_extraspecial pS esS co_j_p. have alpha_i_z i: ((alpha ^+ ephi i) z = z ^+ i.+1)%g. transitivity ((a ^+ ephi i) z)%g. elim: (ephi i : nat) => // e IHe; rewrite !expgS !permM alphaZ //. have Aut_a: a \in Aut 'Z(S) by rewrite defAutZ cycle_id. rewrite -{2}[a](invmK (injm_Zp_unitm z)); last by rewrite im_Zp_unitm -defZ. rewrite /= autE ?cycle_id // -/j /= /cyclem. rewrite -(autmE (groupX _ Aut_a)) -(autmE (groupX _ Aut_alpha)). by rewrite !morphX //= !autmE IHe. rewrite [(a ^+ _)%g](invmK (injm_Zpm a)) /=; last first. by rewrite im_Zpm -defAutZ defZ Aut_aut. by rewrite autE ?cycle_id //= val_Zp_nat ozp ?modIp'. have rphiP i: S :==: autm (groupX (ephi i) Aut_alpha) @* S by rewrite im_autm. pose rphi i := morphim_repr (eqg_repr phi (rphiP i)) (subxx S). have rphi_irr i: mx_irreducible (rphi i) by apply/morphim_mx_irr/eqg_mx_irr. have rphi_fful i: mx_faithful (rphi i). rewrite /mx_faithful rker_morphim rker_eqg. by rewrite (trivgP (fful_nlin _ nlin_i0)) morphpreIdom; apply: injm_autm. have rphi_z i: rphi i z = (w ^+ i.+1)%:M. by rewrite /rphi [phi]lock /= /morphim_mx autmE alpha_i_z -lock phi_ze. pose iphi i := irr_comp sS (rphi i); pose phi_ i := irr_repr (iphi i). have{} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M. rewrite /phi_ !{1}irr_center_scalar ?groupX ?irr_modeX //. suffices ->: irr_mode (iphi i) z = w ^+ i.+1 by rewrite mulnC exprM. have:= mx_rsim_sym (rsim_irr_comp sS F'S (rphi_irr i)). case/mx_rsim_def=> B [B' _ homB]; rewrite /irr_mode homB // rphi_z. rewrite -{1}scalemx1 -scalemxAr -scalemxAl -{1}(repr_mx1 (rphi i)). by rewrite -homB // repr_mx1 scalemx1 mxE. have inj_iphi: injective iphi. move=> i1 i2 eqi12; apply/eqP. move/eqP: (congr1 (fun i => irr_mode i (z ^+ 1)) eqi12). rewrite /irr_mode !{1}[irr_repr _ _]phi_ze !{1}mxE !mul1n. by rewrite (eq_prim_root_expr (prim_w 1 p_gt1)) !modIp'. have deg_phi i: irr_degree (iphi i) = irr_degree i0. by case: (rsim_irr_comp sS F'S (rphi_irr i)). have im_iphi: codom iphi =i ~: linS. apply/subset_cardP; last apply/subsetP=> _ /codomP[i ->]. by rewrite card_image // card_ord cardsCs setCK nb_irr nb_lin addKn. by rewrite !inE /= (deg_phi i) in nlin_i0 *. split=> //; exists iphi; rewrite -/phi_. split=> // [i | ze | i]. - have sim_i := rsim_irr_comp sS F'S (rphi_irr i). by rewrite -(mx_rsim_faithful sim_i) rphi_fful. - rewrite {1}defZ 2!inE andbC; case/andP. case/cyclePmin=> e; rewrite ozp => lt_e_p ->{ze}. case: (posnP e) => [-> | e_gt0 _]; first by rewrite eqxx. exists (w ^+ e) => [|i]; first by rewrite prim_w ?e_gt0. by rewrite phi_ze exprM. rewrite deg_phi {i}; set d := irr_degree i0. apply/eqP; move/eqP: (sum_irr_degree sS F'S splitF). rewrite (bigID [in linS]) /= -/irr_degree. rewrite (eq_bigr (fun=> 1)) => [|i]; last by rewrite !inE; move/eqP->. rewrite sum1_card nb_lin. rewrite (eq_bigl [in codom iphi]) // => [|i]; last first. by rewrite -in_setC -im_iphi. rewrite (eq_bigr (fun=> d ^ 2))%N => [|_ /codomP[i ->]]; last first. by rewrite deg_phi. rewrite sum_nat_const card_image // card_ord oSpn (expnS p) -{3}[p]prednK //. rewrite mulSn eqn_add2l eqn_pmul2l; last by rewrite -ltnS prednK. by rewrite -muln2 expnM eqn_sqr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)