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 1 commit into
base: master
Choose a base branch
from
Open

more on commutator subgroups #2205

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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.
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.
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] _.

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