- -

Library mathcomp.solvable.hall

- -

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

- -

- 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.
-