Products of commutative rings

Content created by Fredrik Bakke, Egbert Rijke, Maša Žaucer and Victor Blanchi.

Created on 2023-05-25.

module commutative-algebra.products-commutative-rings where

Imports
open import commutative-algebra.commutative-rings

open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-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.groups
open import group-theory.semigroups

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


Idea

Given two commutative rings R1 and R2, we define a commutative ring structure on the product of R1 and R2.

Definition

module _
{l1 l2 : Level} (R1 : Commutative-Ring l1) (R2 : Commutative-Ring l2)
where

set-product-Commutative-Ring : Set (l1 ⊔ l2)
set-product-Commutative-Ring =
set-product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

type-product-Commutative-Ring : UU (l1 ⊔ l2)
type-product-Commutative-Ring =
type-product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

is-set-type-product-Commutative-Ring : is-set type-product-Commutative-Ring
is-set-type-product-Commutative-Ring =
is-set-type-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

type-product-Commutative-Ring →
type-product-Commutative-Ring →
type-product-Commutative-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

zero-product-Commutative-Ring : type-product-Commutative-Ring
zero-product-Commutative-Ring =
zero-product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

neg-product-Commutative-Ring :
type-product-Commutative-Ring → type-product-Commutative-Ring
neg-product-Commutative-Ring =
neg-product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

(x : type-product-Commutative-Ring) →
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x : type-product-Commutative-Ring) →
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x : type-product-Commutative-Ring) →
Id
zero-product-Commutative-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x : type-product-Commutative-Ring) →
Id
( zero-product-Commutative-Ring)
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x y z : type-product-Commutative-Ring) →
Id
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x y : type-product-Commutative-Ring) →
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

mul-product-Commutative-Ring :
type-product-Commutative-Ring →
type-product-Commutative-Ring →
type-product-Commutative-Ring
mul-product-Commutative-Ring =
mul-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

one-product-Commutative-Ring : type-product-Commutative-Ring
one-product-Commutative-Ring =
one-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

associative-mul-product-Commutative-Ring :
(x y z : type-product-Commutative-Ring) →
Id
( mul-product-Commutative-Ring (mul-product-Commutative-Ring x y) z)
( mul-product-Commutative-Ring x (mul-product-Commutative-Ring y z))
associative-mul-product-Commutative-Ring =
associative-mul-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

left-unit-law-mul-product-Commutative-Ring :
(x : type-product-Commutative-Ring) →
Id (mul-product-Commutative-Ring one-product-Commutative-Ring x) x
left-unit-law-mul-product-Commutative-Ring =
left-unit-law-mul-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

right-unit-law-mul-product-Commutative-Ring :
(x : type-product-Commutative-Ring) →
Id (mul-product-Commutative-Ring x one-product-Commutative-Ring) x
right-unit-law-mul-product-Commutative-Ring =
right-unit-law-mul-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x y z : type-product-Commutative-Ring) →
Id
( mul-product-Commutative-Ring x (add-product-Commutative-Ring y z))
( mul-product-Commutative-Ring x y)
( mul-product-Commutative-Ring x z))
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

(x y z : type-product-Commutative-Ring) →
Id
( mul-product-Commutative-Ring (add-product-Commutative-Ring x y) z)
( mul-product-Commutative-Ring x z)
( mul-product-Commutative-Ring y z))
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

semigroup-product-Commutative-Ring : Semigroup (l1 ⊔ l2)
semigroup-product-Commutative-Ring =
semigroup-product-Ring
( ring-Commutative-Ring R1)
( ring-Commutative-Ring R2)

group-product-Commutative-Ring : Group (l1 ⊔ l2)
group-product-Commutative-Ring =
group-product-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2)

ab-product-Commutative-Ring : Ab (l1 ⊔ l2)
ab-product-Commutative-Ring =
ab-product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

ring-product-Commutative-Ring : Ring (l1 ⊔ l2)
ring-product-Commutative-Ring =
product-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2)

commutative-mul-product-Commutative-Ring :
(x y : type-product-Commutative-Ring) →
mul-product-Commutative-Ring x y ＝ mul-product-Commutative-Ring y x
commutative-mul-product-Commutative-Ring (x1 , x2) (y1 , y2) =
eq-pair
( commutative-mul-Commutative-Ring R1 x1 y1)
( commutative-mul-Commutative-Ring R2 x2 y2)

product-Commutative-Ring : Commutative-Ring (l1 ⊔ l2)
pr1 product-Commutative-Ring = ring-product-Commutative-Ring
pr2 product-Commutative-Ring = commutative-mul-product-Commutative-Ring