Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

more on commutator subgroups #2205

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

more on commutator subgroups #2205

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0401dc0
more on commutator subgroups
Alizter Jan 15, 2025
822b916
introduce opposite group and use it to shorten proofs
Alizter Jan 30, 2025
fef4619
commutator of subgroups is symmetric
Alizter Jan 30, 2025
3ba228f
shorten argument in isnormal_subgroup_commutator
Alizter Jan 30, 2025
0b90793
shorten proof of isnormal_subgroup_commutator
Alizter Jan 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
173 changes: 147 additions & 26 deletions theories/Algebra/Groups/Commutator.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
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)
Expand Down Expand Up @@ -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].
Expand All @@ -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.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
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.
Comment on lines +335 to +337
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this really require all three to be normal? Where is normality used in the proof?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When we precompose with a commutator the subgroup needs to be normal for the whole predicate to be a subgroup. We need the target to be a subgroup for the subgroup_commutator_rec lemma to be applied.

I got this statement as exercise 5.1.5 in J.S. Robinson's "A Course In the Theory of Groups". There it is stated as all subgroups being normal, but it is not clear if that is necessary.

I can easily come up with counter examples where none of the subgroups are normal, but I haven't been able to come up with one where only one is non-normal.

Copy link
Collaborator Author

@Alizter Alizter Jan 31, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did a beefier search (with GAP) where 2 subgroups where normal and the other was not and I was not able to find any counter examples. I'll need to find some spare time to think about this more deeply.

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.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
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] _.

Expand All @@ -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).
Expand Down Expand Up @@ -329,17 +450,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.
Expand Down
Loading