Central elements of semirings

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

Created on 2023-03-18.
Last modified on 2023-06-10.

module group-theory.central-elements-semigroups where
open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.semigroups


An element x of a semigroup G is said to be central if xy = yx for every y : G.


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

  is-central-element-semigroup-Prop : type-Semigroup G  Prop l
  is-central-element-semigroup-Prop x =
      ( type-Semigroup G)
      ( λ y 
          ( set-Semigroup G)
          ( mul-Semigroup G x y)
          ( mul-Semigroup G y x))

  is-central-element-Semigroup : type-Semigroup G  UU l
  is-central-element-Semigroup x =
    type-Prop (is-central-element-semigroup-Prop x)

  is-prop-is-central-element-Semigroup :
    (x : type-Semigroup G)  is-prop (is-central-element-Semigroup x)
  is-prop-is-central-element-Semigroup x =
    is-prop-type-Prop (is-central-element-semigroup-Prop x)


The product of two central elements is central

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

  is-central-element-mul-Semigroup :
    (x y : type-Semigroup G) 
    is-central-element-Semigroup G x  is-central-element-Semigroup G y 
    is-central-element-Semigroup G (mul-Semigroup G x y)
  is-central-element-mul-Semigroup x y H K z =
    ( associative-mul-Semigroup G x y z) 
    ( ( ap (mul-Semigroup G x) (K z)) 
      ( ( inv (associative-mul-Semigroup G x z y)) 
        ( ( ap (mul-Semigroup' G y) (H z)) 
          ( associative-mul-Semigroup G z x y))))

Recent changes