Library mathcomp.solvable.sylow

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import fintype prime bigop finset fingroup morphism.
From mathcomp Require Import automorphism quotient action cyclic gproduct.
From mathcomp Require Import gfunctor commutator pgroup center nilpotent.

Set Implicit Arguments.

Import GroupScope.

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.

Arguments Zgroup {gT} A%g.

Section NilPGroups.

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

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.