diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..9dcc995c59 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -54,9 +54,36 @@ 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# + ``` + Additions to existing modules ----------------------------- +* In `Algebra.Bundles`: + ```agda + 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# → + NoZeroDivisors _≈_ 0# _∙_ + noZeroDivisors⇒x≉0∧y≉0⇒xẏ≉0 : NoZeroDivisors _≈_ 0# _∙_ → + x ≉ 0# → y ≉ 0# → (x ∙ y) ≉ 0# + ``` + * In `Algebra.Construct.Pointwise`: ```agda isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → @@ -85,3 +112,25 @@ 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)) + +* In `Algebra.Definitions.RawSemiring`: + ```agda + Trivial : Set _ + ``` + (see [discussion on issue #2554](https://github.com/agda/agda-stdlib/issues/2554)) + +* In `Algebra.Structures`: + ```agda + 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 88b195ec7d..951f5693a2 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 _*_ @@ -1124,6 +1154,86 @@ 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 + ) + + +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/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 574ad48a16..9ae2f41be9 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -15,6 +15,11 @@ 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) + +private + variable + x y : A module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where @@ -28,6 +33,30 @@ 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 + + private + _≉_ : Rel A ℓ + x ≉ y = ¬ (x ≈ y) + + 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/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 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/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 + 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#))))) 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 + diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1aae80d1cc..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 @@ -641,6 +642,28 @@ 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 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# @@ -959,6 +982,50 @@ 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 + } + + +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 ------------------------------------------------------------------------