From dfb81007b340e609c985e87768e3cb5b1941b1a9 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Mon, 16 Jan 2023 11:55:09 -0500 Subject: [PATCH 1/3] Direct products --- CHANGELOG.md | 5 ++ src/Algebra/Bundles.agda | 7 +++ src/Algebra/Construct/DirectProduct.agda | 63 ++++++++++++++++++++++++ src/Algebra/Structures.agda | 53 ++++++++++++++++---- 4 files changed, 119 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 51b000a7f8..09bcb163bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1585,6 +1585,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 4997e2596c..b239b59d05 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 (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 b7f3627fdd..ffbf4c3e81 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 1040ae1e65..6db33471f3 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -592,6 +592,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 @@ -681,12 +699,8 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ ; assoc = *-assoc } - open IsMagma *-isMagma public - using () - renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ) + open IsSemigroup *-isSemigroup public + using (∙-cong ; assoc) ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements @@ -696,7 +710,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# * @@ -726,6 +740,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 @@ -733,10 +759,19 @@ 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(identityˡ; identityʳ) record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field From 9b4ff1db2ee9ac492b6d79ea3f877dec934862b1 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Mon, 16 Jan 2023 12:26:49 -0500 Subject: [PATCH 2/3] minor fix --- src/Algebra/Structures.agda | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 6db33471f3..27b642b1d2 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -700,7 +700,11 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ } open IsSemigroup *-isSemigroup public - using (∙-cong ; assoc) + using () + renaming + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ) ------------------------------------------------------------------------ -- Structures with 2 binary operations, 1 unary operation & 2 elements @@ -771,7 +775,11 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a } open IsUnitalMagma *-isUnitalMagma public - using(identityˡ; identityʳ) + using () + renaming + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ) record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field From e3e4cd5fd9d2f60a0b2a41a0cb2ef1606aa3c9c8 Mon Sep 17 00:00:00 2001 From: Akshobhya K M Date: Tue, 17 Jan 2023 10:31:55 -0500 Subject: [PATCH 3/3] minor fix --- src/Algebra/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index b239b59d05..8b2c6e6c2b 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -896,7 +896,7 @@ record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where *-unitalMagma = record { isUnitalMagma = *-isUnitalMagma} open UnitalMagma *-unitalMagma public - using (identity) + using () renaming (magma to *-magma; identity to *-identity) record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_