Library mathcomp.solvable.finmodule
+ +
+(* (c) Copyright 2006-2016 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.
+ +
+
+
++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.
+