# Commutative semirings
```agda
module commutative-algebra.commutative-semirings where
```
<details><summary>Imports</summary>
```agda
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
```
</details>
## Idea
A [semiring](ring-theory.semirings.md) `A` is said to be
{{#concept "commutative" Disambiguation="semiring" Agda=is-commutative-Semiring}}
if its multiplicative operation is commutative, i.e., if `xy = yx` for all
`x, y ∈ A`.
## Definitions
### The predicate on semirings of being commutative
```agda
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
```agda
Commutative-Semiring :
( l : Level) → UU (lsuc l)
Commutative-Semiring l = Σ (Semiring l) is-commutative-Semiring
```
### Immediate infrastructure for commutative semirings
```agda
module _
{l : Level} (A : Commutative-Semiring l)
where
semiring-Commutative-Semiring : Semiring l
semiring-Commutative-Semiring = pr1 A
additive-commutative-monoid-Commutative-Semiring : Commutative-Monoid l
additive-commutative-monoid-Commutative-Semiring =
additive-commutative-monoid-Semiring semiring-Commutative-Semiring
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
add-Commutative-Semiring :
type-Commutative-Semiring → type-Commutative-Semiring →
type-Commutative-Semiring
add-Commutative-Semiring = add-Semiring semiring-Commutative-Semiring
add-Commutative-Semiring' :
type-Commutative-Semiring → type-Commutative-Semiring →
type-Commutative-Semiring
add-Commutative-Semiring' = add-Semiring' semiring-Commutative-Semiring
ap-add-Commutative-Semiring :
{x x' y y' : type-Commutative-Semiring} →
(x ＝ x') → (y ＝ y') →
add-Commutative-Semiring x y ＝ add-Commutative-Semiring x' y'
ap-add-Commutative-Semiring = ap-add-Semiring semiring-Commutative-Semiring
associative-add-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
( add-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
( add-Commutative-Semiring x (add-Commutative-Semiring y z))
associative-add-Commutative-Semiring =
associative-add-Semiring semiring-Commutative-Semiring
left-unit-law-add-Commutative-Semiring :
(x : type-Commutative-Semiring) →
add-Commutative-Semiring zero-Commutative-Semiring x ＝ x
left-unit-law-add-Commutative-Semiring =
left-unit-law-add-Semiring semiring-Commutative-Semiring
right-unit-law-add-Commutative-Semiring :
(x : type-Commutative-Semiring) →
add-Commutative-Semiring x zero-Commutative-Semiring ＝ x
right-unit-law-add-Commutative-Semiring =
right-unit-law-add-Semiring semiring-Commutative-Semiring
commutative-add-Commutative-Semiring :
(x y : type-Commutative-Semiring) →
add-Commutative-Semiring x y ＝ add-Commutative-Semiring y x
commutative-add-Commutative-Semiring =
commutative-add-Semiring semiring-Commutative-Semiring
interchange-add-add-Commutative-Semiring :
(x y x' y' : type-Commutative-Semiring) →
( add-Commutative-Semiring
( add-Commutative-Semiring x y)
( add-Commutative-Semiring x' y')) ＝
( add-Commutative-Semiring
( add-Commutative-Semiring x x')
( add-Commutative-Semiring y y'))
interchange-add-add-Commutative-Semiring =
interchange-add-add-Semiring semiring-Commutative-Semiring
right-swap-add-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
( add-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
( add-Commutative-Semiring (add-Commutative-Semiring x z) y)
right-swap-add-Commutative-Semiring =
right-swap-add-Semiring semiring-Commutative-Semiring
left-swap-add-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
( add-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
( add-Commutative-Semiring y (add-Commutative-Semiring x z))
left-swap-add-Commutative-Semiring =
left-swap-add-Semiring semiring-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
left-distributive-mul-add-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
( mul-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
( add-Commutative-Semiring
( mul-Commutative-Semiring x y)
( mul-Commutative-Semiring x z))
left-distributive-mul-add-Commutative-Semiring =
left-distributive-mul-add-Semiring semiring-Commutative-Semiring
right-distributive-mul-add-Commutative-Semiring :
(x y z : type-Commutative-Semiring) →
( mul-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
( add-Commutative-Semiring
( mul-Commutative-Semiring x z)
( mul-Commutative-Semiring y z))
right-distributive-mul-add-Commutative-Semiring =
right-distributive-mul-add-Semiring semiring-Commutative-Semiring
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
```agda
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
left-distributive-mul-nat-scalar-add-Commutative-Semiring :
(n : ℕ) (x y : type-Commutative-Semiring) →
mul-nat-scalar-Commutative-Semiring n (add-Commutative-Semiring x y) ＝
add-Commutative-Semiring
( mul-nat-scalar-Commutative-Semiring n x)
( mul-nat-scalar-Commutative-Semiring n y)
left-distributive-mul-nat-scalar-add-Commutative-Semiring =
left-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring
right-distributive-mul-nat-scalar-add-Commutative-Semiring :
(m n : ℕ) (x : type-Commutative-Semiring) →
mul-nat-scalar-Commutative-Semiring (m +ℕ n) x ＝
add-Commutative-Semiring
( mul-nat-scalar-Commutative-Semiring m x)
( mul-nat-scalar-Commutative-Semiring n x)
right-distributive-mul-nat-scalar-add-Commutative-Semiring =
right-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring
```