address review comments

Signed-off-by: Ali Caglayan <[email protected]>

theories/Algebra/Groups/Commutator.v

@@ -58,7 +58,8 @@ Proof.
   apply grp_commutator_commutes, commutativity.
 Defined.
 
-Definition grp_commutator_op {G : Group} (x y : G)
+(** The commutator can be thought of as the "error" in the commutativity of two elements of a group. *)
+Definition grp_commutator_swap_op {G : Group} (x y : G)
   : x * y = [x, y] * y * x.
 Proof.
   unfold grp_commutator.
@@ -97,13 +98,15 @@ Proof.
   by rewrite grp_inv_op, !grp_assoc, !grp_inv_gV_g.
 Defined.
 
+(** A commutator with the element on the right being multiplied on the right gives a conjugation. *)
 Definition grp_op_l_commutator {G : Group} (x y : G)
   : [x, y] * y = grp_conj x y.
 Proof.
   unfold grp_commutator, grp_conj, grp_homo_map.
   by rewrite grp_inv_gV_g.
 Defined.
 
+(** A commutator with the inverse element on the left being multiplied on the left gives a conjugation. *)
 Definition grp_op_r_commutator {G : Group} (x y : G)
   : x^ * [x, y] = grp_conj y x^.
 Proof.
@@ -143,6 +146,7 @@ Defined.
 
 (** ** Hall-Witt identity *)
 
+(** The Hall-Witt identtiy is a Jacobi-like identity for groups. It states that the the different commutators of 3 elements (with one conjugated) assemble into an identity. The proof is purely mechanical and simplify cancels all the terms. This is rare instance where a mechanized proof is much shorter than an on-paper proof. *)
 Definition grp_hall_witt {G : Group} (x y z : G)
   : [[x, y], grp_conj y z] * [[y, z], grp_conj z x] * [[z, x], grp_conj x y] = 1.
 Proof.
@@ -152,6 +156,7 @@ Proof.
   apply grp_inv_r.
 Defined.
 
+(** This variant of the Hall-Witt identity is useful later for proving the three subgroups lemma. *)  
 Definition grp_hall_witt' {G : Group} (x y z : G)
   :  grp_conj x [[x^, y], z] * grp_conj z [[z^, x], y] * grp_conj y [[y^, z], x] = 1.
 Proof.
@@ -193,27 +198,29 @@ Definition subgroup_commutator {G : Group@{i}} (H K : Subgroup@{i i} G)
   : Subgroup@{i i} G
   := subgroup_generated (fun g => exists (x : H) (y : K), [x.1, y.1] = g).
 
-Notation "[ G , H ]" := (subgroup_commutator G H) : group_scope.
+Notation "[ H , K ]" := (subgroup_commutator H K) : group_scope.
 
 Local Open Scope group_scope.
 
-Definition subgroup_commutator_rec {G : Group} {J K : Subgroup G} (L : Subgroup G)
-  (i : forall x y, J x -> K y -> L (grp_commutator x y))
-  : forall x, [J, K] x -> L x.
+(** [subgroup_commutator H K] is the smallest subgroup containing the commutators of elements of [H] with elements of [K]. *)
+Definition subgroup_commutator_rec {G : Group} {H K : Subgroup G} (J : Subgroup G)
+  (i : forall x y, H x -> K y -> J (grp_commutator x y))
+  : forall x, [H, K] x -> J x.
 Proof.
   rapply subgroup_generated_rec; intros x [[y Hy] [[z Kz] p]];
     destruct p; simpl.
   by apply i.
 Defined.
 
-Definition subgroup_commutator_2_rec {G : Group} {J K L : Subgroup G}
-  (M : Subgroup G) `{!IsNormalSubgroup M}
-  (i : forall x y z, J x -> K y -> L z -> M (grp_commutator (grp_commutator x y) z))
-  : forall x, [[J, K], L] x -> M x.
+(** Doubly iterated [subgroup_commutator]s of [H], [J] and [K] are the smallest of the normal subgroups containing the doubly iterated commutators of elements of [H], [J] and [K]. *)
+Definition subgroup_commutator_2_rec {G : Group} {H J K : Subgroup G}
+  (N : Subgroup G) `{!IsNormalSubgroup N}
+  (i : forall x y z, H x -> J y -> K z -> N (grp_commutator (grp_commutator x y) z))
+  : forall x, [[H, J], K] x -> N x.
 Proof.
   snrapply subgroup_commutator_rec.
-  intros x z HKx Lz; revert x HKx.
-  change (M (grp_commutator ?x z)) with (subgroup_precomp_commutator M z x).
+  intros x z HJx Kz; revert x HJx.
+  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator N z x).
   rapply subgroup_commutator_rec.
   by intros; apply i.
 Defined.
@@ -222,16 +229,15 @@ Defined.
 Definition istrivial_commutator_subgroup_ab {A : AbGroup} (H K : Subgroup A)
   : IsTrivialGroup [H, K].
 Proof.
-  rapply subgroup_generated_rec.
-  intros _ [a [b []]].
+  rapply subgroup_commutator_rec; intros.
   rapply ab_commutator.
 Defined.
 
 (** ** Derived subgroup *)
 
-(** The commutator subgroup of the maximal subgroups is called the derived subgroup. It is the subgroup generated by all commutators. *)
+(** The commutator subgroup of the maximal subgroup with itself is called the derived subgroup. It is the subgroup generated by all commutators. *)
 
-(** The dervied subgroup is a normal subgroup. *)
+(** The derived subgroup is a normal subgroup. *)
 Global Instance isnormal_subgroup_derived {G : Group}
   : IsNormalSubgroup [G, G].
 Proof.
@@ -278,9 +284,8 @@ Definition abgroup_derived_quotient_rec {G : Group} {A : AbGroup} (f : G $-> A)
 Proof.
   snrapply (grp_quotient_rec _ _ f).
   change (f ?n = 1) with (subgroup_preimage f (trivial_subgroup A) n).
-  snrapply subgroup_generated_rec.
-  intros x [y [z p]].
-  cbn in p; destruct p.
+  snrapply subgroup_commutator_rec.
+  intros x y _ _.
   lhs nrapply grp_homo_commutator.
   apply ab_commutator.
 Defined.
@@ -301,16 +306,15 @@ Defined.
 
 (** *** Three subgroups lemma *)
 
-Definition three_subgroups_lemma (G : Group) (X Y Z N : Subgroup G)
+Definition three_subgroups_lemma (G : Group) (H J K N : Subgroup G)
   `{!IsNormalSubgroup N}
-  : (forall x, [[X, Y], Z] x -> N x)
-    -> (forall x, [[Y, Z], X] x -> N x)
-    -> forall x, [[Z, X], Y] x -> N x.
+  (T1 : forall x, [[H, J], K] x -> N x)
+  (T2 : forall x, [[J, K], H] x -> N x)
+  : forall x, [[K, H], J] x -> N x.
 Proof.
-  intros T1 T2.
   rapply subgroup_commutator_2_rec.
   Local Close Scope group_scope.
-  intros z x y Zz Xx Yy.
+  intros z x y Kz Hx Jy.
   pose proof (grp_hall_witt' x y z^) as p.
   rewrite grp_inv_inv in p.
   apply grp_moveL_1V in p.
@@ -326,24 +330,24 @@ Proof.
     unshelve eexists.
     + exists [x^, y].
       apply tr, sgt_in.
-      by exists (x^; subgroup_in_inv _ _ Xx), (y; Yy). 
-    + by exists (z^; subgroup_in_inv _ _ Zz).
+      by exists (x^; subgroup_in_inv _ _ Hx), (y; Jy). 
+    + by exists (z^; subgroup_in_inv _ _ Kz).
   - apply subgroup_in_inv.
     rapply isnormal_conj.
     apply T2.
     apply tr, sgt_in.
     unshelve eexists.
     + exists [y^, z^].
       apply tr, sgt_in.
-      by exists (y^; subgroup_in_inv _ _ Yy), (z^; subgroup_in_inv _ _ Zz). 
-    + by exists (x; Xx).
+      by exists (y^; subgroup_in_inv _ _ Jy), (z^; subgroup_in_inv _ _ Kz). 
+    + by exists (x; Hx).
   Local Open Scope group_scope.
 Defined.
 
-Definition three_trivial_commutators (G : Group) (X Y Z : Subgroup G)
-  : IsTrivialGroup [[X, Y], Z]
-    -> IsTrivialGroup [[Y, Z], X]
-    -> IsTrivialGroup [[Z, X], Y].
+Definition three_trivial_commutators (G : Group) (H J K : Subgroup G)
+  : IsTrivialGroup [[H, J], K]
+    -> IsTrivialGroup [[J, K], H]
+    -> IsTrivialGroup [[K, H], J].
 Proof.
   rapply three_subgroups_lemma.
 Defined.