# Semirings ```agda module ring-theory.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.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.negation open import foundation.propositions open import foundation.sets open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.commutative-monoids open import group-theory.monoids open import group-theory.semigroups ``` </details> ## Idea The concept of a _semiring_ vastly generalizes the arithmetical structure on the [natural numbers](elementary-number-theory.natural-numbers.md). A {{#concept "semiring" Agda=Semiring}} consists of a [set](foundation-core.sets.md) equipped with addition and multiplication, where the addition operation gives the semiring the structure of a [commutative monoid](group-theory.commutative-monoids.md), and the multiplication is associative, unital, and distributive over addition. ## Definitions ### Semirings ```agda has-mul-Commutative-Monoid : {l : Level} → Commutative-Monoid l → UU l has-mul-Commutative-Monoid M = Σ ( has-associative-mul-Set (set-Commutative-Monoid M)) ( λ μ → ( is-unital (pr1 μ)) × ( ( (a b c : type-Commutative-Monoid M) → pr1 μ a (mul-Commutative-Monoid M b c) = mul-Commutative-Monoid M (pr1 μ a b) (pr1 μ a c)) × ( (a b c : type-Commutative-Monoid M) → pr1 μ (mul-Commutative-Monoid M a b) c = mul-Commutative-Monoid M (pr1 μ a c) (pr1 μ b c)))) zero-laws-Commutative-Monoid : {l : Level} (M : Commutative-Monoid l) → has-mul-Commutative-Monoid M → UU l zero-laws-Commutative-Monoid M ((μ , α) , laws) = ( (x : type-Commutative-Monoid M) → μ (unit-Commutative-Monoid M) x = unit-Commutative-Monoid M) × ((x : type-Commutative-Monoid M) → μ x (unit-Commutative-Monoid M) = unit-Commutative-Monoid M) Semiring : (l : Level) → UU (lsuc l) Semiring l1 = Σ ( Commutative-Monoid l1) ( λ M → Σ (has-mul-Commutative-Monoid M) (zero-laws-Commutative-Monoid M)) module _ {l : Level} (R : Semiring l) where additive-commutative-monoid-Semiring : Commutative-Monoid l additive-commutative-monoid-Semiring = pr1 R additive-monoid-Semiring : Monoid l additive-monoid-Semiring = monoid-Commutative-Monoid additive-commutative-monoid-Semiring additive-semigroup-Semiring : Semigroup l additive-semigroup-Semiring = semigroup-Commutative-Monoid additive-commutative-monoid-Semiring set-Semiring : Set l set-Semiring = set-Commutative-Monoid additive-commutative-monoid-Semiring type-Semiring : UU l type-Semiring = type-Commutative-Monoid additive-commutative-monoid-Semiring is-set-type-Semiring : is-set type-Semiring is-set-type-Semiring = is-set-type-Commutative-Monoid ( additive-commutative-monoid-Semiring) ``` ### Addition in a semiring ```agda module _ {l : Level} (R : Semiring l) where has-associative-add-Semiring : has-associative-mul-Set (set-Semiring R) has-associative-add-Semiring = has-associative-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) add-Semiring : type-Semiring R → type-Semiring R → type-Semiring R add-Semiring = mul-Commutative-Monoid (additive-commutative-monoid-Semiring R) add-Semiring' : type-Semiring R → type-Semiring R → type-Semiring R add-Semiring' = mul-Commutative-Monoid' (additive-commutative-monoid-Semiring R) ap-add-Semiring : {x y x' y' : type-Semiring R} → x = x' → y = y' → add-Semiring x y = add-Semiring x' y' ap-add-Semiring = ap-mul-Commutative-Monoid (additive-commutative-monoid-Semiring R) associative-add-Semiring : (x y z : type-Semiring R) → add-Semiring (add-Semiring x y) z = add-Semiring x (add-Semiring y z) associative-add-Semiring = associative-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) commutative-add-Semiring : (x y : type-Semiring R) → add-Semiring x y = add-Semiring y x commutative-add-Semiring = commutative-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) interchange-add-add-Semiring : (x y x' y' : type-Semiring R) → ( add-Semiring (add-Semiring x y) (add-Semiring x' y')) = ( add-Semiring (add-Semiring x x') (add-Semiring y y')) interchange-add-add-Semiring = interchange-mul-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) right-swap-add-Semiring : (x y z : type-Semiring R) → add-Semiring (add-Semiring x y) z = add-Semiring (add-Semiring x z) y right-swap-add-Semiring = right-swap-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) left-swap-add-Semiring : (x y z : type-Semiring R) → add-Semiring x (add-Semiring y z) = add-Semiring y (add-Semiring x z) left-swap-add-Semiring = left-swap-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ``` ### The zero element of a semiring ```agda module _ {l : Level} (R : Semiring l) where has-zero-Semiring : is-unital (add-Semiring R) has-zero-Semiring = has-unit-Commutative-Monoid ( additive-commutative-monoid-Semiring R) zero-Semiring : type-Semiring R zero-Semiring = unit-Commutative-Monoid (additive-commutative-monoid-Semiring R) is-zero-Semiring : type-Semiring R → UU l is-zero-Semiring x = Id x zero-Semiring is-nonzero-Semiring : type-Semiring R → UU l is-nonzero-Semiring x = ¬ (is-zero-Semiring x) is-zero-semiring-Prop : type-Semiring R → Prop l is-zero-semiring-Prop x = Id-Prop (set-Semiring R) x zero-Semiring left-unit-law-add-Semiring : (x : type-Semiring R) → Id (add-Semiring R zero-Semiring x) x left-unit-law-add-Semiring = left-unit-law-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) right-unit-law-add-Semiring : (x : type-Semiring R) → Id (add-Semiring R x zero-Semiring) x right-unit-law-add-Semiring = right-unit-law-mul-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ``` ### Multiplication in a semiring ```agda module _ {l : Level} (R : Semiring l) where has-associative-mul-Semiring : has-associative-mul-Set (set-Semiring R) has-associative-mul-Semiring = pr1 (pr1 (pr2 R)) mul-Semiring : type-Semiring R → type-Semiring R → type-Semiring R mul-Semiring = pr1 has-associative-mul-Semiring mul-Semiring' : type-Semiring R → type-Semiring R → type-Semiring R mul-Semiring' x y = mul-Semiring y x ap-mul-Semiring : {x x' y y' : type-Semiring R} (p : Id x x') (q : Id y y') → Id (mul-Semiring x y) (mul-Semiring x' y') ap-mul-Semiring p q = ap-binary mul-Semiring p q associative-mul-Semiring : (x y z : type-Semiring R) → Id (mul-Semiring (mul-Semiring x y) z) (mul-Semiring x (mul-Semiring y z)) associative-mul-Semiring = pr2 has-associative-mul-Semiring multiplicative-semigroup-Semiring : Semigroup l pr1 multiplicative-semigroup-Semiring = set-Semiring R pr2 multiplicative-semigroup-Semiring = has-associative-mul-Semiring left-distributive-mul-add-Semiring : (x y z : type-Semiring R) → mul-Semiring x (add-Semiring R y z) = add-Semiring R (mul-Semiring x y) (mul-Semiring x z) left-distributive-mul-add-Semiring = pr1 (pr2 (pr2 (pr1 (pr2 R)))) right-distributive-mul-add-Semiring : (x y z : type-Semiring R) → mul-Semiring (add-Semiring R x y) z = add-Semiring R (mul-Semiring x z) (mul-Semiring y z) right-distributive-mul-add-Semiring = pr2 (pr2 (pr2 (pr1 (pr2 R)))) bidistributive-mul-add-Semiring : (u v x y : type-Semiring R) → mul-Semiring (add-Semiring R u v) (add-Semiring R x y) = add-Semiring R ( add-Semiring R (mul-Semiring u x) (mul-Semiring u y)) ( add-Semiring R (mul-Semiring v x) (mul-Semiring v y)) bidistributive-mul-add-Semiring u v x y = ( right-distributive-mul-add-Semiring u v (add-Semiring R x y)) ∙ ( ap-add-Semiring R ( left-distributive-mul-add-Semiring u x y) ( left-distributive-mul-add-Semiring v x y)) left-zero-law-mul-Semiring : (x : type-Semiring R) → mul-Semiring (zero-Semiring R) x = zero-Semiring R left-zero-law-mul-Semiring = pr1 (pr2 (pr2 R)) right-zero-law-mul-Semiring : (x : type-Semiring R) → mul-Semiring x (zero-Semiring R) = zero-Semiring R right-zero-law-mul-Semiring = pr2 (pr2 (pr2 R)) ``` ### Multiplicative units in a semiring ```agda module _ {l : Level} (R : Semiring l) where is-unital-Semiring : is-unital (mul-Semiring R) is-unital-Semiring = pr1 (pr2 (pr1 (pr2 R))) multiplicative-monoid-Semiring : Monoid l pr1 multiplicative-monoid-Semiring = multiplicative-semigroup-Semiring R pr2 multiplicative-monoid-Semiring = is-unital-Semiring one-Semiring : type-Semiring R one-Semiring = unit-Monoid multiplicative-monoid-Semiring left-unit-law-mul-Semiring : (x : type-Semiring R) → Id (mul-Semiring R one-Semiring x) x left-unit-law-mul-Semiring = left-unit-law-mul-Monoid multiplicative-monoid-Semiring right-unit-law-mul-Semiring : (x : type-Semiring R) → Id (mul-Semiring R x one-Semiring) x right-unit-law-mul-Semiring = right-unit-law-mul-Monoid multiplicative-monoid-Semiring ``` ### Scalar multiplication of semiring elements by natural numbers ```agda module _ {l : Level} (R : Semiring l) where mul-nat-scalar-Semiring : ℕ → type-Semiring R → type-Semiring R mul-nat-scalar-Semiring zero-ℕ x = zero-Semiring R mul-nat-scalar-Semiring (succ-ℕ n) x = add-Semiring R (mul-nat-scalar-Semiring n x) x ap-mul-nat-scalar-Semiring : {m n : ℕ} {x y : type-Semiring R} → (m = n) → (x = y) → mul-nat-scalar-Semiring m x = mul-nat-scalar-Semiring n y ap-mul-nat-scalar-Semiring p q = ap-binary mul-nat-scalar-Semiring p q left-zero-law-mul-nat-scalar-Semiring : (x : type-Semiring R) → mul-nat-scalar-Semiring 0 x = zero-Semiring R left-zero-law-mul-nat-scalar-Semiring x = refl right-zero-law-mul-nat-scalar-Semiring : (n : ℕ) → mul-nat-scalar-Semiring n (zero-Semiring R) = zero-Semiring R right-zero-law-mul-nat-scalar-Semiring zero-ℕ = refl right-zero-law-mul-nat-scalar-Semiring (succ-ℕ n) = ( right-unit-law-add-Semiring R _) ∙ ( right-zero-law-mul-nat-scalar-Semiring n) left-unit-law-mul-nat-scalar-Semiring : (x : type-Semiring R) → mul-nat-scalar-Semiring 1 x = x left-unit-law-mul-nat-scalar-Semiring x = left-unit-law-add-Semiring R x left-nat-scalar-law-mul-Semiring : (n : ℕ) (x y : type-Semiring R) → mul-Semiring R (mul-nat-scalar-Semiring n x) y = mul-nat-scalar-Semiring n (mul-Semiring R x y) left-nat-scalar-law-mul-Semiring zero-ℕ x y = left-zero-law-mul-Semiring R y left-nat-scalar-law-mul-Semiring (succ-ℕ n) x y = ( right-distributive-mul-add-Semiring R ( mul-nat-scalar-Semiring n x) ( x) ( y)) ∙ ( ap ( add-Semiring' R (mul-Semiring R x y)) ( left-nat-scalar-law-mul-Semiring n x y)) right-nat-scalar-law-mul-Semiring : (n : ℕ) (x y : type-Semiring R) → mul-Semiring R x (mul-nat-scalar-Semiring n y) = mul-nat-scalar-Semiring n (mul-Semiring R x y) right-nat-scalar-law-mul-Semiring zero-ℕ x y = right-zero-law-mul-Semiring R x right-nat-scalar-law-mul-Semiring (succ-ℕ n) x y = ( left-distributive-mul-add-Semiring R x ( mul-nat-scalar-Semiring n y) ( y)) ∙ ( ap ( add-Semiring' R (mul-Semiring R x y)) ( right-nat-scalar-law-mul-Semiring n x y)) left-distributive-mul-nat-scalar-add-Semiring : (n : ℕ) (x y : type-Semiring R) → mul-nat-scalar-Semiring n (add-Semiring R x y) = add-Semiring R (mul-nat-scalar-Semiring n x) (mul-nat-scalar-Semiring n y) left-distributive-mul-nat-scalar-add-Semiring zero-ℕ x y = inv (left-unit-law-add-Semiring R (zero-Semiring R)) left-distributive-mul-nat-scalar-add-Semiring (succ-ℕ n) x y = ( ap ( add-Semiring' R (add-Semiring R x y)) ( left-distributive-mul-nat-scalar-add-Semiring n x y)) ∙ ( interchange-add-add-Semiring R ( mul-nat-scalar-Semiring n x) ( mul-nat-scalar-Semiring n y) ( x) ( y)) right-distributive-mul-nat-scalar-add-Semiring : (m n : ℕ) (x : type-Semiring R) → mul-nat-scalar-Semiring (m +ℕ n) x = add-Semiring R (mul-nat-scalar-Semiring m x) (mul-nat-scalar-Semiring n x) right-distributive-mul-nat-scalar-add-Semiring m zero-ℕ x = inv (right-unit-law-add-Semiring R (mul-nat-scalar-Semiring m x)) right-distributive-mul-nat-scalar-add-Semiring m (succ-ℕ n) x = ( ap ( add-Semiring' R x) ( right-distributive-mul-nat-scalar-add-Semiring m n x)) ∙ ( associative-add-Semiring R ( mul-nat-scalar-Semiring m x) ( mul-nat-scalar-Semiring n x) x) ```