Add commutative law to modules

CHANGELOG.md

@@ -782,6 +782,10 @@ Non-backwards compatible changes
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
 
+* `IsSemimodule` and `IsModule` now contain an extra law to enforce that left- and right- multiplication coincide (issue #1888):
+  ```
+  *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ
+  ```
 
 Major improvements
 ------------------
@@ -1347,6 +1351,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)
+    ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm 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)
+    ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm 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
+    ; *ₗ-*ᵣ-comm = λ x m → *-comm x m
     }
   } where open CommutativeSemiring commutativeSemiring
 
@@ -113,5 +114,6 @@ bimodule {R = ring} = record
 ⟨module⟩ {R = commutativeRing} = record
   { isModule = record
     { isBimodule = Bimodule.isBimodule bimodule
+    ; *ₗ-*ᵣ-comm = λ x m → *-comm x m
     }
   } where open CommutativeRing commutativeRing

src/Algebra/Module/Definitions.agda

@@ -14,7 +14,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
+
+Commutative : Opₗ A B → Opᵣ A B → Set _
+Commutative _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x)

src/Algebra/Module/Structures.agda

@@ -164,13 +164,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
+  -- 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ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ
 
     open IsBisemimodule isBisemimodule public
 
@@ -279,14 +282,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
+  -- 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ᴹ -ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ
 
     open IsBimodule isBimodule public
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-comm = *ₗ-*ᵣ-comm }

src/Algebra/Module/Structures/Biased.agda

@@ -55,7 +55,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl
+      }
 
   -- Similarly, a right semimodule over a commutative semiring
   -- is already a semimodule.
@@ -86,7 +89,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl
+      }
 
 
 module _ (commutativeRing : CommutativeRing r ℓr) where
@@ -111,6 +117,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl
       }
 
   -- Similarly, a right module over a commutative ring is already a module.
@@ -132,4 +139,5 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl
       }