From 0401dc048fc929421141a7a667a8aca81c805b7e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 04:01:42 +0100 Subject: [PATCH] more on commutator subgroups Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Commutator.v | 173 +++++++++++++++++++++++---- 1 file changed, 147 insertions(+), 26 deletions(-) diff --git a/theories/Algebra/Groups/Commutator.v b/theories/Algebra/Groups/Commutator.v index 7e5ae6afcf..7e3f3602e1 100644 --- a/theories/Algebra/Groups/Commutator.v +++ b/theories/Algebra/Groups/Commutator.v @@ -1,4 +1,5 @@ -Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc. +Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc + Basics.Iff. Require Import Types.Sigma. Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup Groups.QuotientGroup. @@ -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,36 @@ 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 Build_IsSubgroup; cbn beta. + - exact _. + - rewrite grp_commutator_unit_r. + apply subgroup_in_unit. + - intros y z Hxy Hxz. + rewrite grp_commutator_op_r. + apply subgroup_in_op. + + assumption. + + by rapply isnormal_conj. + - intros y Hxy. + rewrite grp_commutator_inv_r. + rapply isnormal_conj. + rewrite <- grp_commutator_inv. + by apply subgroup_in_inv. +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 +246,33 @@ 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. + (** 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 +281,101 @@ 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_subgorup_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. - lhs_V nrapply (grp_homo_commutator (grp_conj y)). - snrapply (ap (grp_conj y)). - exact p. + intros x. + snrapply functor_sigma. + - snrapply functor_sigma. + + exact (grp_conj y). + + exact (fun _ => isnormal_conj _). + - intros h. + snrapply functor_sigma. + + snrapply functor_sigma. + * exact (grp_conj y). + * exact (fun _ => isnormal_conj _). + + intros j. + intros p; simpl. + lhs_V nrapply (grp_homo_commutator (grp_conj y)). + 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; split. + - revert x; snrapply subgroup_commutator_rec. + intros x y Hx; revert y. + change (subgroup_product ?H ?J (grp_commutator x ?y)) + with (subgroup_precomp_commutator_r (subgroup_product H J) x y). + snrapply subgroup_generated_rec. + intros y [Ky | Ly]. + + 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 [HKx | HLx]. + + revert x HKx. + apply functor_subgroup_commutator; trivial. + apply subgroup_product_incl_l. + + revert x HLx. + apply functor_subgroup_commutator; trivial. + apply subgroup_product_incl_r. +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 +400,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,8 +450,8 @@ 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. @@ -338,8 +459,8 @@ Proof. 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.