# Commutative semirings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Maša Žaucer.

Created on 2023-02-20.

module commutative-algebra.commutative-semirings where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.monoids

open import ring-theory.semirings


## Idea

A semiring A is said to be commutative if its multiplicative operation is commutative, i.e., if xy = yx for all x, y ∈ A.

## Definitions

### The predicate on semirings of being commutative

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

is-commutative-Semiring : UU l
is-commutative-Semiring =
(x y : type-Semiring A) → mul-Semiring A x y ＝ mul-Semiring A y x

is-prop-is-commutative-Semiring : is-prop is-commutative-Semiring
is-prop-is-commutative-Semiring =
is-prop-iterated-Π 2
( λ x y →
is-set-type-Semiring A (mul-Semiring A x y) (mul-Semiring A y x))

is-commutative-prop-Semiring : Prop l
is-commutative-prop-Semiring =
( is-commutative-Semiring , is-prop-is-commutative-Semiring)


### The type of commutative semirings

Commutative-Semiring :
( l : Level) → UU (lsuc l)
Commutative-Semiring l = Σ (Semiring l) is-commutative-Semiring


### Immediate infrastructure for commutative semirings

module _
{l : Level} (A : Commutative-Semiring l)
where

semiring-Commutative-Semiring : Semiring l
semiring-Commutative-Semiring = pr1 A

multiplicative-monoid-Commutative-Semiring : Monoid l
multiplicative-monoid-Commutative-Semiring =
multiplicative-monoid-Semiring semiring-Commutative-Semiring

set-Commutative-Semiring : Set l
set-Commutative-Semiring = set-Semiring semiring-Commutative-Semiring

type-Commutative-Semiring : UU l
type-Commutative-Semiring = type-Semiring semiring-Commutative-Semiring

is-set-type-Commutative-Semiring : is-set type-Commutative-Semiring
is-set-type-Commutative-Semiring =
is-set-type-Semiring semiring-Commutative-Semiring

zero-Commutative-Semiring : type-Commutative-Semiring
zero-Commutative-Semiring = zero-Semiring semiring-Commutative-Semiring

is-zero-Commutative-Semiring : type-Commutative-Semiring → UU l
is-zero-Commutative-Semiring = is-zero-Semiring semiring-Commutative-Semiring

is-nonzero-Commutative-Semiring : type-Commutative-Semiring → UU l
is-nonzero-Commutative-Semiring =
is-nonzero-Semiring semiring-Commutative-Semiring

type-Commutative-Semiring → type-Commutative-Semiring →
type-Commutative-Semiring

type-Commutative-Semiring → type-Commutative-Semiring →
type-Commutative-Semiring

{x x' y y' : type-Commutative-Semiring} →
(x ＝ x') → (y ＝ y') →

(x y z : type-Commutative-Semiring) →

(x : type-Commutative-Semiring) →

(x : type-Commutative-Semiring) →

(x y : type-Commutative-Semiring) →

(x y x' y' : type-Commutative-Semiring) →

(x y z : type-Commutative-Semiring) →

(x y z : type-Commutative-Semiring) →

mul-Commutative-Semiring :
(x y : type-Commutative-Semiring) → type-Commutative-Semiring
mul-Commutative-Semiring = mul-Semiring semiring-Commutative-Semiring

mul-Commutative-Semiring' :
(x y : type-Commutative-Semiring) → type-Commutative-Semiring
mul-Commutative-Semiring' = mul-Semiring' semiring-Commutative-Semiring

one-Commutative-Semiring : type-Commutative-Semiring
one-Commutative-Semiring = one-Semiring semiring-Commutative-Semiring

left-unit-law-mul-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-Commutative-Semiring one-Commutative-Semiring x ＝ x
left-unit-law-mul-Commutative-Semiring =
left-unit-law-mul-Semiring semiring-Commutative-Semiring

right-unit-law-mul-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-Commutative-Semiring x one-Commutative-Semiring ＝ x
right-unit-law-mul-Commutative-Semiring =
right-unit-law-mul-Semiring semiring-Commutative-Semiring

associative-mul-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
mul-Commutative-Semiring (mul-Commutative-Semiring x y) z ＝
mul-Commutative-Semiring x (mul-Commutative-Semiring y z)
associative-mul-Commutative-Semiring =
associative-mul-Semiring semiring-Commutative-Semiring

(x y z : type-Commutative-Semiring) →
( mul-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
( mul-Commutative-Semiring x y)
( mul-Commutative-Semiring x z))

(x y z : type-Commutative-Semiring) →
( mul-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
( mul-Commutative-Semiring x z)
( mul-Commutative-Semiring y z))

commutative-mul-Commutative-Semiring :
(x y : type-Commutative-Semiring) →
mul-Commutative-Semiring x y ＝ mul-Commutative-Semiring y x
commutative-mul-Commutative-Semiring = pr2 A

multiplicative-commutative-monoid-Commutative-Semiring :
Commutative-Monoid l
pr1 multiplicative-commutative-monoid-Commutative-Semiring =
multiplicative-monoid-Commutative-Semiring
pr2 multiplicative-commutative-monoid-Commutative-Semiring =
commutative-mul-Commutative-Semiring

left-zero-law-mul-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-Commutative-Semiring zero-Commutative-Semiring x ＝
zero-Commutative-Semiring
left-zero-law-mul-Commutative-Semiring =
left-zero-law-mul-Semiring semiring-Commutative-Semiring

right-zero-law-mul-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-Commutative-Semiring x zero-Commutative-Semiring ＝
zero-Commutative-Semiring
right-zero-law-mul-Commutative-Semiring =
right-zero-law-mul-Semiring semiring-Commutative-Semiring

right-swap-mul-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
mul-Commutative-Semiring (mul-Commutative-Semiring x y) z ＝
mul-Commutative-Semiring (mul-Commutative-Semiring x z) y
right-swap-mul-Commutative-Semiring =
right-swap-mul-Commutative-Monoid
multiplicative-commutative-monoid-Commutative-Semiring

left-swap-mul-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
mul-Commutative-Semiring x (mul-Commutative-Semiring y z) ＝
mul-Commutative-Semiring y (mul-Commutative-Semiring x z)
left-swap-mul-Commutative-Semiring =
left-swap-mul-Commutative-Monoid
multiplicative-commutative-monoid-Commutative-Semiring


## Operations

### Scalar multiplication of elements of a commutative ring by natural numbers

  mul-nat-scalar-Commutative-Semiring :
ℕ → type-Commutative-Semiring → type-Commutative-Semiring
mul-nat-scalar-Commutative-Semiring =
mul-nat-scalar-Semiring semiring-Commutative-Semiring

ap-mul-nat-scalar-Commutative-Semiring :
{m n : ℕ} {x y : type-Commutative-Semiring} →
(m ＝ n) → (x ＝ y) →
mul-nat-scalar-Commutative-Semiring m x ＝
mul-nat-scalar-Commutative-Semiring n y
ap-mul-nat-scalar-Commutative-Semiring =
ap-mul-nat-scalar-Semiring semiring-Commutative-Semiring

left-zero-law-mul-nat-scalar-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-nat-scalar-Commutative-Semiring 0 x ＝ zero-Commutative-Semiring
left-zero-law-mul-nat-scalar-Commutative-Semiring =
left-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring

right-zero-law-mul-nat-scalar-Commutative-Semiring :
(n : ℕ) →
mul-nat-scalar-Commutative-Semiring n zero-Commutative-Semiring ＝
zero-Commutative-Semiring
right-zero-law-mul-nat-scalar-Commutative-Semiring =
right-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring

left-unit-law-mul-nat-scalar-Commutative-Semiring :
(x : type-Commutative-Semiring) →
mul-nat-scalar-Commutative-Semiring 1 x ＝ x
left-unit-law-mul-nat-scalar-Commutative-Semiring =
left-unit-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring

left-nat-scalar-law-mul-Commutative-Semiring :
(n : ℕ) (x y : type-Commutative-Semiring) →
mul-Commutative-Semiring (mul-nat-scalar-Commutative-Semiring n x) y ＝
mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
left-nat-scalar-law-mul-Commutative-Semiring =
left-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring

right-nat-scalar-law-mul-Commutative-Semiring :
(n : ℕ) (x y : type-Commutative-Semiring) →
mul-Commutative-Semiring x (mul-nat-scalar-Commutative-Semiring n y) ＝
mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
right-nat-scalar-law-mul-Commutative-Semiring =
right-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring

(n : ℕ) (x y : type-Commutative-Semiring) →
mul-nat-scalar-Commutative-Semiring n (add-Commutative-Semiring x y) ＝
( mul-nat-scalar-Commutative-Semiring n x)
( mul-nat-scalar-Commutative-Semiring n y)