# Center of a monoid

Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer and Gregor Perčič.

Created on 2023-03-18.

module group-theory.centers-monoids where

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

open import group-theory.central-elements-monoids
open import group-theory.homomorphisms-monoids
open import group-theory.monoids
open import group-theory.submonoids


## Idea

The center of a monoid consists of those elements that are central.

## Definition

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

subtype-center-Monoid : type-Monoid M → Prop l
subtype-center-Monoid = is-central-element-prop-Monoid M

center-Monoid : Submonoid l M
pr1 center-Monoid = subtype-center-Monoid
pr1 (pr2 center-Monoid) = is-central-element-unit-Monoid M
pr2 (pr2 center-Monoid) = is-central-element-mul-Monoid M

monoid-center-Monoid : Monoid l
monoid-center-Monoid = monoid-Submonoid M center-Monoid

type-center-Monoid : UU l
type-center-Monoid =
type-Submonoid M center-Monoid

mul-center-Monoid :
(x y : type-center-Monoid) → type-center-Monoid
mul-center-Monoid = mul-Submonoid M center-Monoid

associative-mul-center-Monoid :
(x y z : type-center-Monoid) →
mul-center-Monoid (mul-center-Monoid x y) z ＝
mul-center-Monoid x (mul-center-Monoid y z)
associative-mul-center-Monoid =
associative-mul-Submonoid M center-Monoid

inclusion-center-Monoid :
type-center-Monoid → type-Monoid M
inclusion-center-Monoid =
inclusion-Submonoid M center-Monoid

preserves-mul-inclusion-center-Monoid :
{x y : type-center-Monoid} →
inclusion-center-Monoid (mul-center-Monoid x y) ＝
mul-Monoid M
( inclusion-center-Monoid x)
( inclusion-center-Monoid y)
preserves-mul-inclusion-center-Monoid {x} {y} =
preserves-mul-inclusion-Submonoid M center-Monoid {x} {y}

hom-inclusion-center-Monoid :
hom-Monoid monoid-center-Monoid M
hom-inclusion-center-Monoid =
hom-inclusion-Submonoid M center-Monoid