Direct products and minor fixes (#1909)

Author: Akshobhya1234

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`:

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)
+

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)

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,17 +746,42 @@ 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
     ; ∙-cong        = *-cong
     }
 
   *-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