From f640cb65e9106be5674f8f13d9594d12966d823a Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 16 Jan 2022 16:59:55 +0000 Subject: Define ordered algebraic structures. --- src/Helium/Algebra/Ordered/Definitions.agda | 29 ++ .../Algebra/Ordered/StrictTotal/Bundles.agda | 437 +++++++++++++++++++++ .../Algebra/Ordered/StrictTotal/Structures.agda | 250 ++++++++++++ 3 files changed, 716 insertions(+) create mode 100644 src/Helium/Algebra/Ordered/Definitions.agda create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Structures.agda (limited to 'src/Helium') diff --git a/src/Helium/Algebra/Ordered/Definitions.agda b/src/Helium/Algebra/Ordered/Definitions.agda new file mode 100644 index 0000000..4ac1070 --- /dev/null +++ b/src/Helium/Algebra/Ordered/Definitions.agda @@ -0,0 +1,29 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Ordering properties of functions +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Helium.Algebra.Ordered.Definitions + {a ℓ} {A : Set a} -- The underlying set + (_≤_ : Rel A ℓ) -- The underlying order + where + +open import Algebra.Core +open import Data.Product using (_×_) + +LeftInvariant : Op₂ A → Set _ +LeftInvariant _∙_ = ∀ {x y} z → x ≤ y → (z ∙ x) ≤ (z ∙ y) + +RightInvariant : Op₂ A → Set _ +RightInvariant _∙_ = ∀ {x y} z → x ≤ y → (x ∙ z) ≤ (y ∙ z) + +Invariant : Op₂ A → Set _ +Invariant ∙ = LeftInvariant ∙ × RightInvariant ∙ + +PreservesPositive : A → Op₂ A → Set _ +PreservesPositive 0# _∙_ = ∀ {x y} → 0# ≤ x → 0# ≤ y → 0# ≤ (x ∙ y) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda new file mode 100644 index 0000000..6904bfb --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -0,0 +1,437 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definitions of ordered algebraic structures like monoids and rings +-- (packed in records together with sets, operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + + +module Helium.Algebra.Ordered.StrictTotal.Bundles where + +import Algebra.Bundles as Unordered +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) +open import Helium.Algebra.Ordered.StrictTotal.Structures +open import Level using (suc; _⊔_) +open import Relation.Binary +open import Relation.Nullary as N + +record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + + infix 4 _≉_ _≤_ _>_ _≥_ + _≉_ : Rel Carrier _ + x ≉ y = N.¬ x ≈ y + + _≤_ : Rel Carrier _ + x ≤ y = x < y ⊎ x ≈ y + + _>_ : Rel Carrier _ + _>_ = flip _<_ + + _≥_ : Rel Carrier _ + _≥_ = flip _≤_ + +record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + isMagma : IsMagma _≈_ _<_ _∙_ + + open IsMagma isMagma public + + rawMagma : RawMagma _ _ _ + rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } + + open RawMagma rawMagma public + using (_≉_; _≤_; _>_; _≥_) + +record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + isSemigroup : IsSemigroup _≈_ _<_ _∙_ + + open IsSemigroup isSemigroup public + + magma : Magma c ℓ₁ ℓ₂ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; _≤_; _>_; _≥_; rawMagma) + +record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + ε : Carrier + + rawMagma : RawMagma c ℓ₁ ℓ₂ + rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } + + open RawMagma rawMagma public + using (_≉_; _≤_; _>_; _≥_) + +record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + ε : Carrier + isMonoid : IsMonoid _≈_ _<_ _∙_ ε + + open IsMonoid isMonoid public + + semigroup : Semigroup _ _ _ + semigroup = record { isSemigroup = isSemigroup } + + open Semigroup semigroup public + using (_≉_; _≤_; _>_; _≥_; rawMagma; magma) + + rawMonoid : RawMonoid _ _ _ + rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε} + +record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 _⁻¹ + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + + rawMonoid : RawMonoid c ℓ₁ ℓ₂ + rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε } + + open RawMonoid rawMonoid public + using (_≉_; _≤_; _>_; _≥_; rawMagma) + + +record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 _⁻¹ + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹ + + open IsGroup isGroup public + + rawGroup : RawGroup _ _ _ + rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹} + + monoid : Monoid _ _ _ + monoid = record { isMonoid = isMonoid } + + open Monoid monoid public + using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid) + +record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 _⁻¹ + infixl 7 _∙_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹ + + open IsAbelianGroup isAbelianGroup public + + group : Group _ _ _ + group = record { isGroup = isGroup } + + open Group group public + using + ( _≉_; _≤_; _>_; _≥_ + ; magma; semigroup; monoid + ; rawMagma; rawMonoid; rawGroup + ) + +record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + + +-rawGroup : RawGroup c ℓ₁ ℓ₂ + +-rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _+_; ε = 0#; _⁻¹ = -_ } + + open RawGroup +-rawGroup public + using ( _≉_; _≤_; _>_; _≥_ ) + renaming + ( rawMagma to +-rawMagma + ; rawMonoid to +-rawMonoid + ) + + *-rawMonoid : Unordered.RawMonoid c ℓ₁ + *-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# } + + open Unordered.RawMonoid *-rawMonoid public + using () + renaming ( rawMagma to *-rawMagma ) + +record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1# + + open IsRing isRing public + + rawRing : RawRing c ℓ₁ ℓ₂ + rawRing = record + { _≈_ = _≈_ + ; _<_ = _<_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } + + +-abelianGroup : AbelianGroup _ _ _ + +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } + + open AbelianGroup +-abelianGroup public + using ( _≉_; _≤_; _>_; _≥_ ) + renaming + ( rawMagma to +-rawMagma + ; rawMonoid to +-rawMonoid + ; rawGroup to +-rawGroup + ; magma to +-magma + ; semigroup to +-semigroup + ; monoid to +-monoid + ; group to +-group + ) + + *-monoid : Unordered.Monoid _ _ + *-monoid = record { isMonoid = *-isMonoid } + + open Unordered.Monoid *-monoid public + using () + renaming + ( rawMagma to *-rawMagma + ; rawMonoid to *-rawMonoid + ; magma to *-magma + ; semigroup to *-semigroup + ) + +record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1# + + open IsCommutativeRing isCommutativeRing public + + ring : Ring _ _ _ + ring = record { isRing = isRing } + + open Ring ring public + using + ( _≉_; _≤_; _>_; _≥_ + ; +-rawMagma; +-rawMonoid; +-rawGroup + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; *-rawMagma; *-rawMonoid + ; *-magma; *-semigroup; *-monoid + ) + +record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 9 _⁻¹ + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + _⁻¹ : AlmostOp₁ _≈_ 0# + + infixl 7 _/_ + _/_ : AlmostOp₂ _≈_ 0# + x / y≉0 = x * y≉0 ⁻¹ + + rawRing : RawRing c ℓ₁ ℓ₂ + rawRing = record + { _≈_ = _≈_ + ; _<_ = _<_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } + + open RawRing rawRing public + using + ( _≉_; _≤_; _>_; _≥_ + ; +-rawMagma; +-rawMonoid; +-rawGroup + ; *-rawMagma; *-rawMonoid + ) + + *-rawAlmostGroup : RawAlmostGroup c ℓ₁ + *-rawAlmostGroup = record + { _≈_ = _≈_ + ; _∙_ = _*_ + ; 0# = 0# + ; 1# = 1# + ; _⁻¹ = _⁻¹ + } + +record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 9 _⁻¹ + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + _⁻¹ : AlmostOp₁ _≈_ 0# + isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ + + open IsDivisionRing isDivisionRing public + + rawField : RawField c ℓ₁ ℓ₂ + rawField = record + { _≈_ = _≈_ + ; _<_ = _<_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; _⁻¹ = _⁻¹ + } + + ring : Ring c ℓ₁ ℓ₂ + ring = record { isRing = isRing } + + open Ring ring public + using + ( _≉_; _≤_; _>_; _≥_ + ; rawRing + ; +-rawMagma; +-rawMonoid; +-rawGroup + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; *-rawMagma; *-rawMonoid + ; *-magma; *-semigroup; *-monoid + ) + + *-almostGroup : AlmostGroup _ _ + *-almostGroup = record { isAlmostGroup = *-isAlmostGroup } + + open AlmostGroup *-almostGroup public + using () + renaming (rawAlmostGroup to *-rawAlmostGroup) + +record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 9 _⁻¹ + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + infix 4 _≈_ _<_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ + _<_ : Rel Carrier ℓ₂ + _+_ : Op₂ Carrier + _*_ : Op₂ Carrier + -_ : Op₁ Carrier + 0# : Carrier + 1# : Carrier + _⁻¹ : AlmostOp₁ _≈_ 0# + isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ + + open IsField isField public + + divisionRing : DivisionRing c ℓ₁ ℓ₂ + divisionRing = record { isDivisionRing = isDivisionRing } + + open DivisionRing divisionRing + using + ( _≉_; _≤_; _>_; _≥_ + ; +-rawMagma; +-rawMonoid; +-rawGroup + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup + ; *-magma; *-semigroup; *-monoid; *-almostGroup + ) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda new file mode 100644 index 0000000..9dc0043 --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda @@ -0,0 +1,250 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Some ordered algebraic structures (not packed up with sets, +-- operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary + +module Helium.Algebra.Ordered.StrictTotal.Structures + {a ℓ₁ ℓ₂} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ₁) -- The underlying equality + (_<_ : Rel A ℓ₂) -- The underlying order + where + +import Algebra.Consequences.Setoid as Consequences +open import Algebra.Core +open import Algebra.Definitions _≈_ +import Algebra.Structures _≈_ as Unordered +open import Data.Product using (_,_; proj₁; proj₂) +open import Helium.Algebra.Core +open import Helium.Algebra.Definitions _≈_ +open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup) +open import Helium.Algebra.Ordered.Definitions _<_ +open import Level using (_⊔_) + +record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ + ∙-cong : Congruent₂ ∙ + ∙-invariant : Invariant ∙ + + open IsStrictTotalOrder isStrictTotalOrder public + + strictTotalOrder : StrictTotalOrder _ _ _ + strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder } + + open module strictTotalOrder = StrictTotalOrder strictTotalOrder public + using (strictPartialOrder) + + ∙-congˡ : LeftCongruent ∙ + ∙-congˡ y≈z = ∙-cong Eq.refl y≈z + + ∙-congʳ : RightCongruent ∙ + ∙-congʳ y≈z = ∙-cong y≈z Eq.refl + + ∙-invariantˡ : LeftInvariant ∙ + ∙-invariantˡ = proj₁ ∙-invariant + + ∙-invariantʳ : RightInvariant ∙ + ∙-invariantʳ = proj₂ ∙-invariant + +record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isMagma : IsMagma ∙ + assoc : Associative ∙ + + open IsMagma isMagma public + +record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isSemigroup : IsSemigroup ∙ + identity : Identity ε ∙ + + open IsSemigroup isSemigroup public + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity + +record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isMonoid : IsMonoid _∙_ ε + inverse : Inverse ε _⁻¹ _∙_ + ⁻¹-cong : Congruent₁ _⁻¹ + + open IsMonoid isMonoid public + + infixl 6 _-_ + _-_ : Op₂ A + x - y = x ∙ (y ⁻¹) + + inverseˡ : LeftInverse ε _⁻¹ _∙_ + inverseˡ = proj₁ inverse + + inverseʳ : RightInverse ε _⁻¹ _∙_ + inverseʳ = proj₂ inverse + + uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹) + uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique + strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseʳ + + uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹) + uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique + strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ + +record IsAbelianGroup (∙ : Op₂ A) + (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isGroup : IsGroup ∙ ε ⁻¹ + comm : Commutative ∙ + + open IsGroup isGroup public + +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# * + + 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 + ; isGroup to +-isGroup + ) + + open Unordered.IsMonoid *-isMonoid public + using () + renaming + ( assoc to *-assoc + ; ∙-cong to *-cong + ; ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ; identity to *-identity + ; identityˡ to *-identityˡ + ; identityʳ to *-identityʳ + ; isMagma to *-isMagma + ; isSemigroup to *-isSemigroup + ) + + distribˡ : * DistributesOverˡ + + distribˡ = proj₁ distrib + + distribʳ : * DistributesOverʳ + + distribʳ = proj₂ distrib + + zeroˡ : LeftZero 0# * + zeroˡ = proj₁ zero + + zeroʳ : RightZero 0# * + zeroʳ = proj₂ zero + +record IsCommutativeRing + (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isRing : IsRing + * - 0# 1# + *-comm : Commutative * + + open IsRing isRing public + +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# _*_ + + 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 + ; 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 + ; preservesPositive = preservesPositive + } + + open IsRing isRing public + using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ) + +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 + } -- cgit v1.2.3