Skip to content

Commit a1f38c8

Browse files
TanebTaneb
authored
Raw modules bundles (#2263)
* Raw bundles for modules * Export raw bundles from module bundles * Update chnagelog * Remove redundant field * Reexport raw bundles, add raw bundles for zero * Add missing reexports, raw bundles for direct product * Raw bundles for tensor unit * Update changelog again * Remove unused open * Fix typo * Put a few more definitions in the fake record modules for RawModule and RawSemimodule
1 parent bde655f commit a1f38c8

File tree

6 files changed

+539
-23
lines changed

6 files changed

+539
-23
lines changed

‎CHANGELOG.md

+40
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,49 @@ Deprecated names
3333
New modules
3434
-----------
3535

36+
* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
37+
3638
Additions to existing modules
3739
-----------------------------
3840

41+
* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
42+
43+
* In `Algebra.Module.Construct.DirectProduct`:
44+
```agda
45+
rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
46+
rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
47+
rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
48+
rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
49+
rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
50+
rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
51+
rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
52+
rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
53+
```
54+
55+
* In `Algebra.Module.Construct.TensorUnit`:
56+
```agda
57+
rawLeftSemimodule : RawLeftSemimodule _ c ℓ
58+
rawLeftModule : RawLeftModule _ c ℓ
59+
rawRightSemimodule : RawRightSemimodule _ c ℓ
60+
rawRightModule : RawRightModule _ c ℓ
61+
rawBisemimodule : RawBisemimodule _ _ c ℓ
62+
rawBimodule : RawBimodule _ _ c ℓ
63+
rawSemimodule : RawSemimodule _ c ℓ
64+
rawModule : RawModule _ c ℓ
65+
```
66+
67+
* In `Algebra.Module.Construct.Zero`:
68+
```agda
69+
rawLeftSemimodule : RawLeftSemimodule R c ℓ
70+
rawLeftModule : RawLeftModule R c ℓ
71+
rawRightSemimodule : RawRightSemimodule R c ℓ
72+
rawRightModule : RawRightModule R c ℓ
73+
rawBisemimodule : RawBisemimodule R c ℓ
74+
rawBimodule : RawBimodule R c ℓ
75+
rawSemimodule : RawSemimodule R c ℓ
76+
rawModule : RawModule R c ℓ
77+
```
78+
3979
* In `Data.Fin.Properties`:
4080
```agda
4181
nonZeroIndex : Fin n → ℕ.NonZero n

‎src/Algebra/Module/Bundles.agda

+89-16
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ module Algebra.Module.Bundles where
2828
open import Algebra.Bundles
2929
open import Algebra.Core
3030
open import Algebra.Definitions using (Involutive)
31+
import Algebra.Module.Bundles.Raw as Raw
3132
open import Algebra.Module.Core
3233
open import Algebra.Module.Structures
3334
open import Algebra.Module.Definitions
@@ -42,6 +43,16 @@ private
4243
variable
4344
r ℓr s ℓs : Level
4445

46+
------------------------------------------------------------------------
47+
-- Re-export definitions of 'raw' bundles
48+
49+
open Raw public
50+
using ( RawLeftSemimodule; RawLeftModule
51+
; RawRightSemimodule; RawRightModule
52+
; RawBisemimodule; RawBimodule
53+
; RawSemimodule; RawModule
54+
)
55+
4556
------------------------------------------------------------------------
4657
-- Left modules
4758
------------------------------------------------------------------------
@@ -62,10 +73,6 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
6273
0ᴹ : Carrierᴹ
6374
isLeftSemimodule : IsLeftSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_
6475

65-
infix 4 _≉ᴹ_
66-
_≉ᴹ_ : Rel Carrierᴹ _
67-
a ≉ᴹ b = ¬ (a ≈ᴹ b)
68-
6976
open IsLeftSemimodule isLeftSemimodule public
7077

7178
+ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -80,8 +87,17 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
8087
; magma to +ᴹ-magma
8188
; rawMagma to +ᴹ-rawMagma
8289
; rawMonoid to +ᴹ-rawMonoid
90+
; _≉_ to _≉ᴹ_
8391
)
8492

93+
rawLeftSemimodule : RawLeftSemimodule Carrier m ℓm
94+
rawLeftSemimodule = record
95+
{ _≈ᴹ_ = _≈ᴹ_
96+
; _+ᴹ_ = _+ᴹ_
97+
; _*ₗ_ = _*ₗ_
98+
; 0ᴹ = 0ᴹ
99+
}
100+
85101
record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
86102
open Ring ring
87103

@@ -106,14 +122,23 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
106122

107123
open LeftSemimodule leftSemimodule public
108124
using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
109-
; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
125+
; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
110126

111127
+ᴹ-abelianGroup : AbelianGroup m ℓm
112128
+ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
113129

114130
open AbelianGroup +ᴹ-abelianGroup public
115131
using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
116132

133+
rawLeftModule : RawLeftModule Carrier m ℓm
134+
rawLeftModule = record
135+
{ _≈ᴹ_ = _≈ᴹ_
136+
; _+ᴹ_ = _+ᴹ_
137+
; _*ₗ_ = _*ₗ_
138+
; 0ᴹ = 0ᴹ
139+
; -ᴹ_ = -ᴹ_
140+
}
141+
117142
------------------------------------------------------------------------
118143
-- Right modules
119144
------------------------------------------------------------------------
@@ -134,10 +159,6 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
134159
0ᴹ : Carrierᴹ
135160
isRightSemimodule : IsRightSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ᵣ_
136161

137-
infix 4 _≉ᴹ_
138-
_≉ᴹ_ : Rel Carrierᴹ _
139-
a ≉ᴹ b = ¬ (a ≈ᴹ b)
140-
141162
open IsRightSemimodule isRightSemimodule public
142163

143164
+ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -152,8 +173,17 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
152173
; magma to +ᴹ-magma
153174
; rawMagma to +ᴹ-rawMagma
154175
; rawMonoid to +ᴹ-rawMonoid
176+
; _≉_ to _≉ᴹ_
155177
)
156178

179+
rawRightSemimodule : RawRightSemimodule Carrier m ℓm
180+
rawRightSemimodule = record
181+
{ _≈ᴹ_ = _≈ᴹ_
182+
; _+ᴹ_ = _+ᴹ_
183+
; _*ᵣ_ = _*ᵣ_
184+
; 0ᴹ = 0ᴹ
185+
}
186+
157187
record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
158188
open Ring ring
159189

@@ -178,14 +208,23 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
178208

179209
open RightSemimodule rightSemimodule public
180210
using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
181-
; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
211+
; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawRightSemimodule; _≉ᴹ_)
182212

183213
+ᴹ-abelianGroup : AbelianGroup m ℓm
184214
+ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
185215

186216
open AbelianGroup +ᴹ-abelianGroup public
187217
using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup)
188218

219+
rawRightModule : RawRightModule Carrier m ℓm
220+
rawRightModule = record
221+
{ _≈ᴹ_ = _≈ᴹ_
222+
; _+ᴹ_ = _+ᴹ_
223+
; _*ᵣ_ = _*ᵣ_
224+
; 0ᴹ = 0ᴹ
225+
; -ᴹ_ = -ᴹ_
226+
}
227+
189228
------------------------------------------------------------------------
190229
-- Bimodules
191230
------------------------------------------------------------------------
@@ -220,7 +259,19 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs
220259

221260
open LeftSemimodule leftSemimodule public
222261
using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma
223-
; +ᴹ-rawMonoid; _≉ᴹ_)
262+
; +ᴹ-rawMonoid; rawLeftSemimodule; _≉ᴹ_)
263+
264+
open RightSemimodule rightSemimodule public
265+
using ( rawRightSemimodule )
266+
267+
rawBisemimodule : RawBisemimodule R.Carrier S.Carrier m ℓm
268+
rawBisemimodule = record
269+
{ _≈ᴹ_ = _≈ᴹ_
270+
; _+ᴹ_ = _+ᴹ_
271+
; _*ₗ_ = _*ₗ_
272+
; _*ᵣ_ = _*ᵣ_
273+
; 0ᴹ = 0ᴹ
274+
}
224275

225276
record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
226277
: Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
@@ -254,13 +305,26 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
254305
open LeftModule leftModule public
255306
using ( +ᴹ-abelianGroup; +ᴹ-commutativeMonoid; +ᴹ-group; +ᴹ-monoid
256307
; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup
257-
; _≉ᴹ_)
308+
; rawLeftSemimodule; rawLeftModule; _≉ᴹ_)
309+
310+
open RightModule rightModule public
311+
using ( rawRightSemimodule; rawRightModule )
258312

259313
bisemimodule : Bisemimodule R.semiring S.semiring m ℓm
260314
bisemimodule = record { isBisemimodule = isBisemimodule }
261315

262316
open Bisemimodule bisemimodule public
263-
using (leftSemimodule; rightSemimodule)
317+
using (leftSemimodule; rightSemimodule; rawBisemimodule)
318+
319+
rawBimodule : RawBimodule R.Carrier S.Carrier m ℓm
320+
rawBimodule = record
321+
{ _≈ᴹ_ = _≈ᴹ_
322+
; _+ᴹ_ = _+ᴹ_
323+
; _*ₗ_ = _*ₗ_
324+
; _*ᵣ_ = _*ᵣ_
325+
; 0ᴹ = 0ᴹ
326+
; -ᴹ_ = -ᴹ_
327+
}
264328

265329
------------------------------------------------------------------------
266330
-- Modules over commutative structures
@@ -296,7 +360,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
296360
open Bisemimodule bisemimodule public
297361
using ( leftSemimodule; rightSemimodule
298362
; +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
299-
; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
363+
; +ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; rawRightSemimodule
364+
; rawBisemimodule; _≉ᴹ_
365+
)
300366

301367
open SetR ≈ᴹ-setoid
302368

@@ -314,6 +380,9 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
314380
m *ᵣ (y * x) ≈⟨ ≈ᴹ-sym (*ᵣ-assoc m y x) ⟩
315381
m *ᵣ y *ᵣ x ∎
316382

383+
rawSemimodule : RawSemimodule Carrier m ℓm
384+
rawSemimodule = rawBisemimodule
385+
317386
record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
318387
: Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
319388
open CommutativeRing commutativeRing
@@ -343,9 +412,13 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
343412
using ( leftModule; rightModule; leftSemimodule; rightSemimodule
344413
; +ᴹ-abelianGroup; +ᴹ-group; +ᴹ-commutativeMonoid; +ᴹ-monoid
345414
; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma
346-
; +ᴹ-rawGroup; _≉ᴹ_)
415+
; +ᴹ-rawGroup; rawLeftSemimodule; rawLeftModule; rawRightSemimodule
416+
; rawRightModule; rawBisemimodule; rawBimodule; _≉ᴹ_)
347417

348418
semimodule : Semimodule commutativeSemiring m ℓm
349419
semimodule = record { isSemimodule = isSemimodule }
350420

351-
open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm)
421+
open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm; rawSemimodule)
422+
423+
rawModule : RawModule Carrier m ℓm
424+
rawModule = rawBimodule

0 commit comments

Comments
 (0)