Center of a semigroup

module group-theory.centers-semigroups 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-semigroups
open import group-theory.homomorphisms-semigroups
open import group-theory.semigroups
open import group-theory.subsemigroups

Idea

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

Definition

module _
  {l : Level} (G : Semigroup l)
  where

  subtype-center-Semigroup : type-Semigroup G → Prop l
  subtype-center-Semigroup = is-central-element-semigroup-Prop G

  center-Semigroup : Subsemigroup l G
  pr1 center-Semigroup = subtype-center-Semigroup
  pr2 center-Semigroup = is-central-element-mul-Semigroup G

  semigroup-center-Semigroup : Semigroup l
  semigroup-center-Semigroup = semigroup-Subsemigroup G center-Semigroup

  type-center-Semigroup : UU l
  type-center-Semigroup =
    type-Subsemigroup G center-Semigroup

  mul-center-Semigroup :
    (x y : type-center-Semigroup) → type-center-Semigroup
  mul-center-Semigroup = mul-Subsemigroup G center-Semigroup

  associative-mul-center-Semigroup :
    (x y z : type-center-Semigroup) →
    mul-center-Semigroup (mul-center-Semigroup x y) z ＝
    mul-center-Semigroup x (mul-center-Semigroup y z)
  associative-mul-center-Semigroup =
    associative-mul-Subsemigroup G center-Semigroup

  inclusion-center-Semigroup :
    type-center-Semigroup → type-Semigroup G
  inclusion-center-Semigroup =
    inclusion-Subsemigroup G center-Semigroup

  preserves-mul-inclusion-center-Semigroup :
    (x y : type-center-Semigroup) →
    inclusion-center-Semigroup (mul-center-Semigroup x y) ＝
    mul-Semigroup G
      ( inclusion-center-Semigroup x)
      ( inclusion-center-Semigroup y)
  preserves-mul-inclusion-center-Semigroup =
    preserves-mul-inclusion-Subsemigroup G center-Semigroup

  hom-inclusion-center-Semigroup :
    type-hom-Semigroup semigroup-center-Semigroup G
  hom-inclusion-center-Semigroup =
    hom-inclusion-Subsemigroup G center-Semigroup