# Commutators of elements in groups

Content created by Egbert Rijke, Andreas Källberg, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-08-29.

module group-theory.commutators-groups where

Imports
open import foundation.identity-types
open import foundation.universe-levels

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


## Idea

A commutator gives an indication of the extent to which a group multiplication fails to be commutative.

The commutator of two elements, g and h, of a group G, is the element [g, h] = (gh)(hg)⁻¹.

https://en.wikipedia.org/wiki/Commutator#Group_theory

## Definition

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 unit if and only x and y commutes

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]

  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)