Commuting elements of groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-10.

module group-theory.commuting-elements-groups where

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

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


Idea

Two elements x and y of a group G are said to commute if the equality xy ＝ yx holds. For any element x, the subset of elements that commute with x form a subgroup of G called the centralizer of the element x.

Definitions

Commuting elements

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

commute-prop-Group : (x y : type-Group G) → Prop l
commute-prop-Group = commute-prop-Monoid (monoid-Group G)

commute-Group : (x y : type-Group G) → UU l
commute-Group = commute-Monoid (monoid-Group G)

commute-Group' : (x y : type-Group G) → UU l
commute-Group' = commute-Monoid' (monoid-Group G)

is-prop-commute-Group : (x y : type-Group G) → is-prop (commute-Group x y)
is-prop-commute-Group = is-prop-commute-Monoid (monoid-Group G)


Properties

The relation commute-Group is reflexive

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

refl-commute-Group : (x : type-Group G) → commute-Group G x x
refl-commute-Group = refl-commute-Monoid (monoid-Group G)


The relation commute-Group is symmetric

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

symmetric-commute-Group :
(x y : type-Group G) → commute-Group G x y → commute-Group G y x
symmetric-commute-Group = symmetric-commute-Monoid (monoid-Group G)


The unit element commutes with every element of the group

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

commute-unit-Group : (x : type-Group G) → commute-Group G x (unit-Group G)
commute-unit-Group = commute-unit-Monoid (monoid-Group G)


If x commutes with y, then x commutes with y⁻¹

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

commute-inv-Group :
(x y : type-Group G) →
commute-Group G x y → commute-Group G x (inv-Group G y)
commute-inv-Group x y H =
double-transpose-eq-mul-Group' G (inv H)


If x commutes with y, then x * (y * z) ＝ y * (x * z) for any element z

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

private
infix 45 _*_
_*_ = mul-Group G

left-swap-commute-Group :
(x y z : type-Group G) → commute-Group G x y →
x * (y * z) ＝ y * (x * z)
left-swap-commute-Group = left-swap-commute-Monoid (monoid-Group G)

right-swap-commute-Group :
(x y z : type-Group G) → commute-Group G y z →
(x * y) * z ＝ (x * z) * y
right-swap-commute-Group = right-swap-commute-Monoid (monoid-Group G)


If x commutes with y and with z, then x commutes with yz

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

commute-mul-Group :
(x y z : type-Group G) →
commute-Group G x y → commute-Group G x z →
commute-Group G x (mul-Group G y z)
commute-mul-Group = commute-mul-Monoid (monoid-Group G)