# Library mathcomp.solvable.commutator

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

Require Import mathcomp.ssreflect.ssreflect.

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 given in fingroup.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.

Set Implicit Arguments.

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 A : A^`(0) = A.
Lemma derg1 A : A^`(1) = [~: A, A].
Lemma dergSn n A : A^`(n.+1) = [~: A^`(n), A^`(n)].

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

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

End DerivedBasics.

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

Section Basic_commutator_properties.

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

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

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

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

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

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

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

Lemma Hall_Witt_identity 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].
Let cyz' := commuteV cyz.

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) (A B C : {set gT}) (D G H K : {group gT}).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma sub_der1_norm G H : G^`(1) \subset H H \subset G G \subset 'N(H).

Lemma sub_der1_normal G H : G^`(1) \subset H H \subset G H <| G.

Lemma sub_der1_abelian G H : G^`(1) \subset H abelian (G / H).

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

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

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

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

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

Lemma commMG G H K :
H \subset 'N([~: G, K]) [~: G × H , K] = [~: G, K] × [~: H, K].

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

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

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

Lemma commgAC 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 H G K :
H \subset 'N(G) H \subset 'C(K) G \subset 'N(K)
[~: G, H] \subset 'C(K).

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

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

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

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

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

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

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

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

Lemma dergS n G H : G \subset H G^`(n) \subset H^`(n).

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

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

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

End Commutator_properties.

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

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

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