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.

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 abAlet : Fmod x Ax := u in Subg Ax : BaseFinGroup.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).
#[export]
HB.instance Definition _ := [isSub for fmval].
#[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.

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).
This is Aschbacher (37.1).