Add new law to constructed modules

Taneb · Taneb · commit fe42b2c6dcbd · 2023-01-03T00:06:24.000+01:00
diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/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
diff --git a/src/Algebra/Module/Construct/TensorUnit.agda b/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

Original file line number	Diff line number	Diff line change
`@@ -97,6 +97,7 @@ semimodule M N = record`
`97`	`97`	`{ isSemimodule = record`
`98`	`98`	`{ isBisemimodule = Bisemimodule.isBisemimodule`
`99`	`99`	`(bisemimodule M.bisemimodule N.bisemimodule)`
	`100`	`+ ; ₗ-ᵣ-comm = λ x m → M.ₗ-ᵣ-comm x (proj₁ m) , N.ₗ-ᵣ-comm x (proj₂ m)`
`100`	`101`	`}`
`101`	`102`	`} where module M = Semimodule M; module N = Semimodule N`
`102`	`103`
`@@ -155,5 +156,6 @@ bimodule M N = record`
`155`	`156`	`⟨module⟩ M N = record`
`156`	`157`	`{ isModule = record`
`157`	`158`	`{ isBimodule = Bimodule.isBimodule (bimodule M.bimodule N.bimodule)`
	`159`	`+ ; ₗ-ᵣ-comm = λ x m → M.ₗ-ᵣ-comm x (proj₁ m) , N.ₗ-ᵣ-comm x (proj₂ m)`
`158`	`160`	`}`
`159`	`161`	`} where module M = Module M; module N = Module N`
Original file line number	Diff line number	Diff line change
`@@ -77,6 +77,7 @@ semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ`
`77`	`77`	`semimodule {R = commutativeSemiring} = record`
`78`	`78`	`{ isSemimodule = record`
`79`	`79`	`{ isBisemimodule = Bisemimodule.isBisemimodule bisemimodule`
	`80`	`+ ; ₗ-ᵣ-comm = λ x m → *-comm x m`
`80`	`81`	`}`
`81`	`82`	`} where open CommutativeSemiring commutativeSemiring`
`82`	`83`
`@@ -113,5 +114,6 @@ bimodule {R = ring} = record`
`113`	`114`	`⟨module⟩ {R = commutativeRing} = record`
`114`	`115`	`{ isModule = record`
`115`	`116`	`{ isBimodule = Bimodule.isBimodule bimodule`
	`117`	`+ ; ₗ-ᵣ-comm = λ x m → *-comm x m`
`116`	`118`	`}`
`117`	`119`	`} where open CommutativeRing commutativeRing`