diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b82b67ed7..5ca9bbde71 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,19 +30,26 @@ New modules Other minor additions --------------------- -* In `Algebra.Bundles`, `Lattice` now provides +* Added new definitions to `Algebra.Bundles`: + ```agda + record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) + record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) + ``` + and the existing record `Lattice` now provides ```agda ∨-commutativeSemigroup : CommutativeSemigroup c ℓ ∧-commutativeSemigroup : CommutativeSemigroup c ℓ ``` and their corresponding algebraic subbundles. -* In `Algebra.Structures`, `IsLattice` now provides +* Added new definitions to `Algebra.Structures`: + ```agda + record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) + ``` + and the existing record `IsLattice` now provides ``` ∨-isCommutativeSemigroup : IsCommutativeSemigroup ∨ ∧-isCommutativeSemigroup : IsCommutativeSemigroup ∧ ``` and their corresponding algebraic substructures. - -Other minor additions ---------------------- diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index dff225a82d..99d9bb48e0 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -187,6 +187,25 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where using (_≉_) +record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε + + open IsUnitalMagma isUnitalMagma public + + magma : Magma c ℓ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; rawMagma) + + record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -208,6 +227,9 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where rawMonoid : RawMonoid _ _ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε} + unitalMagma : UnitalMagma _ _ + unitalMagma = record { isUnitalMagma = isUnitalMagma } + record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ @@ -225,7 +247,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where monoid = record { isMonoid = isMonoid } open Monoid monoid public - using (_≉_; rawMagma; magma; semigroup; rawMonoid) + using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup } @@ -251,7 +273,8 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeMonoid commutativeMonoid public using - ( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup + ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma + ; semigroup; commutativeSemigroup ; rawMonoid; monoid ) @@ -292,6 +315,27 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where using (_≉_; rawMagma) +record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 _⁻¹ + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + isQuasigroup : IsQuasigroup _≈_ _∙_ ε _⁻¹ + + open IsQuasigroup isQuasigroup public + + magma : Magma _ _ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; rawMagma) + + record Group c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -313,7 +357,13 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where monoid = record { isMonoid = isMonoid } open Monoid monoid public - using (_≉_; rawMagma; magma; semigroup; rawMonoid) + using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) + + quasigroup : Quasigroup c ℓ + quasigroup = record + { isQuasigroup = isQuasigroup + } + record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ @@ -332,8 +382,10 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where group : Group _ _ group = record { isGroup = isGroup } - open Group group public - using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup) + open Group group public using + (_≉_; rawMagma; magma; semigroup + ; rawMonoid; monoid; rawGroup; quasigroup + ) commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } @@ -475,10 +527,11 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open Monoid +-monoid public using (_≉_) renaming - ( rawMagma to +-rawMagma - ; magma to +-magma - ; semigroup to +-semigroup - ; rawMonoid to +-rawMonoid + ( rawMagma to +-rawMagma + ; magma to +-magma + ; semigroup to +-semigroup + ; unitalMagma to +-unitalMagma + ; rawMonoid to +-rawMonoid ) *-semigroup : Semigroup _ _ @@ -510,7 +563,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open NearSemiring nearSemiring public using - ( _≉_; +-rawMagma; +-magma; +-semigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup ; +-rawMonoid; +-monoid ; *-rawMagma; *-magma; *-semigroup ; rawNearSemiring @@ -548,7 +601,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open SemiringWithoutOne semiringWithoutOne public using - ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; nearSemiring; rawNearSemiring @@ -626,6 +679,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where using (_≉_) renaming ( rawMagma to +-rawMagma ; magma to +-magma + ; unitalMagma to +-unitalMagma ; commutativeMagma to +-commutativeMagma ; semigroup to +-semigroup ; commutativeSemigroup to +-commutativeSemigroup @@ -669,7 +723,8 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -704,7 +759,8 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open Semiring semiring public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -752,7 +808,8 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeSemiring commutativeSemiring public using - ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid @@ -808,6 +865,7 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where ; _⁻¹ = -_ } + record Ring c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ @@ -833,7 +891,8 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where open Semiring semiring public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid ; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -842,7 +901,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where ) open AbelianGroup +-abelianGroup public - using () renaming (group to +-group) + using () renaming (group to +-group; quasigroup to +-quasigroup) rawRing : RawRing _ _ rawRing = record @@ -875,7 +934,7 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where ring : Ring _ _ ring = record { isRing = isRing } - open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup) + open Ring ring public using (_≉_; rawRing; +-quasigroup; +-group; +-abelianGroup) commutativeSemiring : CommutativeSemiring _ _ commutativeSemiring = @@ -883,7 +942,8 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeSemiring commutativeSemiring public using - ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index e5e2f3313c..62243f9c7d 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -107,6 +107,20 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where -- Structures with 1 binary operation & 1 element ------------------------------------------------------------------------ +record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma ∙ + identity : Identity ε ∙ + + open IsMagma isMagma public + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity + + record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isSemigroup : IsSemigroup ∙ @@ -120,6 +134,12 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity + isUnitalMagma : IsUnitalMagma ∙ ε + isUnitalMagma = record + { isMagma = isMagma + ; identity = identity + } + record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field @@ -163,6 +183,20 @@ module IsBoundedLattice {∙ : Op₂ A} -- Structures with 1 binary operation, 1 unary operation & 1 element ------------------------------------------------------------------------ +record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma _∙_ + inverse : Inverse ε _⁻¹ _∙_ + + open IsMagma isMagma public + + inverseˡ : LeftInverse ε _⁻¹ _∙_ + inverseˡ = proj₁ inverse + + inverseʳ : RightInverse ε _⁻¹ _∙_ + inverseʳ = proj₂ inverse + + record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field isMonoid : IsMonoid _∙_ ε @@ -189,6 +223,12 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique setoid ∙-cong assoc identity inverseˡ + isQuasigroup : IsQuasigroup _∙_ ε _⁻¹ + isQuasigroup = record + { isMagma = isMagma + ; inverse = inverse + } + record IsAbelianGroup (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where @@ -277,15 +317,16 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where open IsMonoid +-isMonoid public 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 + ( assoc to +-assoc + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; ∙-congʳ to +-congʳ + ; identity to +-identity + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; isMagma to +-isMagma + ; isUnitalMagma to +-isUnitalMagma + ; isSemigroup to +-isSemigroup ) open IsSemigroup *-isSemigroup public @@ -306,8 +347,7 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where distrib : * DistributesOver + zero : Zero 0# * - open IsCommutativeMonoid +-isCommutativeMonoid public - using () + open IsCommutativeMonoid +-isCommutativeMonoid public using () renaming ( comm to +-comm ; isMonoid to +-isMonoid @@ -382,6 +422,7 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A) ; isMagma to +-isMagma ; isSemigroup to +-isSemigroup ; isMonoid to +-isMonoid + ; isUnitalMagma to +-isUnitalMagma ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeSemigroup to +-isCommutativeSemigroup ) @@ -490,9 +531,11 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; isMagma to +-isMagma ; isSemigroup to +-isSemigroup ; isMonoid to +-isMonoid + ; isUnitalMagma to +-isUnitalMagma ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeMonoid to +-isCommutativeMonoid ; isCommutativeSemigroup to +-isCommutativeSemigroup + ; isQuasigroup to +-isQuasigroup ; isGroup to +-isGroup )