(Joint Center)Library MathComp.commutator

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype bigop finset.
Require Import binomial fingroup morphism automorphism quotient gfunctor.

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.
(* gsimpl *)

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 GA \subset 'N([~: G, B]).

Lemma normsRr A G B : A \subset GA \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 HH \subset GG \subset 'N(H).

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

Lemma sub_der1_abelian G H : G^`(1) \subset Habelian (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 Gy \in Gz \in G
  commute y zabelian [~: [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 GK \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 Df @* G^`(n) = (f @* G)^`(n).

Lemma dergS n G H : G \subset HG^`(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.

Implicit Arguments derG1P [gT G].

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 HG^`(n) \isog H^`(n).