diff options
Diffstat (limited to 'src/Helium/Algebra/Structures.agda')
| -rw-r--r-- | src/Helium/Algebra/Structures.agda | 162 |
1 files changed, 162 insertions, 0 deletions
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 + ) |