# Dependent products of commutative semirings

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-03-13.

module commutative-algebra.dependent-products-commutative-semirings where

Imports
open import commutative-algebra.commutative-semirings

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.dependent-products-commutative-monoids

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


## Idea

Given a family of commutative semirings A i indexed by i : I, their dependent product Π (i:I), A i is again a commutative semiring.

## Definition

module _
{l1 l2 : Level} (I : UU l1) (A : I → Commutative-Semiring l2)
where

semiring-Π-Commutative-Semiring : Semiring (l1 ⊔ l2)
semiring-Π-Commutative-Semiring =
Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

Commutative-Monoid (l1 ⊔ l2)
Π-Commutative-Monoid I
( λ i → additive-commutative-monoid-Commutative-Semiring (A i))

multiplicative-commutative-monoid-Π-Commutative-Semiring :
Commutative-Monoid (l1 ⊔ l2)
multiplicative-commutative-monoid-Π-Commutative-Semiring =
Π-Commutative-Monoid I
( λ i → multiplicative-commutative-monoid-Commutative-Semiring (A i))

set-Π-Commutative-Semiring : Set (l1 ⊔ l2)
set-Π-Commutative-Semiring =
set-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

type-Π-Commutative-Semiring : UU (l1 ⊔ l2)
type-Π-Commutative-Semiring =
type-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

is-set-type-Π-Commutative-Semiring : is-set type-Π-Commutative-Semiring
is-set-type-Π-Commutative-Semiring =
is-set-type-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

type-Π-Commutative-Semiring → type-Π-Commutative-Semiring →
type-Π-Commutative-Semiring
add-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

zero-Π-Commutative-Semiring : type-Π-Commutative-Semiring
zero-Π-Commutative-Semiring =
zero-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

(x y z : type-Π-Commutative-Semiring) →
associative-add-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

(x : type-Π-Commutative-Semiring) →
left-unit-law-add-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

(x : type-Π-Commutative-Semiring) →
right-unit-law-add-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

(x y : type-Π-Commutative-Semiring) →
commutative-add-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

mul-Π-Commutative-Semiring :
type-Π-Commutative-Semiring → type-Π-Commutative-Semiring →
type-Π-Commutative-Semiring
mul-Π-Commutative-Semiring =
mul-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

one-Π-Commutative-Semiring : type-Π-Commutative-Semiring
one-Π-Commutative-Semiring =
one-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

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 I (λ i → semiring-Commutative-Semiring (A i))

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 I (λ i → semiring-Commutative-Semiring (A i))

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 I (λ i → semiring-Commutative-Semiring (A i))

(f g h : type-Π-Commutative-Semiring) →
mul-Π-Commutative-Semiring f (add-Π-Commutative-Semiring g h) ＝
( mul-Π-Commutative-Semiring f g)
( mul-Π-Commutative-Semiring f h)
( λ i → semiring-Commutative-Semiring (A i))

(f g h : type-Π-Commutative-Semiring) →
mul-Π-Commutative-Semiring (add-Π-Commutative-Semiring f g) h ＝
( mul-Π-Commutative-Semiring f h)
( mul-Π-Commutative-Semiring g h)
( λ i → semiring-Commutative-Semiring (A i))

left-zero-law-mul-Π-Commutative-Semiring :
(f : type-Π-Commutative-Semiring) →
mul-Π-Commutative-Semiring zero-Π-Commutative-Semiring f ＝
zero-Π-Commutative-Semiring
left-zero-law-mul-Π-Commutative-Semiring =
left-zero-law-mul-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

right-zero-law-mul-Π-Commutative-Semiring :
(f : type-Π-Commutative-Semiring) →
mul-Π-Commutative-Semiring f zero-Π-Commutative-Semiring ＝
zero-Π-Commutative-Semiring
right-zero-law-mul-Π-Commutative-Semiring =
right-zero-law-mul-Π-Semiring I (λ i → semiring-Commutative-Semiring (A i))

commutative-mul-Π-Commutative-Semiring :
(f g : type-Π-Commutative-Semiring) →
mul-Π-Commutative-Semiring f g ＝ mul-Π-Commutative-Semiring g f
commutative-mul-Π-Commutative-Semiring =
commutative-mul-Commutative-Monoid
multiplicative-commutative-monoid-Π-Commutative-Semiring

Π-Commutative-Semiring : Commutative-Semiring (l1 ⊔ l2)
pr1 Π-Commutative-Semiring = semiring-Π-Commutative-Semiring
pr2 Π-Commutative-Semiring = commutative-mul-Π-Commutative-Semiring