# Library mathcomp.solvable.commutator

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

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype.
From mathcomp Require Import bigop finset binomial fingroup morphism.
From mathcomp Require Import 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.

Arguments derived_at n%N {gT} A%g.
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 ****
Aschbacher, exercise 3.6 (used in proofs of Aschbacher 24.7 and B & G 1.10