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.solvable.finmodule.html | 191 +++++++++++++------------- 1 file changed, 96 insertions(+), 95 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.finmodule.html') diff --git a/docs/htmldoc/mathcomp.solvable.finmodule.html b/docs/htmldoc/mathcomp.solvable.finmodule.html index 543d986..4a97ce2 100644 --- a/docs/htmldoc/mathcomp.solvable.finmodule.html +++ b/docs/htmldoc/mathcomp.solvable.finmodule.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.

@@ -77,8 +76,8 @@ Reserved Notation "u ^@ x" (at level 31, left associativity).

-Inductive fmod_of (gT : finGroupType) (A : {group gT}) (abelA : abelian A) :=
-  Fmod x & x \in A.
+Inductive fmod_of (gT : finGroupType) (A : {group gT}) (abelA : abelian A) :=
+  Fmod x & x \in A.

@@ -86,151 +85,151 @@ Section OneFinMod.

-Let f2sub (gT : finGroupType) (A : {group gT}) (abA : abelian A) :=
-  fun u : fmod_of abA ⇒ let : Fmod x Ax := u in Subg Ax : FinGroup.arg_sort _.
+Let f2sub (gT : finGroupType) (A : {group gT}) (abA : abelian A) :=
+  fun u : fmod_of abA ⇒ let : Fmod x Ax := u in Subg Ax : FinGroup.arg_sort _.

-Variables (gT : finGroupType) (A : {group gT}) (abelA : abelian A).
+Variables (gT : finGroupType) (A : {group gT}) (abelA : abelian A).
Implicit Types (x y z : gT) (u v w : fmodA).

-Let sub2f (s : [subg A]) := Fmod abelA (valP s).
+Let sub2f (s : [subg A]) := Fmod abelA (valP s).

Definition fmval u := val (f2sub u).
-Canonical fmod_subType := [subType for fmval].
-Definition fmod_eqMixin := Eval hnf in [eqMixin of fmodA by <:].
+Canonical fmod_subType := [subType for fmval].
+Definition fmod_eqMixin := Eval hnf in [eqMixin of fmodA by <:].
Canonical fmod_eqType := Eval hnf in EqType fmodA fmod_eqMixin.
-Definition fmod_choiceMixin := [choiceMixin of fmodA by <:].
+Definition fmod_choiceMixin := [choiceMixin of fmodA by <:].
Canonical fmod_choiceType := Eval hnf in ChoiceType fmodA fmod_choiceMixin.
-Definition fmod_countMixin := [countMixin of fmodA by <:].
+Definition fmod_countMixin := [countMixin of fmodA by <:].
Canonical fmod_countType := Eval hnf in CountType fmodA fmod_countMixin.
-Canonical fmod_subCountType := Eval hnf in [subCountType of fmodA].
-Definition fmod_finMixin := [finMixin of fmodA by <:].
+Canonical fmod_subCountType := Eval hnf in [subCountType of fmodA].
+Definition fmod_finMixin := [finMixin of fmodA by <:].
Canonical fmod_finType := Eval hnf in FinType fmodA fmod_finMixin.
-Canonical fmod_subFinType := Eval hnf in [subFinType of fmodA].
+Canonical fmod_subFinType := Eval hnf in [subFinType of fmodA].

Definition fmod x := sub2f (subg A x).
-Definition actr u x := if x \in 'N(A) then fmod (fmval u ^ x) else u.
+Definition actr u x := if x \in 'N(A) then fmod (fmval u ^ x) else u.

-Definition fmod_opp u := sub2f u^-1.
-Definition fmod_add u v := sub2f (u × v).
+Definition fmod_opp u := sub2f u^-1.
+Definition fmod_add u v := sub2f (u × v).

-Fact fmod_add0r : left_id (sub2f 1) fmod_add.
+Fact fmod_add0r : left_id (sub2f 1) fmod_add.

-Fact fmod_addrA : associative fmod_add.
+Fact fmod_addrA : associative fmod_add.

-Fact fmod_addNr : left_inverse (sub2f 1) fmod_opp fmod_add.
+Fact fmod_addNr : left_inverse (sub2f 1) fmod_opp fmod_add.

-Fact fmod_addrC : commutative fmod_add.
+Fact fmod_addrC : commutative fmod_add.

Definition fmod_zmodMixin :=
  ZmodMixin fmod_addrA fmod_addrC fmod_add0r fmod_addNr.
Canonical fmod_zmodType := Eval hnf in ZmodType fmodA fmod_zmodMixin.
-Canonical fmod_finZmodType := Eval hnf in [finZmodType of fmodA].
+Canonical fmod_finZmodType := Eval hnf in [finZmodType of fmodA].
Canonical fmod_baseFinGroupType :=
-  Eval hnf in [baseFinGroupType of fmodA for +%R].
+  Eval hnf in [baseFinGroupType of fmodA for +%R].
Canonical fmod_finGroupType :=
-  Eval hnf in [finGroupType of fmodA for +%R].
+  Eval hnf in [finGroupType of fmodA for +%R].

-Lemma fmodP u : val u \in A.
-Lemma fmod_inj : injective fmval.
-Lemma congr_fmod u v : u = v → fmval u = fmval v.
+Lemma fmodP u : val u \in A.
+Lemma fmod_inj : injective fmval.
+Lemma congr_fmod u v : u = v → fmval u = fmval v.

-Lemma fmvalA : {morph valA : x y / x + y >-> (x × y)%g}.
-Lemma fmvalN : {morph valA : x / - x >-> x^-1%g}.
-Lemma fmval0 : valA 0 = 1%g.
-Canonical fmval_morphism := @Morphism _ _ setT fmval (in2W fmvalA).
+Lemma fmvalA : {morph valA : x y / x + y >-> (x × y)%g}.
+Lemma fmvalN : {morph valA : x / - x >-> x^-1%g}.
+Lemma fmval0 : valA 0 = 1%g.
+Canonical fmval_morphism := @Morphism _ _ setT fmval (in2W fmvalA).

Definition fmval_sum := big_morph fmval fmvalA fmval0.

-Lemma fmvalZ n : {morph valA : x / x *+ n >-> (x ^+ n)%g}.
+Lemma fmvalZ n : {morph valA : x / x *+ n >-> (x ^+ n)%g}.

-Lemma fmodKcond x : val (fmod x) = if x \in A then x else 1%g.
- Lemma fmodK : {in A, cancel fmod val}.
-Lemma fmvalK : cancel val fmod.
- Lemma fmod1 : fmod 1 = 0.
-Lemma fmodM : {in A &, {morph fmod : x y / (x × y)%g >-> x + y}}.
+Lemma fmodKcond x : val (fmod x) = if x \in A then x else 1%g.
+ Lemma fmodK : {in A, cancel fmod val}.
+Lemma fmvalK : cancel val fmod.
+ Lemma fmod1 : fmod 1 = 0.
+Lemma fmodM : {in A &, {morph fmod : x y / (x × y)%g >-> x + y}}.
Canonical fmod_morphism := Morphism fmodM.
-Lemma fmodX n : {in A, {morph fmod : x / (x ^+ n)%g >-> x *+ n}}.
- Lemma fmodV : {morph fmod : x / x^-1%g >-> - x}.
+Lemma fmodX n : {in A, {morph fmod : x / (x ^+ n)%g >-> x *+ n}}.
+ Lemma fmodV : {morph fmod : x / x^-1%g >-> - x}.

-Lemma injm_fmod : 'injm fmod.
+Lemma injm_fmod : 'injm fmod.

-Notation "u ^@ x" := (actr u x) : ring_scope.
+Notation "u ^@ x" := (actr u x) : ring_scope.

Lemma fmvalJcond u x :
-  val (u ^@ x) = if x \in 'N(A) then val u ^ x else val u.
+  val (u ^@ x) = if x \in 'N(A) then val u ^ x else val u.

-Lemma fmvalJ u x : x \in 'N(A) → val (u ^@ x) = val u ^ x.
+Lemma fmvalJ u x : x \in 'N(A) → val (u ^@ x) = val u ^ x.

-Lemma fmodJ x y : y \in 'N(A) → fmod (x ^ y) = fmod x ^@ y.
+Lemma fmodJ x y : y \in 'N(A) → fmod (x ^ y) = fmod x ^@ y.

-Fact actr_is_action : is_action 'N(A) actr.
+Fact actr_is_action : is_action 'N(A) actr.

Canonical actr_action := Action actr_is_action.
-Notation "''M'" := actr_action (at level 8) : action_scope.
+Notation "''M'" := actr_action (at level 8) : action_scope.

-Lemma act0r x : 0 ^@ x = 0.
+Lemma act0r x : 0 ^@ x = 0.

-Lemma actAr x : {morph actr^~ x : u v / u + v}.
+Lemma actAr x : {morph actr^~ x : u v / u + v}.

Definition actr_sum x := big_morph _ (actAr x) (act0r x).

-Lemma actNr x : {morph actr^~ x : u / - u}.
+Lemma actNr x : {morph actr^~ x : u / - u}.

-Lemma actZr x n : {morph actr^~ x : u / u *+ n}.
+Lemma actZr x n : {morph actr^~ x : u / u *+ n}.

-Fact actr_is_groupAction : is_groupAction setT 'M.
+Fact actr_is_groupAction : is_groupAction setT 'M.

Canonical actr_groupAction := GroupAction actr_is_groupAction.
-Notation "''M'" := actr_groupAction (at level 8) : groupAction_scope.
+Notation "''M'" := actr_groupAction (at level 8) : groupAction_scope.

-Lemma actr1 u : u ^@ 1 = u.
+Lemma actr1 u : u ^@ 1 = u.

-Lemma actrM : {in 'N(A) &, ∀ x y u, u ^@ (x × y) = u ^@ x ^@ y}.
+Lemma actrM : {in 'N(A) &, ∀ x y u, u ^@ (x × y) = u ^@ x ^@ y}.

-Lemma actrK x : cancel (actr^~ x) (actr^~ x^-1%g).
+Lemma actrK x : cancel (actr^~ x) (actr^~ x^-1%g).

-Lemma actrKV x : cancel (actr^~ x^-1%g) (actr^~ x).
+Lemma actrKV x : cancel (actr^~ x^-1%g) (actr^~ x).

End OneFinMod.

-Notation "u ^@ x" := (actr u x) : ring_scope.
-Notation "''M'" := actr_action (at level 8) : action_scope.
-Notation "''M'" := actr_groupAction : groupAction_scope.
+Notation "u ^@ x" := (actr u x) : ring_scope.
+Notation "''M'" := actr_action (at level 8) : action_scope.
+Notation "''M'" := actr_groupAction : groupAction_scope.

End FiniteModule.
@@ -248,6 +247,8 @@ Canonical FiniteModule.fmod_baseFinGroupType.
Canonical FiniteModule.fmod_finGroupType.
+
+
@@ -261,29 +262,29 @@ Section Gaschutz.

-Variables (gT : finGroupType) (G H P : {group gT}).
-Implicit Types K L : {group gT}.
+Variables (gT : finGroupType) (G H P : {group gT}).
+Implicit Types K L : {group gT}.

-Hypotheses (nsHG : H <| G) (sHP : H \subset P) (sPG : P \subset G).
-Hypotheses (abelH : abelian H) (coHiPG : coprime #|H| #|G : P|).
+Hypotheses (nsHG : H <| G) (sHP : H \subset P) (sPG : P \subset G).
+Hypotheses (abelH : abelian H) (coHiPG : coprime #|H| #|G : P|).

Let sHG := normal_sub nsHG.
Let nHG := subsetP (normal_norm nsHG).

-Let m := (expg_invn H #|G : P|).
+Let m := (expg_invn H #|G : P|).

Implicit Types a b : fmod_of abelH.

-Theorem Gaschutz_split : [splits G, over H] = [splits P, over H].
+Theorem Gaschutz_split : [splits G, over H] = [splits P, over H].

-Theorem Gaschutz_transitive : {in [complements to H in G] &,
-  ∀ K L, K :&: P = L :&: P → exists2 x, x \in H & L :=: K :^ x}.
+Theorem Gaschutz_transitive : {in [complements to H in G] &,
+  ∀ K L, K :&: P = L :&: P → exists2 x, x \in H & L :=: K :^ x}.

End Gaschutz.
@@ -300,30 +301,30 @@ This Lemma is used in maximal.v for the proof of Aschbacher 24.7.
-Lemma coprime_abel_cent_TI (gT : finGroupType) (A G : {group gT}) :
-  A \subset 'N(G) → coprime #|G| #|A| → abelian G → 'C_[~: G, A](A) = 1.
+Lemma coprime_abel_cent_TI (gT : finGroupType) (A G : {group gT}) :
+  A \subset 'N(G) → coprime #|G| #|A| → abelian G → 'C_[~: G, A](A) = 1.

Section Transfer.

-Variables (gT aT : finGroupType) (G H : {group gT}).
-Variable alpha : {morphism H >-> aT}.
+Variables (gT aT : finGroupType) (G H : {group gT}).
+Variable alpha : {morphism H >-> aT}.

-Hypotheses (sHG : H \subset G) (abelA : abelian (alpha @* H)).
+Hypotheses (sHG : H \subset G) (abelA : abelian (alpha @* H)).


-Fact transfer_morph_subproof : H \subset alpha @*^-1 (alpha @* H).
+Fact transfer_morph_subproof : H \subset alpha @*^-1 (alpha @* H).

-Let fmalpha := restrm transfer_morph_subproof (fmod abelA \o alpha).
+Let fmalpha := restrm transfer_morph_subproof (fmod abelA \o alpha).

-Let V (rX : {set gT} → gT) g :=
-  \sum_(Hx in rcosets H G) fmalpha (rX Hx × g × (rX (Hx :* g))^-1).
+Let V (rX : {set gT} → gT) g :=
+  \sum_(Hx in rcosets H G) fmalpha (rX Hx × g × (rX (Hx :* g))^-1).

Definition transfer g := V repr g.
@@ -335,7 +336,7 @@ This is Aschbacher (37.2).
-Lemma transferM : {in G &, {morph transfer : x y / (x × y)%g >-> x + y}}.
+Lemma transferM : {in G &, {morph transfer : x y / (x × y)%g >-> x + y}}.

Canonical transfer_morphism := Morphism transferM.
@@ -348,61 +349,61 @@
Lemma transfer_indep X (rX := transversal_repr 1 X) :
-  is_transversal X HG G → {in G, transfer =1 V rX}.
+  is_transversal X HG G → {in G, transfer =1 V rX}.

Section FactorTransfer.

Variable g : gT.
-Hypothesis Gg : g \in G.
+Hypothesis Gg : g \in G.

-Let sgG : <[g]> \subset G.
-Let H_g_rcosets x : {set {set gT}} := rcosets (H :* x) <[g]>.
-Let n_ x := #|<[g]> : H :* x|.
+Let sgG : <[g]> \subset G.
+Let H_g_rcosets x : {set {set gT}} := rcosets (H :* x) <[g]>.
+Let n_ x := #|<[g]> : H :* x|.

-Lemma mulg_exp_card_rcosets x : x × (g ^+ n_ x) \in H :* x.
+Lemma mulg_exp_card_rcosets x : x × (g ^+ n_ x) \in H :* x.

-Let HGg : {set {set {set gT}}} := orbit 'Rs <[g]> @: HG.
+Let HGg : {set {set {set gT}}} := orbit 'Rs <[g]> @: HG.

Let partHG : partition HG G := rcosets_partition sHG.
-Let actsgHG : [acts <[g]>, on HG | 'Rs].
+Let actsgHG : [acts <[g]>, on HG | 'Rs].
Let partHGg : partition HGg HG := orbit_partition actsgHG.

-Let injHGg : {in HGg &, injective cover}.
+Let injHGg : {in HGg &, injective cover}.

-Let defHGg : HG :* <[g]> = cover @: HGg.
+Let defHGg : HG :* <[g]> = cover @: HGg.

-Lemma rcosets_cycle_partition : partition (HG :* <[g]>) G.
+Lemma rcosets_cycle_partition : partition (HG :* <[g]>) G.

-Variable X : {set gT}.
-Hypothesis trX : is_transversal X (HG :* <[g]>) G.
+Variable X : {set gT}.
+Hypothesis trX : is_transversal X (HG :* <[g]>) G.

-Let sXG : {subset X ≤ G}.
+Let sXG : {subset X ≤ G}.

-Lemma rcosets_cycle_transversal : H_g_rcosets @: X = HGg.
+Lemma rcosets_cycle_transversal : H_g_rcosets @: X = HGg.


-Let injHg: {in X &, injective H_g_rcosets}.
+Let injHg: {in X &, injective H_g_rcosets}.

-Lemma sum_index_rcosets_cycle : (\sum_(x in X) n_ x)%N = #|G : H|.
+Lemma sum_index_rcosets_cycle : (\sum_(x in X) n_ x)%N = #|G : H|.

Lemma transfer_cycle_expansion :
-   transfer g = \sum_(x in X) fmalpha ((g ^+ n_ x) ^ x^-1).
+   transfer g = \sum_(x in X) fmalpha ((g ^+ n_ x) ^ x^-1).

End FactorTransfer.
-- cgit v1.2.3