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).
Lemma coprime_norm_cent 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 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 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 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 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 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 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 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 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 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 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) →
  ∃ 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.

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 G → x \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 G → pi.-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.
Lemma ext_coprime_quotient_cent (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 X : {group gT}.

Lemma sol_coprime_Sylow_exists 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 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 A G X :
  A \subset 'N(G) → coprime #|G| #|A| → solvable A →
  X \subset G → p.-group X → A \subset 'N(X) →
  ∃ P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].

End SylowSolvableAct.