From d89c21fe7e35b866db6313370651d67271c754dd Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 23 Jan 2024 13:40:13 +0100 Subject: [PATCH 01/11] Raw bundles for modules --- src/Algebra/Module/Bundles/Raw.agda | 228 ++++++++++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 src/Algebra/Module/Bundles/Raw.agda diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda new file mode 100644 index 0000000000..701733b6cb --- /dev/null +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -0,0 +1,228 @@ +------------------------------------------------------------------------ +-- 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ᴹ + ; -ᴹ_ = -ᴹ_ + } + + open RawLeftModule rawLeftModule public + using (+ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup; _≉ᴹ_) + +------------------------------------------------------------------------ +-- Modules over commutative structures +------------------------------------------------------------------------ + +RawSemimodule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc (m ⊔ ℓm)) +RawSemimodule R = RawBisemimodule R R + +module RawSemimodule = RawBisemimodule + +RawModule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc(m ⊔ ℓm)) +RawModule R = RawBimodule R R + +module RawModule = RawBimodule From 8c0374da4796aa886fdcf95d464520b32ce7c491 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 23 Jan 2024 14:06:14 +0100 Subject: [PATCH 02/11] Export raw bundles from module bundles --- src/Algebra/Module/Bundles.agda | 96 +++++++++++++++++++++++++++------ 1 file changed, 80 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index f36e5bccd0..19d9341478 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) +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,7 +112,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 +120,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 +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,7 +198,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 +206,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 +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 From 59eccc61f275a10bd3f9ea2c258d168608d9cb63 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 23 Jan 2024 14:14:56 +0100 Subject: [PATCH 03/11] Update chnagelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c690740a1e..f1a1462fd3 100644 --- a/CHANGELOG.md +++ b/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 From 52a870ce752501686a18c99ebfdd0986b793284d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 13:10:17 +0100 Subject: [PATCH 04/11] Remove redundant field --- src/Algebra/Module/Bundles.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index 19d9341478..a95f7ab8f2 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -256,8 +256,7 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs rawBisemimodule : RawBisemimodule R.Carrier S.Carrier m ℓm rawBisemimodule = record - { Carrierᴹ = Carrierᴹ - ; _≈ᴹ_ = _≈ᴹ_ + { _≈ᴹ_ = _≈ᴹ_ ; _+ᴹ_ = _+ᴹ_ ; _*ₗ_ = _*ₗ_ ; _*ᵣ_ = _*ᵣ_ From 78805fbdad86aac4d2af25b4b8a2886a59abd081 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 13:16:28 +0100 Subject: [PATCH 05/11] Reexport raw bundles, add raw bundles for zero --- src/Algebra/Module/Bundles.agda | 12 ++++++++++- src/Algebra/Module/Construct/Zero.agda | 29 ++++++++++++++++++++++---- 2 files changed, 36 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index a95f7ab8f2..56b01fcf97 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -28,7 +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 +import Algebra.Module.Bundles.Raw as Raw open import Algebra.Module.Core open import Algebra.Module.Structures open import Algebra.Module.Definitions @@ -43,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 ------------------------------------------------------------------------ diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index 624cd04598..965cc435d9 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -38,11 +38,32 @@ module ℤero where 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 From 941ff33b5875f021b512179163096af3ee74ea36 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 13:47:04 +0100 Subject: [PATCH 06/11] Add missing reexports, raw bundles for direct product --- src/Algebra/Module/Bundles/Raw.agda | 16 +++- .../Module/Construct/DirectProduct.agda | 79 ++++++++++++++++++- 2 files changed, 92 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda index 701733b6cb..b0dce59ae5 100644 --- a/src/Algebra/Module/Bundles/Raw.agda +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -209,9 +209,21 @@ record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ; 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 (+ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup; _≉ᴹ_) + using (+ᴹ-rawGroup) ------------------------------------------------------------------------ -- Modules over commutative structures 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 From 454833ae6475da568a9048f4bdf28fff64223488 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 13:57:39 +0100 Subject: [PATCH 07/11] Raw bundles for tensor unit --- src/Algebra/Module/Construct/TensorUnit.agda | 56 ++++++++++++++++++++ 1 file changed, 56 insertions(+) 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 From 7f35fc61d54e1856d640c5f55366568fc1faa953 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 14:10:44 +0100 Subject: [PATCH 08/11] Update changelog again --- CHANGELOG.md | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f1a1462fd3..aee42a40ce 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,7 +38,43 @@ New modules Additions to existing modules ----------------------------- -* In `Algebra.Module.Bundles`, the bundles expose their raw counterparts. +* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. + +* In `Algebra.Module.Cosntruct.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 From 869223d5ae6c8c8de1a8d4d0e111e210224215ec Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 14:18:38 +0100 Subject: [PATCH 09/11] Remove unused open --- src/Algebra/Module/Construct/Zero.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index 965cc435d9..256f70e8c0 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -35,8 +35,6 @@ module ℤero where _≈ᴹ_ : Rel Carrierᴹ ℓ _ ≈ᴹ _ = ⊤ -open ℤero - ------------------------------------------------------------------------ -- Raw bundles From 5ef4919606a6c18bdf29ca61bb178060a058a7d8 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 14:32:48 +0100 Subject: [PATCH 10/11] Fix typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index aee42a40ce..97eb05989b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -40,7 +40,7 @@ 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`: +* 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′) From 14b77d74fc71a6c35036a9fe9f961563cda4b357 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 25 Jan 2024 09:30:36 +0100 Subject: [PATCH 11/11] Put a few more definitions in the fake record modules for RawModule and RawSemimodule --- src/Algebra/Module/Bundles/Raw.agda | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda index b0dce59ae5..b9cc108915 100644 --- a/src/Algebra/Module/Bundles/Raw.agda +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -232,9 +232,20 @@ record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ RawSemimodule : ∀ (R : Set r) m ℓm → Set (r ⊔ suc (m ⊔ ℓm)) RawSemimodule R = RawBisemimodule R R -module RawSemimodule = RawBisemimodule +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 = RawBimodule +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