From b7e3d6e787af31d7df8648a92bdd7231cf1bcf86 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 11 Oct 2023 11:32:04 +0200 Subject: [PATCH] Clean up the commutators of elements file (#829) --- src/group-theory.lagda.md | 2 +- ...> commutators-of-elements-groups.lagda.md} | 23 +++++++++++-------- 2 files changed, 15 insertions(+), 10 deletions(-) rename src/group-theory/{commutators-groups.lagda.md => commutators-of-elements-groups.lagda.md} (68%) diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index a7f0482419..ab41f53a15 100644 --- 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 b/src/group-theory/commutators-of-elements-groups.lagda.md similarity index 68% rename from src/group-theory/commutators-groups.lagda.md rename to src/group-theory/commutators-of-elements-groups.lagda.md index 27f20ee768..e2ad900e72 100644 --- a/src/group-theory/commutators-groups.lagda.md +++ b/src/group-theory/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 ```
Imports @@ -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