From 74f82751113455ec48bf699ab95fc738dd46a08b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 13:26:54 +0000
Subject: [PATCH 1/8] add: definitions and one consequence
---
CHANGELOG.md | 7 +++++++
src/Algebra/Consequences/Base.agda | 9 +++++++++
src/Algebra/Definitions.agda | 6 ++++++
3 files changed, 22 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index f16ed00b65..b047b3e217 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -85,3 +85,10 @@ Additions to existing modules
quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
```
+
+* In `Algebra.Definitions`:
+ ```agda
+ NoZeroDivisors : A → Op₂ A → Set _
+ Integral : A → A → Op₂ A → Set _
+ ```
+ (see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 574ad48a16..8dd14bf014 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -15,6 +15,7 @@ open import Algebra.Definitions
open import Data.Sum.Base
open import Relation.Binary.Core
open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
@@ -28,6 +29,14 @@ module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
Involutive _≈_ f
reflexive∧selfInverse⇒involutive refl inv _ = inv refl
+module _ {ℓ} {_•_ : Op₂ A} {0# 1# : A} (_≈_ : Rel A ℓ) where
+
+ integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
+ NoZeroDivisors _≈_ 0# _•_
+ integral⇒noZeroDivisors (inj₁ 1#≈0#) = contradiction 1#≈0#
+ integral⇒noZeroDivisors (inj₂ noZeroDivisors) = λ _ → noZeroDivisors
+
+
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 62528e5b70..dbfc3e703d 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -66,6 +66,12 @@ RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
Zero : A → Op₂ A → Set _
Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)
+NoZeroDivisors : A → Op₂ A → Set _
+NoZeroDivisors z _∙_ = ∀ {x y} → (x ∙ y) ≈ z → x ≈ z ⊎ y ≈ z
+
+Integral : A → A → Op₂ A → Set _
+Integral 1# 0# _∙_ = 1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_
+
LeftInverse : A → Op₁ A → Op₂ A → Set _
LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e
From 37c11d55ba713bfe24db04437fbc19f798a8bdcd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 13:52:31 +0000
Subject: [PATCH 2/8] actually add the consequence to `CHANGELOG`
---
CHANGELOG.md | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b047b3e217..900a4c3f08 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,12 @@ New modules
Additions to existing modules
-----------------------------
+* In `Algebra.Consequences.Base`:
+ ```agda
+ integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
+ NoZeroDivisors _≈_ 0# _•_
+ ```
+
* In `Algebra.Construct.Pointwise`:
```agda
isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
From 3f6bdbb86b3c45f8eb1af8e9d042dac26893123f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 14:29:41 +0000
Subject: [PATCH 3/8] add: `(Is)IntegralSemiring`
---
CHANGELOG.md | 10 ++++++++++
src/Algebra/Bundles.agda | 30 ++++++++++++++++++++++++++++++
src/Algebra/Structures.agda | 8 ++++++++
3 files changed, 48 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 900a4c3f08..a48bb2fcf4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,11 @@ New modules
Additions to existing modules
-----------------------------
+* In `Algebra.Bundles`:
+ ```agda
+ IntegralSemiring : (c ℓ : Level) → Set _
+ ```
+
* In `Algebra.Consequences.Base`:
```agda
integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
@@ -98,3 +103,8 @@ Additions to existing modules
Integral : A → A → Op₂ A → Set _
```
(see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))
+
+* In `Algebra.Structures`:
+ ```agda
+ IsIntegralSemiring : (+ * : Op₂ A) (0# 1# : A) → Set _
+ ```
diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 88b195ec7d..af8e722acc 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -841,6 +841,36 @@ record IdempotentSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
; idempotentMonoid to +-idempotentMonoid
)
+record IntegralSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isIntegralSemiring : IsIntegralSemiring _≈_ _+_ _*_ 0# 1#
+
+ open IsIntegralSemiring isIntegralSemiring public
+
+ semiring : Semiring _ _
+ semiring = record { isSemiring = isSemiring }
+
+ open Semiring semiring public
+ using
+ ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+ ; +-semigroup; +-commutativeSemigroup
+ ; *-rawMagma; *-magma; *-semigroup
+ ; +-rawMonoid; +-monoid; +-commutativeMonoid
+ ; *-rawMonoid; *-monoid
+ ; nearSemiring; semiringWithoutOne
+ ; semiringWithoutAnnihilatingZero
+ ; rawSemiring
+ )
+
record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
infix 8 _⋆
infixl 7 _*_
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1aae80d1cc..c507ecbafc 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -582,6 +582,14 @@ record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
)
+record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ field
+ isSemiring : IsSemiring + * 0# 1#
+ integral : Integral 1# 0# *
+
+ open IsSemiring isSemiring public
+
+
record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
isSemiring : IsSemiring + * 0# 1#
From 3bb0c688e304e2f6db633352ad1f4513774aef0f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 16:32:52 +0000
Subject: [PATCH 4/8] refactor: introduce `variable`s; tighten `import`s
---
src/Algebra/Properties/Semiring/Primality.agda | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index 210d9fb1a0..825c778f6e 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -1,12 +1,12 @@
------------------------------------------------------------------------
-- The Agda standard library
--
--- Some theory for CancellativeCommutativeSemiring.
+-- Some theory for Semiring.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
-open import Algebra using (Semiring)
+open import Algebra.Bundles using (Semiring)
open import Data.Sum.Base using (reduce)
open import Function.Base using (flip)
open import Relation.Binary.Definitions using (Symmetric)
@@ -18,6 +18,10 @@ module Algebra.Properties.Semiring.Primality
open Semiring R renaming (Carrier to A)
open import Algebra.Properties.Semiring.Divisibility R
+private
+ variable
+ x y p : A
+
------------------------------------------------------------------------
-- Re-export primality definitions
@@ -30,12 +34,12 @@ open import Algebra.Definitions.RawSemiring rawSemiring public
Coprime-sym : Symmetric Coprime
Coprime-sym coprime = flip coprime
-∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y
-∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1
+∣1⇒Coprime : ∀ y → x ∣ 1# → Coprime x y
+∣1⇒Coprime y x∣1 z∣x _ = ∣-trans z∣x x∣1
------------------------------------------------------------------------
-- Properties of Irreducible
-Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
+Irreducible⇒≉0 : 0# ≉ 1# → Irreducible p → p ≉ 0#
Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))
From ec52e27c63e33b3f31c8438e910b3f93da3e38a7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 16:34:29 +0000
Subject: [PATCH 5/8] add: `Trivial` definition and property
---
CHANGELOG.md | 11 ++++++
src/Algebra/Definitions/RawSemiring.agda | 8 ++++-
.../Properties/Semiring/Triviality.agda | 36 +++++++++++++++++++
3 files changed, 54 insertions(+), 1 deletion(-)
create mode 100644 src/Algebra/Properties/Semiring/Triviality.agda
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a48bb2fcf4..f49c0e51bf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,11 @@ Deprecated names
New modules
-----------
+* `Algebra.Properties.Semiring.Triviality`, with:
+ ```agda
+ trivial⇒x≈0 : Trivial → ∀ x → x ≈ 0#
+ ```
+
Additions to existing modules
-----------------------------
@@ -104,6 +109,12 @@ Additions to existing modules
```
(see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))
+* In `Algebra.Definitions.RawSemiring`:
+ ```agda
+ Trivial : Set _
+ ```
+ (see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554))
+
* In `Algebra.Structures`:
```agda
IsIntegralSemiring : (+ * : Op₂ A) (0# 1# : A) → Set _
diff --git a/src/Algebra/Definitions/RawSemiring.agda b/src/Algebra/Definitions/RawSemiring.agda
index b1819d856d..3fc5f5da74 100644
--- a/src/Algebra/Definitions/RawSemiring.agda
+++ b/src/Algebra/Definitions/RawSemiring.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --cubical-compatible --safe #-}
-open import Algebra.Bundles using (RawSemiring)
+open import Algebra.Bundles.Raw using (RawSemiring)
open import Data.Sum.Base using (_⊎_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Level using (_⊔_)
@@ -83,3 +83,9 @@ record Prime (p : A) : Set (a ⊔ ℓ) where
p≉0 : p ≉ 0#
p∤1 : p ∤ 1#
split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y
+
+------------------------------------------------------------------------
+-- Triviality
+
+Trivial : Set _
+Trivial = 1# ≈ 0#
diff --git a/src/Algebra/Properties/Semiring/Triviality.agda b/src/Algebra/Properties/Semiring/Triviality.agda
new file mode 100644
index 0000000000..0a9c7a545b
--- /dev/null
+++ b/src/Algebra/Properties/Semiring/Triviality.agda
@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some theory for Semiring.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Semiring)
+
+module Algebra.Properties.Semiring.Triviality
+ {a ℓ} (R : Semiring a ℓ)
+ where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open Semiring R renaming (Carrier to A)
+
+
+------------------------------------------------------------------------
+-- Re-export triviality definitions
+
+open import Algebra.Definitions.RawSemiring rawSemiring public
+ using (Trivial)
+
+------------------------------------------------------------------------
+-- Properties of Trivial
+
+trivial⇒x≈0 : Trivial → ∀ x → x ≈ 0#
+trivial⇒x≈0 trivial x = begin
+ x ≈⟨ *-identityˡ x ⟨
+ 1# * x ≈⟨ *-congʳ trivial ⟩
+ 0# * x ≈⟨ zeroˡ x ⟩
+ 0# ∎
+ where open ≈-Reasoning setoid
+
From 4b9120305f4061e56a966c71a25d21cf5ee79b72 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 17:13:26 +0000
Subject: [PATCH 6/8] add:`Structures` and `Bundles`
---
CHANGELOG.md | 6 ++++--
src/Algebra/Bundles.agda | 40 +++++++++++++++++++++++++++++++++++++
src/Algebra/Structures.agda | 31 ++++++++++++++++++++--------
3 files changed, 67 insertions(+), 10 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index f49c0e51bf..3491e49a86 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -64,7 +64,8 @@ Additions to existing modules
* In `Algebra.Bundles`:
```agda
- IntegralSemiring : (c ℓ : Level) → Set _
+ IntegralRing : (c ℓ : Level) → Set _
+ IntegralSemiring : (c ℓ : Level) → Set _
```
* In `Algebra.Consequences.Base`:
@@ -117,5 +118,6 @@ Additions to existing modules
* In `Algebra.Structures`:
```agda
- IsIntegralSemiring : (+ * : 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 af8e722acc..af84db4801 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -1154,6 +1154,46 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
; commutativeSemiringWithoutOne
)
+
+record IntegralRing 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
+ isIntegralRing : IsIntegralRing _≈_ _+_ _*_ -_ 0# 1#
+
+ open IsIntegralRing isIntegralRing public
+
+ ring : Ring _ _
+ ring = record { isRing = isRing }
+
+ open Ring ring public
+ using (_≉_; rawRing; +-invertibleMagma; +-invertibleUnitalMagma; +-group; +-abelianGroup)
+
+ integralSemiring : IntegralSemiring _ _
+ integralSemiring =
+ record { isIntegralSemiring = isIntegralSemiring }
+
+ open IntegralSemiring integralSemiring public
+ using
+ ( +-rawMagma; +-magma; +-unitalMagma
+ ; +-semigroup
+ ; *-rawMagma; *-magma; *-semigroup
+ ; +-rawMonoid; +-monoid; +-commutativeMonoid
+ ; *-rawMonoid; *-monoid
+ ; nearSemiring; semiringWithoutOne
+ ; semiringWithoutAnnihilatingZero; semiring
+ )
+
+
------------------------------------------------------------------------
-- Bundles with 3 binary operations
------------------------------------------------------------------------
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index c507ecbafc..2ceb801e33 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -582,14 +582,6 @@ record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
)
-record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
- field
- isSemiring : IsSemiring + * 0# 1#
- integral : Integral 1# 0# *
-
- open IsSemiring isSemiring public
-
-
record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
isSemiring : IsSemiring + * 0# 1#
@@ -649,6 +641,14 @@ record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
)
+record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ field
+ isSemiring : IsSemiring + * 0# 1#
+ integral : Integral 1# 0# *
+
+ open IsSemiring isSemiring public
+
+
record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
isIdempotentSemiring : IsIdempotentSemiring + * 0# 1#
@@ -967,6 +967,21 @@ record IsCommutativeRing
; *-isCommutativeMonoid
)
+record IsIntegralRing
+ (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ field
+ isRing : IsRing + * - 0# 1#
+ integral : Integral 1# 0# *
+
+ open IsRing isRing public
+
+ isIntegralSemiring : IsIntegralSemiring + * 0# 1#
+ isIntegralSemiring = record
+ { isSemiring = isSemiring
+ ; integral = integral
+ }
+
+
------------------------------------------------------------------------
-- Structures with 3 binary operations
------------------------------------------------------------------------
From 50bc64ada9ec9541f7e11a6e738197b27ede3db9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 18:01:31 +0000
Subject: [PATCH 7/8] =?UTF-8?q?add:=20`x=E2=89=890=E2=88=A7y=E2=89=890?=
=?UTF-8?q?=E2=87=92x=E1=BA=8F=E2=89=890`=20and=20supporting=20machinery?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
CHANGELOG.md | 11 +++++--
src/Algebra/Consequences/Base.agda | 28 +++++++++++++---
src/Algebra/Properties/IntegralSemiring.agda | 34 ++++++++++++++++++++
3 files changed, 67 insertions(+), 6 deletions(-)
create mode 100644 src/Algebra/Properties/IntegralSemiring.agda
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3491e49a86..5190beaae5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,11 @@ Deprecated names
New modules
-----------
+* `Algebra.Properties.IntegralSemiring`, with:
+ ```agda
+ x≉0∧y≉0⇒xẏ≉0 : x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+ ```
+
* `Algebra.Properties.Semiring.Triviality`, with:
```agda
trivial⇒x≈0 : Trivial → ∀ x → x ≈ 0#
@@ -70,8 +75,10 @@ Additions to existing modules
* In `Algebra.Consequences.Base`:
```agda
- integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
- NoZeroDivisors _≈_ 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#
```
* In `Algebra.Construct.Pointwise`:
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 8dd14bf014..9ae2f41be9 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -17,6 +17,10 @@ open import Relation.Binary.Core
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+private
+ variable
+ x y : A
+
module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
@@ -29,13 +33,29 @@ module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
Involutive _≈_ f
reflexive∧selfInverse⇒involutive refl inv _ = inv refl
-module _ {ℓ} {_•_ : Op₂ A} {0# 1# : A} (_≈_ : Rel A ℓ) where
+module _ {ℓ} {_∙_ : Op₂ A} {0# 1# : A} (_≈_ : Rel A ℓ) where
+
+ private
+ _≉_ : Rel A ℓ
+ x ≉ y = ¬ (x ≈ y)
- integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
- NoZeroDivisors _≈_ 0# _•_
- integral⇒noZeroDivisors (inj₁ 1#≈0#) = contradiction 1#≈0#
+ integral⇒noZeroDivisors : Integral _≈_ 1# 0# _∙_ → 1# ≉ 0# →
+ NoZeroDivisors _≈_ 0# _∙_
+ integral⇒noZeroDivisors (inj₁ trivial) = contradiction trivial
integral⇒noZeroDivisors (inj₂ noZeroDivisors) = λ _ → noZeroDivisors
+module _ {ℓ} {_∙_ : Op₂ A} {0# : A} (_≈_ : Rel A ℓ) where
+
+ private
+ _≉_ : Rel A ℓ
+ x ≉ y = ¬ (x ≈ y)
+
+ noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0 : NoZeroDivisors _≈_ 0# _∙_ →
+ x ≉ 0# → y ≉ 0# → (x ∙ y) ≉ 0#
+ noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0 noZeroDivisors x≉0 y≉0 xy≈0 with noZeroDivisors xy≈0
+ ... | inj₁ x≈0 = x≉0 x≈0
+ ... | inj₂ y≈0 = y≉0 y≈0
+
------------------------------------------------------------------------
-- DEPRECATED NAMES
diff --git a/src/Algebra/Properties/IntegralSemiring.agda b/src/Algebra/Properties/IntegralSemiring.agda
new file mode 100644
index 0000000000..3a9b43a8a2
--- /dev/null
+++ b/src/Algebra/Properties/IntegralSemiring.agda
@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some theory for Semiring.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (IntegralSemiring)
+
+module Algebra.Properties.IntegralSemiring
+ {a ℓ} (R : IntegralSemiring a ℓ)
+ where
+
+open import Algebra.Consequences.Base using (noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0)
+import Algebra.Properties.Semiring.Triviality as Triviality
+open import Data.Sum.Base using (inj₁; inj₂)
+
+open IntegralSemiring R renaming (Carrier to A)
+open Triviality semiring using (trivial⇒x≈0)
+
+private
+ variable
+ x y : A
+
+
+------------------------------------------------------------------------
+-- Properties of Integral
+
+x≉0∧y≉0⇒xẏ≉0 : x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+x≉0∧y≉0⇒xẏ≉0 {x = x} x≉0 y≉0 xy≈0 with integral
+... | inj₁ trivial = x≉0 (trivial⇒x≈0 trivial x)
+... | inj₂ noZeroDivisors = noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0 _≈_ noZeroDivisors x≉0 y≉0 xy≈0
+
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 8/8] 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
------------------------------------------------------------------------