- -

Library mathcomp.character.mxabelem

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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 : core.
- -
-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 : core.
- -
-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.
- -
-

- -

- 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.
- -
-

- -

- 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].
- -
-

- -

- 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.
-