Library mathcomp.solvable.finmodule
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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.
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.
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.
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.
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.