Library mathcomp.solvable.nilpotent

(* (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 path.
From mathcomp Require Import fintype div bigop prime finset fingroup morphism.
From mathcomp Require Import automorphism quotient commutator gproduct.
From mathcomp Require Import gfunctor center gseries cyclic.

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.

Arguments lower_central_at n%N {gT} A%g.
Arguments upper_central_at n%N {gT} A%g.

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.

Arguments nilpotent {gT} A%g.
Arguments nil_class {gT} A%g.
Arguments solvable {gT} A%g.

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)].
FIXME: before, we got a `rewrite inE` right after the apply/setP=> x. *

However, this rewrite unfolds termes to strange internal HB names. *

We fixed the issue by applying the inE more carefully, but the problem *

needs to be investigated.


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.