Library commutator

   This files contains the proofs of several key properties of commutators, 
 including the Hall-Witt identity and the Three Subgroup Lemma.             
   The definition and notation for both pointwise and set wise commutators  
 ([~x, y, ...] and [~: A, B ,...], respectively) are give in groups.v. This 
 file defines the derived group series:                                     
           G^`(0) ==  G                                                     
       G^`(n.+1) == [~: G^`(n), G^`(n)]                                     
 as several classical results involve the (first) derived group G^`(1),     
 such as the equivalence H <| G /\ G / H abelian <-> G^`(1) \subset H. The  
 connection between the derived series and solvable groups will only be     
 established in nilpotent.v, however.                                       


Import GroupScope.

Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) :=
  iter n (fun B => [~: B, B]) A.

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

Notation "G ^` ( n )" := (derived_at n G) : group_scope.

Section DerivedBasics.

Variables gT : finGroupType.
Implicit Type A : {set gT}.
Implicit Types G : {group gT}.

Lemma derg0 : forall A, A^`(0) = A.

Lemma derg1 : forall A, A^`(1) = [~: A, A].

Lemma dergSn : forall n A, A^`(n.+1) = [~: A^`(n), A^`(n)].

Lemma der_group_set : forall G n, group_set G^`(n).

Canonical Structure derived_at_group G n := Group (der_group_set G n).

End DerivedBasics.

Notation "G ^` ( n )" := (derived_at_group G n) : subgroup_scope.

Section Basic_commutator_properties.

Variable gT : finGroupType.
Implicit Types x y z : gT.

Lemma conjg_mulR : forall x y, x ^ y = x * [~ x, y].

Lemma conjg_Rmul : forall x y, x ^ y = [~ y, x^-1] * x.

Lemma commMgJ : forall x y z, [~ x * y, z] = [~ x, z] ^ y * [~ y, z].

Lemma commgMJ : forall x y z, [~ x, y * z] = [~ x, z] * [~ x, y] ^ z.

Lemma commMgR : forall x y z,
  [~ x * y, z] = [~ x, z] * [~ x, z, y] * [~ y, z].

Lemma commgMR : forall x y z,
  [~ x, y * z] = [~ x, z] * [~ x, y] * [~ x, y, z].

Lemma Hall_Witt_identity : forall x y z,
  [~ x, y^-1, z] ^ y * [~ y, z^-1, x] ^ z * [~ z, x^-1, y] ^ x = 1.

 the following properties are useful for studying p-groups of class 2 

Section LeftComm.

Variables (i : nat) (x y : gT).
Hypothesis cxz : commute x [~ x, y].

Lemma commVg : [~ x^-1, y] = [~ x, y]^-1.

Lemma commXg : [~ x ^+ i, y] = [~ x, y] ^+ i.

End LeftComm.

Section RightComm.

Variables (i : nat) (x y : gT).
Hypothesis cyz : commute y [~ x, y].

Lemma commgV : [~ x, y^-1] = [~ x, y]^-1.

Lemma commgX : [~ x, y ^+ i] = [~ x, y] ^+ i.

End RightComm.

Section LeftRightComm.

Variables (i j : nat) (x y : gT).
Hypotheses (cxz : commute x [~ x, y]) (cyz : commute y [~ x, y]).

Lemma commXXg : [~ x ^+ i, y ^+ j] = [~ x, y] ^+ (i * j).

Lemma expMg_Rmul : (y * x) ^+ i = y ^+ i * x ^+ i * [~ x, y] ^+ 'C(i, 2).

End LeftRightComm.

End Basic_commutator_properties.

 Set theoretic commutators 
Section Commutator_properties.

Variable gT : finGroupType.
Implicit Type rT : finGroupType.
Implicit Types A B C : {set gT}.
Implicit Types D G H K : {group gT}.

Lemma commG1 : forall A, [~: A, 1] = 1.

Lemma comm1G : forall A, [~: 1, A] = 1.

Lemma commg_sub : forall A B, [~: A, B] \subset A <*> B.

Lemma commg_norml : forall G A, G \subset 'N([~: G, A]).

Lemma commg_normr : forall G A, G \subset 'N([~: A, G]).

Lemma commg_norm : forall G H, G <*> H \subset 'N([~: G, H]).

Lemma commg_normal : forall G H, [~: G, H] <| G <*> H.

Lemma normsRl : forall A G B, A \subset G -> A \subset 'N([~: G, B]).

Lemma normsRr : forall A G B, A \subset G -> A \subset 'N([~: B, G]).

Lemma commg_subr : forall G H, ([~: G, H] \subset H) = (G \subset 'N(H)).

Lemma commg_subl : forall G H, ([~: G, H] \subset G) = (H \subset 'N(G)).

Lemma commg_subI : forall A B G H,
  A \subset 'N_G(H) -> B \subset 'N_H(G) -> [~: A, B] \subset G :&: H.

Lemma quotient_cents2 : forall A B K,
    A \subset 'N(K) -> B \subset 'N(K) ->
  (A / K \subset 'C(B / K)) = ([~: A, B] \subset K).

Lemma quotient_cents2r : forall A B K,
  [~: A, B] \subset K -> (A / K) \subset 'C(B / K).

Lemma sub_der1_norm : forall G H,
   G^`(1) \subset H -> H \subset G -> G \subset 'N(H).

Lemma sub_der1_normal : forall G H, G^`(1) \subset H -> H \subset G -> H <| G.

Lemma sub_der1_abelian : forall G H, G^`(1) \subset H -> abelian (G / H).

Lemma der1_min : forall G H,
  G \subset 'N(H) -> abelian (G / H) -> G^`(1) \subset H.

Lemma der_abelian : forall n G, abelian (G^`(n) / G^`(n.+1)).

Lemma commg_normSl : forall G H K,
  G \subset 'N(H) -> [~: G, H] \subset 'N([~: K, H]).

Lemma commg_normSr : forall G H K,
  G \subset 'N(H) -> [~: H, G] \subset 'N([~: H, K]).

Lemma commMGr : forall G H K,
  [~: G, K] * [~: H, K] \subset [~: G * H , K].

Lemma commMG : forall G H K,
  H \subset 'N([~: G, K]) -> [~: G * H , K] = [~: G, K] * [~: H, K].

Lemma comm3G1P : forall A B C,
  reflect {in A & B & C, forall h k l, [~ h, k, l] = 1} ([~: A, B, C] :==: 1).

Lemma three_subgroup : forall G H K,
  [~: G, H, K] :=: 1 -> [~: H, K, G] :=: 1-> [~: K, G, H] :=: 1.

Lemma der1_joing_cycles : forall x y : gT,
  let XY := <[x]> <*> <[y]> in let xy := [~ x, y] in
  xy \in 'C(XY) -> XY^`(1) = <[xy]>.

 GG -- unsure about the usefulness of this lemma; keeping it for now. 
Lemma commgAC : forall G x y z, x \in G -> y \in G -> z \in G ->
  commute y z -> abelian [~: [set x], G] -> [~ x, y, z] = [~ x, z, y].

 Aschbacher, exercise 3.6 (used in proofs of Aschbacher 24.7 and B & G 1.10 
Lemma comm_norm_cent_cent : forall H G K,
    H \subset 'N(G) -> H \subset 'C(K) -> G \subset 'N(K) ->
  [~: G, H] \subset 'C(K).

Lemma charR : forall H K G, H \char G -> K \char G -> [~: H, K] \char G.

Lemma der_char : forall n G, G^`(n) \char G.

Lemma der_sub : forall n G, G^`(n) \subset G.

Lemma der_norm : forall n G, G \subset 'N(G^`(n)).

Lemma der_normal : forall n G, G^`(n) <| G.

Lemma der_subS : forall n G, G^`(n.+1) \subset G^`(n).

Lemma der_normalS : forall n G, G^`(n.+1) <| G^`(n).

Lemma morphim_der : forall rT D (f : {morphism D >-> rT}) n G,
   G \subset D -> f @* G^`(n) = (f @* G)^`(n).

Lemma dergS : forall n G H, G \subset H -> G^`(n) \subset H^`(n).

Lemma quotient_der : forall n G H, G \subset 'N(H) -> G^`(n) / H = (G / H)^`(n).

Lemma derJ : forall G n x, (G :^ x)^`(n) = G^`(n) :^ x.

Lemma derG1P : forall G, reflect (G^`(1) = 1) (abelian G).

End Commutator_properties.

Implicit Arguments derG1P [gT G].

Lemma der_cont : forall n, GFunctor.continuous (derived_at n).

Canonical Structure der_igFun n := [igFun by der_sub^~ n & der_cont n].
Canonical Structure der_gFun n := [gFun by der_cont n].
Canonical Structure der_mgFun n := [mgFun by dergS^~ n].

Lemma isog_der : forall (aT rT : finGroupType) n,
  forall (G : {group aT}) (H : {group rT}), G \isog H -> G^`(n) \isog H^`(n).