Library mathcomp.solvable.hall
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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}.
+ +
+
+
++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)
+
+
+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).
+ +
+
+
++ 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 \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)
+
+
+
+
+ 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).
+ +
+
+
++ 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 \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).
+ +
+
+
++ 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).
+ +
+
+
++ 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).
+ +
+
+
++ 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.
+ +
+
+
++ 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.
+ +
+
+
++ 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.
+
++ 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.
+