# Function semirings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-13.

module ring-theory.function-semirings where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

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

open import ring-theory.dependent-products-semirings
open import ring-theory.semirings


## Idea

Given a semiring R and a type X, the function semiring R^X consists of functions from X into the underlying type of R. The semiring operations are defined pointwise

## Definition

module _
{l1 l2 : Level} (R : Semiring l1) (X : UU l2)
where

additive-commutative-monoid-function-Semiring : Commutative-Monoid (l1 ⊔ l2)
additive-commutative-monoid-Π-Semiring X (λ _ → R)

multiplicative-monoid-function-Semiring : Monoid (l1 ⊔ l2)
multiplicative-monoid-function-Semiring =
multiplicative-monoid-Π-Semiring X (λ _ → R)

set-function-Semiring : Set (l1 ⊔ l2)
set-function-Semiring = set-Π-Semiring X (λ _ → R)

type-function-Semiring : UU (l1 ⊔ l2)
type-function-Semiring = type-Π-Semiring X (λ _ → R)

is-set-type-function-Semiring : is-set type-function-Semiring
is-set-type-function-Semiring =
is-set-type-Π-Semiring X (λ _ → R)

type-function-Semiring → type-function-Semiring → type-function-Semiring

zero-function-Semiring : type-function-Semiring
zero-function-Semiring = zero-Π-Semiring X (λ _ → R)

(x y z : type-function-Semiring) →
associative-add-Π-Semiring X (λ _ → R)

(x : type-function-Semiring) →
left-unit-law-add-Π-Semiring X (λ _ → R)

(x : type-function-Semiring) →
right-unit-law-add-Π-Semiring X (λ _ → R)

(x y : type-function-Semiring) →
commutative-add-Π-Semiring X (λ _ → R)

mul-function-Semiring :
type-function-Semiring → type-function-Semiring → type-function-Semiring
mul-function-Semiring =
mul-Π-Semiring X (λ _ → R)

one-function-Semiring : type-function-Semiring
one-function-Semiring = one-Π-Semiring X (λ _ → R)

associative-mul-function-Semiring :
(x y z : type-function-Semiring) →
mul-function-Semiring (mul-function-Semiring x y) z ＝
mul-function-Semiring x (mul-function-Semiring y z)
associative-mul-function-Semiring =
associative-mul-Π-Semiring X (λ _ → R)

left-unit-law-mul-function-Semiring :
(x : type-function-Semiring) →
mul-function-Semiring one-function-Semiring x ＝ x
left-unit-law-mul-function-Semiring =
left-unit-law-mul-Π-Semiring X (λ _ → R)

right-unit-law-mul-function-Semiring :
(x : type-function-Semiring) →
mul-function-Semiring x one-function-Semiring ＝ x
right-unit-law-mul-function-Semiring =
right-unit-law-mul-Π-Semiring X (λ _ → R)

(f g h : type-function-Semiring) →
mul-function-Semiring f (add-function-Semiring g h) ＝
( mul-function-Semiring f g)
( mul-function-Semiring f h)
left-distributive-mul-add-Π-Semiring X (λ _ → R)

(f g h : type-function-Semiring) →
mul-function-Semiring (add-function-Semiring f g) h ＝
( mul-function-Semiring f h)
( mul-function-Semiring g h)
right-distributive-mul-add-Π-Semiring X (λ _ → R)

left-zero-law-mul-function-Semiring :
(f : type-function-Semiring) →
mul-function-Semiring zero-function-Semiring f ＝ zero-function-Semiring
left-zero-law-mul-function-Semiring =
left-zero-law-mul-Π-Semiring X (λ _ → R)

right-zero-law-mul-function-Semiring :
(f : type-function-Semiring) →
mul-function-Semiring f zero-function-Semiring ＝ zero-function-Semiring
right-zero-law-mul-function-Semiring =
right-zero-law-mul-Π-Semiring X (λ _ → R)

function-Semiring : Semiring (l1 ⊔ l2)
pr1 (pr1 (pr1 (pr2 function-Semiring))) = mul-function-Semiring
pr2 (pr1 (pr1 (pr2 function-Semiring))) = associative-mul-function-Semiring
pr1 (pr1 (pr2 (pr1 (pr2 function-Semiring)))) = one-function-Semiring
pr1 (pr2 (pr1 (pr2 (pr1 (pr2 function-Semiring))))) =
left-unit-law-mul-function-Semiring
pr2 (pr2 (pr1 (pr2 (pr1 (pr2 function-Semiring))))) =
right-unit-law-mul-function-Semiring
pr1 (pr2 (pr2 (pr1 (pr2 function-Semiring)))) =