Commutator subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-13.
Last modified on 2024-04-11.

module group-theory.commutator-subgroups where

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)

See also

• The fact that the commutator subgroup is trivial if and only if the ambient group is abelian is recorded in group-theory.abelian-groups.

External links

• Commutator subgroup at $n$Lab
• Commutator subgroup at Wikidata
• Commutator subgroup at Wikipedia
• Commutator subgroup at Wolfram Mathworld

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2023-11-24. Egbert Rijke. Abelianization (#877).
• 2023-11-09. Fredrik Bakke. Typeset nlab as $n$Lab (#911).
• 2023-10-22. Egbert Rijke and Fredrik Bakke. Functoriality of the quotient operation on groups (#838).
• 2023-10-13. Egbert Rijke and Fredrik Bakke. The commutator subgroup (#835).