proposition: Lemma rfix_pgroup_char G H n (rG : mx_representation F G n) : n > 0 -> p.-group H -> H \subset G -> rfix_mx rG H != 0.
proof: Proof. move=> n_gt0 pH sHG; rewrite -(rfix_subg rG sHG). move: {2}_.+1 (ltnSn (n + #|H|)) {rG G sHG}(subg_repr _ _) => m. elim: m gT H pH => // m IHm gT' G pG in n n_gt0 *; rewrite ltnS => le_nG_m rG. apply/eqP=> Gregular; have irrG: mx_irreducible rG. apply/mx_irrP; split=> // U modU; rewrite -mxrank_eq0 -lt0n => Unz. rewrite /row_full eqn_leq rank_leq_col leqNgt; apply/negP=> ltUn. have: rfix_mx (submod_repr modU) G != 0. by apply: IHm => //; apply: leq_trans le_nG_m; rewrite ltn_add2r. by rewrite -mxrank_eq0 (rfix_submod modU) // Gregular capmx0 linear0 mxrank0. have{m le_nG_m IHm} faithfulG: mx_faithful rG. apply/trivgP/eqP/idPn; set C := _ rG => ntC. suffices: rfix_mx (kquo_repr rG) (G / _)%g != 0. by rewrite -mxrank_eq0 rfix_quo // Gregular mxrank0. apply: (IHm _ _ (morphim_pgroup _ _)) => //. by apply: leq_trans le_nG_m; rewrite ltn_add2l ltn_quotient // rstab_sub. have{Gregular} ntG: G :!=: 1%g. apply: contraL n_gt0; move/eqP=> G1; rewrite -leqNgt -(mxrank1 F n). rewrite -(mxrank0 F n n) -Gregular mxrankS //; apply/rfix_mxP=> x. by rewrite {1}G1 mul1mx => /set1P->; rewrite repr_mx1. have p_pr: prime p by case/andP: charFp. have{ntG pG} [z]: {z | z \in 'Z(G) & #[z] = p}; last case/setIP=> Gz cGz ozp. apply: Cauchy => //; apply: contraR ntG; rewrite -p'natE // => p'Z. have pZ: p.-group 'Z(G) by rewrite (pgroupS (center_sub G)). by rewrite (trivg_center_pgroup pG (card1_trivg (pnat_1 pZ p'Z))). have{cGz} cGz1: centgmx rG (rG z - 1%:M). apply/centgmxP=> x Gx; rewrite mulmxBl mulmxBr mulmx1 mul1mx. by rewrite -!repr_mxM // (centP cGz). have{irrG faithfulG cGz1} Urz1: rG z - 1%:M \in unitmx. apply: (mx_Schur irrG) cGz1 _; rewrite subr_eq0. move/implyP: (subsetP faithfulG z). by rewrite !inE Gz mul1mx -order_eq1 ozp -implybNN neq_ltn orbC prime_gt1. do [case: n n_gt0 => // n' _; set n := n'.+1] in rG Urz1 *. have charMp: p \in [char 'M[F]_n]. exact: (rmorph_char (@scalar_mx F n)). have{Urz1}: Frobenius_aut charMp (rG z - 1) \in GRing.unit by rewrite unitrX. rewrite (Frobenius_autB_comm _ (commr1 _)) Frobenius_aut1. by rewrite -[_ (rG z)](repr_mxX rG) // -ozp expg_order repr_mx1 subrr unitr0. 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)