(Joint Center)Library MathComp.sylow

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype prime.
Require Import bigop finset fingroup morphism automorphism quotient action.
Require Import cyclic gproduct commutator pgroup center nilpotent.

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 Gp.-group M{acts G, on group M | to}
  M :!=: 1 → 'C_(M | to)(G) :!=: 1.

Lemma pcore_sub_astab_irr G M :
    p.-group MM \subset Racts_irreducibly G M to
  'O_p(G) \subset 'C_G(M | to).

Lemma pcore_faithful_irr_act G M :
    p.-group MM \subset Racts_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 Gp.-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) Pp.-Sylow(G) Qexists2 x, x \in G & Q :=: P :^ x.

Lemma Sylow_subJ P Q :
    p.-Sylow(G) PQ \subset Gp.-group Q
  exists2 x, x \in G & Q \subset P :^ x.

Lemma Sylow_Jsub P Q :
    p.-Sylow(G) PQ \subset Gp.-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 <| Hp.-Sylow(G) PG × '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 <| Hp.-Sylow(H) Pp.-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 Plogn p #|P| 2 → abelian P.

Lemma card_p2group_abelian P : prime p#|P| = (p ^ 2)%Nabelian P.

Lemma Sylow_transversal_gen (T : {set {group gT}}) G :
    ( P, P \in TP \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) Hp \in piP \subset Gp.-group P
  exists2 x, x \in G & P :^ x \subset H.

Lemma Hall_psubJ p pi G H P :
    pi.-Hall(G) Hp \in piP \subset Gp.-group P
  exists2 x, x \in G & P \subset H :^ x.

Lemma Hall_setI_normal pi G K H :
  K <| Gpi.-Hall(G) Hpi.-Hall(K) (H :&: K).

Lemma coprime_mulG_setI_norm H G K R :
    K × R = GG \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 Pnilpotent P.

Lemma pgroup_sol p P : p.-group Psolvable 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 Gpi.-Hall(G) HH :=: 'O_pi(G).

Lemma nilpotent_pcore_Hall pi G : nilpotent Gpi.-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 GK \subset GH \subset Gcoprime #|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 Pnil_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 GZgroup GZgroup H.

Lemma morphim_Zgroup G : Zgroup GZgroup (f @* G).

Lemma nil_Zgroup_cyclic G : Zgroup Gnilpotent Gcyclic 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 PN <| Pr 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 Gp.-group <<[set x; x ^ y]>>) →
  x \in 'O_p(G).

End NilPGroups.