Library mathcomp.solvable.commutator
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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).
-