Commutators, commutator subgroups and three subgroups lemma

theories/Algebra/Groups/Commutator.v

@@ -0,0 +1,349 @@
+Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
+Require Import Types.Sigma.
+Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
+  Groups.QuotientGroup.
+Require Import WildCat.Core WildCat.EquivGpd.
+Require Import Truncations.Core.
+
+Local Open Scope mc_scope.
+Local Open Scope mc_mult_scope.
+
+Set Universe Minimization ToSet.
+
+(** Commutators in groups *)
+
+(** ** Commutators of group elements *)
+
+(** Note that this convention is chosen due to the convention we chose for group conjugation elsewhere. *)
+Definition grp_commutator {G : Group} (x y : G) : G := x * y * x^ * y^.
+
+Notation "[ x , y ]" := (grp_commutator x y) : mc_mult_scope.
+
+(** ** Easy properties of commutators *)
+
+(** Commuting elements of a group have trivial commutator. *)
+Definition grp_commutator_commutes {G : Group} (x y : G) (p : x * y = y * x)
+  : [x, y] = 1.
+Proof.
+  unfold grp_commutator.
+  rewrite p, grp_inv_gg_V.
+  apply grp_inv_r.
+Defined.
+
+(** A commutator of an element with itself is the unit. *)
+Definition grp_commutator_cancel {G : Group} (x y : G)
+  : [x, x] = 1.
+Proof.
+  by apply grp_commutator_commutes.
+Defined.
+
+(** A commutator of a group element with unit on the left is the unit. *)
+Definition grp_commutator_unit_l {G : Group} (x : G)
+  : [1, x] = 1.
+Proof.
+  by apply grp_commutator_commutes, grp_1g_g1.
+Defined.
+
+(** A commutator of a group element with unit on the right is the unit. *)
+Definition grp_commutator_unit_r {G : Group} (x : G)
+  : [x, 1] = 1.
+Proof.
+  by apply grp_commutator_commutes, grp_g1_1g.
+Defined.
+
+(** Commutators in abelian groups are trivial. *)
+Definition ab_commutator (A : AbGroup) (x y : A)
+  : [x, y] = 1.
+Proof.
+  apply grp_commutator_commutes, commutativity.
+Defined.
+
+Definition grp_commutator_op {G : Group} (x y : G)
+  : x * y = [x, y] * y * x.
+Proof.
+  unfold grp_commutator.
+  by rewrite !grp_inv_gV_g.
+Defined.
+
+(** Inverting a commutator reverses the order. *)
+Definition grp_commutator_inv {G : Group} (x y : G)
+  : [x, y]^ = [y, x].
+Proof.
+  unfold grp_commutator.
+  by rewrite 3 grp_inv_op, 2 grp_inv_inv, 2 grp_assoc.
+Defined.
+
+(** Group homomorphisms commute with commutators. *)
+Definition grp_homo_commutator {G H : Group} (f : G $-> H) (x y : G)
+  : f [x, y] = [f x, f y].
+Proof.
+  unfold grp_commutator.
+  by rewrite !grp_homo_op, !grp_homo_inv.
+Defined.
+
+(** A commutator with a product on the left side can be expanded as the product of a conjugated commutator and another commutator. *)
+Definition grp_commutator_op_l {G : Group} (x y z : G)
+  : [x * y, z] = grp_conj x [y, z] * [x, z].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite grp_inv_op, !grp_assoc, !grp_inv_gV_g.
+Defined.
+
+(** A commutator with a product on the right side can be expanded as the product of a conjugated commutator and another commutator. *)
+Definition grp_commutator_op_r {G : Group} (x y z : G)
+  : [x, y * z] = [x, y] * grp_conj y [x, z].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite grp_inv_op, !grp_assoc, !grp_inv_gV_g.
+Defined.
+
+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.
+
+Definition grp_op_r_commutator {G : Group} (x y : G)
+  : x^ * [x, y] = grp_conj y x^.
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite <- !grp_assoc, grp_inv_V_gg.
+Defined.
+
+(** Commutators with inverted left sides are conjugated commutators. *)
+Definition grp_commutator_inv_l {G : Group} (x y : G)
+  : [x^, y] = grp_conj x^ [y, x].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite !grp_assoc, grp_inv_inv, grp_inv_gV_g.
+Defined.
+
+(** Commutators with inverted right sides are conjugated commutators. *)
+Definition grp_commutator_inv_r {G : Group} (x y : G)
+  : [x, y^] = grp_conj y^ [y, x].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite <- !grp_assoc, grp_inv_inv, grp_inv_V_gg.
+Defined.
+
+Definition grp_conj_commutator_inv_l {G : Group} (x y : G)
+  : grp_conj x [x^, y] = [y, x].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite !grp_inv_inv, <- !grp_assoc, grp_inv_g_Vg.
+Defined.
+
+Definition grp_conj_commutator_inv_r {G : Group} (x y : G)
+  : grp_conj y [x, y^] = [y, x].
+Proof.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  by rewrite grp_inv_inv, !grp_assoc, grp_inv_gg_V.
+Defined.
+
+(** ** Hall-Witt identity *)
+
+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.
+  unfold grp_commutator, grp_conj, grp_homo_map.
+  rewrite !grp_inv_op, !grp_inv_inv, !grp_assoc.
+  do 3 rewrite !grp_inv_gV_g, !grp_inv_gg_V.
+  apply grp_inv_r.
+Defined.
+
+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.
+  rewrite 3 (grp_homo_commutator _ [_^, _]).
+  rewrite 3 grp_conj_commutator_inv_l.
+  apply grp_hall_witt.
+Defined.
+
+(** ** Precomposing normal subgroups with commutators *)
+
+Global Instance issubgroup_precomp_commutator {G : Group} (H : Subgroup G)
+  `{!IsNormalSubgroup H} (y : G)
+  : IsSubgroup (fun x => H [x, y]).
+Proof.
+  snrapply Build_IsSubgroup; cbn beta.
+  - exact _.
+  - rewrite grp_commutator_unit_l.
+    apply subgroup_in_unit.
+  - intros x z Hxy Hzy.
+    rewrite grp_commutator_op_l.
+    apply subgroup_in_op.
+    + by rapply isnormal_conj.
+    + assumption.
+  - intros x Hxy.
+    rewrite grp_commutator_inv_l.
+    rapply isnormal_conj.
+    rewrite <- grp_commutator_inv.
+    by apply subgroup_in_inv.
+Defined.
+
+Definition subgroup_precomp_commutator {G : Group} (H : Subgroup G) (y : G)
+  `{!IsNormalSubgroup H}
+  : Subgroup G
+  := Build_Subgroup _ (fun x => H [x, y]) _.
+
+(** ** Commutator subgroups *)
+
+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.
+
+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.
+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.
+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).
+  rapply subgroup_commutator_rec.
+  by intros; apply i.
+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].
+Proof.
+  rapply subgroup_generated_rec.
+  intros _ [a [b []]].
+  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 dervied subgroup is a normal subgroup. *)
+Global Instance isnormal_subgroup_derived {G : Group}
+  : IsNormalSubgroup [G, G].
+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.
+  lhs_V nrapply (grp_homo_commutator (grp_conj y)).
+  snrapply (ap (grp_conj y)).
+  exact p.
+Defined.
+
+Definition normalsubgroup_derived G : NormalSubgroup G
+  := Build_NormalSubgroup G [G, G] _.
+
+(** We can quotient a group by its derived subgroup. *)
+Definition grp_derived_quotient (G : Group) : Group
+  := QuotientGroup G (normalsubgroup_derived G).
+
+(** We can show that the multiplication then becomes commutative. *)
+Global Instance commutative_grp_derived_quotient (G : Group)
+  : Commutative (A:=grp_derived_quotient G) (.*.).
+Proof.
+  intros x.
+  srapply grp_quotient_ind_hprop; intros y; revert x.
+  srapply grp_quotient_ind_hprop; intros x; cbn beta.
+  apply qglue, tr, sgt_in; exists (y^; tt), (x^; tt).
+  unfold grp_commutator; simpl.
+  by rewrite !grp_inv_op, !grp_inv_inv, !grp_assoc.
+Defined.
+
+(** Hence we have a way of producing abelian groups from groups. *)
+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) 
+  : abgroup_derived_quotient 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.
+  lhs nrapply grp_homo_commutator.
+  apply ab_commutator.
+Defined.
+
+(** Furthermore, this construction is an abelianization. *)
+Definition isabelianization_derived_quotient (G : Group)
+  : IsAbelianization (abgroup_derived_quotient G) grp_quotient_map.
+Proof.
+  intros A.
+  snrapply Build_IsSurjInj.
+  - intros f.
+    nrefine (abgroup_derived_quotient_rec f; _).
+    hnf; reflexivity.
+  - intros f g p.
+    srapply grp_quotient_ind_hprop; intros x; cbn beta.
+    exact (p x).
+Defined.
+
+(** *** Three subgroups lemma *)
+
+Definition three_subgroups_lemma (G : Group) (X Y Z 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.
+Proof.
+  intros T1 T2.
+  rapply subgroup_commutator_2_rec.
+  Local Close Scope group_scope.
+  intros z x y Zz Xx Yy.
+  pose proof (grp_hall_witt' x y z^) as p.
+  rewrite grp_inv_inv in p.
+  apply grp_moveL_1V in p.
+  apply grp_moveL_Vg in p.
+  apply (isnormal_conj _ (y:=z^))^-1.
+  change (N (grp_conj z^ [[z, x], y])).
+  rewrite p.
+  apply subgroup_in_op.
+  - apply subgroup_in_inv.
+    rapply isnormal_conj.
+    apply T1.
+    apply tr, sgt_in.
+    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).
+  - 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).
+  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].
+Proof.
+  rapply three_subgroups_lemma.
+Defined.