# Dependent products of rings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-19.

module ring-theory.dependent-products-rings 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.abelian-groups
open import group-theory.dependent-products-abelian-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

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


## Idea

Given a family of rings R i indexed by i : I, their dependent product Π(i:I), R i is again a ring.

## Definition

module _
{l1 l2 : Level} (I : UU l1) (R : I → Ring l2)
where

semiring-Π-Ring : Semiring (l1 ⊔ l2)
semiring-Π-Ring = Π-Semiring I (λ i → semiring-Ring (R i))

ab-Π-Ring : Ab (l1 ⊔ l2)
ab-Π-Ring = Π-Ab I (λ i → ab-Ring (R i))

group-Π-Ring : Group (l1 ⊔ l2)
group-Π-Ring = group-Ab ab-Π-Ring

semigroup-Π-Ring : Semigroup (l1 ⊔ l2)
semigroup-Π-Ring = semigroup-Ab ab-Π-Ring

multiplicative-monoid-Π-Ring : Monoid (l1 ⊔ l2)
multiplicative-monoid-Π-Ring =
multiplicative-monoid-Semiring semiring-Π-Ring

set-Π-Ring : Set (l1 ⊔ l2)
set-Π-Ring = set-Semiring semiring-Π-Ring

type-Π-Ring : UU (l1 ⊔ l2)
type-Π-Ring = type-Semiring semiring-Π-Ring

is-set-type-Π-Ring : is-set type-Π-Ring
is-set-type-Π-Ring = is-set-type-Semiring semiring-Π-Ring

add-Π-Ring : type-Π-Ring → type-Π-Ring → type-Π-Ring

zero-Π-Ring : type-Π-Ring
zero-Π-Ring = zero-Semiring semiring-Π-Ring

neg-Π-Ring : type-Π-Ring → type-Π-Ring
neg-Π-Ring = neg-Ab ab-Π-Ring

(x y z : type-Π-Ring) →

(x : type-Π-Ring) → Id (add-Π-Ring zero-Π-Ring x) x

(x : type-Π-Ring) → Id (add-Π-Ring x zero-Π-Ring) x

(x : type-Π-Ring) → Id (add-Π-Ring (neg-Π-Ring x) x) zero-Π-Ring

(x : type-Π-Ring) → Id (add-Π-Ring x (neg-Π-Ring x)) zero-Π-Ring

(x y : type-Π-Ring) → Id (add-Π-Ring x y) (add-Π-Ring y x)

mul-Π-Ring : type-Π-Ring → type-Π-Ring → type-Π-Ring
mul-Π-Ring = mul-Semiring semiring-Π-Ring

one-Π-Ring : type-Π-Ring
one-Π-Ring = one-Semiring semiring-Π-Ring

associative-mul-Π-Ring :
(x y z : type-Π-Ring) →
Id (mul-Π-Ring (mul-Π-Ring x y) z) (mul-Π-Ring x (mul-Π-Ring y z))
associative-mul-Π-Ring =
associative-mul-Semiring semiring-Π-Ring

left-unit-law-mul-Π-Ring :
(x : type-Π-Ring) → Id (mul-Π-Ring one-Π-Ring x) x
left-unit-law-mul-Π-Ring =
left-unit-law-mul-Semiring semiring-Π-Ring

right-unit-law-mul-Π-Ring :
(x : type-Π-Ring) → Id (mul-Π-Ring x one-Π-Ring) x
right-unit-law-mul-Π-Ring =
right-unit-law-mul-Semiring semiring-Π-Ring

(f g h : type-Π-Ring) →
mul-Π-Ring f (add-Π-Ring g h) ＝
add-Π-Ring (mul-Π-Ring f g) (mul-Π-Ring f h)

(f g h : type-Π-Ring) →
Id
( mul-Π-Ring (add-Π-Ring f g) h)
( add-Π-Ring (mul-Π-Ring f h) (mul-Π-Ring g h))