[ add ] Algebra.Definitions.Integral and its consequences

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 _
+  ```

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
 ------------------------------------------------------------------------

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
 ------------------------------------------------------------------------

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
 

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#

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
+

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#)))))

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
+