Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Raw modules bundles #2263

Merged
merged 11 commits into from
Jan 27, 2024
Merged

Raw modules bundles #2263

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
d89c21f
Raw bundles for modules
Taneb Jan 23, 2024
8c0374d
Export raw bundles from module bundles
Taneb Jan 23, 2024
59eccc6
Update chnagelog
Taneb Jan 23, 2024
52a870c
Remove redundant field
Taneb Jan 24, 2024
78805fb
Reexport raw bundles, add raw bundles for zero
Taneb Jan 24, 2024
941ff33
Add missing reexports, raw bundles for direct product
Taneb Jan 24, 2024
454833a
Raw bundles for tensor unit
Taneb Jan 24, 2024
7f35fc6
Update changelog again
Taneb Jan 24, 2024
869223d
Remove unused open
Taneb Jan 24, 2024
5ef4919
Fix typo
Taneb Jan 24, 2024
14b77d7
Put a few more definitions in the fake record modules for RawModule a…
Taneb Jan 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,49 @@ Deprecated names
New modules
-----------

* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures

Additions to existing modules
-----------------------------

* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.

* In `Algebra.Module.Cosntruct.DirectProduct`:
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved
```agda
rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
```

* In `Algebra.Module.Construct.TensorUnit`:
```agda
rawLeftSemimodule : RawLeftSemimodule _ c ℓ
rawLeftModule : RawLeftModule _ c ℓ
rawRightSemimodule : RawRightSemimodule _ c ℓ
rawRightModule : RawRightModule _ c ℓ
rawBisemimodule : RawBisemimodule _ _ c ℓ
rawBimodule : RawBimodule _ _ c ℓ
rawSemimodule : RawSemimodule _ c ℓ
rawModule : RawModule _ c ℓ
```

* In `Algebra.Module.Construct.Zero`:
```agda
rawLeftSemimodule : RawLeftSemimodule R c ℓ
rawLeftModule : RawLeftModule R c ℓ
rawRightSemimodule : RawRightSemimodule R c ℓ
rawRightModule : RawRightModule R c ℓ
rawBisemimodule : RawBisemimodule R c ℓ
rawBimodule : RawBimodule R c ℓ
rawSemimodule : RawSemimodule R c ℓ
rawModule : RawModule R c ℓ
```

* In `Data.Fin.Properties`:
```agda
nonZeroIndex : Fin n → ℕ.NonZero n
Expand Down
105 changes: 89 additions & 16 deletions src/Algebra/Module/Bundles.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ module Algebra.Module.Bundles where
open import Algebra.Bundles
open import Algebra.Core
open import Algebra.Definitions using (Involutive)
import Algebra.Module.Bundles.Raw as Raw
open import Algebra.Module.Core
open import Algebra.Module.Structures
open import Algebra.Module.Definitions
Expand All @@ -42,6 +43,16 @@ private
variable
r ℓr s ℓs : Level

------------------------------------------------------------------------
-- Re-export definitions of 'raw' bundles

open Raw public
using ( RawLeftSemimodule; RawLeftModule
; RawRightSemimodule; RawRightModule
; RawBisemimodule; RawBimodule
; RawSemimodule; RawModule
)

------------------------------------------------------------------------
-- Left modules
------------------------------------------------------------------------
Expand All @@ -62,10 +73,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
Expand All @@ -80,8 +87,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ᴹ
}
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved

record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
open Ring ring

Expand All @@ -106,14 +122,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ᴹ
; -ᴹ_ = -ᴹ_
}
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved

------------------------------------------------------------------------
-- Right modules
------------------------------------------------------------------------
Expand All @@ -134,10 +159,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
Expand All @@ -152,8 +173,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ᴹ
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved
}

record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
open Ring ring

Expand All @@ -178,14 +208,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ᴹ
; -ᴹ_ = -ᴹ_
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved
}

------------------------------------------------------------------------
-- Bimodules
------------------------------------------------------------------------
Expand Down Expand Up @@ -220,7 +259,19 @@ 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
{ _≈ᴹ_ = _≈ᴹ_
; _+ᴹ_ = _+ᴹ_
; _*ₗ_ = _*ₗ_
; _*ᵣ_ = _*ᵣ_
; 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
Expand Down Expand Up @@ -254,13 +305,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ᴹ
; -ᴹ_ = -ᴹ_
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved
}

------------------------------------------------------------------------
-- Modules over commutative structures
Expand Down Expand Up @@ -296,7 +360,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

Expand All @@ -314,6 +380,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
Expand Down Expand Up @@ -343,9 +412,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
Loading
Loading