Commutator subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-13.
Last modified on 2023-11-24.

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-∃
              ( 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

Recent changes