From 74f82751113455ec48bf699ab95fc738dd46a08b Mon Sep 17 00:00:00 2001 From: jamesmckinna 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 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 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 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 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 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 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 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 ------------------------------------------------------------------------