- -

Library mathcomp.solvable.finmodule

- -

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

- -

- This file regroups constructions and results that are based on the most - primitive version of representation theory -- viewing an abelian group as - the additive group of a (finite) Z-module. This includes the Gaschutz - splitting and transitivity theorem, from which we will later derive the - Schur-Zassenhaus theorem and the elementary abelian special case of - Maschke's theorem, the coprime abelian centraliser/commutator trivial - intersection theorem, which is used to show that p-groups under coprime - action factor into special groups, and the construction of the transfer - homomorphism and its expansion relative to a cycle, from which we derive - the Higman Focal Subgroup and the Burnside Normal Complement theorems. - The definitions and lemmas for the finite Z-module induced by an abelian - are packaged in an auxiliary FiniteModule submodule: they should not be - needed much outside this file, which contains all the results that exploit - this construction. - FiniteModule defines the Z[N(A) ]-module associated with a finite abelian - abelian group A, given a proof (abelA : abelian A) : - fmod_of abelA == the type of elements of the module (similar to but - distinct from [subg A]). - fmod abelA x == the injection of x into fmod_of abelA if x \in A, else 0 - fmval u == the projection of u : fmod_of abelA onto A - u ^@ x == the action of x \in 'N(A) on u : fmod_of abelA - The transfer morphism is be constructed from a morphism f : H >-> rT, and - a group G, along with the two assumptions sHG : H \subset G and - abfH : abelian (f @* H): - transfer sGH abfH == the function gT -> FiniteModule.fmod_of abfH that - implements the transfer morphism induced by f on G. - The Lemma transfer_indep states that the transfer morphism can be expanded - using any transversal of the partition HG := rcosets H G of G. - Further, for any g \in G, HG :* < [g]> is also a partition of G (Lemma - rcosets_cycle_partition), and for any transversal X of HG :* < [g]> the - function r mapping x : gT to rcosets (H :* x) < [g]> is (constructively) a - bijection from X to the < [g]>-orbit partition of HG, and Lemma - transfer_pcycle_def gives a simplified expansion of the transfer morphism. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope GRing.Theory FinRing.Theory.
-Local Open Scope ring_scope.
- -
-Module FiniteModule.
- -
-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.
- -
- -
-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 _.
- -
-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).
- -
-Definition fmval u := val (f2sub u).
-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 <:].
-Canonical fmod_choiceType := Eval hnf in ChoiceType fmodA fmod_choiceMixin.
-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_finType := Eval hnf in FinType fmodA fmod_finMixin.
-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 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_addrA : associative fmod_add.
- -
-Fact fmod_addNr : left_inverse (sub2f 1) fmod_opp 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_baseFinGroupType :=
-  Eval hnf in [baseFinGroupType of fmodA for +%R ].
-Canonical fmod_finGroupType :=
-  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 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 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 injm_fmod : 'injm fmod.
- -
-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.
- -
-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.
- -
-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.
- -
-Lemma act0r x : 0 ^@ x = 0.
- -
-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 actZr x n : {morph actr ^~ x : u / u *+ n }.
- -
-Fact actr_is_groupAction : is_groupAction setT 'M.
- -
-Canonical actr_groupAction := GroupAction actr_is_groupAction.
-Notation "''M'" := actr_groupAction (at level 8) : groupAction_scope.
- -
-Lemma actr1 u : u ^@ 1 = u.
- -
-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 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.
- -
-End FiniteModule.
- -
-Canonical FiniteModule.fmod_subType.
-Canonical FiniteModule.fmod_eqType.
-Canonical FiniteModule.fmod_choiceType.
-Canonical FiniteModule.fmod_countType.
-Canonical FiniteModule.fmod_finType.
-Canonical FiniteModule.fmod_subCountType.
-Canonical FiniteModule.fmod_subFinType.
-Canonical FiniteModule.fmod_zmodType.
-Canonical FiniteModule.fmod_finZmodType.
-Canonical FiniteModule.fmod_baseFinGroupType.
-Canonical FiniteModule.fmod_finGroupType.
- -
- -
-

- -

- Still allow ring notations, but give priority to groups now. -

-Import FiniteModule GroupScope.
- -
-Section Gaschutz.
- -
-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 |).
- -
-Let sHG := normal_sub nsHG.
-Let nHG := subsetP (normal_norm nsHG).
- -
-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_transitive : {in [complements to H in G ] &,
- ∀ K L, K :&: P = L :&: P → exists2 x, x \in H & L :=: K :^ x }.
- -
-End Gaschutz.
- -
-

- -

- This is the TI part of B & G, Proposition 1.6(d). - We go with B & G rather than Aschbacher and will derive 1.6(e) from (d), - rather than the converse, because the derivation of 24.6 from 24.3 in - Aschbacher requires a separate reduction to p-groups to yield 1.6(d), - making it altogether longer than the direct Gaschutz-style proof. - 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.
- -
-Section Transfer.
- -
-Variables (gT aT : finGroupType) (G H : {group gT }).
-Variable alpha : {morphism H >-> aT }.
- -
-Hypotheses (sHG : H \subset G) (abelA : abelian (alpha @* H)).
- -
- -
-Fact transfer_morph_subproof : H \subset alpha @*^-1 (alpha @* H ).
- -
-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).
- -
-Definition transfer g := V repr g.
- -
-

- -

- This is Aschbacher (37.2). -

-Lemma transferM : {in G &, {morph transfer : x y / (x × y)%g >-> x + y }}.
- -
-Canonical transfer_morphism := Morphism transferM.
- -
-

- -

- This is Aschbacher (37.1). -

-Lemma transfer_indep X (rX := transversal_repr 1 X) :
- is_transversal X HG G → {in G , transfer =1 V rX }.
- -
-Section FactorTransfer.
- -
-Variable g : gT.
-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 |.
- -
-Lemma mulg_exp_card_rcosets x : x × (g ^+ n_ x ) \in H :* x.
- -
-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 partHGg : partition HGg HG := orbit_partition actsgHG.
- -
-Let injHGg : {in HGg &, injective cover }.
- -
-Let defHGg : HG :* <[g ]> = cover @: HGg.
- -
-Lemma rcosets_cycle_partition : partition (HG :* <[g ]>) G.
- -
-Variable X : {set gT }.
-Hypothesis trX : is_transversal X (HG :* <[g ]>) G.
- -
-Let sXG : {subset X ≤ G }.
- -
-Lemma rcosets_cycle_transversal : H_g_rcosets @: X = HGg.
- -
- -
-Let injHg: {in X &, injective H_g_rcosets }.
- -
-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).
- -
-End FactorTransfer.
- -
-End Transfer.
-