Library mxabelem

   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. 


Import GroupScope GRing.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 FiniteRepr.

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 : forall A a, scale_act A a = val a *: A.

Lemma scale_is_action : is_action setT scale_act.
Canonical Structure scale_action := Action scale_is_action.
Lemma scale_is_groupAction : is_groupAction setT scale_action.
Canonical Structure scale_groupAction := GroupAction scale_is_groupAction.

Lemma astab1_scale_act : forall A, A != 0 -> 'C[A | scale_action] = 1%g.

End ScaleAction.

Local Notation "'Zm" := (scale_action _ _) (at level 0) : action_scope.

Section RowGroup.

Variable n : nat.
Local Notation rVn := 'rV[F]_n.

Definition rowg m (A : 'M[F]_(m, n)) : {set rVn} := [set u | u <= A]%MS.

Lemma mem_rowg : forall m A v, (v \in @rowg m A) = (v <= A)%MS.

Lemma rowg_group_set : forall m A, group_set (@rowg m A).
Canonical Structure rowg_group m A := Group (@rowg_group_set m A).

Lemma rowg_stable : forall m (A : 'M_(m, n)), [acts setT, on rowg A | 'Zm].

Lemma rowgS : forall m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (rowg A \subset rowg B) = (A <= B)%MS.

Lemma eq_rowg : forall m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :=: B)%MS -> rowg A = rowg B.

Lemma rowg0 : forall m, rowg (0 : 'M_(m, n)) = 1%g.

Lemma rowg1 : rowg 1%:M = setT.

Lemma trivg_rowg : forall 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 : forall m (A : 'M_(m, n)), (rowg_mx (rowg A) :=: A)%MS.

Lemma rowg_mxS : forall L M : {set 'rV[F]_n},
  L \subset M -> (rowg_mx L <= rowg_mx M)%MS.

Lemma sub_rowg_mx : forall L : {set rVn}, L \subset rowg (rowg_mx L).

Lemma stable_rowg_mxK : forall 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 : forall L : {group rVn}, (rowg_mx L == 0) = (L :==: 1%g).

Lemma rowgI : forall m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  rowg (A :&: B)%MS = rowg A :&: rowg B.

Lemma card_rowg : forall m (A : 'M_(m, n)), #|rowg A| = (#|F| ^ \rank A)%N.

Lemma rowgD : forall m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  rowg (A + B)%MS = (rowg A * rowg B)%g.

 An alternative proof, which avoids the counting argument.
   It's outcommented because the mem_mulg rewrite takes forever to execute.
Lemma rowgD' : forall m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  rowg (A + B)%MS = (rowg A * rowg B)%g.
Proof.
move=> m1 m2 A B; apply/eqP; rewrite eq_sym eqEsubset mulG_subG /= !rowgS.
rewrite addsmxSl addsmxSr; apply/subsetP=> u; rewrite !inE.
by case/sub_addsmxP=> v suvA svB; rewrite -(mulgKV v u) mem_mulg ?inE.
Qed.


End RowGroup.

Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable (rG : mx_representation F G n).

Lemma GL_mx_repr : mx_repr 'GL_n[F] GLval.

Canonical Structure 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 : forall 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 Structure reprGL_morphism := Morphism reprGLmM.

Lemma ker_reprGLm : 'ker reprGLm = rker rG.

Definition mx_repr_act (u : 'rV_n) x := u *m val (reprGLm x).

Lemma mx_repr_actE : forall u x, x \in G -> mx_repr_act u x = u *m rG x.

Lemma mx_repr_is_action : is_action G mx_repr_act.
Canonical Structure mx_repr_action := Action mx_repr_is_action.

Lemma mx_repr_is_groupAction : is_groupAction setT mx_repr_action.
Canonical Structure mx_repr_groupAction := GroupAction mx_repr_is_groupAction.

Local Notation "''MR' 'rG'" := mx_repr_action (at level 10) : action_scope.
Local Notation "''MR' 'rG'" := mx_repr_groupAction : groupAction_scope.

Lemma astab_rowg_repr : forall m (A : 'M_(m, n)),
  'C(rowg A | 'MR rG) = rstab rG A.

Lemma astabs_rowg_repr : forall m (A : 'M_(m, n)),
  'N(rowg A | 'MR rG) = rstabs rG A.

Lemma acts_rowg : forall 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 : forall H : {set gT},
  H \subset G -> 'Fix_('MR rG)(H) = rowg (rfix_mx rG H).

Lemma gacent_repr : forall H : {set gT},
  H \subset G -> 'C_(| 'MR rG)(H) = rowg (rfix_mx rG H).

End FiniteRepr.

Notation "''Zm'" := (scale_action _ _ _) (at level 0) : action_scope.
Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.
Notation "''MR' rG" := (mx_repr_action rG)
  (at level 10, rG at level 8, format "''MR' rG") : action_scope.
Notation "''MR' rG" := (mx_repr_groupAction rG) : groupAction_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") : group_scope.

Notation "''rV' ( E )" := 'rV_('dim E)
  (at level 8, format "''rV' ( E )") : group_scope.
Notation "''M' ( E )" := 'M_('dim E)
  (at level 8, format "''M' ( E )") : group_scope.
Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
  (at level 8, only parsing) : group_scope.
Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
  (at level 8, only parsing) : group_scope.

Section AbelemRepr.

Import FinRing.Theory.

Section FpMatrix.

Variables p m n : nat.
Local Notation Mmn := 'M['F_p]_(m, n).

Lemma mx_Fp_abelem : prime p -> p.-abelem [set: Mmn].

Lemma mx_Fp_stable : forall L : {group Mmn}, [acts setT, on L | 'Zm].

End FpMatrix.

Section FpRow.

Variables p n : nat.
Local Notation rVn := 'rV['F_p]_n.

Lemma rowg_mxK : forall L : {group rVn}, rowg (rowg_mx L) = L.

Lemma rowg_mxSK : forall (L : {set rVn}) (M : {group rVn}),
  (rowg_mx L <= rowg_mx M)%MS = (L \subset M).

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.

Local Notation n' := (abelem_dim' (gval E)).
Local Notation n := n'.+1.
Local Notation rVn := 'rV['F_p](gval E).

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.

Local Notation ErV := abelem_rV.

Lemma abelem_rV_M : {in E &, {morph ErV : x y / (x * y)%g >-> x + y}}.

Canonical Structure 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 : forall u, u \in ErV @* E.

Lemma sub_im_abelem_rV : forall 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 : forall x i, x \in E -> ErV (x ^+ i) = i%:R *: ErV x.

Lemma abelem_rV_V : forall x, x \in E -> ErV x^-1 = - ErV x.

Definition rVabelem : rVn -> gT := invm abelem_rV_injm.
Canonical Structure rVabelem_morphism := [morphism of rVabelem].
Local Notation rV_E := 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 : forall 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 : forall u, rV_E u \in E.

Lemma sub_rVabelem : forall L, rV_E @* L \subset E.
Hint Resolve mem_rVabelem sub_rVabelem.

Lemma card_rVabelem : forall L, #|rV_E @* L| = #|L|.

Lemma abelem_rV_mK : forall H : {set gT}, H \subset E -> rV_E @* (ErV @* H) = H.

Lemma rVabelem_mK : forall L, ErV @* (rV_E @* L) = L.

Lemma rVabelem_minj : injective (morphim (MorPhantom rV_E)).

Lemma rVabelemS : forall L M, (rV_E @* L \subset rV_E @* M) = (L \subset M).

Lemma abelem_rV_S : forall H K : {set gT},
  H \subset E -> (ErV @* H \subset ErV @* K) = (H \subset K).

Lemma sub_rVabelem_im : forall L (H : {set gT}),
  (rV_E @* L \subset H) = (L \subset ErV @* H).

Lemma sub_abelem_rV_im : forall (H : {set gT}) (L : {set 'rV['F_p]_n}),
  H \subset E -> (ErV @* H \subset L) = (H \subset rV_E @* L).

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).
Local Notation r := (abelem_mx nEG).

Lemma abelem_mx_linear_proof : forall g, linear (abelem_mx_fun g).
Canonical Structure abelem_mx_linear g := Linear (abelem_mx_linear_proof g).

Let rVabelemJmx : forall v x, x \in G -> rV_E (v *m r x) = (rV_E v) ^ x.

Lemma abelem_mx_repr : mx_repr G r.
Canonical Structure abelem_repr := MxRepresentation abelem_mx_repr.

Lemma rVabelemJ : forall v x, x \in G -> rV_E (v *m rG x) = (rV_E v) ^ x.

Lemma abelem_rV_J : {in E & G, forall x y, ErV (x ^ y) = ErV x *m rG y}.

Lemma abelem_rowgJ : forall 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 : forall (L : {group gT}) x,
  x \in G -> L \subset E -> ErV @* (L :^ x) = rowg (rowg_mx (ErV @* L) *m rG x).

Lemma rstab_abelem : forall m (A : 'M_(m, n)),
  rstab rG A = 'C_G(rV_E @* rowg A).

Lemma rstabs_abelem : forall m (A : 'M_(m, n)),
  rstabs rG A = 'N_G(rV_E @* rowg A).

Lemma rstabs_abelem_rowg_mx : forall L : {group gT},
  L \subset E -> rstabs rG (rowg_mx (ErV @* L)) = 'N_G(L).

Lemma abelem_mx_irrP : reflect (mx_irreducible rG) (minnormal E G).

Lemma rfix_abelem : forall 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 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 : forall 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 : forall 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 modIp' : forall i : 'I_p.-1, (i.+1 %% p = i.+1)%N.

 This is Aschbacher (34.9), parts (1)-(4). 
Theorem extraspecial_repr_structure : forall 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].

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

Lemma faithful_repr_extraspecial :
 \rank U = (p ^ n)%N /\
   (forall V, mxsimple rS V -> mx_iso rZ U V -> mx_iso rS U V).

End Extraspecial.