Commuting elements of monoids

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-10.
Last modified 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)

Recent changes