From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.character.mxabelem.html | 375 +++++++++++++------------- 1 file changed, 188 insertions(+), 187 deletions(-) (limited to 'docs/htmldoc/mathcomp.character.mxabelem.html') diff --git a/docs/htmldoc/mathcomp.character.mxabelem.html b/docs/htmldoc/mathcomp.character.mxabelem.html index 2830ce6..ffff5d8 100644 --- a/docs/htmldoc/mathcomp.character.mxabelem.html +++ b/docs/htmldoc/mathcomp.character.mxabelem.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -88,29 +87,29 @@
Variable (R : finComUnitRingType) (gT : finGroupType).
-Variables (G : {group gT}) (n : nat) (rG : mx_representation R G n).
+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)).
+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.
+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.
+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)
+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.
+Notation "''MR' rG" := (mx_repr_groupAction rG) : groupAction_scope.

Section FinFieldRepr.
@@ -130,18 +129,18 @@ Section ScaleAction.

-Variables m n : nat.
+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.
+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.
+Lemma astab1_scale_act A : A != 0 → 'C[A | scale_action] = 1%g.

End ScaleAction.
@@ -152,170 +151,170 @@ Section RowGroup.

-Variable n : nat.
+Variable n : nat.

-Definition rowg m (A : 'M[F]_(m, n)) : {set rVn} := [set u | u ≤ A]%MS.
+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.
+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 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 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 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 rowg0 m : rowg (0 : 'M_(m, n)) = 1%g.

-Lemma rowg1 : rowg 1%:M = setT.
+Lemma rowg1 : rowg 1%:M = setT.

-Lemma trivg_rowg m (A : 'M_(m, n)) : (rowg A == 1%g) = (A == 0).
+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.
+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 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 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 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 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_mx1 : rowg_mx 1%g = 0.

-Lemma rowg_mx_eq0 (L : {group rVn}) : (rowg_mx L == 0) = (L :==: 1%g).
+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 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 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 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 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 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 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.
+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).
+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.
+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).
+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 val_reprGLm x : x \in G → val (reprGLm x) = rG x.

-Lemma comp_reprGLm : {in G, GLval \o reprGLm =1 rG}.
+Lemma comp_reprGLm : {in G, GLval \o reprGLm =1 rG}.

-Lemma reprGLmM : {in G &, {morph reprGLm : x y / x × y}}%g.
+Lemma reprGLmM : {in G &, {morph reprGLm : x y / x × y}}%g.
Canonical reprGL_morphism := Morphism reprGLmM.

-Lemma ker_reprGLm : 'ker reprGLm = rker rG.
+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 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 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 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 astab_setT_repr : 'C(setT | 'MR rG) = rker rG.

Lemma mx_repr_action_faithful :
-  [faithful G, on setT | 'MR rG] = mx_faithful rG.
+  [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 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).
+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.
+Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope.
+Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.

Section MatrixGroups.

-Implicit Types m n p q : nat.
+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.
+  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 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 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.
+  q > 1 → abelian_type [set: 'M['Z_q]_(m, n)] = nseq (m × n) q.

End MatrixGroups.
@@ -325,19 +324,19 @@ Open Scope abelem_scope.

-Definition abelem_dim' (gT : finGroupType) (E : {set gT}) :=
-  (logn (pdiv #|E|) #|E|).-1.
-Notation "''dim' E" := (abelem_dim' E).+1
+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)
+Notation "''rV' ( E )" := 'rV_('dim E)
  (at level 8, format "''rV' ( E )") : abelem_scope.
-Notation "''M' ( E )" := 'M_('dim E)
+Notation "''M' ( E )" := 'M_('dim E)
  (at level 8, format "''M' ( E )") : abelem_scope.
-Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
+Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
  (at level 8, only parsing) : abelem_scope.
-Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
+Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
  (at level 8, only parsing) : abelem_scope.

@@ -347,13 +346,13 @@ Section FpMatrix.

-Variables p m n : nat.
+Variables p m n : nat.

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

-Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].
+Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].

End FpMatrix.
@@ -362,48 +361,48 @@ Section FpRow.

-Variables p n : nat.
+Variables p n : nat.

-Lemma rowg_mxK (L : {group rVn}) : rowg (rowg_mx L) = L.
+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 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|.
+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).
+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 pE : p.-group E := abelem_pgroup abelE.
Let p_pr : prime p.


-Lemma dim_abelemE : n = logn p #|E|.
+Lemma dim_abelemE : n = logn p #|E|.

-Lemma card_abelem_rV : #|rVn| = #|E|.
+Lemma card_abelem_rV : #|rVn| = #|E|.

-Lemma isog_abelem_rV : E \isog [set: rVn].
+Lemma isog_abelem_rV : E \isog [set: rVn].

-Definition abelem_rV : gT → rVn := xchoose ab_rV_P.
+Definition abelem_rV : gT → rVn := xchoose ab_rV_P.


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

Canonical abelem_rV_morphism := Morphism abelem_rV_M.
@@ -412,113 +411,113 @@ Lemma abelem_rV_isom : isom E setT ErV.

-Lemma abelem_rV_injm : 'injm ErV.
+Lemma abelem_rV_injm : 'injm ErV.

-Lemma abelem_rV_inj : {in E &, injective ErV}.
+Lemma abelem_rV_inj : {in E &, injective ErV}.

-Lemma im_abelem_rV : ErV @* E = setT.
+Lemma im_abelem_rV : ErV @* E = setT.

-Lemma mem_im_abelem_rV u : u \in ErV @* E.
+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 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_1 : ErV 1 = 0%R.

-Lemma abelem_rV_X x i : x \in E → ErV (x ^+ i) = i%:R *: ErV x.
+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.
+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].
+Definition rVabelem : rVn → gT := invm abelem_rV_injm.
+Canonical rVabelem_morphism := [morphism of rVabelem].

-Lemma rVabelem0 : rV_E 0 = 1%g.
+Lemma rVabelem0 : rV_E 0 = 1%g.

-Lemma rVabelemD : {morph rV_E : u v / u + v >-> (u × v)%g}.
+Lemma rVabelemD : {morph rV_E : u v / u + v >-> (u × v)%g}.

-Lemma rVabelemN : {morph rV_E: u / - u >-> (u^-1)%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 rVabelemZ (m : 'F_p) : {morph rV_E : u / m *: u >-> (u ^+ m)%g}.

-Lemma abelem_rV_K : {in E, cancel ErV rV_E}.
+Lemma abelem_rV_K : {in E, cancel ErV rV_E}.

-Lemma rVabelemK : cancel rV_E ErV.
+Lemma rVabelemK : cancel rV_E ErV.

-Lemma rVabelem_inj : injective rV_E.
+Lemma rVabelem_inj : injective rV_E.

-Lemma rVabelem_injm : 'injm rV_E.
+Lemma rVabelem_injm : 'injm rV_E.

-Lemma im_rVabelem : rV_E @* setT = E.
+Lemma im_rVabelem : rV_E @* setT = E.

-Lemma mem_rVabelem u : rV_E u \in 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 sub_rVabelem L : rV_E @* L \subset E.
+ Hint Resolve mem_rVabelem sub_rVabelem : core.

-Lemma card_rVabelem L : #|rV_E @* L| = #|L|.
+Lemma card_rVabelem L : #|rV_E @* L| = #|L|.

-Lemma abelem_rV_mK (H : {set gT}) : H \subset E → rV_E @* (ErV @* H) = H.
+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_mK L : ErV @* (rV_E @* L) = L.

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

-Lemma rVabelemS L M : (rV_E @* L \subset rV_E @* M) = (L \subset M).
+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 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_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).
+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) :=
+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).
+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.
+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.
@@ -526,57 +525,57 @@ Let rG := abelem_repr.

-Lemma rVabelemJ v x : x \in G → rV_E (v ×m rG x) = (rV_E v) ^ x.
+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_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 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 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 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_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 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_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 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_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 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 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 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 rker_abelem : rker rG = 'C_G(E).

-Lemma abelem_mx_faithful : 'C_G(E) = 1%g → mx_faithful rG.
+Lemma abelem_mx_faithful : 'C_G(E) = 1%g → mx_faithful rG.

End OneGroup.
@@ -585,21 +584,21 @@ Section SubGroup.

-Variables G H : {group gT}.
-Hypotheses (nEG : G \subset 'N(E)) (sHG : H \subset G).
+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 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 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.
+Lemma mxsimple_abelem_subg U : mxsimple rHG U ↔ mxsimple rH U.

End SubGroup.
@@ -607,13 +606,15 @@
End AbelemRepr.
+
+
Section ModularRepresentation.

-Variables (F : fieldType) (p : nat) (gT : finGroupType).
-Hypothesis charFp : p \in [char F].
-Implicit Types G H : {group gT}.
+Variables (F : fieldType) (p : nat) (gT : finGroupType).
+Hypothesis charFp : p \in [char F].
+Implicit Types G H : {group gT}.

@@ -623,16 +624,16 @@
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.
+  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).
+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_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.
+Lemma pcore_sub_rker_mx_irr : mx_irreducible rG → 'O_p(G) \subset rker rG.

@@ -642,7 +643,7 @@
Lemma pcore_faithful_mx_irr :
-  mx_irreducible rG → mx_faithful rG → 'O_p(G) = 1%g.
+  mx_irreducible rG → mx_faithful rG → 'O_p(G) = 1%g.

End ModularRepresentation.
@@ -651,10 +652,10 @@ 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).
+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.
@@ -663,7 +664,7 @@ Let oZp := card_center_extraspecial pS esS.

-Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N.
+Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N.

@@ -673,16 +674,16 @@
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].

@@ -695,15 +696,15 @@

-Variables (m : nat) (rS : mx_representation F S m) (U : 'M[F]_m).
-Hypotheses (simU : mxsimple rS U) (ffulU : rstab rS U == 1%g).
+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).
+ \rank U = (p ^ n)%N ∧
+   (∀ V, mxsimple rS V → mx_iso rZ U V → mx_iso rS U V).

End Extraspecial.
-- cgit v1.2.3