Library mathcomp.solvable.sylow
+ +
+(* (c) Copyright 2006-2016 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.
+ +
+
+
++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
+
+
+