Library hall

  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.                           


Import GroupScope.

Section Hall.

Implicit Type gT : finGroupType.

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

Theorem SchurZassenhaus_trans_sol : forall 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 : forall 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 : forall pi gT (G : {group gT}),
  solvable G -> exists2 H : {group gT}, pi.-Hall(G) H
                & forall 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 : forall pi (G : {group gT}),
  solvable G -> exists H : {group gT}, pi.-Hall(G) H.

Corollary Hall_trans : forall 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 : forall 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 : forall 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 : forall 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 : forall pi (G K H : {group gT}),
  solvable K -> K <| G -> pi.-Hall(K) H -> K * 'N_G(H) = G.

End HallCorollaries.

Section InternalAction.

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

 Part of Aschbacher (18.7.4). 
Lemma coprime_norm_cent : forall A G,
  A \subset 'N(G) -> coprime #|G| #|A| -> 'N_G(A) = 'C_G(A).

 This is B & G, Proposition 1.5(a) 
Proposition coprime_Hall_exists : forall A G,
  A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  exists2 H : {group gT}, pi.-Hall(G) H & A \subset 'N(H).

 This is B & G, Proposition 1.5(c) 
Proposition coprime_Hall_trans : forall A G H1 H2,
  A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  pi.-Hall(G) H1 -> A \subset 'N(H1) ->
  pi.-Hall(G) H2 -> A \subset 'N(H2) ->
  exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x.

 A complement to the above: 'C(A) acts on 'Nby(A) 
Lemma norm_conj_cent : forall A G x, x \in 'C(A) ->
  (A \subset 'N(G :^ x)) = (A \subset 'N(G)).

 Strongest version of the centraliser lemma -- not found in textbooks!  
 Obviously, the solvability condition could be removed once we have the 
 Odd Order Theorem.                                                     
Lemma strongest_coprime_quotient_cent : forall A G H,
    let R := H :&: [~: G, A] in
    A \subset 'N(H) -> R \subset G -> coprime #|R| #|A| ->
    solvable R || solvable A ->
  'C_G(A) / H = 'C_(G / H)(A / H).

 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.                                                    
Lemma coprime_norm_quotient_cent : forall A G H,
    A \subset 'N(G) -> A \subset 'N(H) -> coprime #|H| #|A| -> solvable H ->
  'C_G(A) / H = 'C_(G / H)(A / H).

 A useful consequence (similar to Ex. 6.1 in Aschbacher) of the stronger   
 theorem. 
Lemma coprime_cent_mulG : forall A G H,
     A \subset 'N(G) -> A \subset 'N(H) -> G \subset 'N(H) ->
     coprime #|H| #|A| -> solvable H ->
  'C_(H * G)(A) = 'C_H(A) * 'C_G(A).

 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.                                 
Lemma quotient_TI_subcent : forall K G H,
    G \subset 'N(K) -> G \subset 'N(H) -> K :&: H = 1 ->
  'C_K(G) / H = 'C_(K / H)(G / H).

 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.    
Proposition coprime_quotient_cent : forall A G H,
    H \subset G -> A \subset 'N(H) -> coprime #|G| #|A| -> solvable G ->
  'C_G(A) / H = 'C_(G / H)(A / H).

 This is B & G, Proposition 1.5(e). 
Proposition coprime_comm_pcore : forall A G K,
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
    pi^'.-Hall(G) K -> K \subset 'C_G(A) ->
  [~: G, A] \subset 'O_pi(G).

End InternalAction.

 This is B & G, Proposition 1.5(b). 
Proposition coprime_Hall_subset :
  forall pi (gT : finGroupType) (A G X : {group gT}),
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
    X \subset G -> pi.-group X -> A \subset 'N(X) ->
  exists 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 solG' : solvable G' := morphim_sol _ solG.


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

Lemma ext_coprime_Hall_trans : forall 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 : forall (H : {group gT}) x,
    H \subset G -> x \in 'C_(G | to)(A) ->
  [acts A, on H :^ x | to] = [acts A, on H | to].

Lemma ext_coprime_Hall_subset : forall X : {group gT},
    X \subset G -> pi.-group X -> [acts A, on X | to] ->
  exists 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.                                
Lemma ext_coprime_quotient_cent : forall H : {group gT},
    H \subset G -> [acts A, on H | to] -> coprime #|H| #|A| -> solvable H ->
 'C_(|to)(A) / H = 'C_(|to / H)(A).

End ExternalAction.

Section SylowSolvableAct.

Variables (gT : finGroupType) (p : nat).
Implicit Types A B G : {group gT}.

Lemma sol_coprime_Sylow_exists : forall A G,
    solvable A -> A \subset 'N(G) -> coprime #|G| #|A| ->
  exists2 P : {group gT}, p.-Sylow(G) P & A \subset 'N(P).

Lemma sol_coprime_Sylow_trans : forall A G,
    solvable A -> A \subset 'N(G) -> coprime #|G| #|A| ->
  [transitive 'C_G(A), on [set P \in 'Syl_p(G) | A \subset 'N(P)] | 'JG].

Lemma sol_coprime_Sylow_subset : forall A G X : {group gT},
  A \subset 'N(G) -> coprime #|G| #|A| -> solvable A ->
  X \subset G -> p.-group X -> A \subset 'N(X) ->
  exists P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].

End SylowSolvableAct.