summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Algebra')
-rw-r--r--src/Helium/Algebra/Decidable/Bundles.agda108
-rw-r--r--src/Helium/Algebra/Decidable/Construct/Pointwise.agda (renamed from src/Helium/Algebra/Construct/Pointwise.agda)55
-rw-r--r--src/Helium/Algebra/Decidable/Structures.agda87
-rw-r--r--src/Helium/Algebra/Morphism/Structures.agda42
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda182
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Structures.agda160
6 files changed, 583 insertions, 51 deletions
diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda
new file mode 100644
index 0000000..e446706
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Bundles.agda
@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of decidable algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Helium.Algebra.Decidable.Bundles where
+
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
+open import Helium.Algebra.Decidable.Structures
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Bundles using (DecSetoid)
+open import Relation.Binary.Core using (Rel)
+
+record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ isLattice : IsLattice _≈_ _∨_ _∧_
+
+ open IsLattice isLattice public
+
+ rawLattice : RawLattice c ℓ
+ rawLattice = record
+ { _≈_ = _≈_
+ ; _∧_ = _∧_
+ ; _∨_ = _∨_
+ }
+
+ open RawLattice rawLattice public
+ using (∨-rawMagma; ∧-rawMagma)
+
+ decSetoid : DecSetoid _ _
+ decSetoid = record { isDecEquivalence = isDecEquivalence }
+
+ open DecSetoid decSetoid public
+ using (_≉_; setoid)
+
+record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
+
+ open IsDistributiveLattice isDistributiveLattice public
+
+ lattice : Lattice _ _
+ lattice = record { isLattice = isLattice }
+
+ open Lattice lattice public
+ using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice)
+
+record RawBooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 ¬_
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∧_ : Op₂ Carrier
+ _∨_ : Op₂ Carrier
+ ¬_ : Op₁ Carrier
+ ⊤ : Carrier
+ ⊥ : Carrier
+
+ rawLattice : RawLattice c ℓ
+ rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ }
+
+ open RawLattice rawLattice public
+ using (_≉_; ∨-rawMagma; ∧-rawMagma)
+
+record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 ¬_
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ ¬_ : Op₁ Carrier
+ ⊤ : Carrier
+ ⊥ : Carrier
+ isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
+
+ open IsBooleanAlgebra isBooleanAlgebra public
+
+ distributiveLattice : DistributiveLattice _ _
+ distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
+
+ open DistributiveLattice distributiveLattice public
+ using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice)
diff --git a/src/Helium/Algebra/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
index d3aa560..9f067ba 100644
--- a/src/Helium/Algebra/Construct/Pointwise.agda
+++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
@@ -6,17 +6,20 @@
{-# OPTIONS --safe --without-K #-}
-module Helium.Algebra.Construct.Pointwise where
+module Helium.Algebra.Decidable.Construct.Pointwise where
-open import Algebra
-open import Relation.Binary.Core using (Rel)
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
open import Data.Nat using (ℕ)
open import Data.Product using (_,_)
open import Data.Vec.Functional using (replicate; map; zipWith)
open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
open import Function using (_$_)
+open import Helium.Algebra.Decidable.Bundles
+open import Helium.Algebra.Decidable.Structures
open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
private
@@ -25,22 +28,23 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
module _ {∨ ∧ : Op₂ A} where
isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
isLattice L n = record
- { isEquivalence = Pwₚ.isEquivalence isEquivalence n
- ; ∨-comm = λ x y i → ∨-comm (x i) (y i)
- ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i)
- ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
- ; ∧-comm = λ x y i → ∧-comm (x i) (y i)
- ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i)
- ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
- ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i))
- , (λ x y i → ∧-absorbs-∨ (x i) (y i))
+ { isDecEquivalence = Pwₚ.isDecEquivalence isDecEquivalence n
+ ; ∨-comm = λ x y i → ∨-comm (x i) (y i)
+ ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i)
+ ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
+ ; ∧-comm = λ x y i → ∧-comm (x i) (y i)
+ ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i)
+ ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
+ ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i))
+ , (λ x y i → ∧-absorbs-∨ (x i) (y i))
}
where open IsLattice L
isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
isDistributiveLattice L n = record
{ isLattice = isLattice L.isLattice n
- ; ∨-distribʳ-∧ = λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i)
+ ; ∨-distrib-∧ = (λ x y z i → L.∨-distribˡ-∧ (x i) (y i) (z i))
+ , (λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i))
}
where module L = IsDistributiveLattice L
@@ -48,12 +52,22 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥)
isBooleanAlgebra B n = record
{ isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n
- ; ∨-complementʳ = λ x i → B.∨-complementʳ (x i)
- ; ∧-complementʳ = λ x i → B.∧-complementʳ (x i)
+ ; ∨-complement = (λ x i → B.∨-complementˡ (x i))
+ , (λ x i → B.∨-complementʳ (x i))
+ ; ∧-complement = (λ x i → B.∧-complementˡ (x i))
+ , (λ x i → B.∧-complementʳ (x i))
; ¬-cong = λ x≈y i → B.¬-cong (x≈y i)
}
where module B = IsBooleanAlgebra B
+rawLattice : ∀ {a ℓ} → RawLattice a ℓ → ℕ → RawLattice a ℓ
+rawLattice L n = record
+ { _≈_ = Pointwise _≈_ {n}
+ ; _∧_ = zipWith _∧_
+ ; _∨_ = zipWith _∨_
+ }
+ where open RawLattice L
+
lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ
lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n }
@@ -63,6 +77,17 @@ distributiveLattice L n = record
isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n
}
+rawBooleanAlgebra : ∀ {a ℓ} → RawBooleanAlgebra a ℓ → ℕ → RawBooleanAlgebra a ℓ
+rawBooleanAlgebra B n = record
+ { _≈_ = Pointwise _≈_ {n}
+ ; _∧_ = zipWith _∧_
+ ; _∨_ = zipWith _∨_
+ ; ¬_ = map ¬_
+ ; ⊤ = replicate ⊤
+ ; ⊥ = replicate ⊥
+ }
+ where open RawBooleanAlgebra B
+
booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ
booleanAlgebra B n = record
{ isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n }
diff --git a/src/Helium/Algebra/Decidable/Structures.agda b/src/Helium/Algebra/Decidable/Structures.agda
new file mode 100644
index 0000000..4380cc5
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Structures.agda
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some decidable algebraic structures (not packed up with sets,
+-- operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Decidable.Structures
+ {a ℓ} {A : Set a} -- The underlying set
+ (_≈_ : Rel A ℓ) -- The underlying equality relation
+ where
+
+open import Algebra.Core
+open import Algebra.Definitions (_≈_)
+open import Data.Product using (proj₁; proj₂)
+open import Level using (_⊔_)
+open import Relation.Binary.Structures using (IsDecEquivalence)
+
+record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+ field
+ isDecEquivalence : IsDecEquivalence _≈_
+ ∨-comm : Commutative ∨
+ ∨-assoc : Associative ∨
+ ∨-cong : Congruent₂ ∨
+ ∧-comm : Commutative ∧
+ ∧-assoc : Associative ∧
+ ∧-cong : Congruent₂ ∧
+ absorptive : Absorptive ∨ ∧
+
+ open IsDecEquivalence isDecEquivalence public
+
+ ∨-absorbs-∧ : ∨ Absorbs ∧
+ ∨-absorbs-∧ = proj₁ absorptive
+
+ ∧-absorbs-∨ : ∧ Absorbs ∨
+ ∧-absorbs-∨ = proj₂ absorptive
+
+ ∧-congˡ : LeftCongruent ∧
+ ∧-congˡ y≈z = ∧-cong refl y≈z
+
+ ∧-congʳ : RightCongruent ∧
+ ∧-congʳ y≈z = ∧-cong y≈z refl
+
+ ∨-congˡ : LeftCongruent ∨
+ ∨-congˡ y≈z = ∨-cong refl y≈z
+
+ ∨-congʳ : RightCongruent ∨
+ ∨-congʳ y≈z = ∨-cong y≈z refl
+
+record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+ field
+ isLattice : IsLattice ∨ ∧
+ ∨-distrib-∧ : ∨ DistributesOver ∧
+
+ open IsLattice isLattice public
+
+ ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧
+ ∨-distribˡ-∧ = proj₁ ∨-distrib-∧
+
+ ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
+ ∨-distribʳ-∧ = proj₂ ∨-distrib-∧
+
+record IsBooleanAlgebra
+ (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
+ field
+ isDistributiveLattice : IsDistributiveLattice ∨ ∧
+ ∨-complement : Inverse ⊤ ¬ ∨
+ ∧-complement : Inverse ⊥ ¬ ∧
+ ¬-cong : Congruent₁ ¬
+
+ open IsDistributiveLattice isDistributiveLattice public
+
+ ∨-complementˡ : LeftInverse ⊤ ¬ ∨
+ ∨-complementˡ = proj₁ ∨-complement
+
+ ∨-complementʳ : RightInverse ⊤ ¬ ∨
+ ∨-complementʳ = proj₂ ∨-complement
+
+ ∧-complementˡ : LeftInverse ⊥ ¬ ∧
+ ∧-complementˡ = proj₁ ∧-complement
+
+ ∧-complementʳ : RightInverse ⊥ ¬ ∧
+ ∧-complementʳ = proj₂ ∧-complement
diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda
new file mode 100644
index 0000000..bf219ef
--- /dev/null
+++ b/src/Helium/Algebra/Morphism/Structures.agda
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Redefine Ring monomorphisms to resolve problems with overloading.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Morphism.Structures where
+
+open import Algebra.Bundles using (RawRing)
+open import Algebra.Morphism.Structures
+ hiding (IsRingHomomorphism; module RingMorphisms)
+open import Level using (Level; _⊔_)
+
+private
+ variable
+ a b ℓ₁ ℓ₂ : Level
+
+module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
+ module R₁ = RawRing R₁ renaming (Carrier to A)
+ module R₂ = RawRing R₂ renaming (Carrier to B)
+ open R₁ using (A)
+ open R₂ using (B)
+
+ private
+ module +′ = GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup
+ module *′ = MonoidMorphisms R₁.*-rawMonoid R₂.*-rawMonoid
+
+ record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ +-isGroupHomomorphism : +′.IsGroupHomomorphism ⟦_⟧
+ *-isMonoidHomomorphism : *′.IsMonoidHomomorphism ⟦_⟧
+
+ open +′.IsGroupHomomorphism +-isGroupHomomorphism public
+ renaming (homo to +-homo; ε-homo to 0#-homo; ⁻¹-homo to -‿homo)
+
+ open *′.IsMonoidHomomorphism *-isMonoidHomomorphism public
+ hiding (⟦⟧-cong)
+ renaming (homo to *-homo; ε-homo to 1#-homo)
+
+open RingMorphisms public
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
index 6904bfb..a9430e9 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -10,13 +10,12 @@
module Helium.Algebra.Ordered.StrictTotal.Bundles where
-import Algebra.Bundles as Unordered
+import Algebra.Bundles as NoOrder
open import Algebra.Core
open import Data.Sum using (_⊎_)
open import Function using (flip)
open import Helium.Algebra.Core
-open import Helium.Algebra.Bundles using
- (RawAlmostGroup; AlmostGroup; AlmostAbelianGroup)
+import Helium.Algebra.Bundles as NoOrder′
open import Helium.Algebra.Ordered.StrictTotal.Structures
open import Level using (suc; _⊔_)
open import Relation.Binary
@@ -44,6 +43,10 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
_≥_ : Rel Carrier _
_≥_ = flip _≤_
+ module Unordered where
+ rawMagma : NoOrder.RawMagma c ℓ₁
+ rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ }
+
record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -55,6 +58,7 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isMagma : IsMagma _≈_ _<_ _∙_
open IsMagma isMagma public
+ hiding (module Unordered)
rawMagma : RawMagma _ _ _
rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
@@ -62,6 +66,15 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMagma rawMagma public
using (_≉_; _≤_; _>_; _≥_)
+ module Unordered where
+ magma : NoOrder.Magma c ℓ₁
+ magma = record { isMagma = IsMagma.Unordered.isMagma isMagma }
+
+ open NoOrder.Magma magma public
+ using (rawMagma)
+
+ open IsMagma.Unordered isMagma public
+
record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -73,6 +86,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isSemigroup : IsSemigroup _≈_ _<_ _∙_
open IsSemigroup isSemigroup public
+ hiding (module Unordered)
magma : Magma c ℓ₁ ℓ₂
magma = record { isMagma = isMagma }
@@ -80,6 +94,16 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open Magma magma public
using (_≉_; _≤_; _>_; _≥_; rawMagma)
+ module Unordered where
+ semigroup : NoOrder.Semigroup c ℓ₁
+ semigroup =
+ record { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup }
+
+ open NoOrder.Semigroup semigroup public
+ using (rawMagma; magma)
+
+ open IsSemigroup.Unordered isSemigroup public
+
record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -96,6 +120,13 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMagma rawMagma public
using (_≉_; _≤_; _>_; _≥_)
+ module Unordered where
+ rawMonoid : NoOrder.RawMonoid c ℓ₁
+ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε }
+
+ open NoOrder.RawMonoid rawMonoid public
+ using (rawMagma)
+
record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -108,6 +139,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isMonoid : IsMonoid _≈_ _<_ _∙_ ε
open IsMonoid isMonoid public
+ hiding (module Unordered)
semigroup : Semigroup _ _ _
semigroup = record { isSemigroup = isSemigroup }
@@ -118,6 +150,15 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
rawMonoid : RawMonoid _ _ _
rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε}
+ module Unordered where
+ monoid : NoOrder.Monoid c ℓ₁
+ monoid = record { isMonoid = IsMonoid.Unordered.isMonoid isMonoid }
+
+ open NoOrder.Monoid monoid public
+ using (rawMagma; rawMonoid; magma; semigroup)
+
+ open IsMonoid.Unordered isMonoid public
+
record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
infixl 7 _∙_
@@ -136,6 +177,12 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMonoid rawMonoid public
using (_≉_; _≤_; _>_; _≥_; rawMagma)
+ module Unordered where
+ rawGroup : NoOrder.RawGroup c ℓ₁
+ rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹ }
+
+ open NoOrder.RawGroup rawGroup public
+ using (rawMagma; rawMonoid)
record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
@@ -151,6 +198,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹
open IsGroup isGroup public
+ hiding (module Unordered)
rawGroup : RawGroup _ _ _
rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
@@ -161,6 +209,15 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open Monoid monoid public
using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid)
+ module Unordered where
+ group : NoOrder.Group c ℓ₁
+ group = record { isGroup = IsGroup.Unordered.isGroup isGroup }
+
+ open NoOrder.Group group public
+ using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid)
+
+ open IsGroup.Unordered isGroup public
+
record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
infixl 7 _∙_
@@ -175,6 +232,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹
open IsAbelianGroup isAbelianGroup public
+ hiding (module Unordered)
group : Group _ _ _
group = record { isGroup = isGroup }
@@ -186,6 +244,16 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; rawMagma; rawMonoid; rawGroup
)
+ module Unordered where
+ abelianGroup : NoOrder.AbelianGroup c ℓ₁
+ abelianGroup =
+ record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup }
+
+ open NoOrder.AbelianGroup abelianGroup public
+ using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group)
+
+ open IsAbelianGroup.Unordered isAbelianGroup public
+
record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -211,13 +279,21 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; rawMonoid to +-rawMonoid
)
- *-rawMonoid : Unordered.RawMonoid c ℓ₁
+ *-rawMonoid : NoOrder.RawMonoid c ℓ₁
*-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# }
- open Unordered.RawMonoid *-rawMonoid public
+ open NoOrder.RawMonoid *-rawMonoid public
using ()
renaming ( rawMagma to *-rawMagma )
+ module Unordered where
+ rawRing : NoOrder.RawRing c ℓ₁
+ rawRing =
+ record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# }
+
+ open NoOrder.RawRing rawRing public
+ using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring)
+
record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -235,6 +311,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1#
open IsRing isRing public
+ hiding (module Unordered)
rawRing : RawRing c ℓ₁ ℓ₂
rawRing = record
@@ -262,10 +339,10 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; group to +-group
)
- *-monoid : Unordered.Monoid _ _
+ *-monoid : NoOrder.Monoid _ _
*-monoid = record { isMonoid = *-isMonoid }
- open Unordered.Monoid *-monoid public
+ open NoOrder.Monoid *-monoid public
using ()
renaming
( rawMagma to *-rawMagma
@@ -274,6 +351,19 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; semigroup to *-semigroup
)
+ module Unordered where
+ ring : NoOrder.Ring c ℓ₁
+ ring = record { isRing = IsRing.Unordered.isRing isRing }
+
+ open NoOrder.Ring ring public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawRing; semiring
+ )
+
+ open IsRing.Unordered isRing public
+
record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -291,6 +381,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1#
open IsCommutativeRing isCommutativeRing public
+ hiding (module Unordered)
ring : Ring _ _ _
ring = record { isRing = isRing }
@@ -298,12 +389,30 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
open Ring ring public
using
( _≉_; _≤_; _>_; _≥_
+ ; rawRing
; +-rawMagma; +-rawMonoid; +-rawGroup
; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
; *-rawMagma; *-rawMonoid
; *-magma; *-semigroup; *-monoid
)
+ module Unordered where
+ commutativeRing : NoOrder.CommutativeRing c ℓ₁
+ commutativeRing =
+ record { isCommutativeRing = IsCommutativeRing.Unordered.isCommutativeRing isCommutativeRing }
+
+ open NoOrder.CommutativeRing commutativeRing public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawRing; semiring; ring
+ )
+
+ open NoOrder.Semiring semiring public
+ using (rawSemiring)
+
+ open IsCommutativeRing.Unordered isCommutativeRing public
+
record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -343,7 +452,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; *-rawMagma; *-rawMonoid
)
- *-rawAlmostGroup : RawAlmostGroup c ℓ₁
+ *-rawAlmostGroup : NoOrder′.RawAlmostGroup c ℓ₁
*-rawAlmostGroup = record
{ _≈_ = _≈_
; _∙_ = _*_
@@ -352,6 +461,21 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; _⁻¹ = _⁻¹
}
+ module Unordered where
+ rawField : NoOrder′.RawField c ℓ₁
+ rawField = record
+ { _≈_ = _≈_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+ open NoOrder′.RawField rawField public
+ using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring; rawRing)
+
record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -371,6 +495,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
open IsDivisionRing isDivisionRing public
+ hiding (module Unordered)
rawField : RawField c ℓ₁ ℓ₂
rawField = record
@@ -397,13 +522,28 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; *-magma; *-semigroup; *-monoid
)
- *-almostGroup : AlmostGroup _ _
+ *-almostGroup : NoOrder′.AlmostGroup _ _
*-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
- open AlmostGroup *-almostGroup public
+ open NoOrder′.AlmostGroup *-almostGroup public
using ()
renaming (rawAlmostGroup to *-rawAlmostGroup)
+ module Unordered where
+ divisionRing : NoOrder′.DivisionRing c ℓ₁
+ divisionRing =
+ record { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing }
+
+ open NoOrder′.DivisionRing divisionRing public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawSemiring; rawRing
+ ; semiring; ring
+ )
+
+ open IsDivisionRing.Unordered isDivisionRing public
+
record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -423,15 +563,35 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
open IsField isField public
+ hiding (module Unordered)
divisionRing : DivisionRing c ℓ₁ ℓ₂
divisionRing = record { isDivisionRing = isDivisionRing }
- open DivisionRing divisionRing
+ open DivisionRing divisionRing public
using
( _≉_; _≤_; _>_; _≥_
+ ; rawRing; rawField; ring
; +-rawMagma; +-rawMonoid; +-rawGroup
; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
; *-rawMagma; *-rawMonoid; *-rawAlmostGroup
; *-magma; *-semigroup; *-monoid; *-almostGroup
)
+
+ commutativeRing : CommutativeRing c ℓ₁ ℓ₂
+ commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+ module Unordered where
+ field′ : NoOrder′.Field c ℓ₁
+ field′ =
+ record { isField = IsField.Unordered.isField isField }
+
+ open NoOrder′.Field field′ public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawSemiring; rawRing
+ ; semiring; ring; divisionRing
+ )
+
+ open IsField.Unordered isField public
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
+ )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 23:00:53 +0000