# Library mathcomp.solvable.hall

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

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import fintype finset prime fingroup morphism.
From mathcomp Require Import automorphism quotient action gproduct gfunctor.
From mathcomp Require Import commutator center pgroup finmodule nilpotent.
From mathcomp Require Import sylow 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 H H <| G [splits G, over H].

Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
solvable H K \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 A A \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 G exists2 H : {group gT}, pi.-Hall(G) H
& K : {group gT}, K \subset G pi.-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 G pi.-Hall(G) H1 pi.-Hall(G) H2
exists2 x, x \in G & H1 :=: H2 :^ x.

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

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

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

Lemma Hall_Frattini_arg pi (G K H : {group gT}) :
solvable K K <| G pi.-Hall(K) H K × '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).
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.