Central elements of semirings

module ring-theory.central-elements-semirings where
Imports
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.central-elements-monoids

open import ring-theory.semirings

Idea

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

Definition

module _
  {l : Level} (R : Semiring l)
  where

  is-central-element-semiring-Prop : type-Semiring R  Prop l
  is-central-element-semiring-Prop =
    is-central-element-monoid-Prop
      ( multiplicative-monoid-Semiring R)

  is-central-element-Semiring : type-Semiring R  UU l
  is-central-element-Semiring =
    is-central-element-Monoid (multiplicative-monoid-Semiring R)

  is-prop-is-central-element-Semiring :
    (x : type-Semiring R)  is-prop (is-central-element-Semiring x)
  is-prop-is-central-element-Semiring =
    is-prop-is-central-element-Monoid (multiplicative-monoid-Semiring R)

Properties

The zero element is central

module _
  {l : Level} (R : Semiring l)
  where

  is-central-element-zero-Semiring :
    is-central-element-Semiring R (zero-Semiring R)
  is-central-element-zero-Semiring x =
    left-zero-law-mul-Semiring R x  inv (right-zero-law-mul-Semiring R x)

The unit element is central

module _
  {l : Level} (R : Semiring l)
  where

  is-central-element-one-Semiring :
    is-central-element-Semiring R (one-Semiring R)
  is-central-element-one-Semiring =
    is-central-element-unit-Monoid (multiplicative-monoid-Semiring R)

The sum of two central elements is central

module _
  {l : Level} (R : Semiring l)
  where

  is-central-element-add-Semiring :
    (x y : type-Semiring R)  is-central-element-Semiring R x 
    is-central-element-Semiring R y 
    is-central-element-Semiring R (add-Semiring R x y)
  is-central-element-add-Semiring x y H K z =
    ( right-distributive-mul-add-Semiring R x y z) 
    ( ( ap-add-Semiring R (H z) (K z)) 
      ( inv (left-distributive-mul-add-Semiring R z x y)))

The product of two central elements is central

module _
  {l : Level} (R : Semiring l)
  where

  is-central-element-mul-Semiring :
    (x y : type-Semiring R) 
    is-central-element-Semiring R x  is-central-element-Semiring R y 
    is-central-element-Semiring R (mul-Semiring R x y)
  is-central-element-mul-Semiring =
    is-central-element-mul-Monoid (multiplicative-monoid-Semiring R)