Library finmodule

  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        
 Measchke's theorem, the coprime abelian centraliser/commutator trivial     
 intrsection theorem, from which we will derive 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 Burside 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.      
  rcosets_transversal G H X == the function X : {set gT} -> gT defines a    
                   transversal of the right cosets of H in G: it maps each  
                   coset H :* x to some y_x \in H :* x, for each x \in G.   
                   The Lemma transfer_indep states that the transfer        
                   morphism can be expanded using any transversal.          
  rcosets_pcycle_transversal G H g X == X is a transversal of the orbits of 
                   the regular action of the cycle <[g]> generated by g on  
                   the set of right cosets of H if H \subset G and g \in G, 
                   and more generally the function r mapping x : gT to      
                   rcosets (H :* x) <[g]> is (constructively) a bijection   
                   from X to a partition of a partition of G: we have       
                   {in X &, injective r}, X \subset G  and                  
                   G \subset H * X * <[g]>. The transfer_pcycle_def Lemma   
                   gives a simplified expansion of the transfer morphism,   
                   given a set X with this property.                        
  rcosets_pcycle_transversal_witness G H g == the sigma Type associated     
                   with the predicate above; it encapsulates a set X, the   
                   rcosets_pcycle_transversal G H g X property, and an      
                   abbreviation n_ x for the coefficient #|r x| (with r     
                   defined as above), which is used in the expansion        
                   supplied by transfer_pcycle_def.                         
 For applications that do not require a specific transversal, the           
 rcosets_pcycle_transversal_exists Lemma provides a default instance of an  
 rcosets_pcycle_transversal_witness.                                        


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 _.
Local Coercion f2sub : fmod_of >-> FinGroup.arg_sort.

Variables (gT : finGroupType) (A : {group gT}) (abelA : abelian A).
Local Notation fmodA := (fmod_of abelA).
Implicit Types x y z : gT.
Implicit Types u v w : fmodA.

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

Definition fmval u := val (f2sub u).
Canonical Structure fmod_subType := [subType for fmval by @fmod_of_rect _ _ _].
Local Notation valA := (@val _ _ fmod_subType) (only parsing).
Definition fmod_eqMixin := Eval hnf in [eqMixin of fmodA by <:].
Canonical Structure fmod_eqType := Eval hnf in EqType fmodA fmod_eqMixin.
Definition fmod_choiceMixin := [choiceMixin of fmodA by <:].
Canonical Structure fmod_choiceType :=
  Eval hnf in ChoiceType fmodA fmod_choiceMixin.
Definition fmod_countMixin := [countMixin of fmodA by <:].
Canonical Structure fmod_countType :=
  Eval hnf in CountType fmodA fmod_countMixin.
Canonical Structure fmod_subCountType := Eval hnf in [subCountType of fmodA].
Definition fmod_finMixin := [finMixin of fmodA by <:].
Canonical Structure fmod_finType := Eval hnf in FinType fmodA fmod_finMixin.
Canonical Structure 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).

Lemma fmod_add0r : left_id (sub2f 1) fmod_add.

Lemma fmod_addrA : associative fmod_add.

Lemma fmod_addNr : left_inverse (sub2f 1) fmod_opp fmod_add.

Lemma fmod_addrC : commutative fmod_add.

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

Lemma fmodP : forall u, val u \in A.

Lemma fmod_inj : injective fmval.

Lemma congr_fmod : forall 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 Structure fmval_morphism := @Morphism _ _ setT fmval (in2W fmvalA).

Definition fmval_sum := big_morph fmval fmvalA fmval0.

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

Lemma fmodKcond : forall 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 Structure fmod_morphism := Morphism fmodM.
Lemma fmodX : forall 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 : forall u x,
  val (u ^@ x) = if x \in 'N(A) then val u ^ x else val u.

Lemma fmvalJ : forall u x, x \in 'N(A) -> val (u ^@ x) = val u ^ x.

Lemma fmodJ : forall x y, y \in 'N(A) -> fmod (x ^ y) = fmod x ^@ y.

Lemma actr_is_action : is_action 'N(A) actr.

Canonical Structure actr_action := Action actr_is_action.
Notation "''M'" := actr_action (at level 0) : action_scope.

Lemma act0r : forall x, 0 ^@ x = 0.

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

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

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

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

Lemma actr_is_groupAction : is_groupAction setT 'M.

Canonical Structure actr_groupAction := GroupAction actr_is_groupAction.
Notation "''M'" := actr_groupAction (at level 0) : groupAction_scope.

Lemma actr1 : forall u, u ^@ 1 = u.

Lemma actrM : {in 'N(A) &, forall x y u, u ^@ (x * y) = u ^@ x ^@ y}.

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

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

End OneFinMod.

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

End FiniteModule.

Canonical Structure FiniteModule.fmod_subType.
Canonical Structure FiniteModule.fmod_eqType.
Canonical Structure FiniteModule.fmod_choiceType.
Canonical Structure FiniteModule.fmod_countType.
Canonical Structure FiniteModule.fmod_finType.
Canonical Structure FiniteModule.fmod_subCountType.
Canonical Structure FiniteModule.fmod_subFinType.
Canonical Structure FiniteModule.fmod_zmodType.
Canonical Structure FiniteModule.fmod_finZmodType.
Canonical Structure FiniteModule.fmod_baseFinGroupType.
Canonical Structure 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|).



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] &,
  forall 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 : forall (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)).

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



Definition transfer g := V repr g.

 Aschbacher 37.2 
Lemma transferM : {in G &, {morph transfer : x y / (x * y)%g >-> x + y}}.

Canonical Structure transfer_morphism := Morphism transferM.

Definition coset_transversal X :=
  {in rcosets H G, forall Hx : {set gT}, X Hx \in Hx}.

 Aschbacher 37.1 
Lemma transfer_indep : forall X, coset_transversal X -> {in G, transfer =1 V X}.

Section FactorTransfer.

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

Let Gcycg : <[g]> \subset G.

Lemma mulg_exp_card_rcosets : forall x, x * (g ^+ n_ x) \in H :* x.

Definition rcosets_pcycle_transversal (X : {set gT}) :=
  [/\ {in X &, injective H_g_rcosets}, X \subset G & G \subset H * X * <[ g ]>].

CoInductive rcosets_pcycle_transversal_witness : Prop :=
   RcosetPcycleTransversalWitness X (n_ := n_) of rcosets_pcycle_transversal X.

Lemma rcosets_pcycle_transversal_exists : rcosets_pcycle_transversal_witness.

Variable X : {set gT}.
Hypothesis trX : rcosets_pcycle_transversal X.

Lemma im_rcosets_pcycle_transversal :
  H_g_rcosets @: X = orbit 'Rs <[g]> @: rcosets H G.
Local Notation imHg_eq := im_rcosets_pcycle_transversal.

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

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

End FactorTransfer.

End Transfer.