# Commuting elements of monoids

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-10.

module group-theory.commuting-elements-monoids where

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

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


## Idea

Two elements x and y of a monoid G are said to commute if the equality xy ＝ yx holds.

## Definitions

### Commuting elements

module _
{l : Level} (M : Monoid l)
where

commute-prop-Monoid : (x y : type-Monoid M) → Prop l
commute-prop-Monoid = commute-prop-Semigroup (semigroup-Monoid M)

commute-Monoid : (x y : type-Monoid M) → UU l
commute-Monoid = commute-Semigroup (semigroup-Monoid M)

commute-Monoid' : (x y : type-Monoid M) → UU l
commute-Monoid' = commute-Semigroup' (semigroup-Monoid M)

is-prop-commute-Monoid : (x y : type-Monoid M) → is-prop (commute-Monoid x y)
is-prop-commute-Monoid = is-prop-commute-Semigroup (semigroup-Monoid M)


## Properties

### The relation commute-Monoid is reflexive

module _
{l : Level} (M : Monoid l)
where

refl-commute-Monoid : (x : type-Monoid M) → commute-Monoid M x x
refl-commute-Monoid = refl-commute-Semigroup (semigroup-Monoid M)


### The relation commute-Monoid is symmetric

module _
{l : Level} (M : Monoid l)
where

symmetric-commute-Monoid :
(x y : type-Monoid M) → commute-Monoid M x y → commute-Monoid M y x
symmetric-commute-Monoid = symmetric-commute-Semigroup (semigroup-Monoid M)


### The unit element commutes with every element of the monoid

module _
{l : Level} (M : Monoid l)
where

commute-unit-Monoid : (x : type-Monoid M) → commute-Monoid M x (unit-Monoid M)
commute-unit-Monoid x =
right-unit-law-mul-Monoid M x ∙ inv (left-unit-law-mul-Monoid M x)


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

module _
{l : Level} (M : Monoid l)
where

private
infix 45 _*_
_*_ = mul-Monoid M

left-swap-commute-Monoid :
(x y z : type-Monoid M) → commute-Monoid M x y →
x * (y * z) ＝ y * (x * z)
left-swap-commute-Monoid = left-swap-commute-Semigroup (semigroup-Monoid M)

right-swap-commute-Monoid :
(x y z : type-Monoid M) → commute-Monoid M y z →
(x * y) * z ＝ (x * z) * y
right-swap-commute-Monoid = right-swap-commute-Semigroup (semigroup-Monoid M)


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

module _
{l : Level} (M : Monoid l)
where

commute-mul-Monoid :
(x y z : type-Monoid M) →
commute-Monoid M x y → commute-Monoid M x z →
commute-Monoid M x (mul-Monoid M y z)
commute-mul-Monoid = commute-mul-Semigroup (semigroup-Monoid M)