Clean up the commutators of elements file (#829)

UniMath · Oct 11, 2023 · b7e3d6e · b7e3d6e
1 parent df1669f
commit b7e3d6e
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 10 deletions.
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
@@ -25,7 +25,7 @@ open import group-theory.central-elements-monoids public
 open import group-theory.central-elements-semigroups public
 open import group-theory.centralizer-subgroups public
 open import group-theory.commutative-monoids public
-open import group-theory.commutators-groups public
+open import group-theory.commutators-of-elements-groups public
 open import group-theory.commuting-elements-groups public
 open import group-theory.commuting-elements-monoids public
 open import group-theory.commuting-elements-semigroups public

diff --git a/src/group-theory/commutators-groups.lagda.md → ...y/commutators-of-elements-groups.lagda.md b/src/group-theory/commutators-groups.lagda.md → ...y/commutators-of-elements-groups.lagda.md
@@ -1,7 +1,7 @@
 # Commutators of elements in groups
 
 ```agda
-module group-theory.commutators-groups where
+module group-theory.commutators-of-elements-groups where
 ```
 
 <details><summary>Imports</summary>
@@ -18,16 +18,15 @@ 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
+The **commutator** of two elements `g` and `h` of a
+[group](group-theory.groups.md) `G` is defined to be the element
+`[g, h] = (gh)(hg)⁻¹`. The commutator of two elements `g` and `h` is equal to
+the unit if and only if `g` and `h` commute.
 
 ## Definition
 
+### The commutator operation
+
 ```agda
 module _
   {l : Level} (G : Group l)
@@ -39,7 +38,7 @@ module _
 
 ## Properties
 
-### The commutator of `x` and `y` is unit if and only `x` and `y` commutes
+### The commutator of `x` and `y` is the unit element if and only `x` and `y` commute
 
 ```agda
 module _
@@ -68,3 +67,9 @@ module _
   inv-commutator-Group x y =
     inv-right-div-Group G (mul-Group G x y) (mul-Group G y x)
 ```
+
+## External links
+
+- [Commutator](https://en.wikipedia.org/wiki/Commutator#Group_theory) at
+  Wikipedia
+- [Group commutator](https://ncatlab.org/nlab/show/group+commutator) at nlab