Library mathcomp.solvable.commutator
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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.
(* gsimpl *)
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 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].
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.
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 H → G^`(n) \isog H^`(n).
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.
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 H → G^`(n) \isog H^`(n).