proposition: Lemma faithful_repr_extraspecial : \rank U = (p ^ n)%N /\ (forall V, mxsimple rS V -> mx_iso rZ U V -> mx_iso rS U V).
proof: Proof. suffices IH V: mxsimple rS V -> mx_iso rZ U V -> [&& \rank U == (p ^ n)%N & mxsimple_iso rS U V]. - split=> [|/= V simV isoUV]. by case/andP: (IH U simU (mx_iso_refl _ _)) => /eqP. by case/andP: (IH V simV isoUV) => _ /(mxsimple_isoP simU). move=> simV isoUV; wlog sS: / irrType F S by apply: socle_exists. have [[_ defS'] prZ] := esS. have{prZ} ntZ: 'Z(S) :!=: 1%g by case: eqP prZ => // ->; rewrite cards1. have [_ [iphi]] := extraspecial_repr_structure sS. set phi := fun i => _ => [] [inj_phi im_phi _ phiZ dim_phi] _. have [modU nzU _]:= simU; pose rU := submod_repr modU. have nlinU: \rank U != 1. apply/eqP=> /(rker_linear rU); apply/negP; rewrite /rker rstab_submod. by rewrite (eqmx_rstab _ (val_submod1 _)) (eqP ffulU) defS' subG1. have irrU: mx_irreducible rU by apply/submod_mx_irr. have rsimU := rsim_irr_comp sS F'S irrU. set iU := irr_comp sS rU in rsimU; have [_ degU _ _]:= rsimU. have phiUP: iU \in codom iphi by rewrite im_phi !inE -degU. rewrite degU -(f_iinv phiUP) dim_phi eqxx /=; apply/(mxsimple_isoP simU). have [modV _ _]:= simV; pose rV := submod_repr modV. have irrV: mx_irreducible rV by apply/submod_mx_irr. have rsimV := rsim_irr_comp sS F'S irrV. set iV := irr_comp sS rV in rsimV; have [_ degV _ _]:= rsimV. have phiVP: iV \in codom iphi by rewrite im_phi !inE -degV -(mxrank_iso isoUV). pose jU := iinv phiUP; pose jV := iinv phiVP. have [z Zz ntz]:= trivgPn _ ntZ. have [|w prim_w phi_z] := phiZ z; first by rewrite 2!inE ntz. suffices eqjUV: jU == jV. apply/(mx_rsim_iso modU modV); apply: mx_rsim_trans rsimU _. by rewrite -(f_iinv phiUP) -/jU (eqP eqjUV) f_iinv; apply: mx_rsim_sym. have rsimUV: mx_rsim (subg_repr (phi jU) sZS) (subg_repr (phi jV) sZS). have [bU _ bUfree bUhom] := mx_rsim_sym rsimU. have [bV _ bVfree bVhom] := rsimV. have modUZ := mxmodule_subg sZS modU; have modVZ := mxmodule_subg sZS modV. case/(mx_rsim_iso modUZ modVZ): isoUV => [bZ degZ bZfree bZhom]. rewrite /phi !f_iinv; exists (bU *m bZ *m bV)=> [||x Zx]. - by rewrite -degU degZ degV. - by rewrite /row_free !mxrankMfree. have Sx := subsetP sZS x Zx. by rewrite 2!mulmxA bUhom // -(mulmxA _ _ bZ) bZhom // -4!mulmxA bVhom. have{rsimUV} [B [B' _ homB]] := mx_rsim_def rsimUV. have:= eqxx (irr_mode (iphi jU) z); rewrite /irr_mode; set i0 := Ordinal _. rewrite {2}[_ z]homB // ![_ z]phi_z mxE mulr1n -scalemx1 -scalemxAr -scalemxAl. rewrite -(repr_mx1 (subg_repr (phi jV) sZS)) -{B B'}homB // repr_mx1 scalemx1. by rewrite mxE (eq_prim_root_expr prim_w) !modIp'. 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)