Raw modules bundles

CHANGELOG.md

@@ -33,9 +33,13 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
+
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Module.Bundles`, the bundles expose their raw counterparts.
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

src/Algebra/Module/Bundles.agda

@@ -28,6 +28,7 @@ module Algebra.Module.Bundles where
 open import Algebra.Bundles
 open import Algebra.Core
 open import Algebra.Definitions using (Involutive)
+open import Algebra.Module.Bundles.Raw
 open import Algebra.Module.Core
 open import Algebra.Module.Structures
 open import Algebra.Module.Definitions
@@ -62,10 +63,6 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isLeftSemimodule : IsLeftSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_
 
-  infix 4 _≉ᴹ_
-  _≉ᴹ_ : Rel Carrierᴹ _
-  a ≉ᴹ b = ¬ (a ≈ᴹ b)
-
   open IsLeftSemimodule isLeftSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -80,8 +77,17 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
     ; magma     to +ᴹ-magma
     ; rawMagma  to +ᴹ-rawMagma
     ; rawMonoid to +ᴹ-rawMonoid
+    ; _≉_ to _≉ᴹ_
     )
 
+  rawLeftSemimodule : RawLeftSemimodule Carrier m ℓm
+  rawLeftSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    }
+
 record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open Ring ring
 
@@ -106,14 +112,23 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ 
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
 
   open AbelianGroup +ᴹ-abelianGroup public
     using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
 
+  rawLeftModule : RawLeftModule Carrier m ℓm
+  rawLeftModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+
 ------------------------------------------------------------------------
 -- Right modules
 ------------------------------------------------------------------------
@@ -134,10 +149,6 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isRightSemimodule : IsRightSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ᵣ_
 
-  infix 4 _≉ᴹ_
-  _≉ᴹ_ : Rel Carrierᴹ _
-  a ≉ᴹ b = ¬ (a ≈ᴹ b)
-
   open IsRightSemimodule isRightSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -152,8 +163,17 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
     ; magma     to +ᴹ-magma
     ; rawMagma  to +ᴹ-rawMagma
     ; rawMonoid to +ᴹ-rawMonoid
+    ; _≉_ to _≉ᴹ_
     )
 
+  rawRightSemimodule : RawRightSemimodule Carrier m ℓm
+  rawRightSemimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
+
 record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open Ring ring
 
@@ -178,14 +198,23 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
 
   open RightSemimodule rightSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawRightSemimodule; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
 
   open AbelianGroup +ᴹ-abelianGroup public
     using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
 
+  rawRightModule : RawRightModule Carrier m ℓm
+  rawRightModule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
+
 ------------------------------------------------------------------------
 -- Bimodules
 ------------------------------------------------------------------------
@@ -220,7 +249,20 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma
-          ; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
+
+  open RightSemimodule rightSemimodule public
+    using ( rawRightSemimodule )
+
+  rawBisemimodule : RawBisemimodule R.Carrier S.Carrier m ℓm
+  rawBisemimodule = record
+    { Carrierᴹ = Carrierᴹ
+    ; _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    }
 
 record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
                 : Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
@@ -254,13 +296,26 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
   open LeftModule leftModule public
     using ( +ᴹ-abelianGroup; +ᴹ-commutativeMonoid; +ᴹ-group; +ᴹ-monoid
           ; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup
-          ; _≉ᴹ_)
+          ; rawLeftSemimodule; rawLeftModule; _≉ᴹ_)
+
+  open RightModule rightModule public
+    using ( rawRightSemimodule; rawRightModule )
 
   bisemimodule : Bisemimodule R.semiring S.semiring m ℓm
   bisemimodule = record { isBisemimodule = isBisemimodule }
 
   open Bisemimodule bisemimodule public
-    using (leftSemimodule; rightSemimodule)
+    using (leftSemimodule; rightSemimodule; rawBisemimodule)
+
+  rawBimodule : RawBimodule R.Carrier S.Carrier m ℓm
+  rawBimodule = record
+    { _≈ᴹ_ = _≈ᴹ_
+    ; _+ᴹ_ = _+ᴹ_
+    ; _*ₗ_ = _*ₗ_
+    ; _*ᵣ_ = _*ᵣ_
+    ; 0ᴹ = 0ᴹ
+    ; -ᴹ_ = -ᴹ_
+    }
 
 ------------------------------------------------------------------------
 -- Modules over commutative structures
@@ -296,7 +351,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
   open Bisemimodule bisemimodule public
     using ( leftSemimodule; rightSemimodule
           ; +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; rawRightSemimodule
+          ; rawBisemimodule; _≉ᴹ_
+          )
 
   open SetR ≈ᴹ-setoid
 
@@ -314,6 +371,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
     m *ᵣ (y * x)  ≈⟨ ≈ᴹ-sym (*ᵣ-assoc m y x) ⟩
     m *ᵣ y *ᵣ x   ∎
 
+  rawSemimodule : RawSemimodule Carrier m ℓm
+  rawSemimodule = rawBisemimodule
+
 record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
               : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
   open CommutativeRing commutativeRing
@@ -343,9 +403,13 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
     using ( leftModule; rightModule; leftSemimodule; rightSemimodule
           ; +ᴹ-abelianGroup; +ᴹ-group; +ᴹ-commutativeMonoid; +ᴹ-monoid
           ; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma
-          ; +ᴹ-rawGroup; _≉ᴹ_)
+          ; +ᴹ-rawGroup; rawLeftSemimodule; rawLeftModule; rawRightSemimodule
+          ; rawRightModule; rawBisemimodule; rawBimodule; _≉ᴹ_)
 
   semimodule : Semimodule commutativeSemiring m ℓm
   semimodule = record { isSemimodule = isSemimodule }
 
-  open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm)
+  open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm; rawSemimodule)
+
+  rawModule : RawModule Carrier m ℓm
+  rawModule = rawBimodule