# Library mathcomp.solvable.sylow

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
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}.

B & G 1.22 p.9
Lemma normal_pgroup r P N :
p.-group P N <| P r logn p #|N|
Q : {group gT}, [/\ Q \subset N, Q <| P & #|Q| = (p ^ r)%N].

Theorem Baer_Suzuki x G :
x \in G ( y, y \in G p.-group <<[set x; x ^ y]>>)
x \in 'O_p(G).

End NilPGroups.