# Library MathComp.hall

(* (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 div fintype finset.
Require Import prime fingroup morphism automorphism quotient action gproduct.
Require Import commutator center pgroup finmodule nilpotent sylow.
Require Import abelian maximal.

In this files we prove the Schur-Zassenhaus splitting and transitivity theorems (under solvability assumptions), then derive P. Hall's generalization of Sylow's theorem to solvable groups and its corollaries, in particular the theory of coprime action. We develop both the theory of coprime action of a solvable group on Sylow subgroups (as in Aschbacher 18.7), and that of coprime action on Hall subgroups of a solvable group as per B & G, Proposition 1.5; however we only support external group action (as opposed to internal action by conjugation) for the latter case because it is much harder to apply in practice.

Set Implicit Arguments.

Import GroupScope.

Section Hall.

Implicit Type gT : finGroupType.

Theorem SchurZassenhaus_split gT (G H : {group gT}) :
Hall G HH <| G[splits G, over H].

Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
solvable HK \subset 'N(H)K1 \subset H × K
coprime #|H| #|K|#|K1| = #|K|
exists2 x, x \in H & K1 :=: K :^ x.

Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) :
solvable AA \subset 'N(G)B \subset A <*> G
coprime #|G| #|A|#|A| = #|B|
exists2 x, x \in G & B :=: A :^ x.

Lemma Hall_exists_subJ pi gT (G : {group gT}) :
solvable Gexists2 H : {group gT}, pi.-Hall(G) H
& K : {group gT}, K \subset Gpi.-group K
exists2 x, x \in G & K \subset H :^ x.

End Hall.

Section HallCorollaries.

Variable gT : finGroupType.

Corollary Hall_exists pi (G : {group gT}) :
solvable G H : {group gT}, pi.-Hall(G) H.

Corollary Hall_trans pi (G H1 H2 : {group gT}) :
solvable Gpi.-Hall(G) H1pi.-Hall(G) H2
exists2 x, x \in G & H1 :=: H2 :^ x.

Corollary Hall_superset pi (G K : {group gT}) :
solvable GK \subset Gpi.-group K
exists2 H : {group gT}, pi.-Hall(G) H & K \subset H.

Corollary Hall_subJ pi (G H K : {group gT}) :
solvable Gpi.-Hall(G) HK \subset Gpi.-group K
exists2 x, x \in G & K \subset H :^ x.

Corollary Hall_Jsub pi (G H K : {group gT}) :
solvable Gpi.-Hall(G) HK \subset Gpi.-group K
exists2 x, x \in G & K :^ x \subset H.

Lemma Hall_Frattini_arg pi (G K H : {group gT}) :
solvable KK <| Gpi.-Hall(K) HK × 'N_G(H) = G.

End HallCorollaries.

Section InternalAction.

Variables (pi : nat_pred) (gT : finGroupType).
Implicit Types G H K A X : {group gT}.

Part of Aschbacher (18.7.4).
This is B & G, Proposition 1.5(a)
This is B & G, Proposition 1.5(c)
A complement to the above: 'C(A) acts on 'Nby(A)
Strongest version of the centraliser lemma -- not found in textbooks! Obviously, the solvability condition could be removed once we have the Odd Order Theorem.
A weaker but more practical version, still stronger than the usual form (viz. Aschbacher 18.7.4), similar to the one needed in Aschbacher's proof of Thompson factorization. Note that the coprime and solvability assumptions could be further weakened to H :&: G (and hence become trivial if H and G are TI). However, the assumption that A act on G is needed in this case.
A useful consequence (similar to Ex. 6.1 in Aschbacher) of the stronger theorem.
Another special case of the strong coprime quotient lemma; not found in textbooks, but nevertheless used implicitly throughout B & G, sometimes justified by switching to external action.
This is B & G, Proposition 1.5(d): the more traditional form of the lemma above, with the assumption H <| G weakened to H \subset G. The stronger coprime and solvability assumptions are easier to satisfy in practice.
This is B & G, Proposition 1.5(e).
This is B & G, Proposition 1.5(b).
Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) :
A \subset 'N(G)coprime #|G| #|A|solvable G
X \subset Gpi.-group XA \subset 'N(X)
H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].

Section ExternalAction.

Variables (pi : nat_pred) (aT gT : finGroupType).
Variables (A : {group aT}) (G : {group gT}) (to : groupAction A G).

Section FullExtension.

Local Notation inA := (sdpair2 to).
Local Notation inG := (sdpair1 to).
Local Notation A' := (inA @* gval A).
Local Notation G' := (inG @* gval G).
Let injG : 'injm inG := injm_sdpair1 _.
Let injA : 'injm inA := injm_sdpair2 _.

Hypotheses (coGA : coprime #|G| #|A|) (solG : solvable G).

Lemma external_action_im_coprime : coprime #|G'| #|A'|.

Let coGA' := external_action_im_coprime.

Let solG' : solvable G' := morphim_sol _ solG.

Let nGA' := im_sdpair_norm to.

Lemma ext_coprime_Hall_exists :
exists2 H : {group gT}, pi.-Hall(G) H & [acts A, on H | to].

Lemma ext_coprime_Hall_trans (H1 H2 : {group gT}) :
pi.-Hall(G) H1[acts A, on H1 | to]
pi.-Hall(G) H2[acts A, on H2 | to]
exists2 x, x \in 'C_(G | to)(A) & H1 :=: H2 :^ x.

Lemma ext_norm_conj_cent (H : {group gT}) x :
H \subset Gx \in 'C_(G | to)(A)
[acts A, on H :^ x | to] = [acts A, on H | to].

Lemma ext_coprime_Hall_subset (X : {group gT}) :
X \subset Gpi.-group X[acts A, on X | to]
H : {group gT},
[/\ pi.-Hall(G) H, [acts A, on H | to] & X \subset H].

End FullExtension.

We only prove a weaker form of the coprime group action centraliser lemma, because it is more convenient in practice to make G the range of the action, whence G both contains H and is stable under A. However we do restrict the coprime/solvable assumptions to H, and we do not require that G normalize H.