From deb5d2b61782526ad6f5f14198ef2eadfe08d453 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sat, 15 Jan 2022 16:07:15 -0500 Subject: [PATCH 1/5] Define Rng --- src/Algebra/Bundles.agda | 34 +++++++++++++++++++++++ src/Algebra/Structures.agda | 55 +++++++++++++++++++++++++++++++++++++ 2 files changed, 89 insertions(+) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 5560f84ecf..4afc19b02c 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -750,6 +750,40 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where ; _≉_ ) +------------------------------------------------------------------------ +-- Bundles with 2 binary operations, 1 unary operation & 1 elements +------------------------------------------------------------------------ + +record Rng 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 + isRng : IsRng _≈_ _+_ _*_ -_ 0# + + open IsRng isRng public + + +-abelianGroup : AbelianGroup _ _ + +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } + + *-semigroup : Semigroup _ _ + *-semigroup = record { isSemigroup = *-isSemigroup } + + open AbelianGroup +-abelianGroup public + using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) + + open Semigroup *-semigroup public + using () renaming + ( rawMagma to *-rawMagma + ; magma to *-magma + ) ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 2 elements diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1c0dd7a93a..eaed613a4e 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -450,7 +450,62 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a open IsCommutativeSemiring isCommutativeSemiring public +------------------------------------------------------------------------ +-- Structures with 2 binary operations, 1 unary operation & 1 elements +------------------------------------------------------------------------ +record IsRng (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where + field + +-isAbelianGroup : IsAbelianGroup + 0# -_ + *-cong : Congruent₂ * + *-assoc : Associative * + distrib : * DistributesOver + + zero : Zero 0# * + + open IsAbelianGroup +-isAbelianGroup public + renaming + ( assoc to +-assoc + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; ∙-congʳ to +-congʳ + ; identity to +-identity + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; inverse to -‿inverse + ; inverseˡ to -‿inverseˡ + ; inverseʳ to -‿inverseʳ + ; ⁻¹-cong to -‿cong + ; comm to +-comm + ; isMagma to +-isMagma + ; isSemigroup to +-isSemigroup + ; isMonoid to +-isMonoid + ; isUnitalMagma to +-isUnitalMagma + ; isCommutativeMagma to +-isCommutativeMagma + ; isCommutativeMonoid to +-isCommutativeMonoid + ; isCommutativeSemigroup to +-isCommutativeSemigroup + ; isInvertibleMagma to +-isInvertibleMagma + ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma + ; isGroup to +-isGroup + ) + + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } + + *-isSemigroup : IsSemigroup * + *-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + + open IsMagma *-isMagma public + using () + renaming + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ) ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements From bc5b2d87849fb5f01858bbb409f53a319848c239 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sun, 16 Jan 2022 10:49:40 -0500 Subject: [PATCH 2/5] minor fixes --- src/Algebra/Bundles.agda | 20 ++++++++++---------- src/Algebra/Structures.agda | 4 ++-- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 4afc19b02c..b1761bb5e1 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -751,24 +751,24 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where ) ------------------------------------------------------------------------ --- Bundles with 2 binary operations, 1 unary operation & 1 elements +-- Bundles with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ -record Rng c ℓ : Set (suc (c ⊔ ℓ)) where +record RingWithoutOne 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 - isRng : IsRng _≈_ _+_ _*_ -_ 0# + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + isRingWithoutOne : IsRingWithoutOne _≈_ _+_ _*_ -_ 0# - open IsRng isRng public + open IsRingWithoutOne isRingWithoutOne public +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index eaed613a4e..cbaa3f6f87 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -451,10 +451,10 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a open IsCommutativeSemiring isCommutativeSemiring public ------------------------------------------------------------------------ --- Structures with 2 binary operations, 1 unary operation & 1 elements +-- Structures with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ -record IsRng (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where +record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where field +-isAbelianGroup : IsAbelianGroup + 0# -_ *-cong : Congruent₂ * From 19af2a281816b04d3481fa06f98458c700a86cfc Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sun, 16 Jan 2022 10:57:54 -0500 Subject: [PATCH 3/5] Update CHANGELOG.md --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 47311935e4..e8296e43a1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -741,6 +741,7 @@ Other minor changes record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) record RawLoop c ℓ : Set (suc (c ⊔ ℓ)) record Loop c ℓ : Set (suc (c ⊔ ℓ)) + record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) ``` and the existing record `Lattice` now provides ```agda @@ -805,6 +806,7 @@ Other minor changes record IsInvertibleUnitalMagma (_∙_ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) record IsQuasigroup (∙ \\ // : Op₂ A) : Set (a ⊔ ℓ) record IsLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) ``` and the existing record `IsLattice` now provides ``` From 468c87c47430af288b94e7d1cbbe829a27fa6872 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sun, 23 Jan 2022 13:23:08 -0500 Subject: [PATCH 4/5] add missing instance --- src/Algebra/Structures.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index cbaa3f6f87..c0e264e21b 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -493,6 +493,18 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ { isEquivalence = isEquivalence ; ∙-cong = *-cong } + + zeroˡ : LeftZero 0# * + zeroˡ = proj₁ zero + + zeroʳ : RightZero 0# * + zeroʳ = proj₂ zero + + distribˡ : * DistributesOverˡ + + distribˡ = proj₁ distrib + + distribʳ : * DistributesOverʳ + + distribʳ = proj₂ distrib *-isSemigroup : IsSemigroup * *-isSemigroup = record From 7284e6506300a0a218b44933a928e018d58c7ab8 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Sun, 23 Jan 2022 13:24:04 -0500 Subject: [PATCH 5/5] fix-whitespace --- src/Algebra/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index c0e264e21b..e637b42310 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -493,7 +493,7 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ { isEquivalence = isEquivalence ; ∙-cong = *-cong } - + zeroˡ : LeftZero 0# * zeroˡ = proj₁ zero