# Commutative monoids

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-05-21.

module group-theory.commutative-monoids where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.interchange-law
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.unital-binary-operations
open import foundation.universe-levels

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


## Idea

A commutative monoid is a monoid M in which xy = yx holds for all x y : M.

## Definitions

### The predicate on monoids of being commutative

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

is-commutative-Monoid : UU l
is-commutative-Monoid =
(x y : type-Monoid M) → mul-Monoid M x y ＝ mul-Monoid M y x

is-prop-is-commutative-Monoid : is-prop is-commutative-Monoid
is-prop-is-commutative-Monoid =
is-prop-iterated-Π 2
( λ x y → is-set-type-Monoid M (mul-Monoid M x y) (mul-Monoid M y x))

is-commutative-prop-Monoid : Prop l
is-commutative-prop-Monoid =
( is-commutative-Monoid , is-prop-is-commutative-Monoid)


### Commutative monoids

Commutative-Monoid : (l : Level) → UU (lsuc l)
Commutative-Monoid l = Σ (Monoid l) is-commutative-Monoid

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

monoid-Commutative-Monoid : Monoid l
monoid-Commutative-Monoid = pr1 M

semigroup-Commutative-Monoid : Semigroup l
semigroup-Commutative-Monoid = semigroup-Monoid monoid-Commutative-Monoid

set-Commutative-Monoid : Set l
set-Commutative-Monoid = set-Monoid monoid-Commutative-Monoid

type-Commutative-Monoid : UU l
type-Commutative-Monoid = type-Monoid monoid-Commutative-Monoid

is-set-type-Commutative-Monoid : is-set type-Commutative-Monoid
is-set-type-Commutative-Monoid = is-set-type-Monoid monoid-Commutative-Monoid


### The multiplicative operation of a commutative monoid

  has-associative-mul-Commutative-Monoid :
has-associative-mul-Set set-Commutative-Monoid
has-associative-mul-Commutative-Monoid =
has-associative-mul-Semigroup semigroup-Commutative-Monoid

mul-Commutative-Monoid :
(x y : type-Commutative-Monoid) → type-Commutative-Monoid
mul-Commutative-Monoid = mul-Monoid monoid-Commutative-Monoid

mul-Commutative-Monoid' :
(x y : type-Commutative-Monoid) → type-Commutative-Monoid
mul-Commutative-Monoid' =
mul-Monoid' monoid-Commutative-Monoid

ap-mul-Commutative-Monoid :
{x x' y y' : type-Commutative-Monoid} →
x ＝ x' → y ＝ y' →
mul-Commutative-Monoid x y ＝ mul-Commutative-Monoid x' y'
ap-mul-Commutative-Monoid =
ap-mul-Monoid monoid-Commutative-Monoid

associative-mul-Commutative-Monoid :
(x y z : type-Commutative-Monoid) →
( mul-Commutative-Monoid (mul-Commutative-Monoid x y) z) ＝
( mul-Commutative-Monoid x (mul-Commutative-Monoid y z))
associative-mul-Commutative-Monoid =
associative-mul-Monoid monoid-Commutative-Monoid

commutative-mul-Commutative-Monoid :
(x y : type-Commutative-Monoid) →
mul-Commutative-Monoid x y ＝ mul-Commutative-Monoid y x
commutative-mul-Commutative-Monoid = pr2 M

interchange-mul-mul-Commutative-Monoid :
(x y x' y' : type-Commutative-Monoid) →
( mul-Commutative-Monoid
( mul-Commutative-Monoid x y)
( mul-Commutative-Monoid x' y')) ＝
( mul-Commutative-Monoid
( mul-Commutative-Monoid x x')
( mul-Commutative-Monoid y y'))
interchange-mul-mul-Commutative-Monoid =
interchange-law-commutative-and-associative
mul-Commutative-Monoid
commutative-mul-Commutative-Monoid
associative-mul-Commutative-Monoid

right-swap-mul-Commutative-Monoid :
(x y z : type-Commutative-Monoid) →
mul-Commutative-Monoid (mul-Commutative-Monoid x y) z ＝
mul-Commutative-Monoid (mul-Commutative-Monoid x z) y
right-swap-mul-Commutative-Monoid x y z =
( associative-mul-Commutative-Monoid x y z) ∙
( ap
( mul-Commutative-Monoid x)
( commutative-mul-Commutative-Monoid y z)) ∙
( inv (associative-mul-Commutative-Monoid x z y))

left-swap-mul-Commutative-Monoid :
(x y z : type-Commutative-Monoid) →
mul-Commutative-Monoid x (mul-Commutative-Monoid y z) ＝
mul-Commutative-Monoid y (mul-Commutative-Monoid x z)
left-swap-mul-Commutative-Monoid x y z =
( inv (associative-mul-Commutative-Monoid x y z)) ∙
( ap
( mul-Commutative-Monoid' z)
( commutative-mul-Commutative-Monoid x y)) ∙
( associative-mul-Commutative-Monoid y x z)


### The unit element of a commutative monoid

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

has-unit-Commutative-Monoid : is-unital (mul-Commutative-Monoid M)
has-unit-Commutative-Monoid =
has-unit-Monoid (monoid-Commutative-Monoid M)

unit-Commutative-Monoid : type-Commutative-Monoid M
unit-Commutative-Monoid = unit-Monoid (monoid-Commutative-Monoid M)

left-unit-law-mul-Commutative-Monoid :
(x : type-Commutative-Monoid M) →
mul-Commutative-Monoid M unit-Commutative-Monoid x ＝ x
left-unit-law-mul-Commutative-Monoid =
left-unit-law-mul-Monoid (monoid-Commutative-Monoid M)

right-unit-law-mul-Commutative-Monoid :
(x : type-Commutative-Monoid M) →
mul-Commutative-Monoid M x unit-Commutative-Monoid ＝ x
right-unit-law-mul-Commutative-Monoid =
right-unit-law-mul-Monoid (monoid-Commutative-Monoid M)

is-unit-Commutative-Monoid : type-Commutative-Monoid M → UU l
is-unit-Commutative-Monoid x = Id x unit-Commutative-Monoid

is-unit-prop-Commutative-Monoid : type-Commutative-Monoid M → Prop l
is-unit-prop-Commutative-Monoid x =
Id-Prop (set-Commutative-Monoid M) x unit-Commutative-Monoid