From 1cca7187ab275c03b5e05dd59f3c9845fa83e093 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 19:27:00 +0000
Subject: [PATCH] add: remaining `Structures` and `Bundles`

---
 CHANGELOG.md                | 16 +++++++++-----
 src/Algebra/Bundles.agda    | 40 +++++++++++++++++++++++++++++++++
 src/Algebra/Structures.agda | 44 +++++++++++++++++++++++++++++++++++++
 3 files changed, 95 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5190beaae5..9dcc995c59 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -69,13 +69,16 @@ Additions to existing modules
 
 * In `Algebra.Bundles`:
   ```agda
-  IntegralRing     : (c ℓ : Level) → Set _
-  IntegralSemiring : (c ℓ : Level) → Set _
+  IntegralCommutativeRing     : (c ℓ : Level) → Set _
+  IntegralCommutativeSemiring : (c ℓ : Level) → Set _
+  IntegralDomain              : (c ℓ : Level) → Set _
+  IntegralRing                : (c ℓ : Level) → Set _
+  IntegralSemiring            : (c ℓ : Level) → Set _
   ```
 
 * In `Algebra.Consequences.Base`:
   ```agda
-  integral⇒noZeroDivisors     : Integral _≈_ 1# 0# _∙_ → ¬ (1# ≈ 0#) →
+  integral⇒noZeroDivisors     : Integral _≈_ 1# 0# _∙_ → 1# ≉ 0# →
                                 NoZeroDivisors _≈_ 0# _∙_
   noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0 : NoZeroDivisors _≈_ 0# _∙_ →
                                 x ≉ 0# → y ≉ 0# → (x ∙ y) ≉ 0#
@@ -125,6 +128,9 @@ Additions to existing modules
 
 * In `Algebra.Structures`:
   ```agda
-  IsIntegralSemiring : (+ * : Op₂ A) (0# 1# : A) → Set _
-  IsIntegralRing     : (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) → Set _
+  IsIntegralCommutativeSemiring : (+ * : Op₂ A) (0# 1# : A) → Set _
+  IsIntegralCommutativeRing     : (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) → Set _
+  IsIntegralDomain              : (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) → Set _
+  IsIntegralSemiring            : (+ * : Op₂ A) (0# 1# : A) → Set _
+  IsIntegralRing                : (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) → Set _
   ```
diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index af84db4801..951f5693a2 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -1194,6 +1194,46 @@ record IntegralRing c ℓ : Set (suc (c ⊔ ℓ)) where
     )
 
 
+record IntegralCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier                   : Set c
+    _≈_                       : Rel Carrier ℓ
+    _+_                       : Op₂ Carrier
+    _*_                       : Op₂ Carrier
+    -_                        : Op₁ Carrier
+    0#                        : Carrier
+    1#                        : Carrier
+    isIntegralCommutativeRing : IsIntegralCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsIntegralCommutativeRing isIntegralCommutativeRing public
+
+
+record IntegralDomain c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _+_              : Op₂ Carrier
+    _*_              : Op₂ Carrier
+    -_               : Op₁ Carrier
+    0#               : Carrier
+    1#               : Carrier
+    isIntegralDomain : IsIntegralDomain _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsIntegralDomain isIntegralDomain public
+
+  integralCommutativeRing : IntegralCommutativeRing _ _
+  integralCommutativeRing = record
+    { isIntegralCommutativeRing = isIntegralCommutativeRing }
+
+
 ------------------------------------------------------------------------
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 2ceb801e33..4a1e90031e 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -26,6 +26,7 @@ open import Algebra.Definitions _≈_
 import Algebra.Consequences.Setoid as Consequences
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 ------------------------------------------------------------------------
 -- Structures with 1 unary operation & 1 element
@@ -649,6 +650,20 @@ record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   open IsSemiring isSemiring public
 
 
+record IsIntegralCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
+    integral              : Integral 1# 0# *
+
+  open IsCommutativeSemiring isCommutativeSemiring public
+
+  isIntegralSemiring : IsIntegralSemiring + * 0# 1#
+  isIntegralSemiring = record
+    { isSemiring = isSemiring
+    ; integral = integral
+    }
+
+
 record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   field
     isIdempotentSemiring  : IsIdempotentSemiring + * 0# 1#
@@ -982,6 +997,35 @@ record IsIntegralRing
     }
 
 
+record IsIntegralCommutativeRing
+         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isCommutativeRing   : IsCommutativeRing + * - 0# 1#
+    integral            : Integral 1# 0# *
+
+  open IsCommutativeRing isCommutativeRing public
+
+  isIntegralCommutativeSemiring : IsIntegralCommutativeSemiring + * 0# 1#
+  isIntegralCommutativeSemiring = record
+    { isCommutativeSemiring = isCommutativeSemiring
+    ; integral = integral
+    }
+
+
+record IsIntegralDomain
+         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isIntegralCommutativeRing   : IsIntegralCommutativeRing + * - 0# 1#
+
+  open IsIntegralCommutativeRing isIntegralCommutativeRing public
+
+  field
+    nonTrivial                  : ¬ (1# ≈ 0#)
+
+  noZeroDivisors : NoZeroDivisors 0# *
+  noZeroDivisors = Consequences.integral⇒noZeroDivisors _≈_ integral nonTrivial
+
+
 ------------------------------------------------------------------------
 -- Structures with 3 binary operations
 ------------------------------------------------------------------------