Add commutative law to modules

CHANGELOG.md

@@ -1782,6 +1782,11 @@ New modules
   Algebra.Module.Core
   ```
 
+* Definitions for module-like algebraic structures with left- and right- multiplication over the same scalars:
+  ```
+  Algebra.Module.Definitions.Bi.Simultaneous
+  ```
+
 * Constructive algebraic structures with apartness relations:
   ```
   Algebra.Apartness

src/Algebra/Module/Construct/DirectProduct.agda

@@ -97,6 +97,7 @@ semimodule M N = record
   { isSemimodule = record
     { isBisemimodule = Bisemimodule.isBisemimodule
       (bisemimodule M.bisemimodule N.bisemimodule)
+    ; *ₗ-*ᵣ-coincident = λ x m → M.*ₗ-*ᵣ-coincident x (proj₁ m) , N.*ₗ-*ᵣ-coincident x (proj₂ m)
     }
   } where module M = Semimodule M; module N = Semimodule N
 
@@ -155,5 +156,6 @@ bimodule M N = record
 ⟨module⟩ M N = record
   { isModule = record
     { isBimodule = Bimodule.isBimodule (bimodule M.bimodule N.bimodule)
+    ; *ₗ-*ᵣ-coincident = λ x m → M.*ₗ-*ᵣ-coincident x (proj₁ m) , N.*ₗ-*ᵣ-coincident x (proj₂ m)
     }
   } where module M = Module M; module N = Module N

src/Algebra/Module/Construct/TensorUnit.agda

@@ -77,6 +77,7 @@ semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ
 semimodule {R = commutativeSemiring} = record
   { isSemimodule = record
     { isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
+    ; *ₗ-*ᵣ-coincident = *-comm
     }
   } where open CommutativeSemiring commutativeSemiring
 
@@ -113,5 +114,6 @@ bimodule {R = ring} = record
 ⟨module⟩ {R = commutativeRing} = record
   { isModule = record
     { isBimodule = Bimodule.isBimodule bimodule
+    ; *ₗ-*ᵣ-coincident = *-comm
     }
   } where open CommutativeRing commutativeRing

src/Algebra/Module/Definitions.agda

@@ -12,7 +12,9 @@ module Algebra.Module.Definitions where
   import Algebra.Module.Definitions.Left as L
   import Algebra.Module.Definitions.Right as R
   import Algebra.Module.Definitions.Bi as B
+  import Algebra.Module.Definitions.Bi.Simultaneous as BS
 
   module LeftDefs = L
   module RightDefs = R
   module BiDefs = B
+  module SimultaneousBiDefs = BS

src/Algebra/Module/Definitions/Bi/Simultaneous.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties connecting left-scaling and right-scaling over the same scalars
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary
+
+module Algebra.Module.Definitions.Bi.Simultaneous
+  {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
+  where
+
+open import Algebra.Module.Core
+
+Coincident : Opₗ A B → Opᵣ A B → Set _
+Coincident _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x)

src/Algebra/Module/Structures.agda

@@ -166,14 +166,16 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr)
   open CommutativeSemiring commutativeSemiring renaming (Carrier to R)
 
   -- An R-semimodule is an R-R-bisemimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
-  -- though it may be that they do not coincide up to definitional
-  -- equality.
+  -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
+  -- may be that they do not coincide up to definitional equality.
+
+  open SimultaneousBiDefs R ≈ᴹ
 
   record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
                       : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
 
     open IsBisemimodule isBisemimodule public
 
@@ -282,15 +284,17 @@ module _ (commutativeRing : CommutativeRing r ℓr)
   open CommutativeRing commutativeRing renaming (Carrier to R)
 
   -- An R-module is an R-R-bimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
-  -- though it may be that they do not coincide up to definitional
-  -- equality.
+  -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
+  -- may be that they do not coincide up to definitional equality.
+
+  open SimultaneousBiDefs R ≈ᴹ
 
   record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
 
     open IsBimodule isBimodule public
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident }

src/Algebra/Module/Structures/Biased.agda

@@ -57,7 +57,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
+      }
 
   -- Similarly, a right semimodule over a commutative semiring
   -- is already a semimodule.
@@ -88,7 +91,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
+      }
 
 
 module _ (commutativeRing : CommutativeRing r ℓr) where
@@ -113,6 +119,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
       }
 
   -- Similarly, a right module over a commutative ring is already a module.
@@ -134,4 +141,5 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
       }