Top

Module mathcomp.solvable.commutator

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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope group_scope.

Definition derived_at n (gT : finGroupType) (A : {set gT}) :=
  iter n (fun B => [~: B, B]) A.
Arguments derived_at n%_N {gT} A%_g : simpl never.
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

Proof.

by []. Qed.

Lemma derg1 A : A^`(1) = [~: A, A]

Proof.

by []. Qed.

Lemma dergSn n A : A^`(n.+1) = [~: A^`(n), A^`(n)]

Proof.

by []. Qed.

Lemma der_group_set G n : group_set G^`(n).

Proof.

by case: n => [|n]; apply: groupP. Qed.

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

Proof.

by rewrite mulKVg. Qed.

Lemma conjg_Rmul x y : x ^ y = [~ y, x^-1] * x.

Proof.

by rewrite commgEr invgK mulgKV. Qed.

Lemma commMgJ x y z : [~ x * y, z] = [~ x, z] ^ y * [~ y, z].

Proof.

by rewrite !commgEr conjgM mulgA -conjMg mulgK. Qed.

Lemma commgMJ x y z : [~ x, y * z] = [~ x, z] * [~ x, y] ^ z.

Proof.

by rewrite !commgEl conjgM -mulgA -conjMg mulKVg. Qed.

Lemma commMgR x y z : [~ x * y, z] = [~ x, z] * [~ x, z, y] * [~ y, z].

Proof.

by rewrite commMgJ conjg_mulR. Qed.

Lemma commgMR x y z : [~ x, y * z] = [~ x, z] * [~ x, y] * [~ x, y, z].

Proof.

by rewrite commgMJ conjg_mulR mulgA. Qed.

Lemma Hall_Witt_identity x y z :
  [~ x, y^-1, z] ^ y * [~ y, z^-1, x] ^ z * [~ z, x^-1, y] ^ x = 1.

Proof.

(* gsimpl *)
pose a x y z : gT := x * z * y ^ x.
suffices{x y z} hw_aux x y z: [~ x, y^-1, z] ^ y = (a x y z)^-1 * (a y z x).
  by rewrite !hw_aux; move: a {hw_aux} => a; rewrite 2!mulgA !mulgK mulVg.
by rewrite commgEr conjMg -conjgM -conjg_Rmul conjgE !invMg !mulgA.
Qed.

Section LeftComm.

Variables (i : nat) (x y : gT).
Hypothesis cxz : commute x [~ x, y].

Lemma commVg : [~ x^-1, y] = [~ x, y]^-1.

Proof.

apply/eqP; rewrite commgEl eq_sym eq_invg_mul invgK mulgA -cxz.
by rewrite -conjg_mulR -conjMg mulgV conj1g.
Qed.

Lemma commXg : [~ x ^+ i, y] = [~ x, y] ^+ i.

Proof.

elim: i => [|i' IHi]; first exact: comm1g.
by rewrite !expgS commMgJ /conjg commuteX // mulKg IHi.
Qed.

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.

Proof.

by rewrite -invg_comm commVg -(invg_comm x y) ?invgK. Qed.

Lemma commgX : [~ x, y ^+ i] = [~ x, y] ^+ i.

Proof.

by rewrite -invg_comm commXg -(invg_comm x y) ?expgVn ?invgK. Qed.

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

Proof.

by rewrite expgM commgX commXg //; apply: commuteX. Qed.

Lemma expMg_Rmul : (y * x) ^+ i = y ^+ i * x ^+ i * [~ x, y] ^+ 'C(i, 2).

Proof.

rewrite -bin2_sum; symmetry.
elim: i => [|k IHk] /=; first by rewrite big_geq ?mulg1.
rewrite big_nat_recr //= addnC expgD !expgS -{}IHk !mulgA; congr (_ * _).
by rewrite -!mulgA commuteX2 // -commgX // [mul y]lock 3!mulgA -commgC.
Qed.

End LeftRightComm.

End Basic_commutator_properties.

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.

Proof.

by apply/commG1P; rewrite centsC sub1G. Qed.

Lemma comm1G A : [~: 1, A] = 1.

Proof.

by rewrite commGC commG1. Qed.

Lemma commg_sub A B : [~: A, B] \subset A <*> B.

Proof.

by rewrite comm_subG // (joing_subl, joing_subr). Qed.

Lemma commg_norml G A : G \subset 'N([~: G, A]).

Proof.

apply/subsetP=> x Gx; rewrite inE -genJ gen_subG.
apply/subsetP=> _ /imsetP[_ /imset2P[y z Gy Az ->] ->].
by rewrite -(mulgK [~ x, z] (_ ^ x)) -commMgJ !(mem_commg, groupMl, groupV).
Qed.

Lemma commg_normr G A : G \subset 'N([~: A, G]).

Proof.

by rewrite commGC commg_norml. Qed.

Lemma commg_norm G H : G <*> H \subset 'N([~: G, H]).

Proof.

by rewrite join_subG ?commg_norml ?commg_normr. Qed.

Lemma commg_normal G H : [~: G, H] <| G <*> H.

Proof.

by rewrite /(_ <| _) commg_sub commg_norm. Qed.

Lemma normsRl A G B : A \subset G -> A \subset 'N([~: G, B]).

Proof.

by move=> sAG; apply: subset_trans (commg_norml G B). Qed.

Lemma normsRr A G B : A \subset G -> A \subset 'N([~: B, G]).

Proof.

by move=> sAG; apply: subset_trans (commg_normr G B). Qed.

Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)).

Proof.

rewrite gen_subG; apply/subsetP/subsetP=> [sRH x Gx | nGH xy].
  rewrite inE; apply/subsetP=> _ /imsetP[y Ky ->].
  by rewrite conjg_Rmul groupMr // sRH // imset2_f ?groupV.
case/imset2P=> x y Gx Hy ->{xy}.
by rewrite commgEr groupMr // memJ_norm (groupV, nGH).
Qed.

Lemma commg_subl G H : ([~: G, H] \subset G) = (H \subset 'N(G)).

Proof.

by rewrite commGC commg_subr. Qed.

Lemma commg_subI A B G H :
  A \subset 'N_G(H) -> B \subset 'N_H(G) -> [~: A, B] \subset G :&: H.

Proof.

rewrite !subsetI -(gen_subG _ 'N(G)) -(gen_subG _ 'N(H)).
rewrite -commg_subr -commg_subl; case/andP=> sAG sRH; case/andP=> sBH sRG.
by rewrite (subset_trans _ sRG) ?(subset_trans _ sRH) ?commgSS ?subset_gen.
Qed.

Lemma quotient_cents2 A B K :
    A \subset 'N(K) -> B \subset 'N(K) ->
  (A / K \subset 'C(B / K)) = ([~: A, B] \subset K).

Proof.

move=> nKA nKB.
by rewrite (sameP commG1P trivgP) /= -quotientR // quotient_sub1 // comm_subG.
Qed.

Lemma quotient_cents2r A B K :
  [~: A, B] \subset K -> (A / K) \subset 'C(B / K).

Proof.

move=> sABK; rewrite -2![_ / _]morphimIdom -!quotientE.
by rewrite quotient_cents2 ?subsetIl ?(subset_trans _ sABK) ?commgSS ?subsetIr.
Qed.

Lemma sub_der1_norm G H : G^`(1) \subset H -> H \subset G -> G \subset 'N(H).

Proof.

by move=> sG'H sHG; rewrite -commg_subr (subset_trans _ sG'H) ?commgS.
Qed.

Lemma sub_der1_normal G H : G^`(1) \subset H -> H \subset G -> H <| G.

Proof.

by move=> sG'H sHG; rewrite /(H <| G) sHG sub_der1_norm. Qed.

Lemma sub_der1_abelian G H : G^`(1) \subset H -> abelian (G / H).

Proof.

by move=> sG'H; apply: quotient_cents2r. Qed.

Lemma der1_min G H : G \subset 'N(H) -> abelian (G / H) -> G^`(1) \subset H.

Proof.

by move=> nHG abGH; rewrite -quotient_cents2. Qed.

Lemma der_abelian n G : abelian (G^`(n) / G^`(n.+1)).

Proof.

by rewrite sub_der1_abelian // der_subS. Qed.

Lemma commg_normSl G H K : G \subset 'N(H) -> [~: G, H] \subset 'N([~: K, H]).

Proof.

by move=> nHG; rewrite normsRr // commg_subr. Qed.

Lemma commg_normSr G H K : G \subset 'N(H) -> [~: H, G] \subset 'N([~: H, K]).

Proof.

by move=> nHG; rewrite !(commGC H) commg_normSl. Qed.

Lemma commMGr G H K : [~: G, K] * [~: H, K] \subset [~: G * H , K].

Proof.

by rewrite mul_subG ?commSg ?(mulG_subl, mulG_subr). Qed.

Lemma commMG G H K :
  H \subset 'N([~: G, K]) -> [~: G * H , K] = [~: G, K] * [~: H, K].

Proof.

move=> nRH; apply/eqP; rewrite eqEsubset commMGr andbT.
have nRHK: [~: H, K] \subset 'N([~: G, K]) by rewrite comm_subG ?commg_normr.
have defM := norm_joinEr nRHK; rewrite -defM gen_subG /=.
apply/subsetP=> _ /imset2P[_ z /imset2P[x y Gx Hy ->] Kz ->].
by rewrite commMgJ {}defM mem_mulg ?memJ_norm ?mem_commg // (subsetP nRH).
Qed.

Lemma comm3G1P A B C :
  reflect {in A & B & C, forall h k l, [~ h, k, l] = 1} ([~: A, B, C] :==: 1).

Proof.

have R_C := sameP trivgP commG1P.
rewrite -subG1 R_C gen_subG -{}R_C gen_subG.
apply: (iffP subsetP) => [cABC x y z Ax By Cz | cABC xyz].
  by apply/set1P; rewrite cABC // !imset2_f.
by case/imset2P=> _ z /imset2P[x y Ax By ->] Cz ->; rewrite cABC.
Qed.

Lemma three_subgroup G H K :
  [~: G, H, K] :=: 1 -> [~: H, K, G] :=: 1-> [~: K, G, H] :=: 1.

Proof.

move/eqP/comm3G1P=> cGHK /eqP/comm3G1P cHKG.
apply/eqP/comm3G1P=> x y z Kx Gy Hz; symmetry.
rewrite -(conj1g y) -(Hall_Witt_identity y^-1 z x) invgK.
rewrite [X in X ^ z]cGHK ?groupV // [X in X ^ x]cHKG ?groupV //.
by rewrite !conj1g !mul1g conjgKV.
Qed.

Lemma der1_joing_cycles (x y : gT) :
  let XY := <[x]> <*> <[y]> in let xy := [~ x, y] in
  xy \in 'C(XY) -> XY^`(1) = <[xy]>.

Proof.

rewrite joing_idl joing_idr /= -sub_cent1 => /norms_gen nRxy.
apply/eqP; rewrite eqEsubset cycle_subG mem_commg ?mem_gen ?set21 ?set22 //.
rewrite der1_min // quotient_gen -1?gen_subG // quotientU abelian_gen.
rewrite /abelian subUset centU !subsetI andbC centsC -andbA -!abelianE.
rewrite !quotient_abelian ?(abelianS (subset_gen _) (cycle_abelian _)) //=.
by rewrite andbb quotient_cents2r ?genS // /commg_set imset2_set1l imset_set1.
Qed.

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

Proof.

move=> Gx Gy Gz cyz /centsP cRxG; pose cx' u := [~ x^-1, u].
have xR3 u v: [~ x, u, v] = x^-1 * (cx' u * cx' v) * x ^ (u * v).
  rewrite [X in X * _]mulgA -conjg_mulR conjVg [cx' v]commgEl.
  by rewrite [X in X * _]mulgA -invMg -mulgA conjgM -conjMg -!commgEl.
suffices RxGcx' u: u \in G -> cx' u \in [~: [set x], G].
  by rewrite !xR3 {}cyz; congr (_ * _ * _); rewrite cRxG ?RxGcx'.
move=> Gu; suffices/groupMl <-: [~ x, u] ^ x^-1 \in [~: [set x], G].
  by rewrite -commMgJ mulgV comm1g group1.
by rewrite memJ_norm ?mem_commg ?set11 // groupV (subsetP (commg_normr _ _)).
Qed.

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

Proof.

move=> nGH /centsP cKH nKG; rewrite commGC gen_subG centsC.
apply/centsP=> x Kx _ /imset2P[y z Hy Gz ->]; red.
rewrite mulgA -[x * _]cKH ?groupV // -!mulgA; congr (_ * _).
rewrite (mulgA x) (conjgC x) (conjgCV z) 2!mulgA [in RHS]mulgA; congr (_ * _).
by rewrite -2!mulgA (cKH y) // -mem_conjg (normsP nKG).
Qed.

Lemma charR H K G : H \char G -> K \char G -> [~: H, K] \char G.

Proof.

case/charP=> sHG chH /charP[sKG chK]; apply/charP.
by split=> [|f infj Gf]; [rewrite comm_subG | rewrite morphimR // chH // chK].
Qed.

Lemma der_char n G : G^`(n) \char G.

Proof.

by elim: n => [|n IHn]; rewrite ?char_refl // dergSn charR. Qed.

Lemma der_sub n G : G^`(n) \subset G.

Proof.

by rewrite char_sub ?der_char. Qed.

Lemma der_norm n G : G \subset 'N(G^`(n)).

Proof.

by rewrite char_norm ?der_char. Qed.

Lemma der_normal n G : G^`(n) <| G.

Proof.

by rewrite char_normal ?der_char. Qed.

Lemma der_subS n G : G^`(n.+1) \subset G^`(n).

Proof.

by rewrite comm_subG. Qed.

Lemma der_normalS n G : G^`(n.+1) <| G^`(n).

Proof.

by rewrite sub_der1_normal // der_subS. Qed.

Lemma morphim_der rT D (f : {morphism D >-> rT}) n G :
   G \subset D -> f @* G^`(n) = (f @* G)^`(n).

Proof.

move=> sGD; elim: n => // n IHn.
by rewrite !dergSn -IHn morphimR ?(subset_trans (der_sub n G)).
Qed.

Lemma dergS n G H : G \subset H -> G^`(n) \subset H^`(n).

Proof.

by move=> sGH; elim: n => // n IHn; apply: commgSS. Qed.

Lemma quotient_der n G H : G \subset 'N(H) -> G^`(n) / H = (G / H)^`(n).

Proof.

exact: morphim_der. Qed.

Lemma derJ G n x : (G :^ x)^`(n) = G^`(n) :^ x.

Proof.

by elim: n => //= n IHn; rewrite !dergSn IHn -conjsRg. Qed.

Lemma derG1P G : reflect (G^`(1) = 1) (abelian G).

Proof.

exact: commG1P. Qed.

End Commutator_properties.

Arguments derG1P {gT G}.

Lemma der_cont n : GFunctor.continuous (@derived_at n).

Proof.

by move=> aT rT G f; rewrite morphim_der. Qed.

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

Proof.

exact: gFisog. Qed.