Commutators of elements in groups

Content created by Egbert Rijke and Fredrik Bakke.

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

module group-theory.commutators-of-elements-groups where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.commuting-elements-groups
open import group-theory.conjugation
open import group-theory.groups
open import group-theory.homomorphisms-groups

Idea

The commutator of two elements x and y of a group G is defined to be the element [x,y] = (xy)(yx)⁻¹. The commutator of two elements x and y is equal to the unit if and only if x and y commute.

Definition

The commutator operation

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

  commutator-Group : type-Group G → type-Group G → type-Group G
  commutator-Group x y = right-div-Group G (mul-Group G x y) (mul-Group G y x)

Properties

The commutator of x and y is the unit element if and only x and y commute

Proof: By transposing identifications along the group operation, we have an equivalence (xy ＝ yx) ≃ ((xy)(yx)⁻¹ ＝ e).

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

  is-unit-commutator-commute-Group :
    (x y : type-Group G) →
    commute-Group G x y → is-unit-Group G (commutator-Group G x y)
  is-unit-commutator-commute-Group x y H =
    is-unit-right-div-eq-Group G H

  commute-is-unit-commutator-Group :
    (x y : type-Group G) →
    is-unit-Group G (commutator-Group G x y) → commute-Group G x y
  commute-is-unit-commutator-Group x y H =
    eq-is-unit-right-div-Group G H

The inverse of the commutator [x,y] is [y,x]

Proof: Since (uv⁻¹)⁻¹ ＝ vu⁻¹ for any two elements u,v : G it follows that ((xy)(yx)⁻¹)⁻¹ ＝ (yx)(xy)⁻¹.

  inv-commutator-Group :
    (x y : type-Group G) →
    inv-Group G (commutator-Group G x y) ＝ commutator-Group G y x
  inv-commutator-Group x y =
    inv-right-div-Group G (mul-Group G x y) (mul-Group G y x)

Conjugation distributes over the commutator

Proof: The proof is a simple computation, using the fact that conjugation distributes over multiplication and preserves inverses:

  u(xy)(yx)⁻¹u⁻¹
  ＝ u(xy)u⁻¹u(yx)⁻¹u⁻¹
  ＝ ((uxu⁻¹)(uyu⁻¹))(u(yx)u⁻¹)⁻¹
  ＝ ((uxu⁻¹)(uyu⁻¹))((uyu⁻¹)(uxu⁻¹))⁻¹.

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

  distributive-conjugation-commutator-Group :
    (u x y : type-Group G) →
    conjugation-Group G u (commutator-Group G x y) ＝
    commutator-Group G (conjugation-Group G u x) (conjugation-Group G u y)
  distributive-conjugation-commutator-Group u x y =
    ( distributive-conjugation-mul-Group G u _ _) ∙
    ( ap-mul-Group G
      ( distributive-conjugation-mul-Group G u x y)
      ( ( conjugation-inv-Group G u _) ∙
        ( ap (inv-Group G) (distributive-conjugation-mul-Group G u y x))))

Group homomorphisms preserve commutators

Proof: Consider a group homomorphism f : G → H and two elements x y : G. Then we calculate

  f([x,y]) ≐ f((xy)(yx)⁻¹)
           = f(xy)f(yx)⁻¹
           = (f(x)f(y))(f(y)f(x))⁻¹
           ≐ [f(x),f(y)].

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

  preserves-commutator-hom-Group :
    {x y : type-Group G} →
    map-hom-Group G H f (commutator-Group G x y) ＝
    commutator-Group H (map-hom-Group G H f x) (map-hom-Group G H f y)
  preserves-commutator-hom-Group =
    ( preserves-right-div-hom-Group G H f) ∙
    ( ap-right-div-Group H
      ( preserves-mul-hom-Group G H f)
      ( preserves-mul-hom-Group G H f))

Recent changes