Central elements of semirings

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

Created on 2023-03-18.
Last modified on 2023-11-24.

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-prop-Monoid
      ( 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)

Recent changes