# Library mathcomp.solvable.finmodule

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

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

Definition fmod_zmodMixin :=
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.

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