Skip to content

Commit

Permalink
Raw modules bundles (#2263)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@Taneb @andreasabel
Taneb authored and andreasabel committed Jul 10, 2024
1 parent 6c44d20 commit 63b61c6
Show file tree
Hide file tree
Showing 6 changed files with 539 additions and 23 deletions.
40 changes: 40 additions & 0 deletions CHANGELOG.md
View file
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.Construct.DirectProduct`:
```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
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ᴹ
}

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ᴹ
; -ᴹ_ = -ᴹ_
}

------------------------------------------------------------------------
-- 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ᴹ
}

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ᴹ
; -ᴹ_ = -ᴹ_
}

------------------------------------------------------------------------
-- 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ᴹ
; -ᴹ_ = -ᴹ_
}

------------------------------------------------------------------------
-- 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

0 comments on commit 63b61c6

Please sign in to comment.