---
layout: default
file: "src/Classical/Structures/Group/Commutator.lagda.md"
title: "Classical.Structures.Group.Commutator module"
date: "2026-09-02"
author: "the agda-algebras development team"
---
### Commutators
This is the [Classical.Structures.Group.Commutator][] module of the [Agda Universal Algebra Library][].
For elements `x` and `y` of a group, the **commutator** `[ x ⸴ y ] = x ∙ y ∙ x ⁻¹ ∙ y ⁻¹`
is a measure of the failure of `x` and `y` to commute: it is the identity exactly
when `x ∙ y ≈ y ∙ x`.
This module defines the commutator and the commuting relation, and encodes the
small algebra the normal-subgroup structure theory of powers consumes; these are
the following:
+ `Commutes`{.AgdaFunction} and `[_⸴_]`{.AgdaFunction}, with their congruence lemmas;
+ the two absorption laws: a commutator with the identity in either slot is the identity;
+ the equivalence between `[ x ⸴ y ] ≈ ε` and `Commutes x y`, in both directions.
The absorption laws are the engine of the support-shrinking argument for subgroups
of a power above the diagonal: a commutator of two tuples vanishes at every
coordinate where *either* tuple vanishes, so iterated commutators cut a member's
support down to a prescribed block while the equivalence keeps a designated
coordinate away from the identity.
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Classical.Structures.Group.Commutator where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Product using ( _,_ )
open import Level using ( Level )
open import Relation.Binary using ( Setoid )
open import Relation.Nullary using ( ¬_ )
import Algebra.Properties.Group as GroupProperties
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Classical.Bundles.Group using ( ⟨_⟩ᵍᵖ )
open import Classical.Structures.Group.Basic using ( Group ; module Group-Op )
open import Setoid.Algebras.Basic using ( 𝕌[_] ; 𝔻[_] )
```
-->
#### The commutator and the commuting relation
`Commutator`{.AgdaModule}` 𝒢` packages the two notions and their algebra for a fixed group.
```agda
module Commutator {α ρ : Level} (𝒢@(𝑮 , _) : Group α ρ) where
open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( refl to ≈refl )
open SetoidReasoning 𝔻[ 𝑮 ]
open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; ⁻¹-cong ; assoc-law
; idˡ-law ; idʳ-law ; invˡ-law ; invʳ-law )
open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ε⁻¹≈ε )
```
**The commuting relation**: `x` and `y` commute when the two products agree.
```agda
Commutes : 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ] → Type ρ
Commutes x y = x ∙ y ≈ y ∙ x
```
The relation is a congruence in each slot separately; the right-slot form is the one the finite searches below the diagonal transport along an enumeration.
```agda
Commutes-congʳ : ∀ {x y y'} → y ≈ y' → Commutes x y → Commutes x y'
Commutes-congʳ {x} {y} {y'} e c = begin
x ∙ y' ≈˘⟨ ∙-cong ≈refl e ⟩
x ∙ y ≈⟨ c ⟩
y ∙ x ≈⟨ ∙-cong e ≈refl ⟩
y' ∙ x ∎
```
**The commutator**, in the left-normed convention `x ∙ y ∙ x ⁻¹ ∙ y ⁻¹`.
```agda
[_⸴_] : 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ]
[ x ⸴ y ] = x ∙ y ∙ x ⁻¹ ∙ y ⁻¹
```
The commutator is a congruence in both slots at once, by the congruences of the two group operations.
```agda
commutator-cong : ∀ {x x' y y'} → x ≈ x' → y ≈ y' → [ x ⸴ y ] ≈ [ x' ⸴ y' ]
commutator-cong ex ey = ∙-cong (∙-cong (∙-cong ex ey) (⁻¹-cong ex)) (⁻¹-cong ey)
```
#### The absorption laws
A commutator with the identity in the left slot collapses: the two `x`-factors become `ε` and `ε ⁻¹`, and what remains is `y ∙ y ⁻¹`.
```agda
commutator-εˡ : ∀ {x} y → x ≈ ε → [ x ⸴ y ] ≈ ε
commutator-εˡ {x} y x≈ε = begin
x ∙ y ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-cong (∙-cong (∙-cong x≈ε ≈refl) (⁻¹-cong x≈ε)) ≈refl ⟩
ε ∙ y ∙ ε ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-cong (∙-cong (idˡ-law y) ε⁻¹≈ε) ≈refl ⟩
y ∙ ε ∙ y ⁻¹ ≈⟨ ∙-cong (idʳ-law y) ≈refl ⟩
y ∙ y ⁻¹ ≈⟨ invʳ-law y ⟩
ε ∎
```
Symmetrically for the right slot, where what remains is `x ∙ x ⁻¹`.
```agda
commutator-εʳ : ∀ x {y} → y ≈ ε → [ x ⸴ y ] ≈ ε
commutator-εʳ x {y} y≈ε = begin
x ∙ y ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-cong (∙-cong (∙-cong ≈refl y≈ε) ≈refl) (⁻¹-cong y≈ε) ⟩
x ∙ ε ∙ x ⁻¹ ∙ ε ⁻¹ ≈⟨ ∙-cong (∙-cong (idʳ-law x) ≈refl) ε⁻¹≈ε ⟩
x ∙ x ⁻¹ ∙ ε ≈⟨ idʳ-law (x ∙ x ⁻¹) ⟩
x ∙ x ⁻¹ ≈⟨ invʳ-law x ⟩
ε ∎
```
#### The commutator detects commuting
Multiplying the commutator by `y ∙ x` on the right telescopes back to `x ∙ y`, so a trivial commutator forces the products to agree.
```agda
commutator≈ε→commutes : ∀ x y → [ x ⸴ y ] ≈ ε → Commutes x y
commutator≈ε→commutes x y h = begin
x ∙ y ≈˘⟨ idʳ-law (x ∙ y) ⟩
x ∙ y ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law x) ⟩
x ∙ y ∙ (x ⁻¹ ∙ x) ≈˘⟨ assoc-law (x ∙ y) (x ⁻¹) x ⟩
x ∙ y ∙ x ⁻¹ ∙ x ≈˘⟨ ∙-cong (idʳ-law (x ∙ y ∙ x ⁻¹)) ≈refl ⟩
x ∙ y ∙ x ⁻¹ ∙ ε ∙ x ≈˘⟨ ∙-cong (∙-cong ≈refl (invˡ-law y)) ≈refl ⟩
x ∙ y ∙ x ⁻¹ ∙ (y ⁻¹ ∙ y) ∙ x ≈˘⟨ ∙-cong (assoc-law (x ∙ y ∙ x ⁻¹) (y ⁻¹) y) ≈refl ⟩
x ∙ y ∙ x ⁻¹ ∙ y ⁻¹ ∙ y ∙ x ≈⟨ assoc-law [ x ⸴ y ] y x ⟩
[ x ⸴ y ] ∙ (y ∙ x) ≈⟨ ∙-cong h ≈refl ⟩
ε ∙ (y ∙ x) ≈⟨ idˡ-law (y ∙ x) ⟩
y ∙ x ∎
```
The contrapositive is the form the support-shrinking iteration consumes: a non-commuting pair of coordinate values keeps the commutator of the tuples away from the identity at that coordinate.
```agda
¬commutes→commutator≉ε : ∀ x y → ¬ Commutes x y → ¬ [ x ⸴ y ] ≈ ε
¬commutes→commutator≉ε x y nc h = nc (commutator≈ε→commutes x y h)
```
The forward direction closes the equivalence; it is the same telescope read backwards, recorded so that consumers never redo the rearrangement.
```agda
commutes→commutator≈ε : ∀ x y → Commutes x y → [ x ⸴ y ] ≈ ε
commutes→commutator≈ε x y c = begin
x ∙ y ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-cong (∙-cong c ≈refl) ≈refl ⟩
y ∙ x ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-cong (assoc-law y x (x ⁻¹)) ≈refl ⟩
y ∙ (x ∙ x ⁻¹) ∙ y ⁻¹ ≈⟨ ∙-cong (∙-cong ≈refl (invʳ-law x)) ≈refl ⟩
y ∙ ε ∙ y ⁻¹ ≈⟨ ∙-cong (idʳ-law y) ≈refl ⟩
y ∙ y ⁻¹ ≈⟨ invʳ-law y ⟩
ε ∎
```