Library mathcomp.solvable.sylow
(* (c) Copyright 2006-2015 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.
The Sylow theorem and its consequences, including the Frattini argument,
the nilpotence of p-groups, and the Baer-Suzuki theorem.
This file also defines:
Zgroup G == G is a Z-group, i.e., has only cyclic Sylow p-subgroups.
Set Implicit Arguments.
Import GroupScope.
The mod p lemma for the action of p-groups.
Section ModP.
Variable (aT : finGroupType) (sT : finType) (D : {group aT}).
Variable to : action D sT.
Lemma pgroup_fix_mod (p : nat) (G : {group aT}) (S : {set sT}) :
p.-group G → [acts G, on S | to] → #|S| = #|'Fix_(S | to)(G)| %[mod p].
End ModP.
Section ModularGroupAction.
Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).
Variables (to : groupAction D R) (p : nat).
Implicit Types (G H : {group aT}) (M : {group rT}).
Lemma nontrivial_gacent_pgroup G M :
p.-group G → p.-group M → {acts G, on group M | to} →
M :!=: 1 → 'C_(M | to)(G) :!=: 1.
Lemma pcore_sub_astab_irr G M :
p.-group M → M \subset R → acts_irreducibly G M to →
'O_p(G) \subset 'C_G(M | to).
Lemma pcore_faithful_irr_act G M :
p.-group M → M \subset R → acts_irreducibly G M to →
[faithful G, on M | to] →
'O_p(G) = 1.
End ModularGroupAction.
Section Sylow.
Variables (p : nat) (gT : finGroupType) (G : {group gT}).
Implicit Types P Q H K : {group gT}.
Theorem Sylow's_theorem :
[/\ ∀ P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
[transitive G, on 'Syl_p(G) | 'JG],
∀ P, p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|
& prime p → #|'Syl_p(G)| %% p = 1%N].
Lemma max_pgroup_Sylow P : [max P | p.-subgroup(G) P] = p.-Sylow(G) P.
Lemma Sylow_superset Q :
Q \subset G → p.-group Q → {P : {group gT} | p.-Sylow(G) P & Q \subset P}.
Lemma Sylow_exists : {P : {group gT} | p.-Sylow(G) P}.
Lemma Syl_trans : [transitive G, on 'Syl_p(G) | 'JG].
Lemma Sylow_trans P Q :
p.-Sylow(G) P → p.-Sylow(G) Q → exists2 x, x \in G & Q :=: P :^ x.
Lemma Sylow_subJ P Q :
p.-Sylow(G) P → Q \subset G → p.-group Q →
exists2 x, x \in G & Q \subset P :^ x.
Lemma Sylow_Jsub P Q :
p.-Sylow(G) P → Q \subset G → p.-group Q →
exists2 x, x \in G & Q :^ x \subset P.
Lemma card_Syl P : p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|.
Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|.
Lemma card_Syl_mod : prime p → #|'Syl_p(G)| %% p = 1%N.
Lemma Frattini_arg H P : G <| H → p.-Sylow(G) P → G × 'N_H(P) = H.
End Sylow.
Section MoreSylow.
Variables (gT : finGroupType) (p : nat).
Implicit Types G H P : {group gT}.
Lemma Sylow_setI_normal G H P :
G <| H → p.-Sylow(H) P → p.-Sylow(G) (G :&: P).
Lemma normal_sylowP G :
reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G)
(#|'Syl_p(G)| == 1%N).
Lemma trivg_center_pgroup P : p.-group P → 'Z(P) = 1 → P :=: 1.
Lemma p2group_abelian P : p.-group P → logn p #|P| ≤ 2 → abelian P.
Lemma card_p2group_abelian P : prime p → #|P| = (p ^ 2)%N → abelian P.
Lemma Sylow_transversal_gen (T : {set {group gT}}) G :
(∀ P, P \in T → P \subset G) →
(∀ p, p \in \pi(G) → exists2 P, P \in T & p.-Sylow(G) P) →
<< \bigcup_(P in T) P >> = G.
Lemma Sylow_gen G : <<\bigcup_(P : {group gT} | Sylow G P) P>> = G.
End MoreSylow.
Section SomeHall.
Variable gT : finGroupType.
Implicit Types (p : nat) (pi : nat_pred) (G H K P R : {group gT}).
Lemma Hall_pJsub p pi G H P :
pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
exists2 x, x \in G & P :^ x \subset H.
Lemma Hall_psubJ p pi G H P :
pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
exists2 x, x \in G & P \subset H :^ x.
Lemma Hall_setI_normal pi G K H :
K <| G → pi.-Hall(G) H → pi.-Hall(K) (H :&: K).
Lemma coprime_mulG_setI_norm H G K R :
K × R = G → G \subset 'N(H) → coprime #|K| #|R| →
(K :&: H) × (R :&: H) = G :&: H.
End SomeHall.
Section Nilpotent.
Variable gT : finGroupType.
Implicit Types (G H K P L : {group gT}) (p q : nat).
Lemma pgroup_nil p P : p.-group P → nilpotent P.
Lemma pgroup_sol p P : p.-group P → solvable P.
Lemma small_nil_class G : nil_class G ≤ 5 → nilpotent G.
Lemma nil_class2 G : (nil_class G ≤ 2) = (G^`(1) \subset 'Z(G)).
Lemma nil_class3 G : (nil_class G ≤ 3) = ('L_3(G) \subset 'Z(G)).
Lemma nilpotent_maxp_normal pi G H :
nilpotent G → [max H | pi.-subgroup(G) H] → H <| G.
Lemma nilpotent_Hall_pcore pi G H :
nilpotent G → pi.-Hall(G) H → H :=: 'O_pi(G).
Lemma nilpotent_pcore_Hall pi G : nilpotent G → pi.-Hall(G) 'O_pi(G).
Lemma nilpotent_pcoreC pi G : nilpotent G → 'O_pi(G) \x 'O_pi^'(G) = G.
Lemma sub_nilpotent_cent2 H K G :
nilpotent G → K \subset G → H \subset G → coprime #|K| #|H| →
H \subset 'C(K).
Lemma pi_center_nilpotent G : nilpotent G → \pi('Z(G)) = \pi(G).
Lemma Sylow_subnorm p G P : p.-Sylow('N_G(P)) P = p.-Sylow(G) P.
End Nilpotent.
Lemma nil_class_pgroup (gT : finGroupType) (p : nat) (P : {group gT}) :
p.-group P → nil_class P ≤ maxn 1 (logn p #|P|).-1.
Definition Zgroup (gT : finGroupType) (A : {set gT}) :=
[∀ (V : {group gT} | Sylow A V), cyclic V].
Section Zgroups.
Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
Implicit Types G H K : {group gT}.
Lemma ZgroupS G H : H \subset G → Zgroup G → Zgroup H.
Lemma morphim_Zgroup G : Zgroup G → Zgroup (f @* G).
Lemma nil_Zgroup_cyclic G : Zgroup G → nilpotent G → cyclic G.
End Zgroups.
Section NilPGroups.
Variables (p : nat) (gT : finGroupType).
Implicit Type G P N : {group gT}.
Variable (aT : finGroupType) (sT : finType) (D : {group aT}).
Variable to : action D sT.
Lemma pgroup_fix_mod (p : nat) (G : {group aT}) (S : {set sT}) :
p.-group G → [acts G, on S | to] → #|S| = #|'Fix_(S | to)(G)| %[mod p].
End ModP.
Section ModularGroupAction.
Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).
Variables (to : groupAction D R) (p : nat).
Implicit Types (G H : {group aT}) (M : {group rT}).
Lemma nontrivial_gacent_pgroup G M :
p.-group G → p.-group M → {acts G, on group M | to} →
M :!=: 1 → 'C_(M | to)(G) :!=: 1.
Lemma pcore_sub_astab_irr G M :
p.-group M → M \subset R → acts_irreducibly G M to →
'O_p(G) \subset 'C_G(M | to).
Lemma pcore_faithful_irr_act G M :
p.-group M → M \subset R → acts_irreducibly G M to →
[faithful G, on M | to] →
'O_p(G) = 1.
End ModularGroupAction.
Section Sylow.
Variables (p : nat) (gT : finGroupType) (G : {group gT}).
Implicit Types P Q H K : {group gT}.
Theorem Sylow's_theorem :
[/\ ∀ P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
[transitive G, on 'Syl_p(G) | 'JG],
∀ P, p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|
& prime p → #|'Syl_p(G)| %% p = 1%N].
Lemma max_pgroup_Sylow P : [max P | p.-subgroup(G) P] = p.-Sylow(G) P.
Lemma Sylow_superset Q :
Q \subset G → p.-group Q → {P : {group gT} | p.-Sylow(G) P & Q \subset P}.
Lemma Sylow_exists : {P : {group gT} | p.-Sylow(G) P}.
Lemma Syl_trans : [transitive G, on 'Syl_p(G) | 'JG].
Lemma Sylow_trans P Q :
p.-Sylow(G) P → p.-Sylow(G) Q → exists2 x, x \in G & Q :=: P :^ x.
Lemma Sylow_subJ P Q :
p.-Sylow(G) P → Q \subset G → p.-group Q →
exists2 x, x \in G & Q \subset P :^ x.
Lemma Sylow_Jsub P Q :
p.-Sylow(G) P → Q \subset G → p.-group Q →
exists2 x, x \in G & Q :^ x \subset P.
Lemma card_Syl P : p.-Sylow(G) P → #|'Syl_p(G)| = #|G : 'N_G(P)|.
Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|.
Lemma card_Syl_mod : prime p → #|'Syl_p(G)| %% p = 1%N.
Lemma Frattini_arg H P : G <| H → p.-Sylow(G) P → G × 'N_H(P) = H.
End Sylow.
Section MoreSylow.
Variables (gT : finGroupType) (p : nat).
Implicit Types G H P : {group gT}.
Lemma Sylow_setI_normal G H P :
G <| H → p.-Sylow(H) P → p.-Sylow(G) (G :&: P).
Lemma normal_sylowP G :
reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G)
(#|'Syl_p(G)| == 1%N).
Lemma trivg_center_pgroup P : p.-group P → 'Z(P) = 1 → P :=: 1.
Lemma p2group_abelian P : p.-group P → logn p #|P| ≤ 2 → abelian P.
Lemma card_p2group_abelian P : prime p → #|P| = (p ^ 2)%N → abelian P.
Lemma Sylow_transversal_gen (T : {set {group gT}}) G :
(∀ P, P \in T → P \subset G) →
(∀ p, p \in \pi(G) → exists2 P, P \in T & p.-Sylow(G) P) →
<< \bigcup_(P in T) P >> = G.
Lemma Sylow_gen G : <<\bigcup_(P : {group gT} | Sylow G P) P>> = G.
End MoreSylow.
Section SomeHall.
Variable gT : finGroupType.
Implicit Types (p : nat) (pi : nat_pred) (G H K P R : {group gT}).
Lemma Hall_pJsub p pi G H P :
pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
exists2 x, x \in G & P :^ x \subset H.
Lemma Hall_psubJ p pi G H P :
pi.-Hall(G) H → p \in pi → P \subset G → p.-group P →
exists2 x, x \in G & P \subset H :^ x.
Lemma Hall_setI_normal pi G K H :
K <| G → pi.-Hall(G) H → pi.-Hall(K) (H :&: K).
Lemma coprime_mulG_setI_norm H G K R :
K × R = G → G \subset 'N(H) → coprime #|K| #|R| →
(K :&: H) × (R :&: H) = G :&: H.
End SomeHall.
Section Nilpotent.
Variable gT : finGroupType.
Implicit Types (G H K P L : {group gT}) (p q : nat).
Lemma pgroup_nil p P : p.-group P → nilpotent P.
Lemma pgroup_sol p P : p.-group P → solvable P.
Lemma small_nil_class G : nil_class G ≤ 5 → nilpotent G.
Lemma nil_class2 G : (nil_class G ≤ 2) = (G^`(1) \subset 'Z(G)).
Lemma nil_class3 G : (nil_class G ≤ 3) = ('L_3(G) \subset 'Z(G)).
Lemma nilpotent_maxp_normal pi G H :
nilpotent G → [max H | pi.-subgroup(G) H] → H <| G.
Lemma nilpotent_Hall_pcore pi G H :
nilpotent G → pi.-Hall(G) H → H :=: 'O_pi(G).
Lemma nilpotent_pcore_Hall pi G : nilpotent G → pi.-Hall(G) 'O_pi(G).
Lemma nilpotent_pcoreC pi G : nilpotent G → 'O_pi(G) \x 'O_pi^'(G) = G.
Lemma sub_nilpotent_cent2 H K G :
nilpotent G → K \subset G → H \subset G → coprime #|K| #|H| →
H \subset 'C(K).
Lemma pi_center_nilpotent G : nilpotent G → \pi('Z(G)) = \pi(G).
Lemma Sylow_subnorm p G P : p.-Sylow('N_G(P)) P = p.-Sylow(G) P.
End Nilpotent.
Lemma nil_class_pgroup (gT : finGroupType) (p : nat) (P : {group gT}) :
p.-group P → nil_class P ≤ maxn 1 (logn p #|P|).-1.
Definition Zgroup (gT : finGroupType) (A : {set gT}) :=
[∀ (V : {group gT} | Sylow A V), cyclic V].
Section Zgroups.
Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
Implicit Types G H K : {group gT}.
Lemma ZgroupS G H : H \subset G → Zgroup G → Zgroup H.
Lemma morphim_Zgroup G : Zgroup G → Zgroup (f @* G).
Lemma nil_Zgroup_cyclic G : Zgroup G → nilpotent G → cyclic G.
End Zgroups.
Section NilPGroups.
Variables (p : nat) (gT : finGroupType).
Implicit Type G P N : {group gT}.
B & G 1.22 p.9