summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Structures.agda')
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Structures.agda160
1 files changed, 135 insertions, 25 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
index 9dc0043..6f6b38d 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
@@ -18,11 +18,11 @@ module Helium.Algebra.Ordered.StrictTotal.Structures
import Algebra.Consequences.Setoid as Consequences
open import Algebra.Core
open import Algebra.Definitions _≈_
-import Algebra.Structures _≈_ as Unordered
+import Algebra.Structures _≈_ as NoOrder
open import Data.Product using (_,_; proj₁; proj₂)
open import Helium.Algebra.Core
open import Helium.Algebra.Definitions _≈_
-open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup)
+import Helium.Algebra.Structures _≈_ as NoOrder′
open import Helium.Algebra.Ordered.Definitions _<_
open import Level using (_⊔_)
@@ -52,26 +52,55 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
∙-invariantʳ : RightInvariant ∙
∙-invariantʳ = proj₂ ∙-invariant
+ module Unordered where
+ isMagma : NoOrder.IsMagma ∙
+ isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMagma : IsMagma ∙
assoc : Associative ∙
open IsMagma isMagma public
+ hiding (module Unordered)
+
+ module Unordered where
+ isSemigroup : NoOrder.IsSemigroup ∙
+ isSemigroup = record
+ { isMagma = IsMagma.Unordered.isMagma isMagma
+ ; assoc = assoc
+ }
+
+ open NoOrder.IsSemigroup isSemigroup public
+ using (isMagma)
-record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsMonoid (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- isSemigroup : IsSemigroup ∙
- identity : Identity ε ∙
+ isSemigroup : IsSemigroup _∙_
+ identity : Identity ε _∙_
open IsSemigroup isSemigroup public
+ hiding (module Unordered)
- identityˡ : LeftIdentity ε ∙
+ identityˡ : LeftIdentity ε _∙_
identityˡ = proj₁ identity
- identityʳ : RightIdentity ε ∙
+ identityʳ : RightIdentity ε _∙_
identityʳ = proj₂ identity
+ identity² : (ε ∙ ε) ≈ ε
+ identity² = identityˡ ε
+
+ module Unordered where
+ isMonoid : NoOrder.IsMonoid _∙_ ε
+ isMonoid = record
+ { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup
+ ; identity = identity
+ }
+
+ open NoOrder.IsMonoid isMonoid public
+ using (isMagma; isSemigroup)
+
record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMonoid : IsMonoid _∙_ ε
@@ -79,6 +108,7 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
⁻¹-cong : Congruent₁ _⁻¹
open IsMonoid isMonoid public
+ hiding (module Unordered)
infixl 6 _-_
_-_ : Op₂ A
@@ -98,6 +128,17 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ
+ module Unordered where
+ isGroup : NoOrder.IsGroup _∙_ ε _⁻¹
+ isGroup = record
+ { isMonoid = IsMonoid.Unordered.isMonoid isMonoid
+ ; inverse = inverse
+ ; ⁻¹-cong = ⁻¹-cong
+ }
+
+ open NoOrder.IsGroup isGroup public
+ using (isMagma; isSemigroup; isMonoid)
+
record IsAbelianGroup (∙ : Op₂ A)
(ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
@@ -105,14 +146,25 @@ record IsAbelianGroup (∙ : Op₂ A)
comm : Commutative ∙
open IsGroup isGroup public
+ hiding (module Unordered)
+
+ module Unordered where
+ isAbelianGroup : NoOrder.IsAbelianGroup ∙ ε ⁻¹
+ isAbelianGroup = record
+ { isGroup = IsGroup.Unordered.isGroup isGroup
+ ; comm = comm
+ }
-record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ open NoOrder.IsAbelianGroup isAbelianGroup public
+ using (isMagma; isSemigroup; isMonoid; isGroup)
+
+record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- +-isAbelianGroup : IsAbelianGroup + 0# -_
- *-isMonoid : Unordered.IsMonoid * 1#
- distrib : * DistributesOver +
- zero : Zero 0# *
- preservesPositive : PreservesPositive 0# *
+ +-isAbelianGroup : IsAbelianGroup + 0# -_
+ *-isMonoid : NoOrder.IsMonoid _*_ 1#
+ distrib : _*_ DistributesOver +
+ zero : Zero 0# _*_
+ 0<a+0<b⇒0<ab : PreservesPositive 0# _*_
open IsAbelianGroup +-isAbelianGroup public
renaming
@@ -120,9 +172,13 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; ∙-cong to +-cong
; ∙-congˡ to +-congˡ
; ∙-congʳ to +-congʳ
+ ; ∙-invariant to +-invariant
+ ; ∙-invariantˡ to +-invariantˡ
+ ; ∙-invariantʳ to +-invariantʳ
; identity to +-identity
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
+ ; identity² to +-identity²
; inverse to -‿inverse
; inverseˡ to -‿inverseˡ
; inverseʳ to -‿inverseʳ
@@ -133,8 +189,9 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; isMonoid to +-isMonoid
; isGroup to +-isGroup
)
+ hiding (module Unordered)
- open Unordered.IsMonoid *-isMonoid public
+ open NoOrder.IsMonoid *-isMonoid public
using ()
renaming
( assoc to *-assoc
@@ -148,18 +205,33 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; isSemigroup to *-isSemigroup
)
- distribˡ : * DistributesOverˡ +
+ *-identity² : (1# * 1#) ≈ 1#
+ *-identity² = *-identityˡ 1#
+
+ distribˡ : _*_ DistributesOverˡ +
distribˡ = proj₁ distrib
- distribʳ : * DistributesOverʳ +
+ distribʳ : _*_ DistributesOverʳ +
distribʳ = proj₂ distrib
- zeroˡ : LeftZero 0# *
+ zeroˡ : LeftZero 0# _*_
zeroˡ = proj₁ zero
- zeroʳ : RightZero 0# *
+ zeroʳ : RightZero 0# _*_
zeroʳ = proj₂ zero
+ module Unordered where
+ isRing : NoOrder.IsRing + _*_ -_ 0# 1#
+ isRing = record
+ { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+ ; *-isMonoid = *-isMonoid
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open NoOrder.IsRing isRing
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup)
+
record IsCommutativeRing
(+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
@@ -167,16 +239,27 @@ record IsCommutativeRing
*-comm : Commutative *
open IsRing isRing public
+ hiding (module Unordered)
+
+ module Unordered where
+ isCommutativeRing : NoOrder.IsCommutativeRing + * (-) 0# 1#
+ isCommutativeRing = record
+ { isRing = IsRing.Unordered.isRing isRing
+ ; *-comm = *-comm
+ }
+
+ open NoOrder.IsCommutativeRing isCommutativeRing public
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
record IsDivisionRing
(+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
(_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- +-isAbelianGroup : IsAbelianGroup + 0# -_
- *-isAlmostGroup : IsAlmostGroup _*_ 0# 1# _⁻¹
- distrib : _*_ DistributesOver +
- zero : Zero 0# _*_
- preservesPositive : PreservesPositive 0# _*_
+ +-isAbelianGroup : IsAbelianGroup + 0# -_
+ *-isAlmostGroup : NoOrder′.IsAlmostGroup _*_ 0# 1# _⁻¹
+ distrib : _*_ DistributesOver +
+ zero : Zero 0# _*_
+ 0<a+0<b⇒0<ab : PreservesPositive 0# _*_
infixl 7 _/_
_/_ : AlmostOp₂ _≈_ 0#
@@ -203,8 +286,9 @@ record IsDivisionRing
; isMonoid to +-isMonoid
; isGroup to +-isGroup
)
+ hiding (module Unordered)
- open IsAlmostGroup *-isAlmostGroup public
+ open NoOrder′.IsAlmostGroup *-isAlmostGroup public
using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
renaming
( assoc to *-assoc
@@ -228,12 +312,24 @@ record IsDivisionRing
; *-isMonoid = *-isMonoid
; distrib = distrib
; zero = zero
- ; preservesPositive = preservesPositive
+ ; 0<a+0<b⇒0<ab = 0<a+0<b⇒0<ab
}
open IsRing isRing public
using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ)
+ module Unordered where
+ isDivisionRing : NoOrder′.IsDivisionRing + _*_ -_ 0# 1# _⁻¹
+ isDivisionRing = record
+ { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+ ; *-isAlmostGroup = *-isAlmostGroup
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open NoOrder′.IsDivisionRing isDivisionRing
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
+
record IsField
(+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
(⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -242,9 +338,23 @@ record IsField
*-comm : Commutative *
open IsDivisionRing isDivisionRing public
+ hiding (module Unordered)
isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
isCommutativeRing = record
{ isRing = isRing
; *-comm = *-comm
}
+
+ module Unordered where
+ isField : NoOrder′.IsField + * -_ 0# 1# ⁻¹
+ isField = record
+ { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing
+ ; *-comm = *-comm
+ }
+
+ open NoOrder′.IsField isField
+ using
+ ( +-isMagma; +-isSemigroup; +-isMonoid; +-isGroup
+ ; isRing; isDivisionRing
+ )