# Central elements of monoids

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-03-18.

module group-theory.central-elements-monoids where

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

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


## Idea

An element x of a monoid M is said to be central if xy ＝ yx for every y : M.

## Definition

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

is-central-element-prop-Monoid : type-Monoid M → Prop l
is-central-element-prop-Monoid =
is-central-element-prop-Semigroup (semigroup-Monoid M)

is-central-element-Monoid : type-Monoid M → UU l
is-central-element-Monoid =
is-central-element-Semigroup (semigroup-Monoid M)

is-prop-is-central-element-Monoid :
(x : type-Monoid M) → is-prop (is-central-element-Monoid x)
is-prop-is-central-element-Monoid =
is-prop-is-central-element-Semigroup (semigroup-Monoid M)


## Properties

### The unit element is central

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

is-central-element-unit-Monoid : is-central-element-Monoid M (unit-Monoid M)
is-central-element-unit-Monoid y =
left-unit-law-mul-Monoid M y ∙ inv (right-unit-law-mul-Monoid M y)


### The product of two central elements is central

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

is-central-element-mul-Monoid :
(x y : type-Monoid M) →
is-central-element-Monoid M x → is-central-element-Monoid M y →
is-central-element-Monoid M (mul-Monoid M x y)
is-central-element-mul-Monoid =
is-central-element-mul-Semigroup (semigroup-Monoid M)