From 63b61c6c590dcc1b00a934ce4e9724b305ad6f9d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 27 Jan 2024 19:25:55 +0100 Subject: [PATCH] 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 --- CHANGELOG.md | 40 +++ src/Algebra/Module/Bundles.agda | 105 ++++++-- src/Algebra/Module/Bundles/Raw.agda | 251 ++++++++++++++++++ .../Module/Construct/DirectProduct.agda | 79 +++++- src/Algebra/Module/Construct/TensorUnit.agda | 56 ++++ src/Algebra/Module/Construct/Zero.agda | 31 ++- 6 files changed, 539 insertions(+), 23 deletions(-) create mode 100644 src/Algebra/Module/Bundles/Raw.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index c690740a1e..97eb05989b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index f36e5bccd0..56b01fcf97 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/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) +import Algebra.Module.Bundles.Raw as Raw open import Algebra.Module.Core open import Algebra.Module.Structures open import Algebra.Module.Definitions @@ -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 ------------------------------------------------------------------------ @@ -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 @@ -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 @@ -106,7 +122,7 @@ 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 } @@ -114,6 +130,15 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ 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 +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 @@ -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 @@ -178,7 +208,7 @@ 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 } @@ -186,6 +216,15 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ open AbelianGroup +ᴹ-abelianGroup public using () renaming (group to +ᴹ-group; rawGroup to +ᴹ-rawGroup) + rawRightModule : RawRightModule Carrier m ℓm + rawRightModule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ᵣ_ = _*ᵣ_ + ; 0ᴹ = 0ᴹ + ; -ᴹ_ = -ᴹ_ + } + ------------------------------------------------------------------------ -- Bimodules ------------------------------------------------------------------------ @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda new file mode 100644 index 0000000000..b9cc108915 --- /dev/null +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -0,0 +1,251 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of 'raw' bundles for module-like algebraic structures +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Module.Bundles.Raw where + +open import Algebra.Bundles.Raw +open import Algebra.Core +open import Algebra.Module.Core +open import Level +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Binary.Core using (Rel) + +private + variable + r ℓr s ℓs : Level + +------------------------------------------------------------------------ +-- Raw left modules +------------------------------------------------------------------------ + +record RawLeftSemimodule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where + infixr 7 _*ₗ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ₗ_ : Opₗ R Carrierᴹ + 0ᴹ : Carrierᴹ + + +ᴹ-rawMonoid : RawMonoid m ℓm + +ᴹ-rawMonoid = record + { _≈_ = _≈ᴹ_ + ; _∙_ = _+ᴹ_ + ; ε = 0ᴹ + } + + open RawMonoid +ᴹ-rawMonoid public + using () + renaming (rawMagma to +ᴹ-rawMagma; _≉_ to _≉ᴹ_) + +record RawLeftModule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where + infix 8 -ᴹ_ + infixr 7 _*ₗ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ₗ_ : Opₗ R Carrierᴹ + 0ᴹ : Carrierᴹ + -ᴹ_ : Op₁ Carrierᴹ + + rawLeftSemimodule : RawLeftSemimodule R m ℓm + rawLeftSemimodule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ₗ_ = _*ₗ_ + ; 0ᴹ = 0ᴹ + } + + open RawLeftSemimodule rawLeftSemimodule public + using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_) + + +ᴹ-rawGroup : RawGroup m ℓm + +ᴹ-rawGroup = record + { _≈_ = _≈ᴹ_ + ; _∙_ = _+ᴹ_ + ; ε = 0ᴹ + ; _⁻¹ = -ᴹ_ + } + +------------------------------------------------------------------------ +-- Raw right modules +------------------------------------------------------------------------ + +record RawRightSemimodule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where + infixl 7 _*ᵣ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ᵣ_ : Opᵣ R Carrierᴹ + 0ᴹ : Carrierᴹ + + +ᴹ-rawMonoid : RawMonoid m ℓm + +ᴹ-rawMonoid = record + { _≈_ = _≈ᴹ_ + ; _∙_ = _+ᴹ_ + ; ε = 0ᴹ + } + + open RawMonoid +ᴹ-rawMonoid public + using () + renaming (rawMagma to +ᴹ-rawMagma; _≉_ to _≉ᴹ_) + +record RawRightModule (R : Set r) m ℓm : Set (r ⊔ suc (m ⊔ ℓm)) where + infix 8 -ᴹ_ + infixl 7 _*ᵣ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ᵣ_ : Opᵣ R Carrierᴹ + 0ᴹ : Carrierᴹ + -ᴹ_ : Op₁ Carrierᴹ + + rawRightSemimodule : RawRightSemimodule R m ℓm + rawRightSemimodule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ᵣ_ = _*ᵣ_ + ; 0ᴹ = 0ᴹ + } + + open RawRightSemimodule rawRightSemimodule public + using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_) + + +ᴹ-rawGroup : RawGroup m ℓm + +ᴹ-rawGroup = record + { _≈_ = _≈ᴹ_ + ; _∙_ = _+ᴹ_ + ; ε = 0ᴹ + ; _⁻¹ = -ᴹ_ + } + +------------------------------------------------------------------------ +-- Bimodules +------------------------------------------------------------------------ + +record RawBisemimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ℓm)) where + infixr 7 _*ₗ_ + infixl 7 _*ᵣ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ₗ_ : Opₗ R Carrierᴹ + _*ᵣ_ : Opᵣ S Carrierᴹ + 0ᴹ : Carrierᴹ + + rawLeftSemimodule : RawLeftSemimodule R m ℓm + rawLeftSemimodule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ₗ_ = _*ₗ_ + ; 0ᴹ = 0ᴹ + } + + rawRightSemimodule : RawRightSemimodule S m ℓm + rawRightSemimodule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ᵣ_ = _*ᵣ_ + ; 0ᴹ = 0ᴹ + } + + open RawLeftSemimodule rawLeftSemimodule public + using (+ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_) + +record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ℓm)) where + infix 8 -ᴹ_ + infixr 7 _*ₗ_ + infixl 7 _*ᵣ_ + infixl 6 _+ᴹ_ + infix 4 _≈ᴹ_ + + field + Carrierᴹ : Set m + _≈ᴹ_ : Rel Carrierᴹ ℓm + _+ᴹ_ : Op₂ Carrierᴹ + _*ₗ_ : Opₗ R Carrierᴹ + _*ᵣ_ : Opᵣ S Carrierᴹ + 0ᴹ : Carrierᴹ + -ᴹ_ : Op₁ Carrierᴹ + + rawLeftModule : RawLeftModule R m ℓm + rawLeftModule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ₗ_ = _*ₗ_ + ; 0ᴹ = 0ᴹ + ; -ᴹ_ = -ᴹ_ + } + + rawRightModule : RawRightModule S m ℓm + rawRightModule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ᵣ_ = _*ᵣ_ + ; 0ᴹ = 0ᴹ + ; -ᴹ_ = -ᴹ_ + } + + rawBisemimodule : RawBisemimodule R S m ℓm + rawBisemimodule = record + { _≈ᴹ_ = _≈ᴹ_ + ; _+ᴹ_ = _+ᴹ_ + ; _*ₗ_ = _*ₗ_ + ; _*ᵣ_ = _*ᵣ_ + ; 0ᴹ = 0ᴹ + } + + open RawBisemimodule rawBisemimodule public + using (+ᴹ-rawMagma; +ᴹ-rawMonoid; rawLeftSemimodule; rawRightSemimodule; _≉ᴹ_) + + open RawLeftModule rawLeftModule public + using (+ᴹ-rawGroup) + +------------------------------------------------------------------------ +-- Modules over commutative structures +------------------------------------------------------------------------ + +RawSemimodule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc (m ⊔ ℓm)) +RawSemimodule R = RawBisemimodule R R + +module RawSemimodule {R : Set r} {m ℓm} (M : RawSemimodule R m ℓm) where + open RawBisemimodule M public + + rawBisemimodule : RawBisemimodule R R m ℓm + rawBisemimodule = M + +RawModule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc(m ⊔ ℓm)) +RawModule R = RawBimodule R R + +module RawModule {R : Set r} {m ℓm} (M : RawModule R m ℓm) where + open RawBimodule M public + + rawBimodule : RawBimodule R R m ℓm + rawBimodule = M + + rawSemimodule : RawSemimodule R m ℓm + rawSemimodule = rawBisemimodule diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda index 429a2d11ca..473e240801 100644 --- a/src/Algebra/Module/Construct/DirectProduct.agda +++ b/src/Algebra/Module/Construct/DirectProduct.agda @@ -14,7 +14,7 @@ module Algebra.Module.Construct.DirectProduct where open import Algebra.Bundles open import Algebra.Construct.DirectProduct open import Algebra.Module.Bundles -open import Data.Product.Base using (map; _,_; proj₁; proj₂) +open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Level @@ -22,6 +22,83 @@ private variable r s ℓr ℓs m m′ ℓm ℓm′ : Level +------------------------------------------------------------------------ +-- Raw bundles + +rawLeftSemimodule : {R : Set r} → + RawLeftSemimodule R m ℓm → + RawLeftSemimodule R m′ ℓm′ → + RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawLeftSemimodule M N = record + { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_ + ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_ + ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_) + ; 0ᴹ = M.0ᴹ , N.0ᴹ + } where module M = RawLeftSemimodule M; module N = RawLeftSemimodule N + +rawLeftModule : {R : Set r} → + RawLeftModule R m ℓm → + RawLeftModule R m′ ℓm′ → + RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawLeftModule M N = record + { RawLeftSemimodule (rawLeftSemimodule M.rawLeftSemimodule N.rawLeftSemimodule) + ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + } where module M = RawLeftModule M; module N = RawLeftModule N + + +rawRightSemimodule : {R : Set r} → + RawRightSemimodule R m ℓm → + RawRightSemimodule R m′ ℓm′ → + RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawRightSemimodule M N = record + { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_ + ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_ + ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn + ; 0ᴹ = M.0ᴹ , N.0ᴹ + } where module M = RawRightSemimodule M; module N = RawRightSemimodule N + +rawRightModule : {R : Set r} → + RawRightModule R m ℓm → + RawRightModule R m′ ℓm′ → + RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawRightModule M N = record + { RawRightSemimodule (rawRightSemimodule M.rawRightSemimodule N.rawRightSemimodule) + ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + } where module M = RawRightModule M; module N = RawRightModule N + +rawBisemimodule : {R : Set r} {S : Set s} → + RawBisemimodule R S m ℓm → + RawBisemimodule R S m′ ℓm′ → + RawBisemimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′) +rawBisemimodule M N = record + { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_ + ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_ + ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_) + ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn + ; 0ᴹ = M.0ᴹ , N.0ᴹ + } where module M = RawBisemimodule M; module N = RawBisemimodule N + +rawBimodule : {R : Set r} {S : Set s} → + RawBimodule R S m ℓm → + RawBimodule R S m′ ℓm′ → + RawBimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′) +rawBimodule M N = record + { RawBisemimodule (rawBisemimodule M.rawBisemimodule N.rawBisemimodule) + ; -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + } where module M = RawBimodule M; module N = RawBimodule N + +rawSemimodule : {R : Set r} → + RawSemimodule R m ℓm → + RawSemimodule R m′ ℓm′ → + RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawSemimodule M N = rawBisemimodule M N + +rawModule : {R : Set r} → + RawModule R m ℓm → + RawModule R m′ ℓm′ → + RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) +rawModule M N = rawBimodule M N + ------------------------------------------------------------------------ -- Bundles diff --git a/src/Algebra/Module/Construct/TensorUnit.agda b/src/Algebra/Module/Construct/TensorUnit.agda index c76f2a39ba..6c97b67de0 100644 --- a/src/Algebra/Module/Construct/TensorUnit.agda +++ b/src/Algebra/Module/Construct/TensorUnit.agda @@ -19,6 +19,62 @@ private variable c ℓ : Level +------------------------------------------------------------------------ +-- Raw bundles + +rawLeftSemimodule : {R : RawSemiring c ℓ} → RawLeftSemimodule _ c ℓ +rawLeftSemimodule {R = R} = record + { _≈ᴹ_ = _≈_ + ; _+ᴹ_ = _+_ + ; _*ₗ_ = _*_ + ; 0ᴹ = 0# + } where open RawSemiring R + +rawLeftModule : {R : RawRing c ℓ} → RawLeftModule _ c ℓ +rawLeftModule {R = R} = record + { RawLeftSemimodule (rawLeftSemimodule {R = rawSemiring}) + ; -ᴹ_ = -_ + } where open RawRing R + +rawRightSemimodule : {R : RawSemiring c ℓ} → RawRightSemimodule _ c ℓ +rawRightSemimodule {R = R} = record + { _≈ᴹ_ = _≈_ + ; _+ᴹ_ = _+_ + ; _*ᵣ_ = _*_ + ; 0ᴹ = 0# + } where open RawSemiring R + +rawRightModule : {R : RawRing c ℓ} → RawRightModule _ c ℓ +rawRightModule {R = R} = record + { RawRightSemimodule (rawRightSemimodule {R = rawSemiring}) + ; -ᴹ_ = -_ + } where open RawRing R + +rawBisemimodule : {R : RawSemiring c ℓ} → RawBisemimodule _ _ c ℓ +rawBisemimodule {R = R} = record + { _≈ᴹ_ = _≈_ + ; _+ᴹ_ = _+_ + ; _*ₗ_ = _*_ + ; _*ᵣ_ = _*_ + ; 0ᴹ = 0# + } where open RawSemiring R + +rawBimodule : {R : RawRing c ℓ} → RawBimodule _ _ c ℓ +rawBimodule {R = R} = record + { RawBisemimodule (rawBisemimodule {R = rawSemiring}) + ; -ᴹ_ = -_ + } where open RawRing R + + +rawSemimodule : {R : RawSemiring c ℓ} → RawSemimodule _ c ℓ +rawSemimodule {R = R} = rawBisemimodule {R = R} + +rawModule : {R : RawRing c ℓ} → RawModule _ c ℓ +rawModule {R = R} = rawBimodule {R = R} + +------------------------------------------------------------------------ +-- Bundles + leftSemimodule : {R : Semiring c ℓ} → LeftSemimodule R c ℓ leftSemimodule {R = semiring} = record { Carrierᴹ = Carrier diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index 624cd04598..256f70e8c0 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -35,14 +35,33 @@ module ℤero where _≈ᴹ_ : Rel Carrierᴹ ℓ _ ≈ᴹ _ = ⊤ -open ℤero - ------------------------------------------------------------------------ --- Raw bundles NOT YET IMPLEMENTED issue #1828 -{- -rawModule : RawModule c ℓ +-- Raw bundles + +rawLeftSemimodule : {R : Set r} → RawLeftSemimodule R c ℓ +rawLeftSemimodule = record { ℤero } + +rawLeftModule : {R : Set r} → RawLeftModule R c ℓ +rawLeftModule = record { ℤero } + +rawRightSemimodule : {R : Set r} → RawRightSemimodule R c ℓ +rawRightSemimodule = record { ℤero } + +rawRightModule : {R : Set r} → RawRightModule R c ℓ +rawRightModule = record { ℤero } + +rawBisemimodule : {R : Set r} {S : Set s} → RawBisemimodule R S c ℓ +rawBisemimodule = record { ℤero } + +rawBimodule : {R : Set r} {S : Set s} → RawBimodule R S c ℓ +rawBimodule = record { ℤero } + +rawSemimodule : {R : Set r} → RawSemimodule R c ℓ +rawSemimodule = record { ℤero } + +rawModule : {R : Set r} → RawModule R c ℓ rawModule = record { ℤero } --} + ------------------------------------------------------------------------ -- Bundles