# Commutator subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-13.

module group-theory.commutator-subgroups where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import group-theory.commutators-of-elements-groups
open import group-theory.conjugation
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.images-of-group-homomorphisms
open import group-theory.normal-subgroups
open import group-theory.pullbacks-subgroups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-families-of-elements-groups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.subsets-groups


## Idea

Consider a group G. The commutator subgroup [G,G] of G is the subgroup generated by the commutators of G.

## Definitions

### The commutator subgroup of a group

module _
{l : Level} (G : Group l)
where

family-of-commutators-Group :
type-Group G × type-Group G → type-Group G
family-of-commutators-Group x =
commutator-Group G (pr1 x) (pr2 x)

commutator-subgroup-Group : Subgroup l G
commutator-subgroup-Group =
subgroup-family-of-elements-Group G family-of-commutators-Group

generating-subset-commutator-subgroup-Group : subset-Group l G
generating-subset-commutator-subgroup-Group =
generating-subset-subgroup-family-of-elements-Group G
family-of-commutators-Group

subset-commutator-subgroup-Group : subset-Group l G
subset-commutator-subgroup-Group =
subset-subgroup-family-of-elements-Group G family-of-commutators-Group

is-in-commutator-subgroup-Group : type-Group G → UU l
is-in-commutator-subgroup-Group =
is-in-subgroup-family-of-elements-Group G family-of-commutators-Group

is-closed-under-eq-commutator-subgroup-Group :
{x y : type-Group G} → is-in-commutator-subgroup-Group x →
x ＝ y → is-in-commutator-subgroup-Group y
is-closed-under-eq-commutator-subgroup-Group =
is-closed-under-eq-subgroup-family-of-elements-Group G
family-of-commutators-Group

is-closed-under-eq-commutator-subgroup-Group' :
{x y : type-Group G} → is-in-commutator-subgroup-Group y →
x ＝ y → is-in-commutator-subgroup-Group x
is-closed-under-eq-commutator-subgroup-Group' =
is-closed-under-eq-subgroup-family-of-elements-Group' G
family-of-commutators-Group

contains-unit-commutator-subgroup-Group :
contains-unit-subset-Group G subset-commutator-subgroup-Group
contains-unit-commutator-subgroup-Group =
contains-unit-subgroup-family-of-elements-Group G
family-of-commutators-Group

is-closed-under-multiplication-commutator-subgroup-Group :
is-closed-under-multiplication-subset-Group G
subset-commutator-subgroup-Group
is-closed-under-multiplication-commutator-subgroup-Group =
is-closed-under-multiplication-subgroup-family-of-elements-Group G
family-of-commutators-Group

is-closed-under-inverses-commutator-subgroup-Group :
is-closed-under-inverses-subset-Group G
subset-commutator-subgroup-Group
is-closed-under-inverses-commutator-subgroup-Group =
is-closed-under-inverses-subgroup-family-of-elements-Group G
family-of-commutators-Group

contains-commutator-commutator-subgroup-Group :
(x y : type-Group G) →
is-in-commutator-subgroup-Group (commutator-Group G x y)
contains-commutator-commutator-subgroup-Group x y =
contains-element-subgroup-family-of-elements-Group G
( family-of-commutators-Group)
( x , y)

is-subgroup-generated-by-family-of-commutators-commutator-subgroup-Group :
is-subgroup-generated-by-family-of-elements-Group G
family-of-commutators-Group
commutator-subgroup-Group
is-subgroup-generated-by-family-of-commutators-commutator-subgroup-Group =
is-subgroup-generated-by-family-of-elements-subgroup-family-of-elements-Group
( G)
( family-of-commutators-Group)

abstract
is-closed-under-conjugation-generating-subset-commutator-subgroup-Group :
is-closed-under-conjugation-subset-Group G
generating-subset-commutator-subgroup-Group
is-closed-under-conjugation-generating-subset-commutator-subgroup-Group
x y H =
apply-universal-property-trunc-Prop H
( generating-subset-commutator-subgroup-Group (conjugation-Group G x y))
( λ where
( (y , z) , refl) →
intro-exists
( conjugation-Group G x y , conjugation-Group G x z)
( inv (distributive-conjugation-commutator-Group G x y z)))

abstract
is-normal-commutator-subgroup-Group :
is-normal-Subgroup G commutator-subgroup-Group
is-normal-commutator-subgroup-Group =
is-normal-is-closed-under-conjugation-subgroup-subset-Group G
generating-subset-commutator-subgroup-Group
is-closed-under-conjugation-generating-subset-commutator-subgroup-Group

commutator-normal-subgroup-Group : Normal-Subgroup l G
pr1 commutator-normal-subgroup-Group = commutator-subgroup-Group
pr2 commutator-normal-subgroup-Group = is-normal-commutator-subgroup-Group


## Properties

### Every group homomorphism f : G → H maps [G,G] to [H,H]

There are two equivalent ways to express this fact:

1. The image im f [G,G] of the commutator subgroup of G is contained in the commutator subgroup of H.
2. The commutator subgroup of G is contained in the pullback of the commutator subgroup [H,H] along the group homomorphism f.

Indeed, by the image-pullback Galois connection there is a logical equivalence

  (im f [G,G] ⊆ [H,H]) ↔ ([G,G] ⊆ pullback f [H,H]).

module _
{l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
where

contains-image-commutator-subgroup-hom-Group :
leq-Subgroup H
( im-hom-Subgroup G H f (commutator-subgroup-Group G))
( commutator-subgroup-Group H)
contains-image-commutator-subgroup-hom-Group =
leq-subgroup-is-subgroup-generated-by-family-of-elements-Group H
( map-hom-Group G H f ∘ family-of-commutators-Group G)
( im-hom-Subgroup G H f (commutator-subgroup-Group G))
( is-subgroup-generated-by-family-of-elements-image-subgroup-family-of-elements-Group
( G)
( H)
( f)
( family-of-commutators-Group G))
( commutator-subgroup-Group H)
( λ x →
is-closed-under-eq-commutator-subgroup-Group' H
( contains-commutator-commutator-subgroup-Group H _ _)
( preserves-commutator-hom-Group G H f))

preserves-commutator-subgroup-hom-Group :
leq-Subgroup G
( commutator-subgroup-Group G)
( pullback-Subgroup G H f (commutator-subgroup-Group H))
preserves-commutator-subgroup-hom-Group =
forward-implication-is-image-subgroup-im-hom-Subgroup G H f
( commutator-subgroup-Group G)
( commutator-subgroup-Group H)
( contains-image-commutator-subgroup-hom-Group)