Products of commutative rings
Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer and Victor Blanchi.
Created on 2023-05-25.
Last modified on 2023-06-08.
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-prod-Commutative-Ring : Set (l1 ⊔ l2) set-prod-Commutative-Ring = set-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) type-prod-Commutative-Ring : UU (l1 ⊔ l2) type-prod-Commutative-Ring = type-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) is-set-type-prod-Commutative-Ring : is-set type-prod-Commutative-Ring is-set-type-prod-Commutative-Ring = is-set-type-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) add-prod-Commutative-Ring : type-prod-Commutative-Ring → type-prod-Commutative-Ring → type-prod-Commutative-Ring add-prod-Commutative-Ring = add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) zero-prod-Commutative-Ring : type-prod-Commutative-Ring zero-prod-Commutative-Ring = zero-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) neg-prod-Commutative-Ring : type-prod-Commutative-Ring → type-prod-Commutative-Ring neg-prod-Commutative-Ring = neg-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) left-unit-law-add-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → add-prod-Commutative-Ring zero-prod-Commutative-Ring x = x left-unit-law-add-prod-Commutative-Ring = left-unit-law-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) right-unit-law-add-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → add-prod-Commutative-Ring x zero-prod-Commutative-Ring = x right-unit-law-add-prod-Commutative-Ring = right-unit-law-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) left-inverse-law-add-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → Id ( add-prod-Commutative-Ring (neg-prod-Commutative-Ring x) x) zero-prod-Commutative-Ring left-inverse-law-add-prod-Commutative-Ring = left-inverse-law-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) right-inverse-law-add-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → Id ( add-prod-Commutative-Ring x (neg-prod-Commutative-Ring x)) ( zero-prod-Commutative-Ring) right-inverse-law-add-prod-Commutative-Ring = right-inverse-law-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) associative-add-prod-Commutative-Ring : (x y z : type-prod-Commutative-Ring) → Id ( add-prod-Commutative-Ring (add-prod-Commutative-Ring x y) z) ( add-prod-Commutative-Ring x (add-prod-Commutative-Ring y z)) associative-add-prod-Commutative-Ring = associative-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) commutative-add-prod-Commutative-Ring : (x y : type-prod-Commutative-Ring) → Id (add-prod-Commutative-Ring x y) (add-prod-Commutative-Ring y x) commutative-add-prod-Commutative-Ring = commutative-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) mul-prod-Commutative-Ring : type-prod-Commutative-Ring → type-prod-Commutative-Ring → type-prod-Commutative-Ring mul-prod-Commutative-Ring = mul-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) one-prod-Commutative-Ring : type-prod-Commutative-Ring one-prod-Commutative-Ring = one-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) associative-mul-prod-Commutative-Ring : (x y z : type-prod-Commutative-Ring) → Id ( mul-prod-Commutative-Ring (mul-prod-Commutative-Ring x y) z) ( mul-prod-Commutative-Ring x (mul-prod-Commutative-Ring y z)) associative-mul-prod-Commutative-Ring = associative-mul-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) left-unit-law-mul-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → Id (mul-prod-Commutative-Ring one-prod-Commutative-Ring x) x left-unit-law-mul-prod-Commutative-Ring = left-unit-law-mul-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) right-unit-law-mul-prod-Commutative-Ring : (x : type-prod-Commutative-Ring) → Id (mul-prod-Commutative-Ring x one-prod-Commutative-Ring) x right-unit-law-mul-prod-Commutative-Ring = right-unit-law-mul-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) left-distributive-mul-add-prod-Commutative-Ring : (x y z : type-prod-Commutative-Ring) → Id ( mul-prod-Commutative-Ring x (add-prod-Commutative-Ring y z)) ( add-prod-Commutative-Ring ( mul-prod-Commutative-Ring x y) ( mul-prod-Commutative-Ring x z)) left-distributive-mul-add-prod-Commutative-Ring = left-distributive-mul-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) right-distributive-mul-add-prod-Commutative-Ring : (x y z : type-prod-Commutative-Ring) → Id ( mul-prod-Commutative-Ring (add-prod-Commutative-Ring x y) z) ( add-prod-Commutative-Ring ( mul-prod-Commutative-Ring x z) ( mul-prod-Commutative-Ring y z)) right-distributive-mul-add-prod-Commutative-Ring = right-distributive-mul-add-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) semigroup-prod-Commutative-Ring : Semigroup (l1 ⊔ l2) semigroup-prod-Commutative-Ring = semigroup-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) group-prod-Commutative-Ring : Group (l1 ⊔ l2) group-prod-Commutative-Ring = group-prod-Ring ( ring-Commutative-Ring R1) ( ring-Commutative-Ring R2) ab-prod-Commutative-Ring : Ab (l1 ⊔ l2) ab-prod-Commutative-Ring = ab-prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) ring-prod-Commutative-Ring : Ring (l1 ⊔ l2) ring-prod-Commutative-Ring = prod-Ring (ring-Commutative-Ring R1) (ring-Commutative-Ring R2) commutative-mul-prod-Commutative-Ring : (x y : type-prod-Commutative-Ring) → mul-prod-Commutative-Ring x y = mul-prod-Commutative-Ring y x commutative-mul-prod-Commutative-Ring (x1 , x2) (y1 , y2) = eq-pair ( commutative-mul-Commutative-Ring R1 x1 y1) ( commutative-mul-Commutative-Ring R2 x2 y2) prod-Commutative-Ring : Commutative-Ring (l1 ⊔ l2) pr1 prod-Commutative-Ring = ring-prod-Commutative-Ring pr2 prod-Commutative-Ring = commutative-mul-prod-Commutative-Ring
Recent changes
- 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).
- 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-05-25. Victor Blanchi and Egbert Rijke. Towards Hasse-Weil species (#631).