Library mathcomp.solvable.commutator
+ +
+(* (c) Copyright 2006-2016 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.
+ +
+
+
++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.
+ +
+
+
++ +
+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.
+ +
+
+
++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.
+ +
+ +
+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.
+ +
+ +
+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).
+