diff --git a/CHANGELOG.md b/CHANGELOG.md index 1e9e9dd82c..5121e27af9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1888,6 +1888,11 @@ Other minor changes rightBolLoop : RightBolLoop a ℓ₁ → RightBolLoop b ℓ₂ → RightBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) middleBolLoop : MiddleBolLoop a ℓ₁ → MiddleBolLoop b ℓ₂ → MiddleBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + ringWithoutOne : RingWithoutOne a ℓ₁ → RingWithoutOne b ℓ₂ → RingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + nonAssociativeRing : NonAssociativeRing a ℓ₁ → NonAssociativeRing b ℓ₂ → NonAssociativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + quasiring : Quasiring a ℓ₁ → Quasiring b ℓ₂ → Quasiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + nearring : Nearring a ℓ₁ → Nearring b ℓ₂ → Nearring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index f20cf1ad03..5bc2d5a1d0 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -892,6 +892,12 @@ record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) + *-unitalMagma : UnitalMagma _ _ + *-unitalMagma = record { isUnitalMagma = *-isUnitalMagma} + + open UnitalMagma *-unitalMagma public + using () renaming (magma to *-magma; identity to *-identity) + record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ @@ -1158,3 +1164,4 @@ record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where open Loop loop public using (quasigroup) + diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index 5f7b042017..ef9f377d29 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/src/Algebra/Construct/DirectProduct.agda @@ -61,6 +61,16 @@ rawSemiring R S = record ; 1# = R.1# , S.1# } where module R = RawSemiring R; module S = RawSemiring S +rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +rawRingWithoutOne R S = record + { Carrier = R.Carrier × S.Carrier + ; _≈_ = Pointwise R._≈_ S._≈_ + ; _+_ = zip R._+_ S._+_ + ; _*_ = zip R._*_ S._*_ + ; -_ = map R.-_ S.-_ + ; 0# = R.0# , S.0# + } where module R = RawRingWithoutOne R; module S = RawRingWithoutOne S + rawRing : RawRing a ℓ₁ → RawRing b ℓ₂ → RawRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) rawRing R S = record { Carrier = R.Carrier × S.Carrier @@ -317,6 +327,59 @@ kleeneAlgebra K L = record } } where module K = KleeneAlgebra K; module L = KleeneAlgebra L +ringWithoutOne : RingWithoutOne a ℓ₁ → RingWithoutOne b ℓ₂ → RingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +ringWithoutOne R S = record + { isRingWithoutOne = record + { +-isAbelianGroup = AbelianGroup.isAbelianGroup ((abelianGroup R.+-abelianGroup S.+-abelianGroup)) + ; *-cong = Semigroup.∙-cong (semigroup R.*-semigroup S.*-semigroup) + ; *-assoc = Semigroup.assoc (semigroup R.*-semigroup S.*-semigroup) + ; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z) + , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z) + ; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y) + , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y) + } + + } where module R = RingWithoutOne R; module S = RingWithoutOne S + +nonAssociativeRing : NonAssociativeRing a ℓ₁ → NonAssociativeRing b ℓ₂ → NonAssociativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +nonAssociativeRing R S = record + { isNonAssociativeRing = record + { +-isAbelianGroup = AbelianGroup.isAbelianGroup ((abelianGroup R.+-abelianGroup S.+-abelianGroup)) + ; *-cong = UnitalMagma.∙-cong (unitalMagma R.*-unitalMagma S.*-unitalMagma) + ; *-identity = UnitalMagma.identity (unitalMagma R.*-unitalMagma S.*-unitalMagma) + ; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z) + , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z) + ; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y) + , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y) + } + + } where module R = NonAssociativeRing R; module S = NonAssociativeRing S + +quasiring : Quasiring a ℓ₁ → Quasiring b ℓ₂ → Quasiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +quasiring R S = record + { isQuasiring = record + { +-isMonoid = Monoid.isMonoid ((monoid R.+-monoid S.+-monoid)) + ; *-cong = Monoid.∙-cong (monoid R.*-monoid S.*-monoid) + ; *-assoc = Monoid.assoc (monoid R.*-monoid S.*-monoid) + ; *-identity = Monoid.identity ((monoid R.*-monoid S.*-monoid)) + ; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z) + , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z) + ; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y) + , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y) + } + + } where module R = Quasiring R; module S = Quasiring S + +nearring : Nearring a ℓ₁ → Nearring b ℓ₂ → Nearring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) +nearring R S = record + { isNearring = record + { isQuasiring = Quasiring.isQuasiring (quasiring R.quasiring S.quasiring) + ; +-inverse = (λ x → (R.+-inverseˡ , S.+-inverseˡ) <*> x) + , (λ x → (R.+-inverseʳ , S.+-inverseʳ) <*> x) + ; ⁻¹-cong = map R.⁻¹-cong S.⁻¹-cong + } + } where module R = Nearring R; module S = Nearring S + ring : Ring a ℓ₁ → Ring b ℓ₂ → Ring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ring R S = record { -_ = uncurry (λ x y → R.-_ x , S.-_ y) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 4f9fc7fcb3..e38bbe7ba9 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -594,6 +594,24 @@ record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; 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 + + identityˡ : LeftIdentity 1# * + identityˡ = proj₁ *-identity + + identityʳ : RightIdentity 1# * + identityʳ = proj₂ *-identity + *-isMagma : IsMagma * *-isMagma = record { isEquivalence = isEquivalence @@ -683,11 +701,11 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ ; assoc = *-assoc } - open IsMagma *-isMagma public + open IsSemigroup *-isSemigroup public using () renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ ) ------------------------------------------------------------------------ @@ -698,7 +716,7 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a field +-isAbelianGroup : IsAbelianGroup + 0# -_ *-cong : Congruent₂ * - identity : Identity 1# * + *-identity : Identity 1# * distrib : * DistributesOver + zero : Zero 0# * @@ -728,6 +746,18 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ; isGroup to +-isGroup ) + zeroˡ : LeftZero 0# * + zeroˡ = proj₁ zero + + zeroʳ : RightZero 0# * + zeroʳ = proj₂ zero + + distribˡ : * DistributesOverˡ + + distribˡ = proj₁ distrib + + distribʳ : * DistributesOverʳ + + distribʳ = proj₂ distrib + *-isMagma : IsMagma * *-isMagma = record { isEquivalence = isEquivalence @@ -735,10 +765,23 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a } *-identityˡ : LeftIdentity 1# * - *-identityˡ = proj₁ identity + *-identityˡ = proj₁ *-identity *-identityʳ : RightIdentity 1# * - *-identityʳ = proj₂ identity + *-identityʳ = proj₂ *-identity + + *-isUnitalMagma : IsUnitalMagma * 1# + *-isUnitalMagma = record + { isMagma = *-isMagma + ; identity = *-identity + } + + open IsUnitalMagma *-isUnitalMagma public + using () + renaming + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ) record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field