Products of semigroups, monoids, commutative monoids, groups, abelian…

… groups, semirings, rings, commutative semirings, and commutative rings (#505)

src/commutative-algebra.lagda.md

@@ -8,8 +8,12 @@ open import commutative-algebra.binomial-theorem-commutative-semirings public
 open import commutative-algebra.boolean-rings public
 open import commutative-algebra.commutative-rings public
 open import commutative-algebra.commutative-semirings public
+open import commutative-algebra.dependent-products-commutative-rings public
+open import commutative-algebra.dependent-products-commutative-semirings public
 open import commutative-algebra.discrete-fields public
 open import commutative-algebra.eisenstein-integers public
+open import commutative-algebra.function-commutative-rings public
+open import commutative-algebra.function-commutative-semirings public
 open import commutative-algebra.gaussian-integers public
 open import commutative-algebra.homomorphisms-commutative-rings public
 open import commutative-algebra.ideals-commutative-rings public

src/commutative-algebra/commutative-rings.lagda.md

@@ -7,6 +7,8 @@ module commutative-algebra.commutative-rings where
 <details><summary>Imports</summary>
 
 ```agda
+open import commutative-algebra.commutative-semirings
+
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 
@@ -17,7 +19,11 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import group-theory.abelian-groups
+open import group-theory.commutative-monoids
+
 open import ring-theory.rings
+open import ring-theory.semirings
 ```
 
 </details>
@@ -55,6 +61,9 @@ module _
   ring-Commutative-Ring : Ring l
   ring-Commutative-Ring = pr1 R
 
+  ab-Commutative-Ring : Ab l
+  ab-Commutative-Ring = ab-Ring ring-Commutative-Ring
+
   set-Commutative-Ring : Set l
   set-Commutative-Ring = set-Ring ring-Commutative-Ring
 
@@ -238,6 +247,19 @@ module _
         ( mul-Commutative-Ring' z)
         ( commutative-mul-Commutative-Ring x y)) ∙
       ( associative-mul-Commutative-Ring y x z))
+
+  multiplicative-commutative-monoid-Commutative-Ring : Commutative-Monoid l
+  pr1 multiplicative-commutative-monoid-Commutative-Ring =
+    multiplicative-monoid-Ring ring-Commutative-Ring
+  pr2 multiplicative-commutative-monoid-Commutative-Ring =
+    commutative-mul-Commutative-Ring
+
+  semiring-Commutative-Ring : Semiring l
+  semiring-Commutative-Ring = semiring-Ring ring-Commutative-Ring
+
+  commutative-semiring-Commutative-Ring : Commutative-Semiring l
+  pr1 commutative-semiring-Commutative-Ring = semiring-Commutative-Ring
+  pr2 commutative-semiring-Commutative-Ring = commutative-mul-Commutative-Ring
 ```
 
 ### Scalar multiplication of elements of a commutative ring by natural numbers

src/commutative-algebra/commutative-semirings.lagda.md

@@ -17,6 +17,9 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import group-theory.commutative-monoids
+open import group-theory.monoids
+
 open import ring-theory.semirings
 ```
 
@@ -60,6 +63,14 @@ module _
   semiring-Commutative-Semiring : Semiring l
   semiring-Commutative-Semiring = pr1 R
 
+  additive-commutative-monoid-Commutative-Semiring : Commutative-Monoid l
+  additive-commutative-monoid-Commutative-Semiring =
+    additive-commutative-monoid-Semiring semiring-Commutative-Semiring
+
+  multiplicative-monoid-Commutative-Semiring : Monoid l
+  multiplicative-monoid-Commutative-Semiring =
+    multiplicative-monoid-Semiring semiring-Commutative-Semiring
+
   set-Commutative-Semiring : Set l
   set-Commutative-Semiring = set-Semiring semiring-Commutative-Semiring
 
@@ -199,6 +210,13 @@ module _
     mul-Commutative-Semiring x y ＝ mul-Commutative-Semiring y x
   commutative-mul-Commutative-Semiring = pr2 R
 
+  multiplicative-commutative-monoid-Commutative-Semiring :
+    Commutative-Monoid l
+  pr1 multiplicative-commutative-monoid-Commutative-Semiring =
+    multiplicative-monoid-Commutative-Semiring
+  pr2 multiplicative-commutative-monoid-Commutative-Semiring =
+    commutative-mul-Commutative-Semiring
+
   left-zero-law-mul-Commutative-Semiring :
     (x : type-Commutative-Semiring) →
     mul-Commutative-Semiring zero-Commutative-Semiring x ＝
@@ -217,23 +235,17 @@ module _
     (x y z : type-Commutative-Semiring) →
     mul-Commutative-Semiring (mul-Commutative-Semiring x y) z ＝
     mul-Commutative-Semiring (mul-Commutative-Semiring x z) y
-  right-swap-mul-Commutative-Semiring x y z =
-    ( associative-mul-Commutative-Semiring x y z) ∙
-    ( ( ap
-        ( mul-Commutative-Semiring x)
-        ( commutative-mul-Commutative-Semiring y z)) ∙
-      ( inv (associative-mul-Commutative-Semiring x z y)))
+  right-swap-mul-Commutative-Semiring =
+    right-swap-mul-Commutative-Monoid
+      multiplicative-commutative-monoid-Commutative-Semiring
 
   left-swap-mul-Commutative-Semiring :
     (x y z : type-Commutative-Semiring) →
     mul-Commutative-Semiring x (mul-Commutative-Semiring y z) ＝
     mul-Commutative-Semiring y (mul-Commutative-Semiring x z)
-  left-swap-mul-Commutative-Semiring x y z =
-    ( inv (associative-mul-Commutative-Semiring x y z)) ∙
-    ( ( ap
-        ( mul-Commutative-Semiring' z)
-        ( commutative-mul-Commutative-Semiring x y)) ∙
-      ( associative-mul-Commutative-Semiring y x z))
+  left-swap-mul-Commutative-Semiring =
+    left-swap-mul-Commutative-Monoid
+      multiplicative-commutative-monoid-Commutative-Semiring
 ```
 
 ## Operations

src/commutative-algebra/dependent-products-commutative-rings.lagda.md

@@ -0,0 +1,167 @@
+# Dependent products of commutative rings
+
+```agda
+module commutative-algebra.dependent-products-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.commutative-monoids
+open import group-theory.dependent-products-commutative-monoids
+
+open import ring-theory.dependent-products-rings
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+Given a family of commutative rings `R i` indexed by `i : I`, their dependent
+product `Π(i:I), R i` is again a commutative ring.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (I : UU l1) (R : I → Commutative-Ring l2)
+  where
+
+  ring-Π-Commutative-Ring : Ring (l1 ⊔ l2)
+  ring-Π-Commutative-Ring = Π-Ring I (λ i → ring-Commutative-Ring (R i))
+
+  ab-Π-Commutative-Ring : Ab (l1 ⊔ l2)
+  ab-Π-Commutative-Ring = ab-Ring ring-Π-Commutative-Ring
+
+  multiplicative-commutative-monoid-Π-Commutative-Ring :
+    Commutative-Monoid (l1 ⊔ l2)
+  multiplicative-commutative-monoid-Π-Commutative-Ring =
+    Π-Commutative-Monoid I
+      ( λ i → multiplicative-commutative-monoid-Commutative-Ring (R i))
+
+  set-Π-Commutative-Ring : Set (l1 ⊔ l2)
+  set-Π-Commutative-Ring = set-Ring ring-Π-Commutative-Ring
+
+  type-Π-Commutative-Ring : UU (l1 ⊔ l2)
+  type-Π-Commutative-Ring = type-Ring ring-Π-Commutative-Ring
+
+  is-set-type-Π-Commutative-Ring : is-set type-Π-Commutative-Ring
+  is-set-type-Π-Commutative-Ring =
+    is-set-type-Ring ring-Π-Commutative-Ring
+
+  add-Π-Commutative-Ring :
+    type-Π-Commutative-Ring → type-Π-Commutative-Ring →
+    type-Π-Commutative-Ring
+  add-Π-Commutative-Ring = add-Ring ring-Π-Commutative-Ring
+
+  zero-Π-Commutative-Ring : type-Π-Commutative-Ring
+  zero-Π-Commutative-Ring = zero-Ring ring-Π-Commutative-Ring
+
+  associative-add-Π-Commutative-Ring :
+    (x y z : type-Π-Commutative-Ring) →
+    add-Π-Commutative-Ring (add-Π-Commutative-Ring x y) z ＝
+    add-Π-Commutative-Ring x (add-Π-Commutative-Ring y z)
+  associative-add-Π-Commutative-Ring =
+    associative-add-Ring ring-Π-Commutative-Ring
+
+  left-unit-law-add-Π-Commutative-Ring :
+    (x : type-Π-Commutative-Ring) →
+    add-Π-Commutative-Ring zero-Π-Commutative-Ring x ＝ x
+  left-unit-law-add-Π-Commutative-Ring =
+    left-unit-law-add-Ring ring-Π-Commutative-Ring
+
+  right-unit-law-add-Π-Commutative-Ring :
+    (x : type-Π-Commutative-Ring) →
+    add-Π-Commutative-Ring x zero-Π-Commutative-Ring ＝ x
+  right-unit-law-add-Π-Commutative-Ring =
+    right-unit-law-add-Ring ring-Π-Commutative-Ring
+
+  commutative-add-Π-Commutative-Ring :
+    (x y : type-Π-Commutative-Ring) →
+    add-Π-Commutative-Ring x y ＝ add-Π-Commutative-Ring y x
+  commutative-add-Π-Commutative-Ring =
+    commutative-add-Ring ring-Π-Commutative-Ring
+
+  mul-Π-Commutative-Ring :
+    type-Π-Commutative-Ring → type-Π-Commutative-Ring →
+    type-Π-Commutative-Ring
+  mul-Π-Commutative-Ring =
+    mul-Ring ring-Π-Commutative-Ring
+
+  one-Π-Commutative-Ring : type-Π-Commutative-Ring
+  one-Π-Commutative-Ring =
+    one-Ring ring-Π-Commutative-Ring
+
+  associative-mul-Π-Commutative-Ring :
+    (x y z : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring (mul-Π-Commutative-Ring x y) z ＝
+    mul-Π-Commutative-Ring x (mul-Π-Commutative-Ring y z)
+  associative-mul-Π-Commutative-Ring =
+    associative-mul-Ring ring-Π-Commutative-Ring
+
+  left-unit-law-mul-Π-Commutative-Ring :
+    (x : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring one-Π-Commutative-Ring x ＝ x
+  left-unit-law-mul-Π-Commutative-Ring =
+    left-unit-law-mul-Ring ring-Π-Commutative-Ring
+
+  right-unit-law-mul-Π-Commutative-Ring :
+    (x : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring x one-Π-Commutative-Ring ＝ x
+  right-unit-law-mul-Π-Commutative-Ring =
+    right-unit-law-mul-Ring ring-Π-Commutative-Ring
+
+  left-distributive-mul-add-Π-Commutative-Ring :
+    (f g h : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring f (add-Π-Commutative-Ring g h) ＝
+    add-Π-Commutative-Ring
+      ( mul-Π-Commutative-Ring f g)
+      ( mul-Π-Commutative-Ring f h)
+  left-distributive-mul-add-Π-Commutative-Ring =
+    left-distributive-mul-add-Ring ring-Π-Commutative-Ring
+
+  right-distributive-mul-add-Π-Commutative-Ring :
+    (f g h : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring (add-Π-Commutative-Ring f g) h ＝
+    add-Π-Commutative-Ring
+      ( mul-Π-Commutative-Ring f h)
+      ( mul-Π-Commutative-Ring g h)
+  right-distributive-mul-add-Π-Commutative-Ring =
+    right-distributive-mul-add-Ring ring-Π-Commutative-Ring
+
+  left-zero-law-mul-Π-Commutative-Ring :
+    (f : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring zero-Π-Commutative-Ring f ＝
+    zero-Π-Commutative-Ring
+  left-zero-law-mul-Π-Commutative-Ring =
+    left-zero-law-mul-Ring ring-Π-Commutative-Ring
+
+  right-zero-law-mul-Π-Commutative-Ring :
+    (f : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring f zero-Π-Commutative-Ring ＝
+    zero-Π-Commutative-Ring
+  right-zero-law-mul-Π-Commutative-Ring =
+    right-zero-law-mul-Ring ring-Π-Commutative-Ring
+
+  commutative-mul-Π-Commutative-Ring :
+    (f g : type-Π-Commutative-Ring) →
+    mul-Π-Commutative-Ring f g ＝ mul-Π-Commutative-Ring g f
+  commutative-mul-Π-Commutative-Ring =
+    commutative-mul-Commutative-Monoid
+      multiplicative-commutative-monoid-Π-Commutative-Ring
+
+  Π-Commutative-Ring : Commutative-Ring (l1 ⊔ l2)
+  pr1 Π-Commutative-Ring = ring-Π-Commutative-Ring
+  pr2 Π-Commutative-Ring = commutative-mul-Π-Commutative-Ring
+```