Library sylow

   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.  


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 : forall (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}.
Implicit Types M : {group rT}.

Lemma nontrivial_gacent_pgroup : forall 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 : forall 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 : forall 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 :
  [/\ forall P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
      [transitive G, on 'Syl_p(G) | 'JG],
      forall P, p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)|
   & prime p -> #|'Syl_p(G)| %% p = 1%N].

Lemma max_pgroup_Sylow :
  forall P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P.

Lemma Sylow_superset : forall 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 : forall P Q,
  p.-Sylow(G) P -> p.-Sylow(G) Q -> exists2 x, x \in G & Q :=: P :^ x.

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

Lemma Sylow_Jsub : forall P Q,
  p.-Sylow(G) P -> Q \subset G -> p.-group Q ->
  exists2 x, x \in G & Q :^ x \subset P.

Lemma card_Syl : forall 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 : forall 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 : forall G H P,
  G <| H -> p.-Sylow(H) P -> p.-Sylow(G) (G :&: P).

Lemma normal_sylowP : forall G,
  reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G)
          (#|'Syl_p(G)| == 1%N).

Lemma trivg_center_pgroup : forall P, p.-group P -> 'Z(P) = 1 -> P :=: 1.

Lemma p2group_abelian : forall P, p.-group P -> logn p #|P| <= 2 -> abelian P.

Lemma card_p2group_abelian : forall P, prime p -> #|P| = (p ^ 2)%N -> abelian P.

Lemma Sylow_transversal_gen : forall (T : {set {group gT}}) G,
  (forall P, P \in T -> P \subset G) ->
  (forall p, p \in \pi(G) -> exists2 P, P \in T & p.-Sylow(G) P) ->
  << \bigcup_(P \in T) P >> = G.

Lemma Sylow_gen : forall G,
  << \bigcup_(P : {group gT} | Sylow G P) P >> = G.

End MoreSylow.

Section SomeHall.

Variable gT : finGroupType.
Implicit Types p : nat.
Implicit Type pi : nat_pred.
Implicit Types G H K P R : {group gT}.

Lemma Hall_pJsub : forall 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 : forall 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 : forall pi G K H,
  K <| G -> pi.-Hall(G) H -> pi.-Hall(K) (H :&: K).

Lemma coprime_mulG_setI_norm : forall 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}.
Implicit Types p q : nat.

Lemma pgroup_nil : forall p P, p.-group P -> nilpotent P.

Lemma pgroup_sol : forall p P, p.-group P -> solvable P.

Lemma small_nil_class : forall G, nil_class G <= 5 -> nilpotent G.

Lemma nil_class2 : forall G, (nil_class G <= 2) = (G^`(1) \subset 'Z(G)).

Lemma nil_class3 : forall G, (nil_class G <= 3) = ('L_3(G) \subset 'Z(G)).

Lemma nilpotent_maxp_normal : forall pi G H,
  nilpotent G -> [max H | pi.-subgroup(G) H] -> H <| G.

Lemma nilpotent_Hall_pcore : forall pi G H,
  nilpotent G -> pi.-Hall(G) H -> H :=: 'O_pi(G).

Lemma nilpotent_pcore_Hall : forall pi G, nilpotent G -> pi.-Hall(G) 'O_pi(G).

Lemma nilpotent_pcoreC : forall pi G,
   nilpotent G -> 'O_pi(G) \x 'O_pi^'(G) = G.

Lemma sub_nilpotent_cent2 : forall H K G,
    nilpotent G -> K \subset G -> H \subset G -> coprime #|K| #|H| ->
  H \subset 'C(K).

Lemma pi_center_nilpotent : forall G, nilpotent G -> \pi('Z(G)) = \pi(G).

Lemma Sylow_subnorm : forall p G P,
  p.-Sylow('N_G(P)) P = p.-Sylow(G) P.

End Nilpotent.

Lemma nil_class_pgroup : forall (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}) :=
  forallb 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 : forall G H, H \subset G -> Zgroup G -> Zgroup H.

Lemma morphim_Zgroup : forall G, Zgroup G -> Zgroup (f @* G).

Lemma nil_Zgroup_cyclic : forall G, Zgroup G -> nilpotent G -> cyclic G.

End Zgroups.

Section NilPGroups.

Variables (p : nat) (gT : finGroupType).
Implicit Type G P N : {group gT}.

Lemma cyclic_pgroup_quo_der1_cyclic : forall P,
  p.-group P -> cyclic (P / P^`(1)) -> cyclic P.

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

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

End NilPGroups.