Library mathcomp.character.mxabelem
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient gproduct action finalg.
From mathcomp Require Import zmodp commutator cyclic center pgroup gseries.
From mathcomp Require Import nilpotent sylow maximal abelian matrix.
From mathcomp Require Import mxalgebra mxrepresentation.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient gproduct action finalg.
From mathcomp Require Import zmodp commutator cyclic center pgroup gseries.
From mathcomp Require Import nilpotent sylow maximal abelian matrix.
From mathcomp Require Import mxalgebra mxrepresentation.
This file completes the theory developed in mxrepresentation.v with the
construction and properties of linear representations over finite fields,
and in particular the correspondence 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.
Declare Scope abelem_scope.
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)%g = 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.
Arguments rowg_mx {F n%N} L%g.
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.
Arguments abelem_dim' {gT} E%g.
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.
Arguments rVabelem_inj {p%N gT E%G} abelE ntE [v1%R v2%R] : rename.
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)%g = 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.
Arguments rowg_mx {F n%N} L%g.
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.
Arguments abelem_dim' {gT} E%g.
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.
Arguments rVabelem_inj {p%N gT E%G} abelE ntE [v1%R v2%R] : rename.
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.