Library mathcomp.solvable.nilpotent
(* (c) Copyright 2006-2015 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.
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).
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.
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.
Lemma ucn_group_set gT (G : {group gT}) : group_set 'Z_n(G).
Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G).
Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G.
Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n).
Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn].
Canonical ucn_gFun := [gFun by morphim_ucn].
Canonical ucn_pgFun := [pgFun by morphim_ucn].
Variable (gT : finGroupType) (G : {group gT}).
Lemma ucn_char : 'Z_n(G) \char G.
Lemma ucn_norm : G \subset 'N('Z_n(G)).
Lemma ucn_normal : 'Z_n(G) <| G.
End UpperCentralFunctor.
Notation "''Z_' n ( G )" := (upper_central_at_group n G) : Group_scope.
Section UpperCentral.
Variable gT : finGroupType.
Implicit Types (A B : {set gT}) (G H : {group gT}).
Lemma ucn0 A : 'Z_0(A) = 1.
Lemma ucnSn n A : 'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).
Lemma ucnE n A : 'Z_n(A) = upper_central_at_rec n A.
Lemma ucn_subS n G : 'Z_n(G) \subset 'Z_n.+1(G).
Lemma ucn_sub_geq m n G : n ≥ m → 'Z_m(G) \subset 'Z_n(G).
Lemma ucn_central n G : 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).
Lemma ucn_normalS n G : 'Z_n(G) <| 'Z_n.+1(G).
Lemma ucn_comm n G : [~: 'Z_n.+1(G), G] \subset 'Z_n(G).
Lemma ucn1 G : 'Z_1(G) = 'Z(G).
Lemma ucnSnR n G : 'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].
Lemma ucn_cprod n A B G : A \* B = G → 'Z_n(A) \* 'Z_n(B) = 'Z_n(G).
Lemma ucn_dprod n A B G : A \x B = G → 'Z_n(A) \x 'Z_n(B) = 'Z_n(G).
Lemma ucn_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) 'Z_n(F i) = 'Z_n(G).
Lemma ucn_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) 'Z_n(F i) = 'Z_n(G).
Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G).
Lemma ucnP G : reflect (∃ n, 'Z_n(G) = G) (nilpotent G).
Lemma ucn_nil_classP n G :
nilpotent G → reflect ('Z_n(G) = G) (nil_class G ≤ n).
Lemma ucn_id n G : 'Z_n('Z_n(G)) = 'Z_n(G).
Lemma ucn_nilpotent n G : nilpotent 'Z_n(G).
Lemma nil_class_ucn n G : nil_class 'Z_n(G) ≤ n.
End UpperCentral.
Section MorphNil.
Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Implicit Type G : {group aT}.
Lemma morphim_lcn n G : G \subset D → f @* 'L_n(G) = 'L_n(f @* G).
Lemma injm_ucn n G : 'injm f → G \subset D → f @* 'Z_n(G) = 'Z_n(f @* G).
Lemma morphim_nil G : nilpotent G → nilpotent (f @* G).
Lemma injm_nil G : 'injm f → G \subset D → nilpotent (f @* G) = nilpotent G.
Lemma nil_class_morphim G : nilpotent G → nil_class (f @* G) ≤ nil_class G.
Lemma nil_class_injm G :
'injm f → G \subset D → nil_class (f @* G) = nil_class G.
End MorphNil.
Section QuotientNil.
Variables gT : finGroupType.
Implicit Types (rT : finGroupType) (G H : {group gT}).
Lemma quotient_ucn_add m n G : 'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).
Lemma isog_nil rT G (L : {group rT}) : G \isog L → nilpotent G = nilpotent L.
Lemma isog_nil_class rT G (L : {group rT}) :
G \isog L → nil_class G = nil_class L.
Lemma quotient_nil G H : nilpotent G → nilpotent (G / H).
Lemma quotient_center_nil G : nilpotent (G / 'Z(G)) = nilpotent G.
Lemma nil_class_quotient_center G :
nilpotent (G) → nil_class (G / 'Z(G)) = (nil_class G).-1.
Lemma nilpotent_sub_norm G H :
nilpotent G → H \subset G → 'N_G(H) \subset H → G :=: H.
Lemma nilpotent_proper_norm G H :
nilpotent G → H \proper G → H \proper 'N_G(H).
Lemma nilpotent_subnormal G H : nilpotent G → H \subset G → H <|<| G.
Lemma TI_center_nil G H : nilpotent G → H <| G → H :&: 'Z(G) = 1 → H :=: 1.
Lemma meet_center_nil G H :
nilpotent G → H <| G → H :!=: 1 → H :&: 'Z(G) != 1.
Lemma center_nil_eq1 G : nilpotent G → ('Z(G) == 1) = (G :==: 1).
Lemma cyclic_nilpotent_quo_der1_cyclic G :
nilpotent G → cyclic (G / G^`(1)) → cyclic G.
End QuotientNil.
Section Solvable.
Variable gT : finGroupType.
Implicit Types G H : {group gT}.
Lemma nilpotent_sol G : nilpotent G → solvable G.
Lemma abelian_sol G : abelian G → solvable G.
Lemma solvable1 : solvable [1 gT].
Lemma solvableS G H : H \subset G → solvable G → solvable H.
Lemma sol_der1_proper G H :
solvable G → H \subset G → H :!=: 1 → H^`(1) \proper H.
Lemma derivedP G : reflect (∃ n, G^`(n) = 1) (solvable G).
End Solvable.
Section MorphSol.
Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
Variable G : {group gT}.
Lemma morphim_sol : solvable G → solvable (f @* G).
Lemma injm_sol : 'injm f → G \subset D → solvable (f @* G) = solvable G.
End MorphSol.
Section QuotientSol.
Variables gT rT : finGroupType.
Implicit Types G H K : {group gT}.
Lemma isog_sol G (L : {group rT}) : G \isog L → solvable G = solvable L.
Lemma quotient_sol G H : solvable G → solvable (G / H).
Lemma series_sol G H : H <| G → solvable G = solvable H && solvable (G / H).
Lemma metacyclic_sol G : metacyclic G → solvable G.
End QuotientSol.