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.
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.
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.
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).