(Joint Center)Library MathComp.finmodule

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype bigop ssralg finset fingroup morphism perm.
Require Import finalg action gproduct commutator 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, 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 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 abAlet : 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) (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].
Local Notation valA := (@val _ _ fmod_subType) (only parsing).
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 = vfmval 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.
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 :&: Pexists2 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.

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).