Library mathcomp.solvable.sylow
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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
-
-
-