Library nilpotent

   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.      


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 :=
  forallb 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 :=
  forallb G : {group gT}, (G \subset A :&: [~: G, G]) ==> (G :==: 1).

End PropertiesDefs.


Section NilpotentProps.

Variable gT: finGroupType.

Implicit Type A B : {set gT}.
Implicit Type G H : {group gT}.

Lemma nilpotent1 : nilpotent [1 gT].

Lemma nilpotentS : forall A B, B \subset A -> nilpotent A -> nilpotent B.

Lemma nil_comm_properl : forall G H A,
    nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) ->
  [~: H, A] \proper H.

Lemma nil_comm_properr : forall G A H,
    nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) ->
  [~: A, H] \proper H.

Lemma centrals_nil : forall (s : seq {group gT})(G : {group gT}),
  G.-central.-series 1%G s -> last 1%G s = G -> nilpotent G.

End NilpotentProps.

Section LowerCentral.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Type A B : {set gT}.
Implicit Type G H : {group gT}.

Lemma lcn0 : forall A, 'L_0(A) = A.

Lemma lcn1 : forall A, 'L_1(A) = A.

Lemma lcnSn : forall n A, 'L_n.+2(A) = [~: 'L_n.+1(A), A].

Lemma lcnSnS : forall n G, [~: 'L_n(G), G] \subset 'L_n.+1(G).
Lemma lcnE : forall n A, 'L_n.+1(A) = lower_central_at_rec n A.
Lemma lcn2 : forall A, 'L_2(A) = A^`(1).

Lemma lcn_group_set : forall n G, group_set 'L_n(G).

Canonical Structure lower_central_at_group n G := Group (lcn_group_set n G).

Lemma lcn_char : forall n G, 'L_n(G) \char G.

Lemma lcn_normal : forall n G, 'L_n(G) <| G.

Lemma lcn_sub : forall n G, 'L_n(G) \subset G.

Lemma lcn_norm : forall n G, G \subset 'N('L_n(G)).

Lemma lcn_subS : forall n G, 'L_n.+1(G) \subset 'L_n(G).

Lemma lcn_normalS : forall n G, 'L_n.+1(G) <| 'L_n(G).

Lemma lcn_central : forall n G,
  'L_n(G) / 'L_n.+1(G) \subset 'Z(G / 'L_n.+1(G)).

Lemma lcn_sub_leq : forall m n G, n <= m -> 'L_m(G) \subset 'L_n(G).

Lemma lcnS : forall n A B, A \subset B -> 'L_n(A) \subset 'L_n(B).

Lemma lcn_cprod : forall n A B G, A \* B = G -> 'L_n(A) \* 'L_n(B) = 'L_n(G).

Lemma der_cprod : forall n A B G, A \* B = G -> A^`(n) \* B^`(n) = G^`(n).

Lemma nilpotent_class : forall G, nilpotent G = (nil_class G < #|G|).

Lemma lcn_nil_classP : forall n G,
  nilpotent G -> reflect ('L_n.+1(G) = 1) (nil_class G <= n).

Lemma lcnP : forall G, reflect (exists n, 'L_n.+1(G) = 1) (nilpotent G).

Lemma abelian_nil : forall G, abelian G -> nilpotent G.

Lemma nil_class0 : forall G, (nil_class G == 0) = (G :==: 1).

Lemma nil_class1 : forall G, (nil_class G <= 1) = abelian G.

Lemma cprod_nil : forall A B G,
  A \* B = G -> nilpotent (G) = nilpotent A && nilpotent B.

Lemma mulg_nil : forall G H,
  H \subset 'C(G) -> nilpotent (G * H) = nilpotent G && nilpotent H.

Lemma dprod_nil : forall A B G,
   A \x B = G -> nilpotent G = nilpotent A && nilpotent B.

Lemma bigdprod_nil : forall I r (P : pred I) (A_ : I -> {set gT}) G,
  \big[dprod/1]_(i <- r | P i) A_ i = G
  -> (forall i, P i -> nilpotent (A_ i)) -> nilpotent G.

End LowerCentral.

Notation "''L_' n ( G )" := (lower_central_at_group n G) : subgroup_scope.

Lemma lcn_cont : forall n, GFunctor.continuous (lower_central_at n).

Canonical Structure lcn_igFun n := [igFun by lcn_sub^~ n & lcn_cont n].
Canonical Structure lcn_gFun n := [gFun by lcn_cont n].
Canonical Structure lcn_mgFun n := [mgFun by fun _ G H => @lcnS _ n G H].

Section UpperCentralFunctor.

Variable n : nat.
Implicit Type gT : finGroupType.

Lemma ucn_pmap : exists hZ : GFunctor.pmap, @upper_central_at n = hZ.

 Now extract all the intermediate facts of the last proof. 

Lemma ucn_group_set : forall gT (G : {group gT}), group_set 'Z_n(G).

Canonical Structure upper_central_at_group gT G := Group (@ucn_group_set gT G).

Lemma ucn_sub : forall gT (G : {group gT}), 'Z_n(G) \subset G.

Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n).

Canonical Structure ucn_igFun := [igFun by ucn_sub & morphim_ucn].
Canonical Structure ucn_gFun := [gFun by morphim_ucn].
Canonical Structure 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) : subgroup_scope.

Section UpperCentral.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Type A B : {set gT}.
Implicit Type G H : {group gT}.

Lemma ucn0 : forall A, 'Z_0(A) = 1.

Lemma ucnSn : forall n A, 'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).

Lemma ucnE : forall n A, 'Z_n(A) = upper_central_at_rec n A.

Lemma ucn_subS : forall n G, 'Z_n(G) \subset 'Z_n.+1(G).

Lemma ucn_sub_geq : forall m n G, n >= m -> 'Z_m(G) \subset 'Z_n(G).

Lemma ucn_central : forall n G, 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).

Lemma ucn_normalS : forall n G, 'Z_n(G) <| 'Z_n.+1(G).

Lemma ucn_comm : forall n G, [~: 'Z_n.+1(G), G] \subset 'Z_n(G).

Lemma ucn1 : forall G, 'Z_1(G) = 'Z(G).

Lemma ucnSnR : forall n G,
  'Z_n.+1(G) = [set x \in G | [~: [set x], G] \subset 'Z_n(G)].

Lemma ucn_lcnP : forall n G, ('L_n.+1(G) == 1) = ('Z_n(G) == G).

Lemma ucnP : forall G, reflect (exists n, 'Z_n(G) = G) (nilpotent G).

Lemma ucn_nil_classP : forall n G,
  nilpotent G -> reflect ('Z_n(G) = G) (nil_class G <= n).

Lemma ucn_id : forall n G, 'Z_n('Z_n(G)) = 'Z_n(G).

Lemma ucn_nilpotent : forall n G, nilpotent 'Z_n(G).

Lemma nil_class_ucn : forall 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 : forall n G, G \subset D -> f @* 'L_n(G) = 'L_n(f @* G).

Lemma injm_ucn : forall n G,
  'injm f -> G \subset D -> f @* 'Z_n(G) = 'Z_n(f @* G).

Lemma morphim_nil : forall G, nilpotent G -> nilpotent (f @* G).

Lemma injm_nil : forall G,
  'injm f -> G \subset D -> nilpotent (f @* G) = nilpotent G.

Lemma nil_class_morphim : forall G,
  nilpotent G -> nil_class (f @* G) <= nil_class G.

Lemma nil_class_injm : forall G,
  'injm f -> G \subset D -> nil_class (f @* G) = nil_class G.

End MorphNil.

Section QuotientNil.

Variables gT : finGroupType.
Implicit Types G H : {group gT}.

Lemma quotient_ucn_add : forall m n G,
  'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).

Lemma isog_nil : forall (rT : finGroupType) G (L : {group rT}),
  G \isog L -> nilpotent G = nilpotent L.

Lemma isog_nil_class : forall (rT : finGroupType) G (L : {group rT}),
  G \isog L -> nil_class G = nil_class L.

Lemma quotient_nil : forall G H, nilpotent G -> nilpotent (G / H).

Lemma quotient_center_nil : forall G, nilpotent (G / 'Z(G)) = nilpotent G.

Lemma nil_class_quotient_center : forall G,
  nilpotent (G) -> nil_class (G / 'Z(G)) = (nil_class G).-1.

Lemma nilpotent_sub_norm : forall G H,
  nilpotent G -> H \subset G -> 'N_G(H) \subset H -> G :=: H.

Lemma nilpotent_proper_norm : forall G H,
  nilpotent G -> H \proper G -> H \proper 'N_G(H).

Lemma nilpotent_subnormal : forall G H,
  nilpotent G -> H \subset G -> H <|<| G.

Lemma TI_center_nil : forall G H,
  nilpotent G -> H <| G -> H :&: 'Z(G) = 1 -> H :=: 1.

Lemma meet_center_nil : forall G H,
  nilpotent G -> H <| G -> H :!=: 1 -> H :&: 'Z(G) != 1.

Lemma center_nil_eq1 : forall G, nilpotent G -> ('Z(G) == 1) = (G :==: 1).

End QuotientNil.

Section Solvable.

Variable gT : finGroupType.
Implicit Types G H : {group gT}.

Lemma nilpotent_sol : forall G, nilpotent G -> solvable G.

Lemma abelian_sol : forall G, abelian G -> solvable G.

Lemma solvable1 : solvable [1 gT].

Lemma solvableS : forall G H, H \subset G -> solvable G -> solvable H.

Lemma sol_der1_proper : forall G H,
  solvable G -> H \subset G -> H :!=: 1 -> H^`(1) \proper H.

Lemma derivedP : forall G, reflect (exists 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 : forall G (L : {group rT}),
  G \isog L -> solvable G = solvable L.

Lemma quotient_sol : forall G H, solvable G -> solvable (G / H).

Lemma series_sol : forall G H,
  H <| G -> solvable G = solvable H && solvable (G / H).

End QuotientSol.