more on commutator subgroups

theories/Algebra/AbGroups/AbPushout.v

@@ -123,7 +123,7 @@ Definition path_ab_pushout `{Univalence} {A B C : AbGroup} (f : A $-> B) (g : A
   : @in_cosetL (ab_biprod B C) (ab_pushout_subgroup f g) bc0 bc1
                <~> (grp_quotient_map bc0 = grp_quotient_map bc1 :> ab_pushout f g).
 Proof.
-  rapply path_quotient.
+  nrapply path_quotient; exact _.
 Defined.
 
 (** The pushout of an embedding is an embedding. *)

theories/Algebra/Groups/Commutator.v

@@ -1,8 +1,9 @@
-Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
-Require Import Types.Sigma.
+Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
+  Basics.Iff Basics.Equivalences.
+Require Import Types.Sigma Types.Paths.
 Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
   Groups.QuotientGroup.
-Require Import WildCat.Core WildCat.EquivGpd.
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd.
 Require Import Truncations.Core.
 
 Local Open Scope mc_scope.
@@ -156,7 +157,7 @@ Proof.
   apply grp_inv_r.
 Defined.
 
-(** This variant of the Hall-Witt identity is useful later for proving the three subgroups lemma. *)  
+(** 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.
@@ -167,7 +168,7 @@ Defined.
 
 (** ** Precomposing normal subgroups with commutators *)
 
-Global Instance issubgroup_precomp_commutator {G : Group} (H : Subgroup G)
+Global Instance issubgroup_precomp_commutator_l {G : Group} (H : Subgroup G)
   `{!IsNormalSubgroup H} (y : G)
   : IsSubgroup (fun x => H [x, y]).
 Proof.
@@ -187,11 +188,28 @@ Proof.
     by apply subgroup_in_inv.
 Defined.
 
-Definition subgroup_precomp_commutator {G : Group} (H : Subgroup G) (y : G)
+Global Instance issubgroup_precomp_commutator_r {G : Group} (H : Subgroup G)
+  `{!IsNormalSubgroup H} (x : G)
+  : IsSubgroup (fun y => H [x, y]).
+Proof.
+  snrapply issubgroup_equiv.
+  - exact (fun y => H [y, x]^).
+  - intros y; cbn beta.
+    by rewrite grp_commutator_inv.
+  - exact (issubgroup_precomp_commutator_l
+      (subgroup_preimage (grp_op_iso_inv G) (subgroup_grp_op H)) x).
+Defined.
+
+Definition subgroup_precomp_commutator_l {G : Group} (H : Subgroup G) (y : G)
   `{!IsNormalSubgroup H}
   : Subgroup G
   := Build_Subgroup _ (fun x => H [x, y]) _.
 
+Definition subgroup_precomp_commutator_r {G : Group} (H : Subgroup G) (x : G)
+  `{!IsNormalSubgroup H}
+  : Subgroup G
+  := Build_Subgroup _ (fun y => H [x, y]) _.
+
 (** ** Commutator subgroups *)
 
 Definition subgroup_commutator {G : Group@{i}} (H K : Subgroup@{i i} G)
@@ -220,11 +238,76 @@ Definition subgroup_commutator_2_rec {G : Group} {H J K : Subgroup G}
 Proof.
   snrapply subgroup_commutator_rec.
   intros x z HJx Kz; revert x HJx.
-  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator N z x).
+  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator_l N z x).
   rapply subgroup_commutator_rec.
   by intros; apply i.
 Defined.
 
+(** A commutator of elements from each respective subgroup is in the commutator subgroup. *)
+Definition subgroup_commutator_in {G : Group} {H J : Subgroup G} {x y : G}
+  (Hx : H x) (Jy : J y)
+  : subgroup_commutator H J (grp_commutator x y).
+Proof.
+  apply tr, sgt_in.
+  by exists (x; Hx), (y; Jy).
+Defined.
+
+(** Commutator subgroups are functorial. *)
+Definition functor_subgroup_commutator {G : Group} {H J K L : Subgroup G}
+  (f : forall x, H x -> K x) (g : forall x, J x -> L x)
+  : forall x, [H, J] x -> [K, L] x.
+Proof.
+  snrapply subgroup_commutator_rec.
+  intros x y Hx Jx.
+  apply subgroup_commutator_in.
+  - by apply f.
+  - by apply g.
+Defined.
+
+Definition subgroup_eq_commutator {G : Group} {H J K L : Subgroup G}
+  (f : forall x, H x <-> K x) (g : forall x, J x <-> L x)
+  : forall x, [H, J] x <-> [K, L] x.
+Proof.
+  intros x; split; revert x; apply functor_subgroup_commutator.
+  1,3: apply f.
+  1,2: apply g.
+Defined.
+
+(** Commutator subgroups are symmetric in their arguments. *)
+Definition subgroup_commutator_symm {G : Group} (H J : Subgroup G)
+  : forall x, [H, J] x <-> [J, H] x.
+Proof.
+  intros x; split; revert x; snrapply subgroup_commutator_rec.
+  - intros x y Hx Jy.
+    nrapply subgroup_in_inv'.
+    rewrite grp_commutator_inv.
+    by apply subgroup_commutator_in.
+  - intros x y Jy Hx.
+    nrapply subgroup_in_inv'.
+    rewrite grp_commutator_inv.
+    by apply subgroup_commutator_in.
+Defined.
+
+(** The opposite subgroup of a commutator subgroup is the commutator subgroup of the opposite subgroups. *)
+Definition subgroup_eq_commutator_grp_op {G : Group} (H J : Subgroup G)
+  : forall (x : grp_op G), subgroup_grp_op [H, J] x
+    <-> [subgroup_grp_op H, subgroup_grp_op J] x.
+Proof.
+  intros x.
+  nrapply (iff_compose
+    (subgroup_eq_functor_subgroup_generated _ _ (grp_op_iso_inv G) _ x)
+    (equiv_subgroup_inv _ _)^-1%equiv).
+  clear x; intros x.
+  do 2 (snrapply (equiv_functor_sigma'
+    (grp_iso_subgroup_group (grp_op_iso_inv G)
+      (equiv_subgroup_inv (G:=grp_op G) (subgroup_grp_op _)))); intro).
+  simpl.
+  refine (equiv_moveL_equiv_M _ _ oE _).
+  apply equiv_concat_l.
+  apply moveR_equiv_V; symmetry.
+  nrapply (grp_homo_commutator (grp_op_iso_inv _)).
+Defined.
+
 (** A commutator subgroup of an abelian group is always trivial. *)
 Definition istrivial_commutator_subgroup_ab {A : AbGroup} (H K : Subgroup A)
   : IsTrivialGroup [H, K].
@@ -233,28 +316,80 @@ Proof.
   rapply ab_commutator.
 Defined.
 
-(** ** Derived subgroup *)
-
-(** The commutator subgroup of the maximal subgroup with itself is called the derived subgroup. It is the subgroup generated by all commutators. *)
-
-(** The derived subgroup is a normal subgroup. *)
-Global Instance isnormal_subgroup_derived {G : Group}
-  : IsNormalSubgroup [G, G].
+(** A commutator of normal subgroups is normal. *)
+Global Instance isnormal_subgroup_commutator {G : Group} (H J : Subgroup G)
+  `{!IsNormalSubgroup H, !IsNormalSubgroup J}
+  : IsNormalSubgroup [H, J].
 Proof.
   snrapply Build_IsNormalSubgroup'.
   intros x y; revert x.
   apply (functor_subgroup_generated _ _ (grp_conj y)).
-  intros g.
-  snrapply (functor_sigma (functor_sigma (grp_conj y) (fun _ => idmap)));
-    cbn beta; intros [x []].
-  snrapply (functor_sigma (functor_sigma (grp_conj y) (fun _ => idmap)));
-    cbn beta; intros [z []].
-  intros p; simpl.
+  intros x.
+  do 2 (rapply (functor_sigma (grp_iso_normal_conj _ y)); intro).
+  intros p.
   lhs_V nrapply (grp_homo_commutator (grp_conj y)).
-  snrapply (ap (grp_conj y)).
-  exact p.
+  exact (ap (grp_conj y) p).
 Defined.
 
+(** Commutator subgroups distribute over products of normal subgroups on the left. *)
+Definition subgroup_commutator_normal_prod_l {G : Group}
+  (H K L : NormalSubgroup G)
+  : forall x, [subgroup_product H K, L] x <-> subgroup_product [H, L] [K, L] x.
+Proof.
+  intros x; split.
+  - revert x; snrapply subgroup_commutator_rec.
+    intros x y HKx Ly; revert x HKx.
+    change (subgroup_product ?H ?J (grp_commutator ?x y))
+      with (subgroup_precomp_commutator_l (subgroup_product H J) y x).
+    snrapply subgroup_generated_rec.
+    intros x [Hx | Kx].
+    + apply subgroup_product_incl_l.
+      by apply subgroup_commutator_in.
+    + apply subgroup_product_incl_r.
+      by apply subgroup_commutator_in.
+  - revert x; snrapply subgroup_generated_rec.
+    intros x [HLx | KLx].
+    + revert x HLx.
+      apply functor_subgroup_commutator; trivial.
+      apply subgroup_product_incl_l.
+    + revert x KLx.
+      apply functor_subgroup_commutator; trivial.
+      apply subgroup_product_incl_r.
+Defined.
+
+(** Commutator subgroups distribute over products of normal subgroups on the right. *)
+Definition subgroup_commutator_normal_prod_r {G : Group}
+  (H K L : NormalSubgroup G)
+  : forall x, [H, subgroup_product K L] x <-> subgroup_product [H, K] [H, L] x.
+Proof.
+  intros x.
+  etransitivity.
+  1: symmetry; apply subgroup_commutator_symm.
+  etransitivity.
+  2: nrapply (subgroup_eq_functor_subgroup_product grp_iso_id
+    (subgroup_commutator_symm _ _) (subgroup_commutator_symm _ _)).
+  exact (subgroup_commutator_normal_prod_l K L H x).
+Defined.
+
+(** The subgroup image of a commutator is included in the commutator of the subgroup images. The converse only generally holds for a normal [J] and [K] and a surjective [f]. *)
+Definition subgroup_image_commutator_incl {G H : Group}
+  (f : G $-> H) (J K : Subgroup G)
+  : forall x, subgroup_image f [J, K] x
+    -> [subgroup_image f J, subgroup_image f K] x.
+Proof.
+  snrapply subgroup_image_rec.
+  change ([?G, ?H] (f ?x)) with (subgroup_preimage f [G, H] x).
+  snrapply subgroup_commutator_rec.
+  intros x y Jx Ky.
+  change (subgroup_preimage f [?G, ?H] ?x) with ([G, H] (f x)).
+  rewrite grp_homo_commutator.
+  apply subgroup_commutator_in;
+    by apply subgroup_image_in.
+Defined.
+
+(** ** Derived subgroup *)
+
+(** The commutator subgroup of the maximal subgroup with itself is called the derived subgroup. It is the subgroup generated by all commutators. *)
 Definition normalsubgroup_derived G : NormalSubgroup G
   := Build_NormalSubgroup G [G, G] _.
 
@@ -279,7 +414,7 @@ Definition abgroup_derived_quotient (G : Group) : AbGroup
   := Build_AbGroup (grp_derived_quotient G) _.
 
 (** We get a recursion principle into abelian groups. *)
-Definition abgroup_derived_quotient_rec {G : Group} {A : AbGroup} (f : G $-> A) 
+Definition abgroup_derived_quotient_rec {G : Group} {A : AbGroup} (f : G $-> A)
   : abgroup_derived_quotient G $-> A.
 Proof.
   snrapply (grp_quotient_rec _ _ f).
@@ -329,17 +464,17 @@ Proof.
     apply tr, sgt_in.
     unshelve eexists.
     + exists [x^, y].
-      apply tr, sgt_in.
-      by exists (x^; subgroup_in_inv _ _ Hx), (y; Jy). 
+      apply subgroup_commutator_in; trivial.
+      by apply subgroup_in_inv.
     + 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 _ _ Jy), (z^; subgroup_in_inv _ _ Kz). 
+      apply subgroup_commutator_in;
+        by apply subgroup_in_inv.
     + by exists (x; Hx).
   Local Open Scope group_scope.
 Defined.

theories/Algebra/Groups/Group.v

@@ -892,6 +892,39 @@ Defined.
 Definition grp_homo_const {G H : Group} : GroupHomomorphism G H
   := zero_morphism.
 
+(** ** Opposite Group *)
+
+(** The opposite group of a group is the group with the same elements but with the group operation reversed. *)
+Definition grp_op : Group -> Group.
+Proof.
+  intros G.
+  snrapply Build_Group'.
+  - exact G.
+  - exact _.
+  - exact (flip (.*.)).
+  - exact 1.
+  - exact (^).
+  - intros x y z.
+    symmetry.
+    exact (grp_assoc z y x).
+  - intro x.
+    exact (grp_unit_r x).
+  - intro x.
+    exact (grp_inv_r x).
+Defined.
+
+(** Taking the inverse is an isomorphism from the group to the opposite group. *)
+Definition grp_op_iso_inv (G : Group)
+  : G $<~> (grp_op G).
+Proof.
+  snrapply Build_GroupIsomorphism.
+  - snrapply Build_GroupHomomorphism.
+    + exact inv.
+    + intros x y.
+      rapply grp_inv_op.
+  - simpl; exact _.
+Defined.
+
 (** ** The direct product of groups *)
 
 (** The cartesian product of the underlying sets of two groups has a natural group structure. We call this the direct product of groups. *)