summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Helium/Algebra/Bundles.agda250
-rw-r--r--src/Helium/Algebra/Consequences/Setoid.agda48
-rw-r--r--src/Helium/Algebra/Core.agda19
-rw-r--r--src/Helium/Algebra/Definitions.agda32
-rw-r--r--src/Helium/Algebra/Structures.agda162
5 files changed, 511 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Bundles.agda b/src/Helium/Algebra/Bundles.agda
new file mode 100644
index 0000000..06a0bf2
--- /dev/null
+++ b/src/Helium/Algebra/Bundles.agda
@@ -0,0 +1,250 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions for more algebraic structures
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Bundles where
+
+open import Algebra.Bundles
+open import Algebra.Core
+open import Helium.Algebra.Core
+open import Helium.Algebra.Structures
+open import Level using (_⊔_; suc)
+open import Relation.Binary.Core using (Rel)
+
+record RawAlmostGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infixl 6 _-_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+
+ _-_ : AlmostOp₂ _≈_ 0#
+ x - y≉0 = x ∙ y≉0 ⁻¹
+
+ rawMonoid : RawMonoid c ℓ
+ rawMonoid = record
+ { _≈_ = _≈_
+ ; _∙_ = _∙_
+ ; ε = 1#
+ }
+
+ open RawMonoid rawMonoid public
+ using (_≉_; rawMagma)
+
+record AlmostGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isAlmostGroup : IsAlmostGroup _≈_ _∙_ 0# 1# _⁻¹
+
+ open IsAlmostGroup isAlmostGroup public
+
+ rawAlmostGroup : RawAlmostGroup _ _
+ rawAlmostGroup = record
+ { _≈_ = _≈_
+ ; _∙_ = _∙_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+ monoid : Monoid _ _
+ monoid = record { isMonoid = isMonoid }
+
+ open Monoid monoid public
+ using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+
+record AlmostAbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isAlmostAbelianGroup : IsAlmostAbelianGroup _≈_ _∙_ 0# 1# _⁻¹
+
+ open IsAlmostAbelianGroup isAlmostAbelianGroup public
+
+ almostGroup : AlmostGroup _ _
+ almostGroup = record { isAlmostGroup = isAlmostGroup }
+
+ open AlmostGroup almostGroup public
+ using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawAlmostGroup)
+
+ commutativeMonoid : CommutativeMonoid _ _
+ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+ open CommutativeMonoid commutativeMonoid public
+ using (commutativeMagma; commutativeSemigroup)
+
+record RawField c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_ _/_
+ infixl 6 _+_ _-_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+
+ rawRing : RawRing c ℓ
+ rawRing = record
+ { _≈_ = _≈_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ }
+
+ open RawRing rawRing public
+ using
+ ( _≉_
+ ; +-rawMagma; +-rawMonoid; +-rawGroup
+ ; *-rawMagma; *-rawMonoid
+ ; rawSemiring
+ )
+
+ *-rawAlmostGroup : RawAlmostGroup _ _
+ *-rawAlmostGroup = record
+ { _≈_ = _≈_ ; _∙_ = _*_ ; 0# = 0# ; 1# = 1# ; _⁻¹ = _⁻¹ }
+
+ _-_ : Op₂ Carrier
+ x - y = x + - y
+
+ _/_ : AlmostOp₂ _≈_ 0#
+ x / y≉0 = x * y≉0 ⁻¹
+
+record DivisionRing c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isDivisionRing : IsDivisionRing _≈_ _+_ _*_ -_ 0# 1# _⁻¹
+
+ open IsDivisionRing isDivisionRing public
+
+ ring : Ring _ _
+ ring = record
+ { _≈_ = _≈_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; isRing = isRing
+ }
+
+ open Ring ring public
+ using
+ ( _≉_
+ ; +-rawMagma; +-magma; +-commutativeMagma
+ ; +-semigroup; +-commutativeSemigroup
+ ; +-rawMonoid; +-monoid; +-commutativeMonoid
+ ; +-group; +-abelianGroup
+ ; *-rawMagma; *-magma ; *-semigroup; *-rawMonoid; *-monoid
+ ; nearSemiring ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+ ; semiring
+ ; rawRing
+ )
+
+ rawField : RawField _ _
+ rawField = record
+ { _≈_ = _≈_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+ open RawField rawField public
+ using (+-rawGroup; *-rawAlmostGroup; rawSemiring)
+
+ *-almostGroup : AlmostGroup _ _
+ *-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
+
+record Field c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isField : IsField _≈_ _+_ _*_ -_ 0# 1# _⁻¹
+
+ open IsField isField public
+
+ divisionRing : DivisionRing _ _
+ divisionRing = record { isDivisionRing = isDivisionRing }
+
+ open DivisionRing divisionRing public
+ using
+ ( _≉_
+ ; +-rawMagma; +-magma; +-commutativeMagma
+ ; +-semigroup; +-commutativeSemigroup
+ ; +-rawMonoid; +-monoid; +-commutativeMonoid
+ ; +-rawGroup; +-group; +-abelianGroup
+ ; *-rawMagma; *-magma ; *-semigroup
+ ; *-rawMonoid; *-monoid
+ ; *-rawAlmostGroup; *-almostGroup
+ ; nearSemiring ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+ ; rawSemiring; semiring
+ ; rawRing; ring; rawField
+ )
+
+ commutativeRing : CommutativeRing _ _
+ commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+ open CommutativeRing commutativeRing public
+ using
+ ( *-commutativeMagma; *-commutativeSemigroup; *-commutativeMonoid
+ ; commutativeSemiringWithoutOne; commutativeSemiring
+ )
diff --git a/src/Helium/Algebra/Consequences/Setoid.agda b/src/Helium/Algebra/Consequences/Setoid.agda
new file mode 100644
index 0000000..ab8d41e
--- /dev/null
+++ b/src/Helium/Algebra/Consequences/Setoid.agda
@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Relations between properties of functions when the underlying relation is a setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Helium.Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
+
+open Setoid S renaming (Carrier to A)
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+open import Data.Product using (_,_)
+open import Helium.Algebra.Core
+open import Helium.Algebra.Definitions _≈_
+open import Relation.Nullary using (¬_)
+
+open import Relation.Binary.Reasoning.Setoid S
+
+module _ {0# 1#} {_∙_ : Op₂ A} {_⁻¹ : AlmostOp₁ _≈_ 0#} (cong : Congruent₂ _∙_) where
+ assoc+id+invʳ⇒invˡ-unique : Associative _∙_ →
+ Identity 1# _∙_ →
+ AlmostRightInverse 1# _⁻¹ _∙_ →
+ ∀ x {y} (y≉0 : ¬ y ≈ 0#) →
+ (x ∙ y) ≈ 1# → x ≈ (y≉0 ⁻¹)
+ assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x {y} y≉0 eq = begin
+ x ≈˘⟨ idʳ x ⟩
+ x ∙ 1# ≈˘⟨ cong refl (invʳ y≉0) ⟩
+ x ∙ (y ∙ (y≉0 ⁻¹)) ≈˘⟨ assoc x y (y≉0 ⁻¹) ⟩
+ (x ∙ y) ∙ (y≉0 ⁻¹) ≈⟨ cong eq refl ⟩
+ 1# ∙ (y≉0 ⁻¹) ≈⟨ idˡ (y≉0 ⁻¹) ⟩
+ y≉0 ⁻¹ ∎
+
+ assoc+id+invˡ⇒invʳ-unique : Associative _∙_ →
+ Identity 1# _∙_ →
+ AlmostLeftInverse 1# _⁻¹ _∙_ →
+ ∀ {x} (x≉0 : ¬ x ≈ 0#) y →
+ (x ∙ y) ≈ 1# → y ≈ (x≉0 ⁻¹)
+ assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ {x} x≉0 y eq = begin
+ y ≈˘⟨ idˡ y ⟩
+ 1# ∙ y ≈˘⟨ cong (invˡ x≉0) refl ⟩
+ ((x≉0 ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x≉0 ⁻¹) x y ⟩
+ (x≉0 ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
+ (x≉0 ⁻¹) ∙ 1# ≈⟨ idʳ (x≉0 ⁻¹) ⟩
+ x≉0 ⁻¹ ∎
diff --git a/src/Helium/Algebra/Core.agda b/src/Helium/Algebra/Core.agda
new file mode 100644
index 0000000..afe7053
--- /dev/null
+++ b/src/Helium/Algebra/Core.agda
@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- More core algebraic definitions
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Core where
+
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary using (¬_)
+
+AlmostOp₁ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ)
+AlmostOp₁ {A = A} _≈_ ε = ∀ {x} → ¬ x ≈ ε → A
+
+AlmostOp₂ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ)
+AlmostOp₂ {A = A} _≈_ ε = ∀ (x : A) {y} → ¬ y ≈ ε → A
diff --git a/src/Helium/Algebra/Definitions.agda b/src/Helium/Algebra/Definitions.agda
new file mode 100644
index 0000000..217b353
--- /dev/null
+++ b/src/Helium/Algebra/Definitions.agda
@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- More properties of functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Definitions
+ {a ℓ} {A : Set a} -- The underlying set
+ (_≈_ : Rel A ℓ) -- The underlying equality
+ where
+
+open import Algebra.Core
+open import Data.Product using (_×_)
+open import Helium.Algebra.Core
+open import Relation.Nullary using (¬_)
+
+AlmostCongruent₁ : ∀ {ε} → AlmostOp₁ _≈_ ε → Set _
+AlmostCongruent₁ {ε} f =
+ ∀ {x y} {x≉ε : ¬ x ≈ ε} {y≉ε : ¬ y ≈ ε} → x ≈ y → f x≉ε ≈ f y≉ε
+
+AlmostLeftInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostLeftInverse {ε} e _⁻¹ _∙_ = ∀ {x} (x≉ε : ¬ x ≈ ε) → ((x≉ε ⁻¹) ∙ x) ≈ e
+
+AlmostRightInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostRightInverse {ε} e _⁻¹ _∙_ = ∀ {x} (x≉ε : ¬ x ≈ ε) → (x ∙ (x≉ε ⁻¹)) ≈ e
+
+AlmostInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostInverse e ⁻¹ ∙ = AlmostLeftInverse e ⁻¹ ∙ × AlmostRightInverse e ⁻¹ ∙
diff --git a/src/Helium/Algebra/Structures.agda b/src/Helium/Algebra/Structures.agda
new file mode 100644
index 0000000..b64b4c7
--- /dev/null
+++ b/src/Helium/Algebra/Structures.agda
@@ -0,0 +1,162 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some more algebraic structures
+-- (not packed up with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary.Core using (Rel)
+module Helium.Algebra.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 Algebra.Structures _≈_
+open import Data.Product using (proj₁; proj₂)
+open import Helium.Algebra.Core
+open import Helium.Algebra.Definitions _≈_
+import Helium.Algebra.Consequences.Setoid as Consequences
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_)
+
+record IsAlmostGroup
+ (_∙_ : Op₂ A) (0# 1# : A) (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+ field
+ isMonoid : IsMonoid _∙_ 1#
+ inverse : AlmostInverse 1# _⁻¹ _∙_
+ ⁻¹-cong : AlmostCongruent₁ _⁻¹
+
+ open IsMonoid isMonoid public
+
+ infixl 6 _-_
+ _-_ : AlmostOp₂ _≈_ 0#
+ x - y≉0 = x ∙ (y≉0 ⁻¹)
+
+ inverseˡ : AlmostLeftInverse 1# _⁻¹ _∙_
+ inverseˡ = proj₁ inverse
+
+ inverseʳ : AlmostRightInverse 1# _⁻¹ _∙_
+ inverseʳ = proj₂ inverse
+
+ uniqueˡ-⁻¹ : ∀ x {y} (y≉0 : ¬ y ≈ 0#) → (x ∙ y) ≈ 1# → x ≈ (y≉0 ⁻¹)
+ uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
+ setoid ∙-cong assoc identity inverseʳ
+
+ uniqueʳ-⁻¹ : ∀ {x} (x≉0 : ¬ x ≈ 0#) y → (x ∙ y) ≈ 1# → y ≈ (x≉0 ⁻¹)
+ uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
+ setoid ∙-cong assoc identity inverseˡ
+
+record IsAlmostAbelianGroup
+ (∙ : Op₂ A) (0# 1# : A) (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+ field
+ isAlmostGroup : IsAlmostGroup ∙ 0# 1# ⁻¹
+ comm : Commutative ∙
+
+ open IsAlmostGroup isAlmostGroup
+
+ isCommutativeMonoid : IsCommutativeMonoid ∙ 1#
+ isCommutativeMonoid = record
+ { isMonoid = isMonoid
+ ; comm = comm
+ }
+
+ open IsCommutativeMonoid isCommutativeMonoid public
+ using (isCommutativeMagma; isCommutativeSemigroup)
+
+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# _*_
+
+ infixl 7 _/_
+ _/_ : AlmostOp₂ _≈_ 0#
+ x / y≉0 = x * (y≉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
+ ; uniqueˡ-⁻¹ to uniqueˡ‿-
+ ; uniqueʳ-⁻¹ to uniqueʳ‿-
+ ; comm to +-comm
+ ; isMagma to +-isMagma
+ ; isSemigroup to +-isSemigroup
+ ; isMonoid to +-isMonoid
+ ; isCommutativeMagma to +-isCommutativeMagma
+ ; isCommutativeMonoid to +-isCommutativeMonoid
+ ; isCommutativeSemigroup to +-isCommutativeSemigroup
+ ; isGroup to +-isGroup
+ )
+
+ open IsAlmostGroup *-isAlmostGroup public
+ using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
+ 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ʳ
+ ; isMagma to *-isMagma
+ ; isSemigroup to *-isSemigroup
+ ; isMonoid to *-isMonoid
+ )
+
+ isRing : IsRing + _*_ -_ 0# 1#
+ isRing = record
+ { +-isAbelianGroup = +-isAbelianGroup
+ ; *-isMonoid = *-isMonoid
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open IsRing isRing public
+ using
+ ( distribˡ ; distribʳ ; zeroˡ ; zeroʳ
+ ; isNearSemiring ; isSemiringWithoutOne ; isSemiringWithoutAnnihilatingZero
+ )
+
+record IsField
+ (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
+ (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+ field
+ isDivisionRing : IsDivisionRing + * -_ 0# 1# ⁻¹
+ *-comm : Commutative *
+
+ open IsDivisionRing isDivisionRing public
+
+ isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
+ isCommutativeRing = record
+ { isRing = isRing
+ ; *-comm = *-comm
+ }
+
+ open IsCommutativeRing isCommutativeRing public
+ using
+ ( isCommutativeSemiring
+ ; isCommutativeSemiringWithoutOne
+ ; *-isCommutativeMagma
+ ; *-isCommutativeSemigroup
+ ; *-isCommutativeMonoid
+ )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 11:57:47 +0000