Add commutative law to modules

Author: Taneb

src/Algebra/Module/Structures.agda

@@ -171,6 +171,7 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr)
                       : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x)
 
     open IsBisemimodule isBisemimodule public
 
@@ -285,8 +286,9 @@ module _ (commutativeRing : CommutativeRing r ℓr)
   record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x)
 
     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
       }