- -

Library mathcomp.solvable.nilpotent

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This file defines nilpotent and solvable groups, and give some of their - elementary properties; more will be added later (e.g., the nilpotence of - p-groups in sylow.v, or the fact that minimal normal subgroups of solvable - groups are elementary abelian in maximal.v). This file defines: - nilpotent G == G is nilpotent, i.e., [~: H, G] is a proper subgroup of H - for all nontrivial H <| G. - solvable G == G is solvable, i.e., H^`(1) is a proper subgroup of H for - all nontrivial subgroups H of G. - 'L_n(G) == the nth term of the lower central series, namely - [~: G, ..., G] (n Gs) if n > 0, with 'L_0(G) = G. - G is nilpotent iff 'L_n(G) = 1 for some n. - 'Z_n(G) == the nth term of the upper central series, i.e., - with 'Z_0(G) = 1, 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)). - nil_class G == the nilpotence class of G, i.e., the least n such that - 'L_n.+1(G) = 1 (or, equivalently, 'Z_n(G) = G), if G is - nilpotent; we take nil_class G = #|G| when G is not - nilpotent, so nil_class G < #|G| iff G is nilpotent. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope.
- -
-Section SeriesDefs.
- -
-Variables (n : nat) (gT : finGroupType) (A : {set gT }).
- -
-Definition lower_central_at_rec := iter n (fun B ⇒ [~: B , A ]) A.
- -
-Definition upper_central_at_rec := iter n (fun B ⇒ coset B @*^-1 'Z (A / B )) 1.
- -
-End SeriesDefs.
- -
-

- -

- By convention, the lower central series starts at 1 while the upper series - starts at 0 (sic). -

-Definition lower_central_at n := lower_central_at_rec n .-1.
- -
-

- -

- Note: 'nosimpl' MUST be used outside of a section -- the end of section - "cooking" destroys it. -

-Definition upper_central_at := nosimpl upper_central_at_rec.
- -
- -
-Notation "''L_' n ( G )" := (lower_central_at n G)
-  (at level 8, n at level 2, format "''L_' n ( G )") : group_scope.
- -
-Notation "''Z_' n ( G )" := (upper_central_at n G)
-  (at level 8, n at level 2, format "''Z_' n ( G )") : group_scope.
- -
-Section PropertiesDefs.
- -
-Variables (gT : finGroupType) (A : {set gT }).
- -
-Definition nilpotent :=
-  [∀ (G : {group gT } | G \subset A :&: [~: G , A ]), G :==: 1].
- -
-Definition nil_class := index 1 (mkseq (fun n ⇒ 'L_n .+1 (A )) #|A |).
- -
-Definition solvable :=
-  [∀ (G : {group gT } | G \subset A :&: [~: G , G ]), G :==: 1].
- -
-End PropertiesDefs.
- -
- -
-Section NilpotentProps.
- -
-Variable gT: finGroupType.
-Implicit Types (A B : {set gT }) (G H : {group gT }).
- -
-Lemma nilpotent1 : nilpotent [1 gT ].
- -
-Lemma nilpotentS A B : B \subset A → nilpotent A → nilpotent B.
- -
-Lemma nil_comm_properl G H A :
-    nilpotent G → H \subset G → H :!=: 1 → A \subset 'N_G (H ) →
-  [~: H , A ] \proper H.
- -
-Lemma nil_comm_properr G A H :
-    nilpotent G → H \subset G → H :!=: 1 → A \subset 'N_G (H ) →
-  [~: A , H ] \proper H.
- -
-Lemma centrals_nil (s : seq {group gT }) G :
-  G .-central .-series 1%G s → last 1%G s = G → nilpotent G.
- -
-End NilpotentProps.
- -
-Section LowerCentral.
- -
-Variable gT : finGroupType.
-Implicit Types (A B : {set gT }) (G H : {group gT }).
- -
-Lemma lcn0 A : 'L_0 (A ) = A.
-Lemma lcn1 A : 'L_1 (A ) = A.
-Lemma lcnSn n A : 'L_n .+2 (A ) = [~: 'L_n .+1 (A ), A ].
-Lemma lcnSnS n G : [~: 'L_n (G ), G ] \subset 'L_n .+1 (G ).
- Lemma lcnE n A : 'L_n .+1 (A ) = lower_central_at_rec n A.
- Lemma lcn2 A : 'L_2 (A ) = A ^`(1).
- -
-Lemma lcn_group_set n G : group_set 'L_n (G ).
- -
-Canonical lower_central_at_group n G := Group (lcn_group_set n G).
- -
-Lemma lcn_char n G : 'L_n (G ) \char G.
- -
-Lemma lcn_normal n G : 'L_n (G ) <| G.
- -
-Lemma lcn_sub n G : 'L_n (G ) \subset G.
- -
-Lemma lcn_norm n G : G \subset 'N ('L_n (G )).
- -
-Lemma lcn_subS n G : 'L_n .+1 (G ) \subset 'L_n (G ).
- -
-Lemma lcn_normalS n G : 'L_n .+1 (G ) <| 'L_n (G ).
- -
-Lemma lcn_central n G : 'L_n (G ) / 'L_n .+1 (G ) \subset 'Z (G / 'L_n .+1 (G )).
- -
-Lemma lcn_sub_leq m n G : n ≤ m → 'L_m (G ) \subset 'L_n (G ).
- -
-Lemma lcnS n A B : A \subset B → 'L_n (A ) \subset 'L_n (B ).
- -
-Lemma lcn_cprod n A B G : A \* B = G → 'L_n (A ) \* 'L_n (B ) = 'L_n (G ).
- -
-Lemma lcn_dprod n A B G : A \x B = G → 'L_n (A ) \x 'L_n (B ) = 'L_n (G ).
- -
-Lemma der_cprod n A B G : A \* B = G → A ^`(n ) \* B ^`(n ) = G ^`(n ).
- -
-Lemma der_dprod n A B G : A \x B = G → A ^`(n ) \x B ^`(n ) = G ^`(n ).
- -
-Lemma lcn_bigcprod n I r P (F : I → {set gT }) G :
-    \big [cprod /1]_(i <- r | P i ) F i = G →
-  \big [cprod /1]_(i <- r | P i ) 'L_n (F i ) = 'L_n (G ).
- -
-Lemma lcn_bigdprod n I r P (F : I → {set gT }) G :
-    \big [dprod /1]_(i <- r | P i ) F i = G →
-  \big [dprod /1]_(i <- r | P i ) 'L_n (F i ) = 'L_n (G ).
- -
-Lemma der_bigcprod n I r P (F : I → {set gT }) G :
-    \big [cprod /1]_(i <- r | P i ) F i = G →
-  \big [cprod /1]_(i <- r | P i ) (F i )^`(n ) = G ^`(n ).
- -
-Lemma der_bigdprod n I r P (F : I → {set gT }) G :
-    \big [dprod /1]_(i <- r | P i ) F i = G →
-  \big [dprod /1]_(i <- r | P i ) (F i )^`(n ) = G ^`(n ).
- -
-Lemma nilpotent_class G : nilpotent G = (nil_class G < #|G |).
- -
-Lemma lcn_nil_classP n G :
-  nilpotent G → reflect ('L_n .+1 (G ) = 1) (nil_class G ≤ n).
- -
-Lemma lcnP G : reflect (∃ n, 'L_n .+1 (G ) = 1) (nilpotent G).
- -
-Lemma abelian_nil G : abelian G → nilpotent G.
- -
-Lemma nil_class0 G : (nil_class G == 0) = (G :==: 1).
- -
-Lemma nil_class1 G : (nil_class G ≤ 1) = abelian G.
- -
-Lemma cprod_nil A B G : A \* B = G → nilpotent G = nilpotent A && nilpotent B.
- -
-Lemma mulg_nil G H :
-  H \subset 'C (G ) → nilpotent (G × H) = nilpotent G && nilpotent H.
- -
-Lemma dprod_nil A B G : A \x B = G → nilpotent G = nilpotent A && nilpotent B.
- -
-Lemma bigdprod_nil I r (P : pred I) (A_ : I → {set gT }) G :
-  \big [dprod /1]_(i <- r | P i ) A_ i = G
-  → (∀ i, P i → nilpotent (A_ i)) → nilpotent G.
- -
-End LowerCentral.
- -
-Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope.
- -
-Lemma lcn_cont n : GFunctor.continuous (@lower_central_at n).
- -
-Canonical lcn_igFun n := [igFun by lcn_sub ^~ n & lcn_cont n ].
-Canonical lcn_gFun n := [gFun by lcn_cont n ].
-Canonical lcn_mgFun n := [mgFun by fun _ G H ⇒ @lcnS _ n G H ].
- -
-Section UpperCentralFunctor.
- -
-Variable n : nat.
-Implicit Type gT : finGroupType.
- -
-Lemma ucn_pmap : ∃ hZ : GFunctor.pmap , @upper_central_at n = hZ.
- -
-

- -

- Now extract all the intermediate facts of the last proof. -