Skip to content

Commit aa12b7d

Browse files
Akshobhya1234Akshobhya1234
authored
Add IsUnitalMagma and IsQuasigroup algebraic structures (agda#1501)
1 parent caaea3a commit aa12b7d

File tree

3 files changed

+144
-34
lines changed

3 files changed

+144
-34
lines changed

‎CHANGELOG.md

+12-5
Original file line numberDiff line numberDiff line change
@@ -30,19 +30,26 @@ New modules
3030
Other minor additions
3131
---------------------
3232

33-
* In `Algebra.Bundles`, `Lattice` now provides
33+
* Added new definitions to `Algebra.Bundles`:
34+
```agda
35+
record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ))
36+
record Quasigroup c ℓ : Set (suc (c ⊔ ℓ))
37+
```
38+
and the existing record `Lattice` now provides
3439
```agda
3540
∨-commutativeSemigroup : CommutativeSemigroup c ℓ
3641
∧-commutativeSemigroup : CommutativeSemigroup c ℓ
3742
```
3843
and their corresponding algebraic subbundles.
3944

40-
* In `Algebra.Structures`, `IsLattice` now provides
45+
* Added new definitions to `Algebra.Structures`:
46+
```agda
47+
record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
48+
record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ)
49+
```
50+
and the existing record `IsLattice` now provides
4151
```
4252
∨-isCommutativeSemigroup : IsCommutativeSemigroup ∨
4353
∧-isCommutativeSemigroup : IsCommutativeSemigroup ∧
4454
```
4555
and their corresponding algebraic substructures.
46-
47-
Other minor additions
48-
---------------------

‎src/Algebra/Bundles.agda

+78-18
Original file line numberDiff line numberDiff line change
@@ -187,6 +187,25 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
187187
using (_≉_)
188188

189189

190+
record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
191+
infixl 7 _∙_
192+
infix 4 _≈_
193+
field
194+
Carrier : Set c
195+
_≈_ : Rel Carrier ℓ
196+
_∙_ : Op₂ Carrier
197+
ε : Carrier
198+
isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε
199+
200+
open IsUnitalMagma isUnitalMagma public
201+
202+
magma : Magma c ℓ
203+
magma = record { isMagma = isMagma }
204+
205+
open Magma magma public
206+
using (_≉_; rawMagma)
207+
208+
190209
record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
191210
infixl 7 _∙_
192211
infix 4 _≈_
@@ -208,6 +227,9 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
208227
rawMonoid : RawMonoid _ _
209228
rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
210229

230+
unitalMagma : UnitalMagma _ _
231+
unitalMagma = record { isUnitalMagma = isUnitalMagma }
232+
211233

212234
record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
213235
infixl 7 _∙_
@@ -225,7 +247,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
225247
monoid = record { isMonoid = isMonoid }
226248

227249
open Monoid monoid public
228-
using (_≉_; rawMagma; magma; semigroup; rawMonoid)
250+
using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid)
229251

230252
commutativeSemigroup : CommutativeSemigroup _ _
231253
commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
@@ -251,7 +273,8 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
251273

252274
open CommutativeMonoid commutativeMonoid public
253275
using
254-
( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup
276+
( _≉_; rawMagma; magma; unitalMagma; commutativeMagma
277+
; semigroup; commutativeSemigroup
255278
; rawMonoid; monoid
256279
)
257280

@@ -292,6 +315,27 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
292315
using (_≉_; rawMagma)
293316

294317

318+
record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
319+
infix 8 _⁻¹
320+
infixl 7 _∙_
321+
infix 4 _≈_
322+
field
323+
Carrier : Set c
324+
_≈_ : Rel Carrier ℓ
325+
_∙_ : Op₂ Carrier
326+
ε : Carrier
327+
_⁻¹ : Op₁ Carrier
328+
isQuasigroup : IsQuasigroup _≈_ _∙_ ε _⁻¹
329+
330+
open IsQuasigroup isQuasigroup public
331+
332+
magma : Magma _ _
333+
magma = record { isMagma = isMagma }
334+
335+
open Magma magma public
336+
using (_≉_; rawMagma)
337+
338+
295339
record Group c ℓ : Set (suc (c ⊔ ℓ)) where
296340
infix 8 _⁻¹
297341
infixl 7 _∙_
@@ -313,7 +357,13 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
313357
monoid = record { isMonoid = isMonoid }
314358

315359
open Monoid monoid public
316-
using (_≉_; rawMagma; magma; semigroup; rawMonoid)
360+
using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid)
361+
362+
quasigroup : Quasigroup c ℓ
363+
quasigroup = record
364+
{ isQuasigroup = isQuasigroup
365+
}
366+
317367

318368
record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
319369
infix 8 _⁻¹
@@ -332,8 +382,10 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
332382
group : Group _ _
333383
group = record { isGroup = isGroup }
334384

335-
open Group group public
336-
using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
385+
open Group group public using
386+
(_≉_; rawMagma; magma; semigroup
387+
; rawMonoid; monoid; rawGroup; quasigroup
388+
)
337389

338390
commutativeMonoid : CommutativeMonoid _ _
339391
commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
@@ -475,10 +527,11 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
475527

476528
open Monoid +-monoid public
477529
using (_≉_) renaming
478-
( rawMagma to +-rawMagma
479-
; magma to +-magma
480-
; semigroup to +-semigroup
481-
; rawMonoid to +-rawMonoid
530+
( rawMagma to +-rawMagma
531+
; magma to +-magma
532+
; semigroup to +-semigroup
533+
; unitalMagma to +-unitalMagma
534+
; rawMonoid to +-rawMonoid
482535
)
483536

484537
*-semigroup : Semigroup _ _
@@ -510,7 +563,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
510563

511564
open NearSemiring nearSemiring public
512565
using
513-
( _≉_; +-rawMagma; +-magma; +-semigroup
566+
( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup
514567
; +-rawMonoid; +-monoid
515568
; *-rawMagma; *-magma; *-semigroup
516569
; rawNearSemiring
@@ -548,7 +601,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
548601

549602
open SemiringWithoutOne semiringWithoutOne public
550603
using
551-
( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
604+
( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup
552605
; *-rawMagma; *-magma; *-semigroup
553606
; +-rawMonoid; +-monoid; +-commutativeMonoid
554607
; nearSemiring; rawNearSemiring
@@ -626,6 +679,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
626679
using (_≉_) renaming
627680
( rawMagma to +-rawMagma
628681
; magma to +-magma
682+
; unitalMagma to +-unitalMagma
629683
; commutativeMagma to +-commutativeMagma
630684
; semigroup to +-semigroup
631685
; commutativeSemigroup to +-commutativeSemigroup
@@ -669,7 +723,8 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
669723
open SemiringWithoutAnnihilatingZero
670724
semiringWithoutAnnihilatingZero public
671725
using
672-
( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
726+
( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
727+
; +-semigroup; +-commutativeSemigroup
673728
; *-rawMagma; *-magma; *-semigroup
674729
; +-rawMonoid; +-monoid; +-commutativeMonoid
675730
; *-rawMonoid; *-monoid
@@ -704,7 +759,8 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
704759

705760
open Semiring semiring public
706761
using
707-
( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
762+
( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
763+
; +-semigroup; +-commutativeSemigroup
708764
; *-rawMagma; *-magma; *-semigroup
709765
; +-rawMonoid; +-monoid; +-commutativeMonoid
710766
; *-rawMonoid; *-monoid
@@ -752,7 +808,8 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
752808

753809
open CommutativeSemiring commutativeSemiring public
754810
using
755-
( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
811+
( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
812+
; +-semigroup; +-commutativeSemigroup
756813
; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
757814
; +-rawMonoid; +-monoid; +-commutativeMonoid
758815
; *-rawMonoid; *-monoid; *-commutativeMonoid
@@ -808,6 +865,7 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
808865
; _⁻¹ = -_
809866
}
810867

868+
811869
record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
812870
infix 8 -_
813871
infixl 7 _*_
@@ -833,7 +891,8 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
833891

834892
open Semiring semiring public
835893
using
836-
( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
894+
( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
895+
; +-semigroup; +-commutativeSemigroup
837896
; *-rawMagma; *-magma; *-semigroup
838897
; +-rawMonoid; +-monoid ; +-commutativeMonoid
839898
; *-rawMonoid; *-monoid
@@ -842,7 +901,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
842901
)
843902

844903
open AbelianGroup +-abelianGroup public
845-
using () renaming (group to +-group)
904+
using () renaming (group to +-group; quasigroup to +-quasigroup)
846905

847906
rawRing : RawRing _ _
848907
rawRing = record
@@ -875,15 +934,16 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
875934
ring : Ring _ _
876935
ring = record { isRing = isRing }
877936

878-
open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup)
937+
open Ring ring public using (_≉_; rawRing; +-quasigroup; +-group; +-abelianGroup)
879938

880939
commutativeSemiring : CommutativeSemiring _ _
881940
commutativeSemiring =
882941
record { isCommutativeSemiring = isCommutativeSemiring }
883942

884943
open CommutativeSemiring commutativeSemiring public
885944
using
886-
( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
945+
( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
946+
; +-semigroup; +-commutativeSemigroup
887947
; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
888948
; +-rawMonoid; +-monoid; +-commutativeMonoid
889949
; *-rawMonoid; *-monoid; *-commutativeMonoid

‎src/Algebra/Structures.agda

+54-11
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,20 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
107107
-- Structures with 1 binary operation & 1 element
108108
------------------------------------------------------------------------
109109

110+
record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
111+
field
112+
isMagma : IsMagma ∙
113+
identity : Identity ε ∙
114+
115+
open IsMagma isMagma public
116+
117+
identityˡ : LeftIdentity ε ∙
118+
identityˡ = proj₁ identity
119+
120+
identityʳ : RightIdentity ε ∙
121+
identityʳ = proj₂ identity
122+
123+
110124
record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
111125
field
112126
isSemigroup : IsSemigroup ∙
@@ -120,6 +134,12 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
120134
identityʳ : RightIdentity ε ∙
121135
identityʳ = proj₂ identity
122136

137+
isUnitalMagma : IsUnitalMagma ∙ ε
138+
isUnitalMagma = record
139+
{ isMagma = isMagma
140+
; identity = identity
141+
}
142+
123143

124144
record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
125145
field
@@ -163,6 +183,20 @@ module IsBoundedLattice {∙ : Op₂ A}
163183
-- Structures with 1 binary operation, 1 unary operation & 1 element
164184
------------------------------------------------------------------------
165185

186+
record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
187+
field
188+
isMagma : IsMagma _∙_
189+
inverse : Inverse ε _⁻¹ _∙_
190+
191+
open IsMagma isMagma public
192+
193+
inverseˡ : LeftInverse ε _⁻¹ _∙_
194+
inverseˡ = proj₁ inverse
195+
196+
inverseʳ : RightInverse ε _⁻¹ _∙_
197+
inverseʳ = proj₂ inverse
198+
199+
166200
record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
167201
field
168202
isMonoid : IsMonoid _∙_ ε
@@ -189,6 +223,12 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w
189223
uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
190224
setoid ∙-cong assoc identity inverseˡ
191225

226+
isQuasigroup : IsQuasigroup _∙_ ε _⁻¹
227+
isQuasigroup = record
228+
{ isMagma = isMagma
229+
; inverse = inverse
230+
}
231+
192232

193233
record IsAbelianGroup (∙ : Op₂ A)
194234
(ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
@@ -277,15 +317,16 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
277317

278318
open IsMonoid +-isMonoid public
279319
renaming
280-
( assoc to +-assoc
281-
; ∙-cong to +-cong
282-
; ∙-congˡ to +-congˡ
283-
; ∙-congʳ to +-congʳ
284-
; identity to +-identity
285-
; identityˡ to +-identityˡ
286-
; identityʳ to +-identityʳ
287-
; isMagma to +-isMagma
288-
; isSemigroup to +-isSemigroup
320+
( assoc to +-assoc
321+
; ∙-cong to +-cong
322+
; ∙-congˡ to +-congˡ
323+
; ∙-congʳ to +-congʳ
324+
; identity to +-identity
325+
; identityˡ to +-identityˡ
326+
; identityʳ to +-identityʳ
327+
; isMagma to +-isMagma
328+
; isUnitalMagma to +-isUnitalMagma
329+
; isSemigroup to +-isSemigroup
289330
)
290331

291332
open IsSemigroup *-isSemigroup public
@@ -306,8 +347,7 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
306347
distrib : * DistributesOver +
307348
zero : Zero 0# *
308349

309-
open IsCommutativeMonoid +-isCommutativeMonoid public
310-
using ()
350+
open IsCommutativeMonoid +-isCommutativeMonoid public using ()
311351
renaming
312352
( comm to +-comm
313353
; isMonoid to +-isMonoid
@@ -382,6 +422,7 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
382422
; isMagma to +-isMagma
383423
; isSemigroup to +-isSemigroup
384424
; isMonoid to +-isMonoid
425+
; isUnitalMagma to +-isUnitalMagma
385426
; isCommutativeMagma to +-isCommutativeMagma
386427
; isCommutativeSemigroup to +-isCommutativeSemigroup
387428
)
@@ -490,9 +531,11 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
490531
; isMagma to +-isMagma
491532
; isSemigroup to +-isSemigroup
492533
; isMonoid to +-isMonoid
534+
; isUnitalMagma to +-isUnitalMagma
493535
; isCommutativeMagma to +-isCommutativeMagma
494536
; isCommutativeMonoid to +-isCommutativeMonoid
495537
; isCommutativeSemigroup to +-isCommutativeSemigroup
538+
; isQuasigroup to +-isQuasigroup
496539
; isGroup to +-isGroup
497540
)
498541

0 commit comments

Comments
 (0)