Library mathcomp.character.mxabelem
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file completes the theory developed in mxrepresentation.v with the
+ construction and properties of linear representations over finite fields,
+ and in particular the correspondance between internal action on a (normal)
+ elementary abelian p-subgroup and a linear representation on an Fp-module.
+ We provide the following next constructions for a finite field F:
+ 'Zm%act == the action of {unit F} on 'M[F](m, n).
+ rowg A == the additive group of 'rV[F]_n spanned by the row space
+ of the matrix A.
+ rowg_mx L == the partial inverse to rowg; for any 'Zm-stable group L
+ of 'rV[F]_n we have rowg (rowg_mx L) = L.
+ GLrepr F n == the natural, faithful representation of 'GL_n[F].
+ reprGLm rG == the morphism G >-> 'GL_n[F] equivalent to the
+ representation r of G (with rG : mx_repr r G).
+ ('MR rG)%act == the action of G on 'rV[F]_n equivalent to the
+ representation r of G (with rG : mx_repr r G).
+ The second set of constructions defines the interpretation of a normal
+ non-trivial elementary abelian p-subgroup as an 'F_p module. We assume
+ abelE : p.-abelem E and ntE : E != 1, throughout, as these are needed to
+ build the isomorphism between E and a nontrivial 'rV['F_p]_n.
+ 'rV(E) == the type of row vectors of the 'F_p module equivalent
+ to E when E is a non-trivial p.-abelem group.
+ 'M(E) == the type of matrices corresponding to E.
+ 'dim E == the width of vectors/matrices in 'rV(E) / 'M(E).
+ abelem_rV abelE ntE == the one-to-one injection of E onto 'rV(E).
+ rVabelem abelE ntE == the one-to-one projection of 'rV(E) onto E.
+ abelem_repr abelE ntE nEG == the representation of G on 'rV(E) that is
+ equivalent to conjugation by G in E; here abelE, ntE are
+ as above, and G \subset 'N(E).
+ This file end with basic results on p-modular representations of p-groups,
+ and theorems giving the structure of the representation of extraspecial
+ groups; these results use somewhat more advanced group theory than the
+ rest of mxrepresentation, in particular, results of sylow.v and maximal.v.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory FinRing.Theory.
+Local Open Scope ring_scope.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory FinRing.Theory.
+Local Open Scope ring_scope.
+ +
+
+ Special results for representations on a finite field. In this case, the
+ representation is equivalent to a morphism into the general linear group
+ 'GL_n[F]. It is furthermore equivalent to a group action on the finite
+ additive group of the corresponding row space 'rV_n. In addition, row
+ spaces of matrices in 'M[F]_n correspond to subgroups of that vector group
+ (this is only surjective when F is a prime field 'F_p), with moduleules
+ corresponding to subgroups stabilized by the external action.
+
+
+
+
+Section FinRingRepr.
+ +
+Variable (R : finComUnitRingType) (gT : finGroupType).
+Variables (G : {group gT}) (n : nat) (rG : mx_representation R G n).
+ +
+Definition mx_repr_act (u : 'rV_n) x := u ×m rG (val (subg G x)).
+ +
+Lemma mx_repr_actE u x : x \in G → mx_repr_act u x = u ×m rG x.
+ +
+Fact mx_repr_is_action : is_action G mx_repr_act.
+Canonical Structure mx_repr_action := Action mx_repr_is_action.
+ +
+Fact mx_repr_is_groupAction : is_groupAction [set: 'rV[R]_n] mx_repr_action.
+Canonical Structure mx_repr_groupAction := GroupAction mx_repr_is_groupAction.
+ +
+End FinRingRepr.
+ +
+Notation "''MR' rG" := (mx_repr_action rG)
+ (at level 10, rG at level 8) : action_scope.
+Notation "''MR' rG" := (mx_repr_groupAction rG) : groupAction_scope.
+ +
+Section FinFieldRepr.
+ +
+Variable F : finFieldType.
+ +
+
+
++Section FinRingRepr.
+ +
+Variable (R : finComUnitRingType) (gT : finGroupType).
+Variables (G : {group gT}) (n : nat) (rG : mx_representation R G n).
+ +
+Definition mx_repr_act (u : 'rV_n) x := u ×m rG (val (subg G x)).
+ +
+Lemma mx_repr_actE u x : x \in G → mx_repr_act u x = u ×m rG x.
+ +
+Fact mx_repr_is_action : is_action G mx_repr_act.
+Canonical Structure mx_repr_action := Action mx_repr_is_action.
+ +
+Fact mx_repr_is_groupAction : is_groupAction [set: 'rV[R]_n] mx_repr_action.
+Canonical Structure mx_repr_groupAction := GroupAction mx_repr_is_groupAction.
+ +
+End FinRingRepr.
+ +
+Notation "''MR' rG" := (mx_repr_action rG)
+ (at level 10, rG at level 8) : action_scope.
+Notation "''MR' rG" := (mx_repr_groupAction rG) : groupAction_scope.
+ +
+Section FinFieldRepr.
+ +
+Variable F : finFieldType.
+ +
+
+ The external group action (by scaling) of the multiplicative unit group
+ of the finite field, and the correspondence between additive subgroups
+ of row vectors that are stable by this action, and the matrix row spaces.
+
+
+Section ScaleAction.
+ +
+Variables m n : nat.
+ +
+Definition scale_act (A : 'M[F]_(m, n)) (a : {unit F}) := val a *: A.
+Lemma scale_actE A a : scale_act A a = val a *: A.
+Fact scale_is_action : is_action setT scale_act.
+Canonical scale_action := Action scale_is_action.
+Fact scale_is_groupAction : is_groupAction setT scale_action.
+Canonical scale_groupAction := GroupAction scale_is_groupAction.
+ +
+Lemma astab1_scale_act A : A != 0 → 'C[A | scale_action] = 1%g.
+ +
+End ScaleAction.
+ +
+ +
+Section RowGroup.
+ +
+Variable n : nat.
+ +
+Definition rowg m (A : 'M[F]_(m, n)) : {set rVn} := [set u | u ≤ A]%MS.
+ +
+Lemma mem_rowg m A v : (v \in @rowg m A) = (v ≤ A)%MS.
+ +
+Fact rowg_group_set m A : group_set (@rowg m A).
+Canonical rowg_group m A := Group (@rowg_group_set m A).
+ +
+Lemma rowg_stable m (A : 'M_(m, n)) : [acts setT, on rowg A | 'Zm].
+ +
+Lemma rowgS m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ (rowg A \subset rowg B) = (A ≤ B)%MS.
+ +
+Lemma eq_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ (A :=: B)%MS → rowg A = rowg B.
+ +
+Lemma rowg0 m : rowg (0 : 'M_(m, n)) = 1%g.
+ +
+Lemma rowg1 : rowg 1%:M = setT.
+ +
+Lemma trivg_rowg m (A : 'M_(m, n)) : (rowg A == 1%g) = (A == 0).
+ +
+Definition rowg_mx (L : {set rVn}) := <<\matrix_(i < #|L|) enum_val i>>%MS.
+ +
+Lemma rowgK m (A : 'M_(m, n)) : (rowg_mx (rowg A) :=: A)%MS.
+ +
+Lemma rowg_mxS (L M : {set 'rV[F]_n}) :
+ L \subset M → (rowg_mx L ≤ rowg_mx M)%MS.
+ +
+Lemma sub_rowg_mx (L : {set rVn}) : L \subset rowg (rowg_mx L).
+ +
+Lemma stable_rowg_mxK (L : {group rVn}) :
+ [acts setT, on L | 'Zm] → rowg (rowg_mx L) = L.
+ +
+Lemma rowg_mx1 : rowg_mx 1%g = 0.
+ +
+Lemma rowg_mx_eq0 (L : {group rVn}) : (rowg_mx L == 0) = (L :==: 1%g).
+ +
+Lemma rowgI m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg (A :&: B)%MS = rowg A :&: rowg B.
+ +
+Lemma card_rowg m (A : 'M_(m, n)) : #|rowg A| = (#|F| ^ \rank A)%N.
+ +
+Lemma rowgD m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg (A + B)%MS = (rowg A × rowg B)%g.
+ +
+Lemma cprod_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg A \* rowg B = rowg (A + B)%MS.
+ +
+Lemma dprod_rowg m1 m2 (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)) :
+ mxdirect (A + B) → rowg A \x rowg B = rowg (A + B)%MS.
+ +
+Lemma bigcprod_rowg m I r (P : pred I) (A : I → 'M[F]_n) (B : 'M[F]_(m, n)) :
+ (\sum_(i <- r | P i) A i :=: B)%MS →
+ \big[cprod/1%g]_(i <- r | P i) rowg (A i) = rowg B.
+ +
+Lemma bigdprod_rowg m (I : finType) (P : pred I) A (B : 'M[F]_(m, n)) :
+ let S := (\sum_(i | P i) A i)%MS in (S :=: B)%MS → mxdirect S →
+ \big[dprod/1%g]_(i | P i) rowg (A i) = rowg B.
+ +
+End RowGroup.
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variable (rG : mx_representation F G n).
+ +
+Fact GL_mx_repr : mx_repr 'GL_n[F] GLval.
+Canonical GLrepr := MxRepresentation GL_mx_repr.
+ +
+Lemma GLmx_faithful : mx_faithful GLrepr.
+ +
+Definition reprGLm x : {'GL_n[F]} := insubd (1%g : {'GL_n[F]}) (rG x).
+ +
+Lemma val_reprGLm x : x \in G → val (reprGLm x) = rG x.
+ +
+Lemma comp_reprGLm : {in G, GLval \o reprGLm =1 rG}.
+ +
+Lemma reprGLmM : {in G &, {morph reprGLm : x y / x × y}}%g.
+Canonical reprGL_morphism := Morphism reprGLmM.
+ +
+Lemma ker_reprGLm : 'ker reprGLm = rker rG.
+ +
+Lemma astab_rowg_repr m (A : 'M_(m, n)) : 'C(rowg A | 'MR rG) = rstab rG A.
+ +
+Lemma astabs_rowg_repr m (A : 'M_(m, n)) : 'N(rowg A | 'MR rG) = rstabs rG A.
+ +
+Lemma acts_rowg (A : 'M_n) : [acts G, on rowg A | 'MR rG] = mxmodule rG A.
+ +
+Lemma astab_setT_repr : 'C(setT | 'MR rG) = rker rG.
+ +
+Lemma mx_repr_action_faithful :
+ [faithful G, on setT | 'MR rG] = mx_faithful rG.
+ +
+Lemma afix_repr (H : {set gT}) :
+ H \subset G → 'Fix_('MR rG)(H) = rowg (rfix_mx rG H).
+ +
+Lemma gacent_repr (H : {set gT}) :
+ H \subset G → 'C_(| 'MR rG)(H) = rowg (rfix_mx rG H).
+ +
+End FinFieldRepr.
+ +
+Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope.
+Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.
+ +
+Section MatrixGroups.
+ +
+Implicit Types m n p q : nat.
+ +
+Lemma exponent_mx_group m n q :
+ m > 0 → n > 0 → q > 1 → exponent [set: 'M['Z_q]_(m, n)] = q.
+ +
+Lemma rank_mx_group m n q : 'r([set: 'M['Z_q]_(m, n)]) = (m × n)%N.
+ +
+Lemma mx_group_homocyclic m n q : homocyclic [set: 'M['Z_q]_(m, n)].
+ +
+Lemma abelian_type_mx_group m n q :
+ q > 1 → abelian_type [set: 'M['Z_q]_(m, n)] = nseq (m × n) q.
+ +
+End MatrixGroups.
+ +
+Delimit Scope abelem_scope with Mg.
+Open Scope abelem_scope.
+ +
+Definition abelem_dim' (gT : finGroupType) (E : {set gT}) :=
+ (logn (pdiv #|E|) #|E|).-1.
+Notation "''dim' E" := (abelem_dim' E).+1
+ (at level 10, E at level 8, format "''dim' E") : abelem_scope.
+ +
+Notation "''rV' ( E )" := 'rV_('dim E)
+ (at level 8, format "''rV' ( E )") : abelem_scope.
+Notation "''M' ( E )" := 'M_('dim E)
+ (at level 8, format "''M' ( E )") : abelem_scope.
+Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
+ (at level 8, only parsing) : abelem_scope.
+Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
+ (at level 8, only parsing) : abelem_scope.
+ +
+Section AbelemRepr.
+ +
+Section FpMatrix.
+ +
+Variables p m n : nat.
+ +
+Lemma mx_Fp_abelem : prime p → p.-abelem [set: Mmn].
+ +
+Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].
+ +
+End FpMatrix.
+ +
+Section FpRow.
+ +
+Variables p n : nat.
+ +
+Lemma rowg_mxK (L : {group rVn}) : rowg (rowg_mx L) = L.
+ +
+Lemma rowg_mxSK (L : {set rVn}) (M : {group rVn}) :
+ (rowg_mx L ≤ rowg_mx M)%MS = (L \subset M).
+ +
+Lemma mxrank_rowg (L : {group rVn}) :
+ prime p → \rank (rowg_mx L) = logn p #|L|.
+ +
+End FpRow.
+ +
+Variables (p : nat) (gT : finGroupType) (E : {group gT}).
+Hypotheses (abelE : p.-abelem E) (ntE : E :!=: 1%g).
+ +
+Let pE : p.-group E := abelem_pgroup abelE.
+Let p_pr : prime p.
+ +
+ +
+Lemma dim_abelemE : n = logn p #|E|.
+ +
+Lemma card_abelem_rV : #|rVn| = #|E|.
+ +
+Lemma isog_abelem_rV : E \isog [set: rVn].
+ +
+Definition abelem_rV : gT → rVn := xchoose ab_rV_P.
+ +
+ +
+Lemma abelem_rV_M : {in E &, {morph ErV : x y / (x × y)%g >-> x + y}}.
+ +
+Canonical abelem_rV_morphism := Morphism abelem_rV_M.
+ +
+Lemma abelem_rV_isom : isom E setT ErV.
+ +
+Lemma abelem_rV_injm : 'injm ErV.
+ +
+Lemma abelem_rV_inj : {in E &, injective ErV}.
+ +
+Lemma im_abelem_rV : ErV @* E = setT.
+ +
+Lemma mem_im_abelem_rV u : u \in ErV @* E.
+ +
+Lemma sub_im_abelem_rV mA : subset mA (mem (ErV @* E)).
+ Hint Resolve mem_im_abelem_rV sub_im_abelem_rV.
+ +
+Lemma abelem_rV_1 : ErV 1 = 0%R.
+ +
+Lemma abelem_rV_X x i : x \in E → ErV (x ^+ i) = i%:R *: ErV x.
+ +
+Lemma abelem_rV_V x : x \in E → ErV x^-1 = - ErV x.
+ +
+Definition rVabelem : rVn → gT := invm abelem_rV_injm.
+Canonical rVabelem_morphism := [morphism of rVabelem].
+ +
+Lemma rVabelem0 : rV_E 0 = 1%g.
+ +
+Lemma rVabelemD : {morph rV_E : u v / u + v >-> (u × v)%g}.
+ +
+Lemma rVabelemN : {morph rV_E: u / - u >-> (u^-1)%g}.
+ +
+Lemma rVabelemZ (m : 'F_p) : {morph rV_E : u / m *: u >-> (u ^+ m)%g}.
+ +
+Lemma abelem_rV_K : {in E, cancel ErV rV_E}.
+ +
+Lemma rVabelemK : cancel rV_E ErV.
+ +
+Lemma rVabelem_inj : injective rV_E.
+ +
+Lemma rVabelem_injm : 'injm rV_E.
+ +
+Lemma im_rVabelem : rV_E @* setT = E.
+ +
+Lemma mem_rVabelem u : rV_E u \in E.
+ +
+Lemma sub_rVabelem L : rV_E @* L \subset E.
+ Hint Resolve mem_rVabelem sub_rVabelem.
+ +
+Lemma card_rVabelem L : #|rV_E @* L| = #|L|.
+ +
+Lemma abelem_rV_mK (H : {set gT}) : H \subset E → rV_E @* (ErV @* H) = H.
+ +
+Lemma rVabelem_mK L : ErV @* (rV_E @* L) = L.
+ +
+Lemma rVabelem_minj : injective (morphim (MorPhantom rV_E)).
+ +
+Lemma rVabelemS L M : (rV_E @* L \subset rV_E @* M) = (L \subset M).
+ +
+Lemma abelem_rV_S (H K : {set gT}) :
+ H \subset E → (ErV @* H \subset ErV @* K) = (H \subset K).
+ +
+Lemma sub_rVabelem_im L (H : {set gT}) :
+ (rV_E @* L \subset H) = (L \subset ErV @* H).
+ +
+Lemma sub_abelem_rV_im (H : {set gT}) (L : {set 'rV['F_p]_n}) :
+ H \subset E → (ErV @* H \subset L) = (H \subset rV_E @* L).
+ +
+Section OneGroup.
+ +
+Variable G : {group gT}.
+Definition abelem_mx_fun (g : subg_of G) v := ErV ((rV_E v) ^ val g).
+Definition abelem_mx of G \subset 'N(E) :=
+ fun x ⇒ lin1_mx (abelem_mx_fun (subg G x)).
+ +
+Hypothesis nEG : G \subset 'N(E).
+ +
+Fact abelem_mx_linear_proof g : linear (abelem_mx_fun g).
+Canonical abelem_mx_linear g := Linear (abelem_mx_linear_proof g).
+ +
+Let rVabelemJmx v x : x \in G → rV_E (v ×m r x) = (rV_E v) ^ x.
+ +
+Fact abelem_mx_repr : mx_repr G r.
+Canonical abelem_repr := MxRepresentation abelem_mx_repr.
+Let rG := abelem_repr.
+ +
+Lemma rVabelemJ v x : x \in G → rV_E (v ×m rG x) = (rV_E v) ^ x.
+ +
+Lemma abelem_rV_J : {in E & G, ∀ x y, ErV (x ^ y) = ErV x ×m rG y}.
+ +
+Lemma abelem_rowgJ m (A : 'M_(m, n)) x :
+ x \in G → rV_E @* rowg (A ×m rG x) = (rV_E @* rowg A) :^ x.
+ +
+Lemma rV_abelem_sJ (L : {group gT}) x :
+ x \in G → L \subset E → ErV @* (L :^ x) = rowg (rowg_mx (ErV @* L) ×m rG x).
+ +
+Lemma rstab_abelem m (A : 'M_(m, n)) : rstab rG A = 'C_G(rV_E @* rowg A).
+ +
+Lemma rstabs_abelem m (A : 'M_(m, n)) : rstabs rG A = 'N_G(rV_E @* rowg A).
+ +
+Lemma rstabs_abelemG (L : {group gT}) :
+ L \subset E → rstabs rG (rowg_mx (ErV @* L)) = 'N_G(L).
+ +
+Lemma mxmodule_abelem m (U : 'M['F_p]_(m, n)) :
+ mxmodule rG U = (G \subset 'N(rV_E @* rowg U)).
+ +
+Lemma mxmodule_abelemG (L : {group gT}) :
+ L \subset E → mxmodule rG (rowg_mx (ErV @* L)) = (G \subset 'N(L)).
+ +
+Lemma mxsimple_abelemP (U : 'M['F_p]_n) :
+ reflect (mxsimple rG U) (minnormal (rV_E @* rowg U) G).
+ +
+Lemma mxsimple_abelemGP (L : {group gT}) :
+ L \subset E → reflect (mxsimple rG (rowg_mx (ErV @* L))) (minnormal L G).
+ +
+Lemma abelem_mx_irrP : reflect (mx_irreducible rG) (minnormal E G).
+ +
+Lemma rfix_abelem (H : {set gT}) :
+ H \subset G → (rfix_mx rG H :=: rowg_mx (ErV @* 'C_E(H)%g))%MS.
+ +
+Lemma rker_abelem : rker rG = 'C_G(E).
+ +
+Lemma abelem_mx_faithful : 'C_G(E) = 1%g → mx_faithful rG.
+ +
+End OneGroup.
+ +
+Section SubGroup.
+ +
+Variables G H : {group gT}.
+Hypotheses (nEG : G \subset 'N(E)) (sHG : H \subset G).
+Let nEH := subset_trans sHG nEG.
+ +
+Lemma eq_abelem_subg_repr : {in H, rHG =1 rH}.
+ +
+Lemma rsim_abelem_subg : mx_rsim rHG rH.
+ +
+Lemma mxmodule_abelem_subg m (U : 'M_(m, n)) : mxmodule rHG U = mxmodule rH U.
+ +
+Lemma mxsimple_abelem_subg U : mxsimple rHG U ↔ mxsimple rH U.
+ +
+End SubGroup.
+ +
+End AbelemRepr.
+ +
+Section ModularRepresentation.
+ +
+Variables (F : fieldType) (p : nat) (gT : finGroupType).
+Hypothesis charFp : p \in [char F].
+Implicit Types G H : {group gT}.
+ +
+
+
++ +
+Variables m n : nat.
+ +
+Definition scale_act (A : 'M[F]_(m, n)) (a : {unit F}) := val a *: A.
+Lemma scale_actE A a : scale_act A a = val a *: A.
+Fact scale_is_action : is_action setT scale_act.
+Canonical scale_action := Action scale_is_action.
+Fact scale_is_groupAction : is_groupAction setT scale_action.
+Canonical scale_groupAction := GroupAction scale_is_groupAction.
+ +
+Lemma astab1_scale_act A : A != 0 → 'C[A | scale_action] = 1%g.
+ +
+End ScaleAction.
+ +
+ +
+Section RowGroup.
+ +
+Variable n : nat.
+ +
+Definition rowg m (A : 'M[F]_(m, n)) : {set rVn} := [set u | u ≤ A]%MS.
+ +
+Lemma mem_rowg m A v : (v \in @rowg m A) = (v ≤ A)%MS.
+ +
+Fact rowg_group_set m A : group_set (@rowg m A).
+Canonical rowg_group m A := Group (@rowg_group_set m A).
+ +
+Lemma rowg_stable m (A : 'M_(m, n)) : [acts setT, on rowg A | 'Zm].
+ +
+Lemma rowgS m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ (rowg A \subset rowg B) = (A ≤ B)%MS.
+ +
+Lemma eq_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ (A :=: B)%MS → rowg A = rowg B.
+ +
+Lemma rowg0 m : rowg (0 : 'M_(m, n)) = 1%g.
+ +
+Lemma rowg1 : rowg 1%:M = setT.
+ +
+Lemma trivg_rowg m (A : 'M_(m, n)) : (rowg A == 1%g) = (A == 0).
+ +
+Definition rowg_mx (L : {set rVn}) := <<\matrix_(i < #|L|) enum_val i>>%MS.
+ +
+Lemma rowgK m (A : 'M_(m, n)) : (rowg_mx (rowg A) :=: A)%MS.
+ +
+Lemma rowg_mxS (L M : {set 'rV[F]_n}) :
+ L \subset M → (rowg_mx L ≤ rowg_mx M)%MS.
+ +
+Lemma sub_rowg_mx (L : {set rVn}) : L \subset rowg (rowg_mx L).
+ +
+Lemma stable_rowg_mxK (L : {group rVn}) :
+ [acts setT, on L | 'Zm] → rowg (rowg_mx L) = L.
+ +
+Lemma rowg_mx1 : rowg_mx 1%g = 0.
+ +
+Lemma rowg_mx_eq0 (L : {group rVn}) : (rowg_mx L == 0) = (L :==: 1%g).
+ +
+Lemma rowgI m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg (A :&: B)%MS = rowg A :&: rowg B.
+ +
+Lemma card_rowg m (A : 'M_(m, n)) : #|rowg A| = (#|F| ^ \rank A)%N.
+ +
+Lemma rowgD m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg (A + B)%MS = (rowg A × rowg B)%g.
+ +
+Lemma cprod_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+ rowg A \* rowg B = rowg (A + B)%MS.
+ +
+Lemma dprod_rowg m1 m2 (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)) :
+ mxdirect (A + B) → rowg A \x rowg B = rowg (A + B)%MS.
+ +
+Lemma bigcprod_rowg m I r (P : pred I) (A : I → 'M[F]_n) (B : 'M[F]_(m, n)) :
+ (\sum_(i <- r | P i) A i :=: B)%MS →
+ \big[cprod/1%g]_(i <- r | P i) rowg (A i) = rowg B.
+ +
+Lemma bigdprod_rowg m (I : finType) (P : pred I) A (B : 'M[F]_(m, n)) :
+ let S := (\sum_(i | P i) A i)%MS in (S :=: B)%MS → mxdirect S →
+ \big[dprod/1%g]_(i | P i) rowg (A i) = rowg B.
+ +
+End RowGroup.
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
+Variable (rG : mx_representation F G n).
+ +
+Fact GL_mx_repr : mx_repr 'GL_n[F] GLval.
+Canonical GLrepr := MxRepresentation GL_mx_repr.
+ +
+Lemma GLmx_faithful : mx_faithful GLrepr.
+ +
+Definition reprGLm x : {'GL_n[F]} := insubd (1%g : {'GL_n[F]}) (rG x).
+ +
+Lemma val_reprGLm x : x \in G → val (reprGLm x) = rG x.
+ +
+Lemma comp_reprGLm : {in G, GLval \o reprGLm =1 rG}.
+ +
+Lemma reprGLmM : {in G &, {morph reprGLm : x y / x × y}}%g.
+Canonical reprGL_morphism := Morphism reprGLmM.
+ +
+Lemma ker_reprGLm : 'ker reprGLm = rker rG.
+ +
+Lemma astab_rowg_repr m (A : 'M_(m, n)) : 'C(rowg A | 'MR rG) = rstab rG A.
+ +
+Lemma astabs_rowg_repr m (A : 'M_(m, n)) : 'N(rowg A | 'MR rG) = rstabs rG A.
+ +
+Lemma acts_rowg (A : 'M_n) : [acts G, on rowg A | 'MR rG] = mxmodule rG A.
+ +
+Lemma astab_setT_repr : 'C(setT | 'MR rG) = rker rG.
+ +
+Lemma mx_repr_action_faithful :
+ [faithful G, on setT | 'MR rG] = mx_faithful rG.
+ +
+Lemma afix_repr (H : {set gT}) :
+ H \subset G → 'Fix_('MR rG)(H) = rowg (rfix_mx rG H).
+ +
+Lemma gacent_repr (H : {set gT}) :
+ H \subset G → 'C_(| 'MR rG)(H) = rowg (rfix_mx rG H).
+ +
+End FinFieldRepr.
+ +
+Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope.
+Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.
+ +
+Section MatrixGroups.
+ +
+Implicit Types m n p q : nat.
+ +
+Lemma exponent_mx_group m n q :
+ m > 0 → n > 0 → q > 1 → exponent [set: 'M['Z_q]_(m, n)] = q.
+ +
+Lemma rank_mx_group m n q : 'r([set: 'M['Z_q]_(m, n)]) = (m × n)%N.
+ +
+Lemma mx_group_homocyclic m n q : homocyclic [set: 'M['Z_q]_(m, n)].
+ +
+Lemma abelian_type_mx_group m n q :
+ q > 1 → abelian_type [set: 'M['Z_q]_(m, n)] = nseq (m × n) q.
+ +
+End MatrixGroups.
+ +
+Delimit Scope abelem_scope with Mg.
+Open Scope abelem_scope.
+ +
+Definition abelem_dim' (gT : finGroupType) (E : {set gT}) :=
+ (logn (pdiv #|E|) #|E|).-1.
+Notation "''dim' E" := (abelem_dim' E).+1
+ (at level 10, E at level 8, format "''dim' E") : abelem_scope.
+ +
+Notation "''rV' ( E )" := 'rV_('dim E)
+ (at level 8, format "''rV' ( E )") : abelem_scope.
+Notation "''M' ( E )" := 'M_('dim E)
+ (at level 8, format "''M' ( E )") : abelem_scope.
+Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
+ (at level 8, only parsing) : abelem_scope.
+Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
+ (at level 8, only parsing) : abelem_scope.
+ +
+Section AbelemRepr.
+ +
+Section FpMatrix.
+ +
+Variables p m n : nat.
+ +
+Lemma mx_Fp_abelem : prime p → p.-abelem [set: Mmn].
+ +
+Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].
+ +
+End FpMatrix.
+ +
+Section FpRow.
+ +
+Variables p n : nat.
+ +
+Lemma rowg_mxK (L : {group rVn}) : rowg (rowg_mx L) = L.
+ +
+Lemma rowg_mxSK (L : {set rVn}) (M : {group rVn}) :
+ (rowg_mx L ≤ rowg_mx M)%MS = (L \subset M).
+ +
+Lemma mxrank_rowg (L : {group rVn}) :
+ prime p → \rank (rowg_mx L) = logn p #|L|.
+ +
+End FpRow.
+ +
+Variables (p : nat) (gT : finGroupType) (E : {group gT}).
+Hypotheses (abelE : p.-abelem E) (ntE : E :!=: 1%g).
+ +
+Let pE : p.-group E := abelem_pgroup abelE.
+Let p_pr : prime p.
+ +
+ +
+Lemma dim_abelemE : n = logn p #|E|.
+ +
+Lemma card_abelem_rV : #|rVn| = #|E|.
+ +
+Lemma isog_abelem_rV : E \isog [set: rVn].
+ +
+Definition abelem_rV : gT → rVn := xchoose ab_rV_P.
+ +
+ +
+Lemma abelem_rV_M : {in E &, {morph ErV : x y / (x × y)%g >-> x + y}}.
+ +
+Canonical abelem_rV_morphism := Morphism abelem_rV_M.
+ +
+Lemma abelem_rV_isom : isom E setT ErV.
+ +
+Lemma abelem_rV_injm : 'injm ErV.
+ +
+Lemma abelem_rV_inj : {in E &, injective ErV}.
+ +
+Lemma im_abelem_rV : ErV @* E = setT.
+ +
+Lemma mem_im_abelem_rV u : u \in ErV @* E.
+ +
+Lemma sub_im_abelem_rV mA : subset mA (mem (ErV @* E)).
+ Hint Resolve mem_im_abelem_rV sub_im_abelem_rV.
+ +
+Lemma abelem_rV_1 : ErV 1 = 0%R.
+ +
+Lemma abelem_rV_X x i : x \in E → ErV (x ^+ i) = i%:R *: ErV x.
+ +
+Lemma abelem_rV_V x : x \in E → ErV x^-1 = - ErV x.
+ +
+Definition rVabelem : rVn → gT := invm abelem_rV_injm.
+Canonical rVabelem_morphism := [morphism of rVabelem].
+ +
+Lemma rVabelem0 : rV_E 0 = 1%g.
+ +
+Lemma rVabelemD : {morph rV_E : u v / u + v >-> (u × v)%g}.
+ +
+Lemma rVabelemN : {morph rV_E: u / - u >-> (u^-1)%g}.
+ +
+Lemma rVabelemZ (m : 'F_p) : {morph rV_E : u / m *: u >-> (u ^+ m)%g}.
+ +
+Lemma abelem_rV_K : {in E, cancel ErV rV_E}.
+ +
+Lemma rVabelemK : cancel rV_E ErV.
+ +
+Lemma rVabelem_inj : injective rV_E.
+ +
+Lemma rVabelem_injm : 'injm rV_E.
+ +
+Lemma im_rVabelem : rV_E @* setT = E.
+ +
+Lemma mem_rVabelem u : rV_E u \in E.
+ +
+Lemma sub_rVabelem L : rV_E @* L \subset E.
+ Hint Resolve mem_rVabelem sub_rVabelem.
+ +
+Lemma card_rVabelem L : #|rV_E @* L| = #|L|.
+ +
+Lemma abelem_rV_mK (H : {set gT}) : H \subset E → rV_E @* (ErV @* H) = H.
+ +
+Lemma rVabelem_mK L : ErV @* (rV_E @* L) = L.
+ +
+Lemma rVabelem_minj : injective (morphim (MorPhantom rV_E)).
+ +
+Lemma rVabelemS L M : (rV_E @* L \subset rV_E @* M) = (L \subset M).
+ +
+Lemma abelem_rV_S (H K : {set gT}) :
+ H \subset E → (ErV @* H \subset ErV @* K) = (H \subset K).
+ +
+Lemma sub_rVabelem_im L (H : {set gT}) :
+ (rV_E @* L \subset H) = (L \subset ErV @* H).
+ +
+Lemma sub_abelem_rV_im (H : {set gT}) (L : {set 'rV['F_p]_n}) :
+ H \subset E → (ErV @* H \subset L) = (H \subset rV_E @* L).
+ +
+Section OneGroup.
+ +
+Variable G : {group gT}.
+Definition abelem_mx_fun (g : subg_of G) v := ErV ((rV_E v) ^ val g).
+Definition abelem_mx of G \subset 'N(E) :=
+ fun x ⇒ lin1_mx (abelem_mx_fun (subg G x)).
+ +
+Hypothesis nEG : G \subset 'N(E).
+ +
+Fact abelem_mx_linear_proof g : linear (abelem_mx_fun g).
+Canonical abelem_mx_linear g := Linear (abelem_mx_linear_proof g).
+ +
+Let rVabelemJmx v x : x \in G → rV_E (v ×m r x) = (rV_E v) ^ x.
+ +
+Fact abelem_mx_repr : mx_repr G r.
+Canonical abelem_repr := MxRepresentation abelem_mx_repr.
+Let rG := abelem_repr.
+ +
+Lemma rVabelemJ v x : x \in G → rV_E (v ×m rG x) = (rV_E v) ^ x.
+ +
+Lemma abelem_rV_J : {in E & G, ∀ x y, ErV (x ^ y) = ErV x ×m rG y}.
+ +
+Lemma abelem_rowgJ m (A : 'M_(m, n)) x :
+ x \in G → rV_E @* rowg (A ×m rG x) = (rV_E @* rowg A) :^ x.
+ +
+Lemma rV_abelem_sJ (L : {group gT}) x :
+ x \in G → L \subset E → ErV @* (L :^ x) = rowg (rowg_mx (ErV @* L) ×m rG x).
+ +
+Lemma rstab_abelem m (A : 'M_(m, n)) : rstab rG A = 'C_G(rV_E @* rowg A).
+ +
+Lemma rstabs_abelem m (A : 'M_(m, n)) : rstabs rG A = 'N_G(rV_E @* rowg A).
+ +
+Lemma rstabs_abelemG (L : {group gT}) :
+ L \subset E → rstabs rG (rowg_mx (ErV @* L)) = 'N_G(L).
+ +
+Lemma mxmodule_abelem m (U : 'M['F_p]_(m, n)) :
+ mxmodule rG U = (G \subset 'N(rV_E @* rowg U)).
+ +
+Lemma mxmodule_abelemG (L : {group gT}) :
+ L \subset E → mxmodule rG (rowg_mx (ErV @* L)) = (G \subset 'N(L)).
+ +
+Lemma mxsimple_abelemP (U : 'M['F_p]_n) :
+ reflect (mxsimple rG U) (minnormal (rV_E @* rowg U) G).
+ +
+Lemma mxsimple_abelemGP (L : {group gT}) :
+ L \subset E → reflect (mxsimple rG (rowg_mx (ErV @* L))) (minnormal L G).
+ +
+Lemma abelem_mx_irrP : reflect (mx_irreducible rG) (minnormal E G).
+ +
+Lemma rfix_abelem (H : {set gT}) :
+ H \subset G → (rfix_mx rG H :=: rowg_mx (ErV @* 'C_E(H)%g))%MS.
+ +
+Lemma rker_abelem : rker rG = 'C_G(E).
+ +
+Lemma abelem_mx_faithful : 'C_G(E) = 1%g → mx_faithful rG.
+ +
+End OneGroup.
+ +
+Section SubGroup.
+ +
+Variables G H : {group gT}.
+Hypotheses (nEG : G \subset 'N(E)) (sHG : H \subset G).
+Let nEH := subset_trans sHG nEG.
+ +
+Lemma eq_abelem_subg_repr : {in H, rHG =1 rH}.
+ +
+Lemma rsim_abelem_subg : mx_rsim rHG rH.
+ +
+Lemma mxmodule_abelem_subg m (U : 'M_(m, n)) : mxmodule rHG U = mxmodule rH U.
+ +
+Lemma mxsimple_abelem_subg U : mxsimple rHG U ↔ mxsimple rH U.
+ +
+End SubGroup.
+ +
+End AbelemRepr.
+ +
+Section ModularRepresentation.
+ +
+Variables (F : fieldType) (p : nat) (gT : finGroupType).
+Hypothesis charFp : p \in [char F].
+Implicit Types G H : {group gT}.
+ +
+
+ This is Gorenstein, Lemma 2.6.3.
+
+
+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.
+ +
+Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
+ +
+Lemma pcore_sub_rstab_mxsimple M : mxsimple rG M → 'O_p(G) \subset rstab rG M.
+ +
+Lemma pcore_sub_rker_mx_irr : mx_irreducible rG → 'O_p(G) \subset rker rG.
+ +
+
+
++ n > 0 → p.-group H → H \subset G → rfix_mx rG H != 0.
+ +
+Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).
+ +
+Lemma pcore_sub_rstab_mxsimple M : mxsimple rG M → 'O_p(G) \subset rstab rG M.
+ +
+Lemma pcore_sub_rker_mx_irr : mx_irreducible rG → 'O_p(G) \subset rker rG.
+ +
+
+ This is Gorenstein, Lemma 3.1.3.
+
+
+Lemma pcore_faithful_mx_irr :
+ mx_irreducible rG → mx_faithful rG → 'O_p(G) = 1%g.
+ +
+End ModularRepresentation.
+ +
+Section Extraspecial.
+ +
+Variables (F : fieldType) (gT : finGroupType) (S : {group gT}) (p n : nat).
+Hypotheses (pS : p.-group S) (esS : extraspecial S).
+Hypothesis oSpn : #|S| = (p ^ n.*2.+1)%N.
+Hypotheses (splitF : group_splitting_field F S) (F'S : [char F]^'.-group S).
+ +
+Let p_pr := extraspecial_prime pS esS.
+Let p_gt0 := prime_gt0 p_pr.
+Let p_gt1 := prime_gt1 p_pr.
+Let oZp := card_center_extraspecial pS esS.
+ +
+Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N.
+ +
+
+
++ mx_irreducible rG → mx_faithful rG → 'O_p(G) = 1%g.
+ +
+End ModularRepresentation.
+ +
+Section Extraspecial.
+ +
+Variables (F : fieldType) (gT : finGroupType) (S : {group gT}) (p n : nat).
+Hypotheses (pS : p.-group S) (esS : extraspecial S).
+Hypothesis oSpn : #|S| = (p ^ n.*2.+1)%N.
+Hypotheses (splitF : group_splitting_field F S) (F'S : [char F]^'.-group S).
+ +
+Let p_pr := extraspecial_prime pS esS.
+Let p_gt0 := prime_gt0 p_pr.
+Let p_gt1 := prime_gt1 p_pr.
+Let oZp := card_center_extraspecial pS esS.
+ +
+Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N.
+ +
+
+ This is Aschbacher (34.9), parts (1)-(4).
+
+
+Theorem extraspecial_repr_structure (sS : irrType F S) :
+ [/\ #|linear_irr sS| = (p ^ n.*2)%N,
+ ∃ iphi : 'I_p.-1 → sS, let phi i := irr_repr (iphi i) in
+ [/\ injective iphi,
+ codom iphi =i ~: linear_irr sS,
+ ∀ i, mx_faithful (phi i),
+ ∀ z, z \in 'Z(S)^# →
+ exists2 w, primitive_root_of_unity p w
+ & ∀ i, phi i z = (w ^+ i.+1)%:M
+ & ∀ i, irr_degree (iphi i) = (p ^ n)%N]
+ & #|sS| = (p ^ n.*2 + p.-1)%N].
+ +
+
+
++ [/\ #|linear_irr sS| = (p ^ n.*2)%N,
+ ∃ iphi : 'I_p.-1 → sS, let phi i := irr_repr (iphi i) in
+ [/\ injective iphi,
+ codom iphi =i ~: linear_irr sS,
+ ∀ i, mx_faithful (phi i),
+ ∀ z, z \in 'Z(S)^# →
+ exists2 w, primitive_root_of_unity p w
+ & ∀ i, phi i z = (w ^+ i.+1)%:M
+ & ∀ i, irr_degree (iphi i) = (p ^ n)%N]
+ & #|sS| = (p ^ n.*2 + p.-1)%N].
+ +
+
+ This is the corolloray of the above that is actually used in the proof of
+ B & G, Theorem 2.5. It encapsulates the dependency on a socle of the
+ regular representation.
+
+
+
+
+Variables (m : nat) (rS : mx_representation F S m) (U : 'M[F]_m).
+Hypotheses (simU : mxsimple rS U) (ffulU : rstab rS U == 1%g).
+Let sZS := center_sub S.
+Let rZ := subg_repr rS sZS.
+ +
+Lemma faithful_repr_extraspecial :
+ \rank U = (p ^ n)%N ∧
+ (∀ V, mxsimple rS V → mx_iso rZ U V → mx_iso rS U V).
+ +
+End Extraspecial.
+
++Variables (m : nat) (rS : mx_representation F S m) (U : 'M[F]_m).
+Hypotheses (simU : mxsimple rS U) (ffulU : rstab rS U == 1%g).
+Let sZS := center_sub S.
+Let rZ := subg_repr rS sZS.
+ +
+Lemma faithful_repr_extraspecial :
+ \rank U = (p ^ n)%N ∧
+ (∀ V, mxsimple rS V → mx_iso rZ U V → mx_iso rS U V).
+ +
+End Extraspecial.
+