Library mathcomp.solvable.finmodule
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype bigop ssralg finset fingroup.
From mathcomp Require Import morphism perm finalg action gproduct commutator.
From mathcomp Require Import cyclic.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype bigop ssralg finset fingroup.
From mathcomp Require Import morphism perm finalg action gproduct commutator.
From mathcomp Require Import cyclic.
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_cycle_expansion 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.
Bind Scope ring_scope with fmod_of.
Section OneFinMod.
TODO: understand why FinGroup has to be changed to BaseFinGroup here.
Let f2sub (gT : finGroupType) (A : {group gT}) (abA : abelian A) :=
fun u : fmod_of abA ⇒ let : Fmod x Ax := u in Subg Ax : BaseFinGroup.arg_sort _.
Local Coercion f2sub : fmod_of >-> BaseFinGroup.arg_sort.
Variables (gT : finGroupType) (A : {group gT}) (abelA : abelian A).
Local Notation fmodA := (fmod_of abelA).
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).
#[export]
HB.instance Definition _ := [isSub for fmval].
Local Notation valA := (val: fmodA → gT) (only parsing).
#[export]
HB.instance Definition _ := [Finite of fmodA by <:].
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.
#[export]
HB.instance Definition _ :=
GRing.isZmodule.Build fmodA fmod_addrA fmod_addrC fmod_add0r fmod_addNr.
fun u : fmod_of abA ⇒ let : Fmod x Ax := u in Subg Ax : BaseFinGroup.arg_sort _.
Local Coercion f2sub : fmod_of >-> BaseFinGroup.arg_sort.
Variables (gT : finGroupType) (A : {group gT}) (abelA : abelian A).
Local Notation fmodA := (fmod_of abelA).
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).
#[export]
HB.instance Definition _ := [isSub for fmval].
Local Notation valA := (val: fmodA → gT) (only parsing).
#[export]
HB.instance Definition _ := [Finite of fmodA by <:].
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.
#[export]
HB.instance Definition _ :=
GRing.isZmodule.Build fmodA fmod_addrA fmod_addrC fmod_add0r fmod_addNr.
TODO: Should isZmodule and the like be exported from ssralg
#[export]
HB.instance Definition _ := [finGroupMixin 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.
Bind Scope ring_scope with fmod_of.
Notation "u ^@ x" := (actr u x) : ring_scope.
Notation "''M'" := actr_action (at level 8) : action_scope.
Notation "''M'" := actr_groupAction : groupAction_scope.
Module Exports.
End Exports.
End FiniteModule.
Arguments FiniteModule.fmodK {gT A} abelA [x] Ax.
Arguments FiniteModule.fmvalK {gT A abelA} x.
Arguments FiniteModule.actrK {gT A abelA} x.
Arguments FiniteModule.actrKV {gT A abelA} x.
HB.instance Definition _ := [finGroupMixin 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.
Bind Scope ring_scope with fmod_of.
Notation "u ^@ x" := (actr u x) : ring_scope.
Notation "''M'" := actr_action (at level 8) : action_scope.
Notation "''M'" := actr_groupAction : groupAction_scope.
Module Exports.
End Exports.
End FiniteModule.
Arguments FiniteModule.fmodK {gT A} abelA [x] Ax.
Arguments FiniteModule.fmvalK {gT A abelA} x.
Arguments FiniteModule.actrK {gT A abelA} x.
Arguments FiniteModule.actrKV {gT A abelA} x.
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.
Local Notation fmod := (fmod 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.
Local Notation fmod := (fmod 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)).
Local Notation HG := (rcosets (gval H) (gval G)).
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)).
Local Notation HG := (rcosets (gval H) (gval G)).
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.
Local Notation defHgX := rcosets_cycle_transversal.
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.
Local Notation defHgX := rcosets_cycle_transversal.
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.