From a295308da9d42e2a3f78a121898c8e6c17f8ac30 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 00:41:49 -0300 Subject: [PATCH 01/25] added Functional Algebra Properties --- .../Vec/Functional/Algebra/Properties.agda | 172 ++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100644 src/Data/Vec/Functional/Algebra/Properties.agda diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda new file mode 100644 index 0000000000..12318c3ac6 --- /dev/null +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -0,0 +1,172 @@ +open import Function using (_$_) +open import Data.Product hiding (map) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Vec.Functional +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Module +open import Relation.Binary +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid +import Algebra.Definitions as AD +import Algebra.Structures as AS + +module Data.Vec.Functional.Algebra.Properties + {c ℓ} (ring : Ring c ℓ) where + +private variable + n : ℕ + +open Ring ring +module SR = Semiring semiring +open VecSetoid setoid + +VC = Vector Carrier + +_≈ᴹ_ : Rel (VC n) ℓ +_≈ᴹ_ = _≋_ + +open module AD' {n} = AD (_≈ᴹ_ {n}) +open module AS' {n} = AS (_≈ᴹ_ {n}) +open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) + +_+ᴹ_ : Op₂ $ VC n +_+ᴹ_ = zipWith _+_ + +0ᴹ : VC n +0ᴹ = replicate 0# + +-ᴹ_ : Op₁ $ VC n +-ᴹ_ = map $ -_ + +_*ₗ_ : Opₗ Carrier (VC n) +_*ₗ_ r = map (r *_) + ++ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) ++ᴹ-cong x≈y u≈v _ = +-cong (x≈y _) (u≈v _) + ++ᴹ-assoc : Associative (_+ᴹ_ {n}) ++ᴹ-assoc _ _ _ _ = +-assoc _ _ _ + ++ᴹ-comm : Commutative (_+ᴹ_ {n}) ++ᴹ-comm _ _ _ = +-comm _ _ + ++ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ ++ᴹ-identityˡ _ _ = +-identityˡ _ + ++ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ ++ᴹ-identityʳ _ _ = +-identityʳ _ + ++ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ ++ᴹ-identity = +ᴹ-identityˡ , +ᴹ-identityʳ + +-ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) +-ᴹ‿cong f _ = -‿cong (f _) + +-ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ +-ᴹ‿inverseˡ _ _ = -‿inverseˡ _ + +-ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ +-ᴹ‿inverseʳ _ _ = -‿inverseʳ _ + +-ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ +-ᴹ‿inverse = -ᴹ‿inverseˡ , -ᴹ‿inverseʳ + +*ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n}) +*ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) + +*ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ +*ₗ-zeroˡ f i = zeroˡ (f i) + +*ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) +*ₗ-distribʳ _ _ _ _ = distribʳ _ _ _ + +*ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) +*ₗ-identityˡ _ _ = *-identityˡ _ + +*ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) +*ₗ-assoc _ _ _ _ = *-assoc _ _ _ + +*ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ +*ₗ-zeroʳ _ _ = zeroʳ _ + +*ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) +*ₗ-distribˡ _ _ _ _ = distribˡ _ _ _ + +isMagma : IsMagma (_+ᴹ_ {n}) +isMagma = record + { isEquivalence = ≋-isEquivalence _ + ; ∙-cong = +ᴹ-cong + } + +isSemigroup : IsSemigroup (_+ᴹ_ {n}) +isSemigroup = record + { isMagma = isMagma + ; assoc = +ᴹ-assoc + } + +isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ +isMonoid = record + { isSemigroup = isSemigroup + ; identity = +ᴹ-identity + } + +isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ +isCommutativeMonoid = record + { isMonoid = isMonoid + ; comm = +ᴹ-comm + } + +isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ +isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ + } + +isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ +isLeftSemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimodule + } + +isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ +isLeftModule = record + { isLeftSemimodule = isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse + } + +magma : ℕ → Magma _ _ +magma n = record + { isMagma = isMagma {n} + } + +semiGroup : ℕ → Semigroup _ _ +semiGroup n = record + { isSemigroup = isSemigroup {n} + } + +monoid : ℕ → Monoid _ _ +monoid n = record + { isMonoid = isMonoid {n} + } + +commutativeMonoid : ℕ → CommutativeMonoid _ _ +commutativeMonoid n = record + { isCommutativeMonoid = isCommutativeMonoid {n} + } + +leftSemimodule : ℕ → LeftSemimodule _ _ _ +leftSemimodule n = record + { isLeftSemimodule = isLeftSemimodule {n} + } + +leftModule : ℕ → LeftModule _ _ _ +leftModule n = record + { isLeftModule = isLeftModule {n} + } From 3037439dd089c9b4a3e293b4a6405314eb64a872 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 00:48:39 -0300 Subject: [PATCH 02/25] put some things in Base --- src/Data/Vec/Functional/Algebra/Base.agda | 46 +++++++++++++++++++ .../Vec/Functional/Algebra/Properties.agda | 37 +++++++-------- 2 files changed, 65 insertions(+), 18 deletions(-) create mode 100644 src/Data/Vec/Functional/Algebra/Base.agda diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda new file mode 100644 index 0000000000..3d575f8df1 --- /dev/null +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -0,0 +1,46 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some Vector-related module Definitions +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Function using (_$_) +open import Data.Product hiding (map) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Vec.Functional +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Module +open import Relation.Binary +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid +import Algebra.Definitions as AD +import Algebra.Structures as AS + +module Data.Vec.Functional.Algebra.Base + {c ℓ} (ring : Ring c ℓ) where + +private variable + n : ℕ + +open Ring ring +open VecSetoid setoid + +VC = Vector Carrier + +_≈ᴹ_ : Rel (VC n) ℓ +_≈ᴹ_ = _≋_ + +_+ᴹ_ : Op₂ $ VC n +_+ᴹ_ = zipWith _+_ + +0ᴹ : VC n +0ᴹ = replicate 0# + +-ᴹ_ : Op₁ $ VC n +-ᴹ_ = map $ -_ + +_*ₗ_ : Opₗ Carrier (VC n) +_*ₗ_ r = map (r *_) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 12318c3ac6..1fb00a9d8b 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -1,3 +1,11 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some Vector-related module properties +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + open import Function using (_$_) open import Data.Product hiding (map) open import Data.Nat using (ℕ) @@ -10,6 +18,7 @@ open import Relation.Binary import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid import Algebra.Definitions as AD import Algebra.Structures as AS +import Data.Vec.Functional.Algebra.Base as VFA module Data.Vec.Functional.Algebra.Properties {c ℓ} (ring : Ring c ℓ) where @@ -18,29 +27,15 @@ private variable n : ℕ open Ring ring -module SR = Semiring semiring open VecSetoid setoid - -VC = Vector Carrier - -_≈ᴹ_ : Rel (VC n) ℓ -_≈ᴹ_ = _≋_ - +open VFA ring +module SR = Semiring semiring open module AD' {n} = AD (_≈ᴹ_ {n}) open module AS' {n} = AS (_≈ᴹ_ {n}) open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) -_+ᴹ_ : Op₂ $ VC n -_+ᴹ_ = zipWith _+_ - -0ᴹ : VC n -0ᴹ = replicate 0# - --ᴹ_ : Op₁ $ VC n --ᴹ_ = map $ -_ - -_*ₗ_ : Opₗ Carrier (VC n) -_*ₗ_ r = map (r *_) +------------------------------------------------------------------------ +-- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ +ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) +ᴹ-cong x≈y u≈v _ = +-cong (x≈y _) (u≈v _) @@ -93,6 +88,9 @@ _*ₗ_ r = map (r *_) *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) *ₗ-distribˡ _ _ _ _ = distribˡ _ _ _ +------------------------------------------------------------------------ +-- Structures + isMagma : IsMagma (_+ᴹ_ {n}) isMagma = record { isEquivalence = ≋-isEquivalence _ @@ -141,6 +139,9 @@ isLeftModule = record ; -ᴹ‿inverse = -ᴹ‿inverse } +------------------------------------------------------------------------ +-- Bundles + magma : ℕ → Magma _ _ magma n = record { isMagma = isMagma {n} From 468bb690d374a58de810db4f4ebb27d51a378457 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 00:54:06 -0300 Subject: [PATCH 03/25] added changelog --- CHANGELOG.md | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index fdd629e825..2cae2ebbdd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3027,3 +3027,54 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j ``` + +* In `Data.Vec.Functional.Algebra.Base` +```agda + _≈ᴹ_ : Rel (VC n) ℓ + _+ᴹ_ : Op₂ $ VC n + 0ᴹ : VC n + -ᴹ_ : Op₁ $ VC n + _*ₗ_ : Opₗ Carrier (VC n) +``` + +* Added algebraic properties in `Data.Vec.Functional.Algebra.Properties` +```agda + +ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) + +ᴹ-assoc : Associative (_+ᴹ_ {n}) + +ᴹ-comm : Commutative (_+ᴹ_ {n}) + +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ + +ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ + -ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) + -ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + *ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n}) + *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ + *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) + *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) + *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) + *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ + *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) +``` + +* Added structures in `Data.Vec.Functional.Algebra.Properties` +```agda + isMagma : IsMagma (_+ᴹ_ {n}) + isSemigroup : IsSemigroup (_+ᴹ_ {n}) + isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ + isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ + isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ + isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ + isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ +``` + +* Added bundles in `Data.Vec.Functional.Algebra.Properties` +```agda + magma : ℕ → Magma _ _ + semiGroup : ℕ → Semigroup _ _ + monoid : ℕ → Monoid _ _ + commutativeMonoid : ℕ → CommutativeMonoid _ _ + leftSemimodule : ℕ → LeftSemimodule _ _ _ + leftModule : ℕ → LeftModule _ _ _ +``` From 700b114434c86cbf39e2feb39be33873fd31b5a6 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 08:01:48 -0300 Subject: [PATCH 04/25] added the names --- .../Vec/Functional/Algebra/Properties.agda | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 1fb00a9d8b..90539ef4cc 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -38,31 +38,31 @@ open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ +ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) -+ᴹ-cong x≈y u≈v _ = +-cong (x≈y _) (u≈v _) ++ᴹ-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) +ᴹ-assoc : Associative (_+ᴹ_ {n}) -+ᴹ-assoc _ _ _ _ = +-assoc _ _ _ ++ᴹ-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) +ᴹ-comm : Commutative (_+ᴹ_ {n}) -+ᴹ-comm _ _ _ = +-comm _ _ ++ᴹ-comm xs ys i = +-comm (xs i) (ys i) +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ -+ᴹ-identityˡ _ _ = +-identityˡ _ ++ᴹ-identityˡ xs i = +-identityˡ (xs i) +ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ -+ᴹ-identityʳ _ _ = +-identityʳ _ ++ᴹ-identityʳ xs is = +-identityʳ (xs is) +ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ +ᴹ-identity = +ᴹ-identityˡ , +ᴹ-identityʳ -ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) --ᴹ‿cong f _ = -‿cong (f _) +-ᴹ‿cong xs i = -‿cong (xs i) -ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ --ᴹ‿inverseˡ _ _ = -‿inverseˡ _ +-ᴹ‿inverseˡ xs i = -‿inverseˡ (xs i) -ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ --ᴹ‿inverseʳ _ _ = -‿inverseʳ _ +-ᴹ‿inverseʳ xs i = -‿inverseʳ (xs i) -ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverse = -ᴹ‿inverseˡ , -ᴹ‿inverseʳ @@ -71,22 +71,22 @@ open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) *ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ -*ₗ-zeroˡ f i = zeroˡ (f i) +*ₗ-zeroˡ xs i = zeroˡ (xs i) *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) -*ₗ-distribʳ _ _ _ _ = distribʳ _ _ _ +*ₗ-distribʳ xs m n i = distribʳ (xs i) m n *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) -*ₗ-identityˡ _ _ = *-identityˡ _ +*ₗ-identityˡ xs i = *-identityˡ (xs i) *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) -*ₗ-assoc _ _ _ _ = *-assoc _ _ _ +*ₗ-assoc m n xs i = *-assoc m n (xs i) *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ -*ₗ-zeroʳ _ _ = zeroʳ _ +*ₗ-zeroʳ m _ = zeroʳ m *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) -*ₗ-distribˡ _ _ _ _ = distribˡ _ _ _ +*ₗ-distribˡ m xs ys i = distribˡ m (xs i) (ys i) ------------------------------------------------------------------------ -- Structures From 623d474a40f355b8cd5d261bd8d16bf8fbb8eceb Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 08:03:07 -0300 Subject: [PATCH 05/25] changed VC to Vector Carrier --- src/Data/Vec/Functional/Algebra/Base.agda | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 3d575f8df1..4f67142c50 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -28,19 +28,17 @@ private variable open Ring ring open VecSetoid setoid -VC = Vector Carrier - -_≈ᴹ_ : Rel (VC n) ℓ +_≈ᴹ_ : Rel (Vector Carrier n) ℓ _≈ᴹ_ = _≋_ -_+ᴹ_ : Op₂ $ VC n +_+ᴹ_ : Op₂ $ Vector Carrier n _+ᴹ_ = zipWith _+_ -0ᴹ : VC n +0ᴹ : Vector Carrier n 0ᴹ = replicate 0# --ᴹ_ : Op₁ $ VC n +-ᴹ_ : Op₁ $ Vector Carrier n -ᴹ_ = map $ -_ -_*ₗ_ : Opₗ Carrier (VC n) +_*ₗ_ : Opₗ Carrier (Vector Carrier n) _*ₗ_ r = map (r *_) From a5f6a10411f5bac64bd919da997190b3ddb6b20b Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 08:03:47 -0300 Subject: [PATCH 06/25] changed semiGroup to semigroup --- src/Data/Vec/Functional/Algebra/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 90539ef4cc..37f98670ff 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -147,8 +147,8 @@ magma n = record { isMagma = isMagma {n} } -semiGroup : ℕ → Semigroup _ _ -semiGroup n = record +semigroup : ℕ → Semigroup _ _ +semigroup n = record { isSemigroup = isSemigroup {n} } From 514ef927c9a3162cc0f4ec561d8b9b7b604ed49a Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 08:05:41 -0300 Subject: [PATCH 07/25] modified the CHANGELOG --- CHANGELOG.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2cae2ebbdd..221f887c85 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3030,11 +3030,11 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.Vec.Functional.Algebra.Base` ```agda - _≈ᴹ_ : Rel (VC n) ℓ - _+ᴹ_ : Op₂ $ VC n - 0ᴹ : VC n - -ᴹ_ : Op₁ $ VC n - _*ₗ_ : Opₗ Carrier (VC n) + _≈ᴹ_ : Rel (Vector Carrier n) ℓ + _+ᴹ_ : Op₂ $ Vector Carrier n + 0ᴹ : Vector Carrier n + -ᴹ_ : Op₁ $ Vector Carrier n + _*ₗ_ : Opₗ Carrier (Vector Carrier n) ``` * Added algebraic properties in `Data.Vec.Functional.Algebra.Properties` @@ -3072,7 +3072,7 @@ This is a full list of proofs that have changed form to use irrelevant instance * Added bundles in `Data.Vec.Functional.Algebra.Properties` ```agda magma : ℕ → Magma _ _ - semiGroup : ℕ → Semigroup _ _ + semigroup : ℕ → Semigroup _ _ monoid : ℕ → Monoid _ _ commutativeMonoid : ℕ → CommutativeMonoid _ _ leftSemimodule : ℕ → LeftSemimodule _ _ _ From ce75303b67a48471b5b4b5118fa74b0dccef5fab Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 13:44:55 -0300 Subject: [PATCH 08/25] added all the definitions --- CHANGELOG.md | 22 ++++ src/Data/Vec/Functional/Algebra/Base.agda | 3 + .../Vec/Functional/Algebra/Properties.agda | 124 +++++++++++++++++- 3 files changed, 147 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 221f887c85..1c481770ef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3056,17 +3056,34 @@ This is a full list of proofs that have changed form to use irrelevant instance *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) + *ᵣ-cong : RD.Congruent SR._≈_ (_*ᵣ_ {n}) + *ᵣ-distribˡ : _*ᵣ_ RD.DistributesOverˡ SR._+_ ⟶ (_+ᴹ_ {n}) + *ᵣ-zeroˡ : RD.LeftZero (0ᴹ {n}) _*ᵣ_ + *ᵣ-identityʳ : RD.RightIdentity SR.1# (_*ᵣ_ {n}) + *ᵣ-assoc : RD.Associative SR._*_ (_*ᵣ_ {n}) + *ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ + *ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) + *ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ ``` * Added structures in `Data.Vec.Functional.Algebra.Properties` ```agda isMagma : IsMagma (_+ᴹ_ {n}) + isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) isSemigroup : IsSemigroup (_+ᴹ_ {n}) + isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ + isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ + isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ + isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ + isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ + isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ + isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ + isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ ``` * Added bundles in `Data.Vec.Functional.Algebra.Properties` @@ -3077,4 +3094,9 @@ This is a full list of proofs that have changed form to use irrelevant instance commutativeMonoid : ℕ → CommutativeMonoid _ _ leftSemimodule : ℕ → LeftSemimodule _ _ _ leftModule : ℕ → LeftModule _ _ _ + commutativeMagma : ℕ → CommutativeMagma _ _ + group : ℕ → Group _ _ + bisemimodule : ℕ → Bisemimodule _ _ _ _ + rightModule : ℕ → RightModule _ _ _ + bimodule : ℕ → Bimodule _ _ _ _ ``` diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 4f67142c50..dd97b2055a 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -42,3 +42,6 @@ _+ᴹ_ = zipWith _+_ _*ₗ_ : Opₗ Carrier (Vector Carrier n) _*ₗ_ r = map (r *_) + +_*ᵣ_ : Opᵣ Carrier (Vector Carrier n) +xs *ᵣ r = map (_* r) xs diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 37f98670ff..82e1abbb05 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -32,7 +32,9 @@ open VFA ring module SR = Semiring semiring open module AD' {n} = AD (_≈ᴹ_ {n}) open module AS' {n} = AS (_≈ᴹ_ {n}) -open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) +module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) +module RD {n} = RightDefs Carrier (_≈ᴹ_ {n}) +module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n}) ------------------------------------------------------------------------ -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ @@ -67,7 +69,7 @@ open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) -ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverse = -ᴹ‿inverseˡ , -ᴹ‿inverseʳ -*ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n}) +*ₗ-cong : LD.Congruent SR._≈_ (_*ₗ_ {n}) *ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ @@ -88,6 +90,30 @@ open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent) *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) *ₗ-distribˡ m xs ys i = distribˡ m (xs i) (ys i) +*ᵣ-cong : RD.Congruent SR._≈_ (_*ᵣ_ {n}) +*ᵣ-cong x≈y u≈v i = *-cong (x≈y i) u≈v + +*ᵣ-distribˡ : _*ᵣ_ RD.DistributesOverˡ SR._+_ ⟶ (_+ᴹ_ {n}) +*ᵣ-distribˡ xs m n i = distribˡ (xs i) m n + +*ᵣ-zeroˡ : RD.LeftZero (0ᴹ {n}) _*ᵣ_ +*ᵣ-zeroˡ xs i = zeroˡ xs + +*ᵣ-identityʳ : RD.RightIdentity SR.1# (_*ᵣ_ {n}) +*ᵣ-identityʳ xs i = *-identityʳ (xs i) + +*ᵣ-assoc : RD.Associative SR._*_ (_*ᵣ_ {n}) +*ᵣ-assoc xs m n i = *-assoc (xs i) m n + +*ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ +*ᵣ-zeroʳ xs i = zeroʳ (xs i) + +*ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) +*ᵣ-distribʳ xs m n i = distribʳ xs (m i) (n i) + +*ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ +*ₗ-*ᵣ-assoc m xs n i = *-assoc m (xs i) n + ------------------------------------------------------------------------ -- Structures @@ -97,12 +123,24 @@ isMagma = record ; ∙-cong = +ᴹ-cong } +isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) +isCommutativeMagma = record + { isMagma = isMagma + ; comm = +ᴹ-comm + } + isSemigroup : IsSemigroup (_+ᴹ_ {n}) isSemigroup = record { isMagma = isMagma ; assoc = +ᴹ-assoc } +isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) +isCommutativeSemigroup = record + { isSemigroup = isSemigroup + ; comm = +ᴹ-comm + } + isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ isMonoid = record { isSemigroup = isSemigroup @@ -115,6 +153,19 @@ isCommutativeMonoid = record ; comm = +ᴹ-comm } +isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ +isGroup = record + { isMonoid = isMonoid + ; inverse = -ᴹ‿inverse + ; ⁻¹-cong = -ᴹ‿cong + } + +isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ +isAbelianGroup = record + { isGroup = isGroup + ; comm = +ᴹ-comm + } + isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isPreleftSemimodule = record { *ₗ-cong = *ₗ-cong @@ -126,6 +177,45 @@ isPreleftSemimodule = record ; *ₗ-distribˡ = *ₗ-distribˡ } +isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ +isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ + } + +isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ +isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid + ; isPrerightSemimodule = isPrerightSemimodule + } + +isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ +isBisemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimodule + ; isPrerightSemimodule = isPrerightSemimodule + ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc + } + +isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ +isRightModule = record + { isRightSemimodule = isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse + } + +isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ +isBimodule = record + { isBisemimodule = isBisemimodule + ; -ᴹ‿cong = -ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse + } + isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isLeftSemimodule = record { +ᴹ-isCommutativeMonoid = isCommutativeMonoid @@ -147,11 +237,21 @@ magma n = record { isMagma = isMagma {n} } +commutativeMagma : ℕ → CommutativeMagma _ _ +commutativeMagma n = record { + isCommutativeMagma = isCommutativeMagma {n} + } + semigroup : ℕ → Semigroup _ _ semigroup n = record { isSemigroup = isSemigroup {n} } +commutativeSemigroup : ℕ → CommutativeSemigroup _ _ +commutativeSemigroup n = record + { isCommutativeSemigroup = isCommutativeSemigroup {n} + } + monoid : ℕ → Monoid _ _ monoid n = record { isMonoid = isMonoid {n} @@ -162,6 +262,11 @@ commutativeMonoid n = record { isCommutativeMonoid = isCommutativeMonoid {n} } +group : ℕ → Group _ _ +group n = record + { isGroup = isGroup {n} + } + leftSemimodule : ℕ → LeftSemimodule _ _ _ leftSemimodule n = record { isLeftSemimodule = isLeftSemimodule {n} @@ -171,3 +276,18 @@ leftModule : ℕ → LeftModule _ _ _ leftModule n = record { isLeftModule = isLeftModule {n} } + +bisemimodule : ℕ → Bisemimodule _ _ _ _ +bisemimodule n = record + { isBisemimodule = isBisemimodule {n} + } + +rightModule : ℕ → RightModule _ _ _ +rightModule n = record + { isRightModule = isRightModule {n} + } + +bimodule : ℕ → Bimodule _ _ _ _ +bimodule n = record + { isBimodule = isBimodule {n} + } From 7d62c1cdc180755e4203e8fc611f81a7497b07c8 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 14:09:26 -0300 Subject: [PATCH 09/25] changed to commutative ring to add module --- CHANGELOG.md | 2 ++ src/Data/Vec/Functional/Algebra/Base.agda | 4 ++-- src/Data/Vec/Functional/Algebra/Properties.agda | 14 +++++++++++--- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1c481770ef..e6687939c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3084,6 +3084,7 @@ This is a full list of proofs that have changed form to use irrelevant instance isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ ``` * Added bundles in `Data.Vec.Functional.Algebra.Properties` @@ -3099,4 +3100,5 @@ This is a full list of proofs that have changed form to use irrelevant instance bisemimodule : ℕ → Bisemimodule _ _ _ _ rightModule : ℕ → RightModule _ _ _ bimodule : ℕ → Bimodule _ _ _ _ +module' : ℕ → Module _ _ _ ``` diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index dd97b2055a..acddcf6d14 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -20,12 +20,12 @@ import Algebra.Definitions as AD import Algebra.Structures as AS module Data.Vec.Functional.Algebra.Base - {c ℓ} (ring : Ring c ℓ) where + {c ℓ} (cring : CommutativeRing c ℓ) where private variable n : ℕ -open Ring ring +open CommutativeRing cring open VecSetoid setoid _≈ᴹ_ : Rel (Vector Carrier n) ℓ diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 82e1abbb05..17a6468584 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -21,14 +21,14 @@ import Algebra.Structures as AS import Data.Vec.Functional.Algebra.Base as VFA module Data.Vec.Functional.Algebra.Properties - {c ℓ} (ring : Ring c ℓ) where + {c ℓ} (cring : CommutativeRing c ℓ) where private variable n : ℕ -open Ring ring +open CommutativeRing cring open VecSetoid setoid -open VFA ring +open VFA cring module SR = Semiring semiring open module AD' {n} = AD (_≈ᴹ_ {n}) open module AS' {n} = AS (_≈ᴹ_ {n}) @@ -229,6 +229,9 @@ isLeftModule = record ; -ᴹ‿inverse = -ᴹ‿inverse } +isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ +isModule = record { isBimodule = isBimodule } + ------------------------------------------------------------------------ -- Bundles @@ -291,3 +294,8 @@ bimodule : ℕ → Bimodule _ _ _ _ bimodule n = record { isBimodule = isBimodule {n} } + +module' : ℕ → Module _ _ _ +module' n = record + { isModule = isModule {n} + } From 3ed6e0bf69c2aa057df9b0f2ac7c5f8416bebaa0 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 14:10:38 -0300 Subject: [PATCH 10/25] fixed isModule --- src/Data/Vec/Functional/Algebra/Properties.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 17a6468584..78e0cf9ff7 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -230,7 +230,9 @@ isLeftModule = record } isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ -isModule = record { isBimodule = isBimodule } +isModule = record + { isBimodule = isBimodule + } ------------------------------------------------------------------------ -- Bundles From 81548b066af311d958f8f0c8a15074052d12c427 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 17 Apr 2023 23:37:13 -0300 Subject: [PATCH 11/25] added ring * and 1m --- CHANGELOG.md | 2 +- src/Data/Vec/Functional/Algebra/Base.agda | 6 +++ .../Vec/Functional/Algebra/Properties.agda | 43 +++++++++++++++++++ 3 files changed, 50 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e6687939c8..b9e03a14a7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3100,5 +3100,5 @@ This is a full list of proofs that have changed form to use irrelevant instance bisemimodule : ℕ → Bisemimodule _ _ _ _ rightModule : ℕ → RightModule _ _ _ bimodule : ℕ → Bimodule _ _ _ _ -module' : ℕ → Module _ _ _ + module' : ℕ → Module _ _ _ ``` diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index acddcf6d14..ea5898114c 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -34,9 +34,15 @@ _≈ᴹ_ = _≋_ _+ᴹ_ : Op₂ $ Vector Carrier n _+ᴹ_ = zipWith _+_ +_*ᴹ_ : Op₂ $ Vector Carrier n +_*ᴹ_ = zipWith _*_ + 0ᴹ : Vector Carrier n 0ᴹ = replicate 0# +1ᴹ : Vector Carrier n +1ᴹ = replicate 1# + -ᴹ_ : Op₁ $ Vector Carrier n -ᴹ_ = map $ -_ diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 78e0cf9ff7..fbb466429c 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -42,21 +42,36 @@ module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n}) +ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) +ᴹ-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) +*ᴹ-cong : Congruent₂ (_*ᴹ_ {n}) +*ᴹ-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) + +ᴹ-assoc : Associative (_+ᴹ_ {n}) +ᴹ-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) +*ᴹ-assoc : Associative (_*ᴹ_ {n}) +*ᴹ-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) + +ᴹ-comm : Commutative (_+ᴹ_ {n}) +ᴹ-comm xs ys i = +-comm (xs i) (ys i) +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ +ᴹ-identityˡ xs i = +-identityˡ (xs i) +*ᴹ-identityˡ : LeftIdentity (1ᴹ {n}) _*ᴹ_ +*ᴹ-identityˡ xs i = *-identityˡ (xs i) + +ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ +ᴹ-identityʳ xs is = +-identityʳ (xs is) +*ᴹ-identityʳ : RightIdentity (1ᴹ {n}) _*ᴹ_ +*ᴹ-identityʳ xs is = *-identityʳ (xs is) + +ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ +ᴹ-identity = +ᴹ-identityˡ , +ᴹ-identityʳ +*ᴹ-identity : Identity (1ᴹ {n}) _*ᴹ_ +*ᴹ-identity = *ᴹ-identityˡ , *ᴹ-identityʳ + -ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) -ᴹ‿cong xs i = -‿cong (xs i) @@ -114,6 +129,24 @@ module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n}) *ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ *ₗ-*ᵣ-assoc m xs n i = *-assoc m (xs i) n +*ᴹ-zeroˡ : AD'.LeftZero (0ᴹ {n}) _*ᴹ_ +*ᴹ-zeroˡ xs i = zeroˡ (xs i) + +*ᴹ-zeroʳ : AD'.RightZero (0ᴹ {n}) _*ᴹ_ +*ᴹ-zeroʳ xs i = zeroʳ (xs i) + +*ᴹ-zero : AD'.Zero (0ᴹ {n}) _*ᴹ_ +*ᴹ-zero = *ᴹ-zeroˡ , *ᴹ-zeroʳ + +*ᴹ-+ᴹ-distribˡ : (_*ᴹ_ {n}) AD'.DistributesOverˡ _+ᴹ_ +*ᴹ-+ᴹ-distribˡ xs ys zs i = distribˡ (xs i) (ys i) (zs i) + +*ᴹ-+ᴹ-distribʳ : (_*ᴹ_ {n}) AD'.DistributesOverʳ _+ᴹ_ +*ᴹ-+ᴹ-distribʳ xs ys zs i = distribʳ (xs i) (ys i) (zs i) + +*ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ +*ᴹ-+ᴹ-distrib = *ᴹ-+ᴹ-distribˡ , *ᴹ-+ᴹ-distribʳ + ------------------------------------------------------------------------ -- Structures @@ -234,6 +267,16 @@ isModule = record { isBimodule = isBimodule } ++ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ ++ᴹ-*-isRing = record + { +-isAbelianGroup = isAbelianGroup + ; *-cong = *ᴹ-cong + ; *-assoc = *ᴹ-assoc + ; *-identity = *ᴹ-identity + ; distrib = *ᴹ-+ᴹ-distrib + ; zero = *ᴹ-zero + } + ------------------------------------------------------------------------ -- Bundles From 1b684fc309d2b96a6922c43b6dd5291237a970eb Mon Sep 17 00:00:00 2001 From: Guilherme Date: Tue, 18 Apr 2023 19:04:08 -0300 Subject: [PATCH 12/25] add all operators of functional vec --- CHANGELOG.md | 45 +++++- .../Vec/Functional/Algebra/Properties.agda | 131 ++++++++++++++++++ 2 files changed, 171 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b9e03a14a7..5ef821bce2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3040,16 +3040,22 @@ This is a full list of proofs that have changed form to use irrelevant instance * Added algebraic properties in `Data.Vec.Functional.Algebra.Properties` ```agda +ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) + *ᴹ-cong : Congruent₂ (_*ᴹ_ {n}) +ᴹ-assoc : Associative (_+ᴹ_ {n}) + *ᴹ-assoc : Associative (_*ᴹ_ {n}) +ᴹ-comm : Commutative (_+ᴹ_ {n}) + *ᴹ-comm : Commutative (_*ᴹ_ {n}) +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ + *ᴹ-identityˡ : LeftIdentity (1ᴹ {n}) _*ᴹ_ +ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ + *ᴹ-identityʳ : RightIdentity (1ᴹ {n}) _*ᴹ_ +ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ + *ᴹ-identity : Identity (1ᴹ {n}) _*ᴹ_ -ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) -ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ - *ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n}) + *ₗ-cong : LD.Congruent SR._≈_ (_*ₗ_ {n}) *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) @@ -3064,41 +3070,70 @@ This is a full list of proofs that have changed form to use irrelevant instance *ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ *ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) *ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ + *ᴹ-zeroˡ : AD'.LeftZero (0ᴹ {n}) _*ᴹ_ + *ᴹ-zeroʳ : AD'.RightZero (0ᴹ {n}) _*ᴹ_ + *ᴹ-zero : AD'.Zero (0ᴹ {n}) _*ᴹ_ + *ᴹ-+ᴹ-distribˡ : (_*ᴹ_ {n}) AD'.DistributesOverˡ _+ᴹ_ + *ᴹ-+ᴹ-distribʳ : (_*ᴹ_ {n}) AD'.DistributesOverʳ _+ᴹ_ + *ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ ``` * Added structures in `Data.Vec.Functional.Algebra.Properties` ```agda isMagma : IsMagma (_+ᴹ_ {n}) + *ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) isSemigroup : IsSemigroup (_+ᴹ_ {n}) + *ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ + *ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ - isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ - isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ + isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + +ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isSemiring : IsSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isRingWithoutOne : IsRingWithoutOne (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ + +ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isCommutativeRing : IsCommutativeRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ ``` * Added bundles in `Data.Vec.Functional.Algebra.Properties` ```agda magma : ℕ → Magma _ _ + *ᴹ-magma : ℕ → Magma _ _ + commutativeMagma : ℕ → CommutativeMagma _ _ semigroup : ℕ → Semigroup _ _ + *ᴹ-semigroup : ℕ → Semigroup _ _ + commutativeSemigroup : ℕ → CommutativeSemigroup _ _ monoid : ℕ → Monoid _ _ + *ᴹ-monoid : ℕ → Monoid _ _ commutativeMonoid : ℕ → CommutativeMonoid _ _ + group : ℕ → Group _ _ leftSemimodule : ℕ → LeftSemimodule _ _ _ leftModule : ℕ → LeftModule _ _ _ - commutativeMagma : ℕ → CommutativeMagma _ _ - group : ℕ → Group _ _ bisemimodule : ℕ → Bisemimodule _ _ _ _ rightModule : ℕ → RightModule _ _ _ bimodule : ℕ → Bimodule _ _ _ _ module' : ℕ → Module _ _ _ + +ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ + +ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ + +ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ + +ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ + +ᴹ-*-semiring : ℕ → Semiring _ _ + +ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ + +ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ ``` diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index fbb466429c..9723233dd4 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -54,6 +54,9 @@ module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n}) +ᴹ-comm : Commutative (_+ᴹ_ {n}) +ᴹ-comm xs ys i = +-comm (xs i) (ys i) +*ᴹ-comm : Commutative (_*ᴹ_ {n}) +*ᴹ-comm xs ys i = *-comm (xs i) (ys i) + +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ +ᴹ-identityˡ xs i = +-identityˡ (xs i) @@ -156,6 +159,12 @@ isMagma = record ; ∙-cong = +ᴹ-cong } +*ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) +*ᴹ-isMagma = record + { isEquivalence = ≋-isEquivalence _ + ; ∙-cong = *ᴹ-cong + } + isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) isCommutativeMagma = record { isMagma = isMagma @@ -168,6 +177,12 @@ isSemigroup = record ; assoc = +ᴹ-assoc } +*ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) +*ᴹ-isSemigroup = record + { isMagma = *ᴹ-isMagma + ; assoc = *ᴹ-assoc + } + isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) isCommutativeSemigroup = record { isSemigroup = isSemigroup @@ -180,6 +195,12 @@ isMonoid = record ; identity = +ᴹ-identity } +*ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ +*ᴹ-isMonoid = record + { isSemigroup = *ᴹ-isSemigroup + ; identity = *ᴹ-identity + } + isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ isCommutativeMonoid = record { isMonoid = isMonoid @@ -267,6 +288,60 @@ isModule = record { isBimodule = isBimodule } ++ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ ++ᴹ-*-isNearSemiring = record + { +-isMonoid = isMonoid + ; *-cong = *ᴹ-cong + ; *-assoc = *ᴹ-assoc + ; distribʳ = *ᴹ-+ᴹ-distribʳ + ; zeroˡ = *ᴹ-zeroˡ + } + ++ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ ++ᴹ-*-isSemiringWithoutOne = record + { +-isCommutativeMonoid = isCommutativeMonoid + ; *-cong = *ᴹ-cong + ; *-assoc = *ᴹ-assoc + ; distrib = *ᴹ-+ᴹ-distrib + ; zero = *ᴹ-zero + } + ++ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ ++ᴹ-*-isCommutativeSemiringWithoutOne = record + {isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne + ; *-comm = *ᴹ-comm + } + ++ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ ++ᴹ-*-isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = isCommutativeMonoid + ; *-cong = *ᴹ-cong + ; *-assoc = *ᴹ-assoc + ; *-identity = *ᴹ-identity + ; distrib = *ᴹ-+ᴹ-distrib + } + ++ᴹ-*-isSemiring : IsSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ ++ᴹ-*-isSemiring = record + { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero + ; zero = *ᴹ-zero + } + ++ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ ++ᴹ-*-isCommutativeSemiring = record + { isSemiring = +ᴹ-*-isSemiring + ; *-comm = *ᴹ-comm + } + ++ᴹ-*-isRingWithoutOne : IsRingWithoutOne (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ ++ᴹ-*-isRingWithoutOne = record + { +-isAbelianGroup = isAbelianGroup + ; *-cong = *ᴹ-cong + ; *-assoc = *ᴹ-assoc + ; distrib = *ᴹ-+ᴹ-distrib + ; zero = *ᴹ-zero + } + +ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ +ᴹ-*-isRing = record { +-isAbelianGroup = isAbelianGroup @@ -277,6 +352,12 @@ isModule = record ; zero = *ᴹ-zero } ++ᴹ-*-isCommutativeRing : IsCommutativeRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ ++ᴹ-*-isCommutativeRing = record + { isRing = +ᴹ-*-isRing + ; *-comm = *ᴹ-comm + } + ------------------------------------------------------------------------ -- Bundles @@ -285,6 +366,11 @@ magma n = record { isMagma = isMagma {n} } +*ᴹ-magma : ℕ → Magma _ _ +*ᴹ-magma n = record + { isMagma = *ᴹ-isMagma {n} + } + commutativeMagma : ℕ → CommutativeMagma _ _ commutativeMagma n = record { isCommutativeMagma = isCommutativeMagma {n} @@ -295,6 +381,11 @@ semigroup n = record { isSemigroup = isSemigroup {n} } +*ᴹ-semigroup : ℕ → Semigroup _ _ +*ᴹ-semigroup n = record + { isSemigroup = *ᴹ-isSemigroup {n} + } + commutativeSemigroup : ℕ → CommutativeSemigroup _ _ commutativeSemigroup n = record { isCommutativeSemigroup = isCommutativeSemigroup {n} @@ -305,6 +396,11 @@ monoid n = record { isMonoid = isMonoid {n} } +*ᴹ-monoid : ℕ → Monoid _ _ +*ᴹ-monoid n = record + { isMonoid = *ᴹ-isMonoid {n} + } + commutativeMonoid : ℕ → CommutativeMonoid _ _ commutativeMonoid n = record { isCommutativeMonoid = isCommutativeMonoid {n} @@ -344,3 +440,38 @@ module' : ℕ → Module _ _ _ module' n = record { isModule = isModule {n} } + ++ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ ++ᴹ-*-nearSemiring n = record + { isNearSemiring = +ᴹ-*-isNearSemiring {n} + } + ++ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ ++ᴹ-*-semiringWithoutOne n = record + { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne {n} + } + ++ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ ++ᴹ-*-commutativeSemiringWithoutOne n = record + { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne {n} + } + ++ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ ++ᴹ-*-semiringWithoutAnnihilatingZero n = record + { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero {n} + } + ++ᴹ-*-semiring : ℕ → Semiring _ _ ++ᴹ-*-semiring n = record + { isSemiring = +ᴹ-*-isSemiring {n} + } + ++ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ ++ᴹ-*-commutativeSemiring n = record + { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring {n} + } + ++ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ ++ᴹ-*-ringWithoutOne n = record + { isRingWithoutOne = +ᴹ-*-isRingWithoutOne {n} + } From 6604b6ed35e232e8e2cd1be0ef8e2de8fa5f75d2 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Wed, 17 May 2023 22:01:47 -0300 Subject: [PATCH 13/25] changed the code to be more general --- src/Data/Vec/Functional/Algebra/Base.agda | 48 +- .../Vec/Functional/Algebra/Properties.agda | 842 +++++++++--------- 2 files changed, 459 insertions(+), 431 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index ea5898114c..7b59b58df4 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -6,6 +6,9 @@ {-# OPTIONS --cubical-compatible --safe #-} +module Data.Vec.Functional.Algebra.Base where + +open import Level using (Level) open import Function using (_$_) open import Data.Product hiding (map) open import Data.Nat using (ℕ) @@ -19,35 +22,40 @@ import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid import Algebra.Definitions as AD import Algebra.Structures as AS -module Data.Vec.Functional.Algebra.Base - {c ℓ} (cring : CommutativeRing c ℓ) where + -- {c ℓ} (cring : CommutativeRing c ℓ) where private variable + a ℓ : Level + A : Set ℓ n : ℕ -open CommutativeRing cring -open VecSetoid setoid +-- open CommutativeRing cring +-- open VecSetoid setoid + +module EqualityVecFunc (S : Setoid a ℓ) where + open Setoid S + open VecSetoid S -_≈ᴹ_ : Rel (Vector Carrier n) ℓ -_≈ᴹ_ = _≋_ + _≈ᴹ_ : Rel (Vector Carrier n) ℓ + _≈ᴹ_ = _≋_ -_+ᴹ_ : Op₂ $ Vector Carrier n -_+ᴹ_ = zipWith _+_ +_+ᴹ_ : (_+_ : Op₂ A) → Op₂ $ Vector A n +_+ᴹ_ _+_ = zipWith _+_ -_*ᴹ_ : Op₂ $ Vector Carrier n -_*ᴹ_ = zipWith _*_ +_*ᴹ_ : (_*_ : Op₂ A) → Op₂ $ Vector A n +_*ᴹ_ _*_ = zipWith _*_ -0ᴹ : Vector Carrier n -0ᴹ = replicate 0# +0ᴹ : A → Vector A n +0ᴹ 0# = replicate 0# -1ᴹ : Vector Carrier n -1ᴹ = replicate 1# +1ᴹ : A → Vector A n +1ᴹ 1# = replicate 1# --ᴹ_ : Op₁ $ Vector Carrier n --ᴹ_ = map $ -_ +-ᴹ_ : Op₁ A → Op₁ $ Vector A n +-ᴹ_ -_ = map $ -_ -_*ₗ_ : Opₗ Carrier (Vector Carrier n) -_*ₗ_ r = map (r *_) +_*ₗ_ : Op₂ A → Opₗ A (Vector A n) +_*ₗ_ _*_ r = map (r *_) -_*ᵣ_ : Opᵣ Carrier (Vector Carrier n) -xs *ᵣ r = map (_* r) xs +_*ᵣ_ : Op₂ A → Opᵣ A (Vector A n) +_*ᵣ_ _*_ xs r = map (_* r) xs diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 9723233dd4..37f065d8fa 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -6,6 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} +open import Level using (Level) open import Function using (_$_) open import Data.Product hiding (map) open import Data.Nat using (ℕ) @@ -16,462 +17,481 @@ open import Algebra.Bundles open import Algebra.Module open import Relation.Binary import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid -import Algebra.Definitions as AD +open import Algebra.Definitions import Algebra.Structures as AS -import Data.Vec.Functional.Algebra.Base as VFA +import Data.Vec.Functional.Algebra.Base as AB -module Data.Vec.Functional.Algebra.Properties - {c ℓ} (cring : CommutativeRing c ℓ) where +module Data.Vec.Functional.Algebra.Properties {a ℓ} (S : Setoid a ℓ) where + -- {c ℓ} (cring : CommutativeRing c ℓ) where private variable n : ℕ -open CommutativeRing cring -open VecSetoid setoid -open VFA cring -module SR = Semiring semiring -open module AD' {n} = AD (_≈ᴹ_ {n}) -open module AS' {n} = AS (_≈ᴹ_ {n}) -module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) -module RD {n} = RightDefs Carrier (_≈ᴹ_ {n}) -module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n}) +open Setoid S renaming (Carrier to A) +open VecSetoid S +open AB.EqualityVecFunc S + +-- open CommutativeRing cring +-- open AD +-- module SR = Semiring semiring +-- open module AD' {n} = AD (_≈ᴹ_ setoid {n}) +-- open module AS' {n} = AS (_≈ᴹ_ setoid {n}) +-- module LD {n} = LeftDefs Carrier (_≈ᴹ_ setoid {n}) +-- module RD {n} = RightDefs Carrier (_≈ᴹ_ setoid {n}) +-- module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ setoid {n}) ------------------------------------------------------------------------ -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ -+ᴹ-cong : Congruent₂ (_+ᴹ_ {n}) -+ᴹ-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) +module AddProperties (_+_ : Op₂ A) where + private + _+ᴹ_ : Op₂ $ Vector A n + _+ᴹ_ = AB._+ᴹ_ _+_ -*ᴹ-cong : Congruent₂ (_*ᴹ_ {n}) -*ᴹ-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) + +ᴹ-cong : Congruent₂ _≈_ _+_ → Congruent₂ _≈ᴹ_ (_+ᴹ_ {n = n}) + +ᴹ-cong +-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) -+ᴹ-assoc : Associative (_+ᴹ_ {n}) -+ᴹ-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) + +ᴹ-assoc : Associative _≈_ _+_ → Associative _≈ᴹ_ (_+ᴹ_ {n}) + +ᴹ-assoc +-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) -*ᴹ-assoc : Associative (_*ᴹ_ {n}) -*ᴹ-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) + +ᴹ-comm : Commutative _≈_ _+_ → Commutative _≈ᴹ_ (_+ᴹ_ {n}) + +ᴹ-comm +-comm xs ys i = +-comm (xs i) (ys i) -+ᴹ-comm : Commutative (_+ᴹ_ {n}) -+ᴹ-comm xs ys i = +-comm (xs i) (ys i) + module ZeroProperties (0# : A) where + private + 0ᴹ : Vector A n + 0ᴹ = AB.0ᴹ 0# -*ᴹ-comm : Commutative (_*ᴹ_ {n}) -*ᴹ-comm xs ys i = *-comm (xs i) (ys i) + +ᴹ-identityˡ : LeftIdentity _≈_ 0# _+_ → LeftIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityˡ +-identityˡ xs i = +-identityˡ (xs i) -+ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_ -+ᴹ-identityˡ xs i = +-identityˡ (xs i) + +ᴹ-identityʳ : RightIdentity _≈_ 0# _+_ → RightIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityʳ +-identityʳ xs is = +-identityʳ (xs is) -*ᴹ-identityˡ : LeftIdentity (1ᴹ {n}) _*ᴹ_ -*ᴹ-identityˡ xs i = *-identityˡ (xs i) + +ᴹ-identity : Identity _≈_ 0# _+_ → Identity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ -+ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_ -+ᴹ-identityʳ xs is = +-identityʳ (xs is) + module NegativeProperties (-_ : Op₁ A) where + private + -ᴹ_ : Op₁ $ Vector A n + -ᴹ_ = AB.-ᴹ_ -_ -*ᴹ-identityʳ : RightIdentity (1ᴹ {n}) _*ᴹ_ -*ᴹ-identityʳ xs is = *-identityʳ (xs is) + -ᴹ‿inverseˡ : LeftInverse _≈_ 0# -_ _+_ → LeftInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) -+ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_ -+ᴹ-identity = +ᴹ-identityˡ , +ᴹ-identityʳ + -ᴹ‿inverseʳ : RightInverse _≈_ 0# -_ _+_ → RightInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) -*ᴹ-identity : Identity (1ᴹ {n}) _*ᴹ_ -*ᴹ-identity = *ᴹ-identityˡ , *ᴹ-identityʳ + -ᴹ‿inverse : Inverse _≈_ 0# -_ _+_ → Inverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ --ᴹ‿cong : Congruent₁ (-ᴹ_ {n}) --ᴹ‿cong xs i = -‿cong (xs i) --ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ --ᴹ‿inverseˡ xs i = -‿inverseˡ (xs i) +module NegativeProperties (-_ : Op₁ A) where + private + -ᴹ_ : Op₁ $ Vector A n + -ᴹ_ = AB.-ᴹ_ -_ --ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ --ᴹ‿inverseʳ xs i = -‿inverseʳ (xs i) + -ᴹ‿cong : Congruent₁ _≈_ -_ → Congruent₁ _≈ᴹ_ (-ᴹ_ {n}) + -ᴹ‿cong -‿cong xs i = -‿cong (xs i) --ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ --ᴹ‿inverse = -ᴹ‿inverseˡ , -ᴹ‿inverseʳ -*ₗ-cong : LD.Congruent SR._≈_ (_*ₗ_ {n}) -*ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) +-- *ₗ-cong : LD.Congruent SR._≈_ (_*ₗ_ {n}) +-- *ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) -*ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ -*ₗ-zeroˡ xs i = zeroˡ (xs i) +-- *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ +-- *ₗ-zeroˡ xs i = zeroˡ (xs i) -*ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) -*ₗ-distribʳ xs m n i = distribʳ (xs i) m n +-- *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) +-- *ₗ-distribʳ xs m n i = distribʳ (xs i) m n -*ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) -*ₗ-identityˡ xs i = *-identityˡ (xs i) +-- *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) +-- *ₗ-identityˡ xs i = *-identityˡ (xs i) -*ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) -*ₗ-assoc m n xs i = *-assoc m n (xs i) +-- *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) +-- *ₗ-assoc m n xs i = *-assoc m n (xs i) -*ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ -*ₗ-zeroʳ m _ = zeroʳ m +-- *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ +-- *ₗ-zeroʳ m _ = zeroʳ m -*ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) -*ₗ-distribˡ m xs ys i = distribˡ m (xs i) (ys i) +-- *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) +-- *ₗ-distribˡ m xs ys i = distribˡ m (xs i) (ys i) -*ᵣ-cong : RD.Congruent SR._≈_ (_*ᵣ_ {n}) -*ᵣ-cong x≈y u≈v i = *-cong (x≈y i) u≈v +-- *ᵣ-cong : RD.Congruent SR._≈_ (_*ᵣ_ {n}) +-- *ᵣ-cong x≈y u≈v i = *-cong (x≈y i) u≈v -*ᵣ-distribˡ : _*ᵣ_ RD.DistributesOverˡ SR._+_ ⟶ (_+ᴹ_ {n}) -*ᵣ-distribˡ xs m n i = distribˡ (xs i) m n +-- *ᵣ-distribˡ : _*ᵣ_ RD.DistributesOverˡ SR._+_ ⟶ (_+ᴹ_ {n}) +-- *ᵣ-distribˡ xs m n i = distribˡ (xs i) m n -*ᵣ-zeroˡ : RD.LeftZero (0ᴹ {n}) _*ᵣ_ -*ᵣ-zeroˡ xs i = zeroˡ xs +-- *ᵣ-zeroˡ : RD.LeftZero (0ᴹ {n}) _*ᵣ_ +-- *ᵣ-zeroˡ xs i = zeroˡ xs -*ᵣ-identityʳ : RD.RightIdentity SR.1# (_*ᵣ_ {n}) -*ᵣ-identityʳ xs i = *-identityʳ (xs i) +-- *ᵣ-identityʳ : RD.RightIdentity SR.1# (_*ᵣ_ {n}) +-- *ᵣ-identityʳ xs i = *-identityʳ (xs i) -*ᵣ-assoc : RD.Associative SR._*_ (_*ᵣ_ {n}) -*ᵣ-assoc xs m n i = *-assoc (xs i) m n +-- *ᵣ-assoc : RD.Associative SR._*_ (_*ᵣ_ {n}) +-- *ᵣ-assoc xs m n i = *-assoc (xs i) m n -*ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ -*ᵣ-zeroʳ xs i = zeroʳ (xs i) +-- *ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ +-- *ᵣ-zeroʳ xs i = zeroʳ (xs i) -*ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) -*ᵣ-distribʳ xs m n i = distribʳ xs (m i) (n i) +-- *ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) +-- *ᵣ-distribʳ xs m n i = distribʳ xs (m i) (n i) -*ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ -*ₗ-*ᵣ-assoc m xs n i = *-assoc m (xs i) n +-- *ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ +-- *ₗ-*ᵣ-assoc m xs n i = *-assoc m (xs i) n -*ᴹ-zeroˡ : AD'.LeftZero (0ᴹ {n}) _*ᴹ_ -*ᴹ-zeroˡ xs i = zeroˡ (xs i) +-- *ᴹ-zeroˡ : AD'.LeftZero (0ᴹ {n}) _*ᴹ_ +-- *ᴹ-zeroˡ xs i = zeroˡ (xs i) -*ᴹ-zeroʳ : AD'.RightZero (0ᴹ {n}) _*ᴹ_ -*ᴹ-zeroʳ xs i = zeroʳ (xs i) +-- *ᴹ-zeroʳ : AD'.RightZero (0ᴹ {n}) _*ᴹ_ +-- *ᴹ-zeroʳ xs i = zeroʳ (xs i) -*ᴹ-zero : AD'.Zero (0ᴹ {n}) _*ᴹ_ -*ᴹ-zero = *ᴹ-zeroˡ , *ᴹ-zeroʳ +-- *ᴹ-zero : AD'.Zero (0ᴹ {n}) _*ᴹ_ +-- *ᴹ-zero = *ᴹ-zeroˡ , *ᴹ-zeroʳ -*ᴹ-+ᴹ-distribˡ : (_*ᴹ_ {n}) AD'.DistributesOverˡ _+ᴹ_ -*ᴹ-+ᴹ-distribˡ xs ys zs i = distribˡ (xs i) (ys i) (zs i) +-- *ᴹ-+ᴹ-distribˡ : (_*ᴹ_ {n}) AD'.DistributesOverˡ _+ᴹ_ +-- *ᴹ-+ᴹ-distribˡ xs ys zs i = distribˡ (xs i) (ys i) (zs i) -*ᴹ-+ᴹ-distribʳ : (_*ᴹ_ {n}) AD'.DistributesOverʳ _+ᴹ_ -*ᴹ-+ᴹ-distribʳ xs ys zs i = distribʳ (xs i) (ys i) (zs i) +-- *ᴹ-+ᴹ-distribʳ : (_*ᴹ_ {n}) AD'.DistributesOverʳ _+ᴹ_ +-- *ᴹ-+ᴹ-distribʳ xs ys zs i = distribʳ (xs i) (ys i) (zs i) -*ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ -*ᴹ-+ᴹ-distrib = *ᴹ-+ᴹ-distribˡ , *ᴹ-+ᴹ-distribʳ +-- *ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ +-- *ᴹ-+ᴹ-distrib = *ᴹ-+ᴹ-distribˡ , *ᴹ-+ᴹ-distribʳ ------------------------------------------------------------------------- --- Structures - -isMagma : IsMagma (_+ᴹ_ {n}) -isMagma = record - { isEquivalence = ≋-isEquivalence _ - ; ∙-cong = +ᴹ-cong - } - -*ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) -*ᴹ-isMagma = record - { isEquivalence = ≋-isEquivalence _ - ; ∙-cong = *ᴹ-cong - } - -isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) -isCommutativeMagma = record - { isMagma = isMagma - ; comm = +ᴹ-comm - } - -isSemigroup : IsSemigroup (_+ᴹ_ {n}) -isSemigroup = record - { isMagma = isMagma - ; assoc = +ᴹ-assoc - } - -*ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) -*ᴹ-isSemigroup = record - { isMagma = *ᴹ-isMagma - ; assoc = *ᴹ-assoc - } - -isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) -isCommutativeSemigroup = record - { isSemigroup = isSemigroup - ; comm = +ᴹ-comm - } - -isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ -isMonoid = record - { isSemigroup = isSemigroup - ; identity = +ᴹ-identity - } - -*ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ -*ᴹ-isMonoid = record - { isSemigroup = *ᴹ-isSemigroup - ; identity = *ᴹ-identity - } - -isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ -isCommutativeMonoid = record - { isMonoid = isMonoid - ; comm = +ᴹ-comm - } - -isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ -isGroup = record - { isMonoid = isMonoid - ; inverse = -ᴹ‿inverse - ; ⁻¹-cong = -ᴹ‿cong - } - -isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ -isAbelianGroup = record - { isGroup = isGroup - ; comm = +ᴹ-comm - } - -isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ -isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ - } - -isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ -isPrerightSemimodule = record - { *ᵣ-cong = *ᵣ-cong - ; *ᵣ-zeroʳ = *ᵣ-zeroʳ - ; *ᵣ-distribˡ = *ᵣ-distribˡ - ; *ᵣ-identityʳ = *ᵣ-identityʳ - ; *ᵣ-assoc = *ᵣ-assoc - ; *ᵣ-zeroˡ = *ᵣ-zeroˡ - ; *ᵣ-distribʳ = *ᵣ-distribʳ - } - -isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ -isRightSemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid - ; isPrerightSemimodule = isPrerightSemimodule - } - -isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ -isBisemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid - ; isPreleftSemimodule = isPreleftSemimodule - ; isPrerightSemimodule = isPrerightSemimodule - ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc - } - -isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ -isRightModule = record - { isRightSemimodule = isRightSemimodule - ; -ᴹ‿cong = -ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse - } - -isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ -isBimodule = record - { isBisemimodule = isBisemimodule - ; -ᴹ‿cong = -ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse - } - -isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ -isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid - ; isPreleftSemimodule = isPreleftSemimodule - } - -isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ -isLeftModule = record - { isLeftSemimodule = isLeftSemimodule - ; -ᴹ‿cong = -ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse - } - -isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ -isModule = record - { isBimodule = isBimodule - } - -+ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ -+ᴹ-*-isNearSemiring = record - { +-isMonoid = isMonoid - ; *-cong = *ᴹ-cong - ; *-assoc = *ᴹ-assoc - ; distribʳ = *ᴹ-+ᴹ-distribʳ - ; zeroˡ = *ᴹ-zeroˡ - } - -+ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ -+ᴹ-*-isSemiringWithoutOne = record - { +-isCommutativeMonoid = isCommutativeMonoid - ; *-cong = *ᴹ-cong - ; *-assoc = *ᴹ-assoc - ; distrib = *ᴹ-+ᴹ-distrib - ; zero = *ᴹ-zero - } - -+ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ -+ᴹ-*-isCommutativeSemiringWithoutOne = record - {isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne - ; *-comm = *ᴹ-comm - } - -+ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ -+ᴹ-*-isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = isCommutativeMonoid - ; *-cong = *ᴹ-cong - ; *-assoc = *ᴹ-assoc - ; *-identity = *ᴹ-identity - ; distrib = *ᴹ-+ᴹ-distrib - } - -+ᴹ-*-isSemiring : IsSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ -+ᴹ-*-isSemiring = record - { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero - ; zero = *ᴹ-zero - } - -+ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ -+ᴹ-*-isCommutativeSemiring = record - { isSemiring = +ᴹ-*-isSemiring - ; *-comm = *ᴹ-comm - } - -+ᴹ-*-isRingWithoutOne : IsRingWithoutOne (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ -+ᴹ-*-isRingWithoutOne = record - { +-isAbelianGroup = isAbelianGroup - ; *-cong = *ᴹ-cong - ; *-assoc = *ᴹ-assoc - ; distrib = *ᴹ-+ᴹ-distrib - ; zero = *ᴹ-zero - } - -+ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ -+ᴹ-*-isRing = record - { +-isAbelianGroup = isAbelianGroup - ; *-cong = *ᴹ-cong - ; *-assoc = *ᴹ-assoc - ; *-identity = *ᴹ-identity - ; distrib = *ᴹ-+ᴹ-distrib - ; zero = *ᴹ-zero - } - -+ᴹ-*-isCommutativeRing : IsCommutativeRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ -+ᴹ-*-isCommutativeRing = record - { isRing = +ᴹ-*-isRing - ; *-comm = *ᴹ-comm - } +module MultiplicationProperties (_*_ : Op₂ A) where + _*ᴹ_ : Op₂ $ Vector A n + _*ᴹ_ {n = n} = AB._*ᴹ_ {n = n} _*_ ------------------------------------------------------------------------- --- Bundles - -magma : ℕ → Magma _ _ -magma n = record - { isMagma = isMagma {n} - } - -*ᴹ-magma : ℕ → Magma _ _ -*ᴹ-magma n = record - { isMagma = *ᴹ-isMagma {n} - } - -commutativeMagma : ℕ → CommutativeMagma _ _ -commutativeMagma n = record { - isCommutativeMagma = isCommutativeMagma {n} - } - -semigroup : ℕ → Semigroup _ _ -semigroup n = record - { isSemigroup = isSemigroup {n} - } - -*ᴹ-semigroup : ℕ → Semigroup _ _ -*ᴹ-semigroup n = record - { isSemigroup = *ᴹ-isSemigroup {n} - } - -commutativeSemigroup : ℕ → CommutativeSemigroup _ _ -commutativeSemigroup n = record - { isCommutativeSemigroup = isCommutativeSemigroup {n} - } - -monoid : ℕ → Monoid _ _ -monoid n = record - { isMonoid = isMonoid {n} - } - -*ᴹ-monoid : ℕ → Monoid _ _ -*ᴹ-monoid n = record - { isMonoid = *ᴹ-isMonoid {n} - } - -commutativeMonoid : ℕ → CommutativeMonoid _ _ -commutativeMonoid n = record - { isCommutativeMonoid = isCommutativeMonoid {n} - } - -group : ℕ → Group _ _ -group n = record - { isGroup = isGroup {n} - } - -leftSemimodule : ℕ → LeftSemimodule _ _ _ -leftSemimodule n = record - { isLeftSemimodule = isLeftSemimodule {n} - } - -leftModule : ℕ → LeftModule _ _ _ -leftModule n = record - { isLeftModule = isLeftModule {n} - } - -bisemimodule : ℕ → Bisemimodule _ _ _ _ -bisemimodule n = record - { isBisemimodule = isBisemimodule {n} - } - -rightModule : ℕ → RightModule _ _ _ -rightModule n = record - { isRightModule = isRightModule {n} - } - -bimodule : ℕ → Bimodule _ _ _ _ -bimodule n = record - { isBimodule = isBimodule {n} - } - -module' : ℕ → Module _ _ _ -module' n = record - { isModule = isModule {n} - } - -+ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ -+ᴹ-*-nearSemiring n = record - { isNearSemiring = +ᴹ-*-isNearSemiring {n} - } - -+ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ -+ᴹ-*-semiringWithoutOne n = record - { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne {n} - } - -+ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ -+ᴹ-*-commutativeSemiringWithoutOne n = record - { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne {n} - } - -+ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ -+ᴹ-*-semiringWithoutAnnihilatingZero n = record - { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero {n} - } - -+ᴹ-*-semiring : ℕ → Semiring _ _ -+ᴹ-*-semiring n = record - { isSemiring = +ᴹ-*-isSemiring {n} - } - -+ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ -+ᴹ-*-commutativeSemiring n = record - { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring {n} - } - -+ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ -+ᴹ-*-ringWithoutOne n = record - { isRingWithoutOne = +ᴹ-*-isRingWithoutOne {n} - } + -- *ᴹ-cong : Congruent₂ _≈_ _*_ → Congruent₂ _≈ᴹ_ (_*ᴹ_ {n = n}) + -- *ᴹ-cong *-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) + + -- *ᴹ-assoc : Associative (_*ᴹ_ {n}) + -- *ᴹ-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) + + + +-- ------------------------------------------------------------------------ +-- -- Structures + +-- isMagma : IsMagma (_+ᴹ_ {n}) +-- isMagma = record +-- { isEquivalence = ≋-isEquivalence _ +-- ; ∙-cong = +ᴹ-cong +-- } + +-- *ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) +-- *ᴹ-isMagma = record +-- { isEquivalence = ≋-isEquivalence _ +-- ; ∙-cong = *ᴹ-cong +-- } + +-- isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) +-- isCommutativeMagma = record +-- { isMagma = isMagma +-- ; comm = +ᴹ-comm +-- } + +-- isSemigroup : IsSemigroup (_+ᴹ_ {n}) +-- isSemigroup = record +-- { isMagma = isMagma +-- ; assoc = +ᴹ-assoc +-- } + +-- *ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) +-- *ᴹ-isSemigroup = record +-- { isMagma = *ᴹ-isMagma +-- ; assoc = *ᴹ-assoc +-- } + +-- isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) +-- isCommutativeSemigroup = record +-- { isSemigroup = isSemigroup +-- ; comm = +ᴹ-comm +-- } + +-- isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ +-- isMonoid = record +-- { isSemigroup = isSemigroup +-- ; identity = +ᴹ-identity +-- } + +-- *ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ +-- *ᴹ-isMonoid = record +-- { isSemigroup = *ᴹ-isSemigroup +-- ; identity = *ᴹ-identity +-- } + +-- isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ +-- isCommutativeMonoid = record +-- { isMonoid = isMonoid +-- ; comm = +ᴹ-comm +-- } + +-- isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ +-- isGroup = record +-- { isMonoid = isMonoid +-- ; inverse = -ᴹ‿inverse +-- ; ⁻¹-cong = -ᴹ‿cong +-- } + +-- isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ +-- isAbelianGroup = record +-- { isGroup = isGroup +-- ; comm = +ᴹ-comm +-- } + +-- isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ +-- isPreleftSemimodule = record +-- { *ₗ-cong = *ₗ-cong +-- ; *ₗ-zeroˡ = *ₗ-zeroˡ +-- ; *ₗ-distribʳ = *ₗ-distribʳ +-- ; *ₗ-identityˡ = *ₗ-identityˡ +-- ; *ₗ-assoc = *ₗ-assoc +-- ; *ₗ-zeroʳ = *ₗ-zeroʳ +-- ; *ₗ-distribˡ = *ₗ-distribˡ +-- } + +-- isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ +-- isPrerightSemimodule = record +-- { *ᵣ-cong = *ᵣ-cong +-- ; *ᵣ-zeroʳ = *ᵣ-zeroʳ +-- ; *ᵣ-distribˡ = *ᵣ-distribˡ +-- ; *ᵣ-identityʳ = *ᵣ-identityʳ +-- ; *ᵣ-assoc = *ᵣ-assoc +-- ; *ᵣ-zeroˡ = *ᵣ-zeroˡ +-- ; *ᵣ-distribʳ = *ᵣ-distribʳ +-- } + +-- isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ +-- isRightSemimodule = record +-- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-- ; isPrerightSemimodule = isPrerightSemimodule +-- } + +-- isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ +-- isBisemimodule = record +-- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-- ; isPreleftSemimodule = isPreleftSemimodule +-- ; isPrerightSemimodule = isPrerightSemimodule +-- ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc +-- } + +-- isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ +-- isRightModule = record +-- { isRightSemimodule = isRightSemimodule +-- ; -ᴹ‿cong = -ᴹ‿cong +-- ; -ᴹ‿inverse = -ᴹ‿inverse +-- } + +-- isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ +-- isBimodule = record +-- { isBisemimodule = isBisemimodule +-- ; -ᴹ‿cong = -ᴹ‿cong +-- ; -ᴹ‿inverse = -ᴹ‿inverse +-- } + +-- isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ +-- isLeftSemimodule = record +-- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-- ; isPreleftSemimodule = isPreleftSemimodule +-- } + +-- isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ +-- isLeftModule = record +-- { isLeftSemimodule = isLeftSemimodule +-- ; -ᴹ‿cong = -ᴹ‿cong +-- ; -ᴹ‿inverse = -ᴹ‿inverse +-- } + +-- isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ +-- isModule = record +-- { isBimodule = isBimodule +-- } + +-- +ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ +-- +ᴹ-*-isNearSemiring = record +-- { +-isMonoid = isMonoid +-- ; *-cong = *ᴹ-cong +-- ; *-assoc = *ᴹ-assoc +-- ; distribʳ = *ᴹ-+ᴹ-distribʳ +-- ; zeroˡ = *ᴹ-zeroˡ +-- } + +-- +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ +-- +ᴹ-*-isSemiringWithoutOne = record +-- { +-isCommutativeMonoid = isCommutativeMonoid +-- ; *-cong = *ᴹ-cong +-- ; *-assoc = *ᴹ-assoc +-- ; distrib = *ᴹ-+ᴹ-distrib +-- ; zero = *ᴹ-zero +-- } + +-- +ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ +-- +ᴹ-*-isCommutativeSemiringWithoutOne = record +-- {isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne +-- ; *-comm = *ᴹ-comm +-- } + +-- +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ +-- +ᴹ-*-isSemiringWithoutAnnihilatingZero = record +-- { +-isCommutativeMonoid = isCommutativeMonoid +-- ; *-cong = *ᴹ-cong +-- ; *-assoc = *ᴹ-assoc +-- ; *-identity = *ᴹ-identity +-- ; distrib = *ᴹ-+ᴹ-distrib +-- } + +-- +ᴹ-*-isSemiring : IsSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ +-- +ᴹ-*-isSemiring = record +-- { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero +-- ; zero = *ᴹ-zero +-- } + +-- +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ +-- +ᴹ-*-isCommutativeSemiring = record +-- { isSemiring = +ᴹ-*-isSemiring +-- ; *-comm = *ᴹ-comm +-- } + +-- +ᴹ-*-isRingWithoutOne : IsRingWithoutOne (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ +-- +ᴹ-*-isRingWithoutOne = record +-- { +-isAbelianGroup = isAbelianGroup +-- ; *-cong = *ᴹ-cong +-- ; *-assoc = *ᴹ-assoc +-- ; distrib = *ᴹ-+ᴹ-distrib +-- ; zero = *ᴹ-zero +-- } + +-- +ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ +-- +ᴹ-*-isRing = record +-- { +-isAbelianGroup = isAbelianGroup +-- ; *-cong = *ᴹ-cong +-- ; *-assoc = *ᴹ-assoc +-- ; *-identity = *ᴹ-identity +-- ; distrib = *ᴹ-+ᴹ-distrib +-- ; zero = *ᴹ-zero +-- } + +-- +ᴹ-*-isCommutativeRing : IsCommutativeRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ +-- +ᴹ-*-isCommutativeRing = record +-- { isRing = +ᴹ-*-isRing +-- ; *-comm = *ᴹ-comm +-- } + +-- ------------------------------------------------------------------------ +-- -- Bundles + +-- magma : ℕ → Magma _ _ +-- magma n = record +-- { isMagma = isMagma {n} +-- } + +-- *ᴹ-magma : ℕ → Magma _ _ +-- *ᴹ-magma n = record +-- { isMagma = *ᴹ-isMagma {n} +-- } + +-- commutativeMagma : ℕ → CommutativeMagma _ _ +-- commutativeMagma n = record { +-- isCommutativeMagma = isCommutativeMagma {n} +-- } + +-- semigroup : ℕ → Semigroup _ _ +-- semigroup n = record +-- { isSemigroup = isSemigroup {n} +-- } + +-- *ᴹ-semigroup : ℕ → Semigroup _ _ +-- *ᴹ-semigroup n = record +-- { isSemigroup = *ᴹ-isSemigroup {n} +-- } + +-- commutativeSemigroup : ℕ → CommutativeSemigroup _ _ +-- commutativeSemigroup n = record +-- { isCommutativeSemigroup = isCommutativeSemigroup {n} +-- } + +-- monoid : ℕ → Monoid _ _ +-- monoid n = record +-- { isMonoid = isMonoid {n} +-- } + +-- *ᴹ-monoid : ℕ → Monoid _ _ +-- *ᴹ-monoid n = record +-- { isMonoid = *ᴹ-isMonoid {n} +-- } + +-- commutativeMonoid : ℕ → CommutativeMonoid _ _ +-- commutativeMonoid n = record +-- { isCommutativeMonoid = isCommutativeMonoid {n} +-- } + +-- group : ℕ → Group _ _ +-- group n = record +-- { isGroup = isGroup {n} +-- } + +-- leftSemimodule : ℕ → LeftSemimodule _ _ _ +-- leftSemimodule n = record +-- { isLeftSemimodule = isLeftSemimodule {n} +-- } + +-- leftModule : ℕ → LeftModule _ _ _ +-- leftModule n = record +-- { isLeftModule = isLeftModule {n} +-- } + +-- bisemimodule : ℕ → Bisemimodule _ _ _ _ +-- bisemimodule n = record +-- { isBisemimodule = isBisemimodule {n} +-- } + +-- rightModule : ℕ → RightModule _ _ _ +-- rightModule n = record +-- { isRightModule = isRightModule {n} +-- } + +-- bimodule : ℕ → Bimodule _ _ _ _ +-- bimodule n = record +-- { isBimodule = isBimodule {n} +-- } + +-- module' : ℕ → Module _ _ _ +-- module' n = record +-- { isModule = isModule {n} +-- } + +-- +ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ +-- +ᴹ-*-nearSemiring n = record +-- { isNearSemiring = +ᴹ-*-isNearSemiring {n} +-- } + +-- +ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ +-- +ᴹ-*-semiringWithoutOne n = record +-- { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne {n} +-- } + +-- +ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ +-- +ᴹ-*-commutativeSemiringWithoutOne n = record +-- { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne {n} +-- } + +-- +ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ +-- +ᴹ-*-semiringWithoutAnnihilatingZero n = record +-- { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero {n} +-- } + +-- +ᴹ-*-semiring : ℕ → Semiring _ _ +-- +ᴹ-*-semiring n = record +-- { isSemiring = +ᴹ-*-isSemiring {n} +-- } + +-- +ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ +-- +ᴹ-*-commutativeSemiring n = record +-- { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring {n} +-- } + +-- +ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ +-- +ᴹ-*-ringWithoutOne n = record +-- { isRingWithoutOne = +ᴹ-*-isRingWithoutOne {n} +-- } From bc7d02d999228b96c0efc74397ab1a555ba02878 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 18 May 2023 22:33:05 -0300 Subject: [PATCH 14/25] using rawStructures instead --- src/Data/Vec/Functional/Algebra/Base.agda | 70 +++++++----- .../Vec/Functional/Algebra/Properties.agda | 103 ++++++++---------- 2 files changed, 87 insertions(+), 86 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 7b59b58df4..8da7c91d20 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -10,52 +10,66 @@ module Data.Vec.Functional.Algebra.Base where open import Level using (Level) open import Function using (_$_) -open import Data.Product hiding (map) open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Vec.Functional open import Algebra.Core open import Algebra.Bundles open import Algebra.Module -open import Relation.Binary -import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid -import Algebra.Definitions as AD -import Algebra.Structures as AS - - -- {c ℓ} (cring : CommutativeRing c ℓ) where +open import Relation.Binary using (Rel) +open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) private variable a ℓ : Level A : Set ℓ n : ℕ --- open CommutativeRing cring --- open VecSetoid setoid +module EqualityVecFunc (_≈_ : Rel A ℓ) where + _≈ᴹ_ : Rel (Vector A n) ℓ + _≈ᴹ_ = Pointwise _≈_ + +module VecAddition (_+_ : Op₂ A) where + _+ᴹ_ : Op₂ $ Vector A n + _+ᴹ_ = zipWith _+_ + +module VecMagma (rawMagma : RawMagma a ℓ) where + open RawMagma rawMagma + open VecAddition _∙_ public + open EqualityVecFunc _≈_ public + +module VecMonoid (rawMonoid : RawMonoid a ℓ) where + open RawMonoid rawMonoid + open VecMagma rawMagma public -module EqualityVecFunc (S : Setoid a ℓ) where - open Setoid S - open VecSetoid S + 0ᴹ : Vector Carrier n + 0ᴹ = replicate ε - _≈ᴹ_ : Rel (Vector Carrier n) ℓ - _≈ᴹ_ = _≋_ +module VecGroup (rawGroup : RawGroup a ℓ) where + open RawGroup rawGroup + open VecMonoid rawMonoid public -_+ᴹ_ : (_+_ : Op₂ A) → Op₂ $ Vector A n -_+ᴹ_ _+_ = zipWith _+_ + -ᴹ_ : Op₁ $ Vector Carrier n + -ᴹ_ = map $ _⁻¹ -_*ᴹ_ : (_*_ : Op₂ A) → Op₂ $ Vector A n -_*ᴹ_ _*_ = zipWith _*_ +module VecNearSemiring (rawNearSemiring : RawNearSemiring a ℓ) where + open RawNearSemiring rawNearSemiring + open VecMonoid +-rawMonoid public + open VecMagma *-rawMagma public renaming (_+ᴹ_ to _*ᴹ_) using () -0ᴹ : A → Vector A n -0ᴹ 0# = replicate 0# +module VecSemiring (rawSemiring : RawSemiring a ℓ) where + open RawSemiring rawSemiring + open VecNearSemiring rawNearSemiring public -1ᴹ : A → Vector A n -1ᴹ 1# = replicate 1# + 1ᴹ : Vector Carrier n + 1ᴹ = replicate 1# --ᴹ_ : Op₁ A → Op₁ $ Vector A n --ᴹ_ -_ = map $ -_ + _*ₗ_ : Op₂ A → Opₗ A (Vector A n) + _*ₗ_ _*_ r = map (r *_) -_*ₗ_ : Op₂ A → Opₗ A (Vector A n) -_*ₗ_ _*_ r = map (r *_) + _*ᵣ_ : Op₂ A → Opᵣ A (Vector A n) + _*ᵣ_ _*_ xs r = map (_* r) xs -_*ᵣ_ : Op₂ A → Opᵣ A (Vector A n) -_*ᵣ_ _*_ xs r = map (_* r) xs +module VecRing (rawRing : RawRing a ℓ) where + open RawRing rawRing + open VecGroup +-rawGroup public using (-ᴹ_) + open VecSemiring rawSemiring public diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 37f065d8fa..60d1b3527e 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -6,47 +6,38 @@ {-# OPTIONS --cubical-compatible --safe #-} +module Data.Vec.Functional.Algebra.Properties where + open import Level using (Level) -open import Function using (_$_) +open import Function using (_$_; flip) open import Data.Product hiding (map) open import Data.Nat using (ℕ) -open import Data.Fin using (Fin) +open import Data.Fin using (Fin; zero; suc) open import Data.Vec.Functional open import Algebra.Core open import Algebra.Bundles open import Algebra.Module open import Relation.Binary -import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid open import Algebra.Definitions -import Algebra.Structures as AS -import Data.Vec.Functional.Algebra.Base as AB - -module Data.Vec.Functional.Algebra.Properties {a ℓ} (S : Setoid a ℓ) where - -- {c ℓ} (cring : CommutativeRing c ℓ) where +open import Algebra.Structures +open import Data.Vec.Functional.Algebra.Base +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pointwise private variable + a ℓ : Level + A : Set ℓ n : ℕ -open Setoid S renaming (Carrier to A) -open VecSetoid S -open AB.EqualityVecFunc S - --- open CommutativeRing cring --- open AD --- module SR = Semiring semiring --- open module AD' {n} = AD (_≈ᴹ_ setoid {n}) --- open module AS' {n} = AS (_≈ᴹ_ setoid {n}) --- module LD {n} = LeftDefs Carrier (_≈ᴹ_ setoid {n}) --- module RD {n} = RightDefs Carrier (_≈ᴹ_ setoid {n}) --- module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ setoid {n}) - ------------------------------------------------------------------------ -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ -module AddProperties (_+_ : Op₂ A) where - private - _+ᴹ_ : Op₂ $ Vector A n - _+ᴹ_ = AB._+ᴹ_ _+_ +module MagmaProperties (rawMagma : RawMagma a ℓ) where + open RawMagma rawMagma renaming (_∙_ to _+_) + open VecMagma rawMagma + open IsEquivalence + + ≈ᴹ-isEquivalence : IsEquivalence _≈_ → IsEquivalence (_≈ᴹ_ {n = n}) + ≈ᴹ-isEquivalence = flip Pointwise.isEquivalence _ +ᴹ-cong : Congruent₂ _≈_ _+_ → Congruent₂ _≈ᴹ_ (_+ᴹ_ {n = n}) +ᴹ-cong +-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) @@ -57,39 +48,41 @@ module AddProperties (_+_ : Op₂ A) where +ᴹ-comm : Commutative _≈_ _+_ → Commutative _≈ᴹ_ (_+ᴹ_ {n}) +ᴹ-comm +-comm xs ys i = +-comm (xs i) (ys i) - module ZeroProperties (0# : A) where - private - 0ᴹ : Vector A n - 0ᴹ = AB.0ᴹ 0# + isMagma : IsMagma _≈_ _+_ → IsMagma _≈ᴹ_ (_+ᴹ_ {n}) + isMagma isMagma = record + { isEquivalence = ≈ᴹ-isEquivalence isEquivalence + ; ∙-cong = +ᴹ-cong ∙-cong + } where open IsMagma isMagma - +ᴹ-identityˡ : LeftIdentity _≈_ 0# _+_ → LeftIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ - +ᴹ-identityˡ +-identityˡ xs i = +-identityˡ (xs i) - +ᴹ-identityʳ : RightIdentity _≈_ 0# _+_ → RightIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ - +ᴹ-identityʳ +-identityʳ xs is = +-identityʳ (xs is) +module MonoidProperties (rawMonoid : RawMonoid a ℓ) where + open RawMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) + open VecMonoid rawMonoid + open MagmaProperties rawMagma public - +ᴹ-identity : Identity _≈_ 0# _+_ → Identity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ - +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ + +ᴹ-identityˡ : LeftIdentity _≈_ 0# _+_ → LeftIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityˡ +-identityˡ xs i = +-identityˡ (xs i) - module NegativeProperties (-_ : Op₁ A) where - private - -ᴹ_ : Op₁ $ Vector A n - -ᴹ_ = AB.-ᴹ_ -_ + +ᴹ-identityʳ : RightIdentity _≈_ 0# _+_ → RightIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityʳ +-identityʳ xs is = +-identityʳ (xs is) - -ᴹ‿inverseˡ : LeftInverse _≈_ 0# -_ _+_ → LeftInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ - -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) + +ᴹ-identity : Identity _≈_ 0# _+_ → Identity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ - -ᴹ‿inverseʳ : RightInverse _≈_ 0# -_ _+_ → RightInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ - -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) - -ᴹ‿inverse : Inverse _≈_ 0# -_ _+_ → Inverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ - -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ +module GroupProperties (rawGroup : RawGroup a ℓ) where + open RawGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) + open VecGroup rawGroup + open MonoidProperties rawMonoid public + -ᴹ‿inverseˡ : LeftInverse _≈_ 0# -_ _+_ → LeftInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) -module NegativeProperties (-_ : Op₁ A) where - private - -ᴹ_ : Op₁ $ Vector A n - -ᴹ_ = AB.-ᴹ_ -_ + -ᴹ‿inverseʳ : RightInverse _≈_ 0# -_ _+_ → RightInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) + + -ᴹ‿inverse : Inverse _≈_ 0# -_ _+_ → Inverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ -ᴹ‿cong : Congruent₁ _≈_ -_ → Congruent₁ _≈ᴹ_ (-ᴹ_ {n}) -ᴹ‿cong -‿cong xs i = -‿cong (xs i) @@ -158,9 +151,9 @@ module NegativeProperties (-_ : Op₁ A) where -- *ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ -- *ᴹ-+ᴹ-distrib = *ᴹ-+ᴹ-distribˡ , *ᴹ-+ᴹ-distribʳ -module MultiplicationProperties (_*_ : Op₂ A) where - _*ᴹ_ : Op₂ $ Vector A n - _*ᴹ_ {n = n} = AB._*ᴹ_ {n = n} _*_ +-- module MultiplicationProperties (_*_ : Op₂ A) where +-- _*ᴹ_ : Op₂ $ Vector A n +-- _*ᴹ_ {n = n} = AB._*ᴹ_ {n = n} _*_ -- *ᴹ-cong : Congruent₂ _≈_ _*_ → Congruent₂ _≈ᴹ_ (_*ᴹ_ {n = n}) -- *ᴹ-cong *-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) @@ -173,12 +166,6 @@ module MultiplicationProperties (_*_ : Op₂ A) where -- ------------------------------------------------------------------------ -- -- Structures --- isMagma : IsMagma (_+ᴹ_ {n}) --- isMagma = record --- { isEquivalence = ≋-isEquivalence _ --- ; ∙-cong = +ᴹ-cong --- } - -- *ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) -- *ᴹ-isMagma = record -- { isEquivalence = ≋-isEquivalence _ From 51a8adc32e0b35c4976ed614841547cd2c3238b7 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 25 May 2023 18:54:49 -0300 Subject: [PATCH 15/25] fixed base exportation --- src/Data/Vec/Functional/Algebra/Base.agda | 22 +++++++++---------- .../Vec/Functional/Algebra/Properties.agda | 21 +++++++++++------- 2 files changed, 24 insertions(+), 19 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 8da7c91d20..d300cef480 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -33,43 +33,43 @@ module VecAddition (_+_ : Op₂ A) where _+ᴹ_ = zipWith _+_ module VecMagma (rawMagma : RawMagma a ℓ) where - open RawMagma rawMagma + open RawMagma rawMagma public open VecAddition _∙_ public open EqualityVecFunc _≈_ public module VecMonoid (rawMonoid : RawMonoid a ℓ) where - open RawMonoid rawMonoid + open RawMonoid rawMonoid using (rawMagma; ε) public open VecMagma rawMagma public 0ᴹ : Vector Carrier n 0ᴹ = replicate ε module VecGroup (rawGroup : RawGroup a ℓ) where - open RawGroup rawGroup + open RawGroup rawGroup using (rawMonoid; _⁻¹) public open VecMonoid rawMonoid public -ᴹ_ : Op₁ $ Vector Carrier n -ᴹ_ = map $ _⁻¹ module VecNearSemiring (rawNearSemiring : RawNearSemiring a ℓ) where - open RawNearSemiring rawNearSemiring - open VecMonoid +-rawMonoid public + open RawNearSemiring rawNearSemiring using (+-rawMonoid; *-rawMagma) public + open VecMonoid +-rawMonoid renaming (ε to 0#; _∙_ to _*_) public open VecMagma *-rawMagma public renaming (_+ᴹ_ to _*ᴹ_) using () module VecSemiring (rawSemiring : RawSemiring a ℓ) where - open RawSemiring rawSemiring + open RawSemiring rawSemiring using (rawNearSemiring; 1#) public open VecNearSemiring rawNearSemiring public 1ᴹ : Vector Carrier n 1ᴹ = replicate 1# - _*ₗ_ : Op₂ A → Opₗ A (Vector A n) - _*ₗ_ _*_ r = map (r *_) + _*ₗ_ : Opₗ Carrier (Vector Carrier n) + _*ₗ_ r = map (r *_) - _*ᵣ_ : Op₂ A → Opᵣ A (Vector A n) - _*ᵣ_ _*_ xs r = map (_* r) xs + _*ᵣ_ : Opᵣ Carrier (Vector Carrier n) + _*ᵣ_ xs r = map (_* r) xs module VecRing (rawRing : RawRing a ℓ) where - open RawRing rawRing + open RawRing rawRing using (+-rawGroup; rawSemiring) public open VecGroup +-rawGroup public using (-ᴹ_) open VecSemiring rawSemiring public diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 60d1b3527e..9566daf6d5 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -32,8 +32,7 @@ private variable -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ module MagmaProperties (rawMagma : RawMagma a ℓ) where - open RawMagma rawMagma renaming (_∙_ to _+_) - open VecMagma rawMagma + open VecMagma rawMagma renaming (_∙_ to _+_) open IsEquivalence ≈ᴹ-isEquivalence : IsEquivalence _≈_ → IsEquivalence (_≈ᴹ_ {n = n}) @@ -56,8 +55,7 @@ module MagmaProperties (rawMagma : RawMagma a ℓ) where module MonoidProperties (rawMonoid : RawMonoid a ℓ) where - open RawMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) - open VecMonoid rawMonoid + open VecMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) open MagmaProperties rawMagma public +ᴹ-identityˡ : LeftIdentity _≈_ 0# _+_ → LeftIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ @@ -71,8 +69,7 @@ module MonoidProperties (rawMonoid : RawMonoid a ℓ) where module GroupProperties (rawGroup : RawGroup a ℓ) where - open RawGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) - open VecGroup rawGroup + open VecGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) open MonoidProperties rawMonoid public -ᴹ‿inverseˡ : LeftInverse _≈_ 0# -_ _+_ → LeftInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ @@ -88,8 +85,16 @@ module GroupProperties (rawGroup : RawGroup a ℓ) where -ᴹ‿cong -‿cong xs i = -‿cong (xs i) --- *ₗ-cong : LD.Congruent SR._≈_ (_*ₗ_ {n}) --- *ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i) +module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where + open VecSemiring rawSemiring + module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n = n}) + + *ₗ-cong : Congruent₂ _≈_ _*_ → LD.Congruent _≈_ (_*ₗ_ {n}) + *ₗ-cong *-cong x≈y u≈v i = *-cong x≈y (u≈v i) + + *ₗ-zeroˡ : LeftZero _≈_ 0# _*_ → LD.LeftZero 0# 0ᴹ (_*ₗ_ {n}) + *ₗ-zeroˡ zeroˡ xs i = zeroˡ (xs i) + -- *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ -- *ₗ-zeroˡ xs i = zeroˡ (xs i) From 841be8c0fe359c5cf89e2c76cc3d8b2d4af81927 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 25 May 2023 22:00:20 -0300 Subject: [PATCH 16/25] proved more definitions --- src/Data/Vec/Functional/Algebra/Base.agda | 4 +- .../Vec/Functional/Algebra/Properties.agda | 127 ++++++++++-------- 2 files changed, 72 insertions(+), 59 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index d300cef480..69eb74b861 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -53,8 +53,8 @@ module VecGroup (rawGroup : RawGroup a ℓ) where module VecNearSemiring (rawNearSemiring : RawNearSemiring a ℓ) where open RawNearSemiring rawNearSemiring using (+-rawMonoid; *-rawMagma) public - open VecMonoid +-rawMonoid renaming (ε to 0#; _∙_ to _*_) public - open VecMagma *-rawMagma public renaming (_+ᴹ_ to _*ᴹ_) using () + open VecMonoid +-rawMonoid renaming (ε to 0#; _∙_ to _+_) public + open VecMagma *-rawMagma public renaming (_+ᴹ_ to _*ᴹ_; _∙_ to _*_) using () module VecSemiring (rawSemiring : RawSemiring a ℓ) where open RawSemiring rawSemiring using (rawNearSemiring; 1#) public diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 9566daf6d5..3fb1d6a39e 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -18,7 +18,7 @@ open import Algebra.Core open import Algebra.Bundles open import Algebra.Module open import Relation.Binary -open import Algebra.Definitions +import Algebra.Definitions as ADefinitions open import Algebra.Structures open import Data.Vec.Functional.Algebra.Base import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pointwise @@ -34,17 +34,20 @@ private variable module MagmaProperties (rawMagma : RawMagma a ℓ) where open VecMagma rawMagma renaming (_∙_ to _+_) open IsEquivalence + private + module ≈ = ADefinitions _≈_ + module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) ≈ᴹ-isEquivalence : IsEquivalence _≈_ → IsEquivalence (_≈ᴹ_ {n = n}) ≈ᴹ-isEquivalence = flip Pointwise.isEquivalence _ - +ᴹ-cong : Congruent₂ _≈_ _+_ → Congruent₂ _≈ᴹ_ (_+ᴹ_ {n = n}) + +ᴹ-cong : ≈.Congruent₂ _+_ → ≈ᴹ.Congruent₂ (_+ᴹ_ {n = n}) +ᴹ-cong +-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) - +ᴹ-assoc : Associative _≈_ _+_ → Associative _≈ᴹ_ (_+ᴹ_ {n}) + +ᴹ-assoc : ≈.Associative _+_ → ≈ᴹ.Associative (_+ᴹ_ {n}) +ᴹ-assoc +-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) - +ᴹ-comm : Commutative _≈_ _+_ → Commutative _≈ᴹ_ (_+ᴹ_ {n}) + +ᴹ-comm : ≈.Commutative _+_ → ≈ᴹ.Commutative (_+ᴹ_ {n}) +ᴹ-comm +-comm xs ys i = +-comm (xs i) (ys i) isMagma : IsMagma _≈_ _+_ → IsMagma _≈ᴹ_ (_+ᴹ_ {n}) @@ -57,104 +60,114 @@ module MagmaProperties (rawMagma : RawMagma a ℓ) where module MonoidProperties (rawMonoid : RawMonoid a ℓ) where open VecMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) open MagmaProperties rawMagma public + private + module ≈ = ADefinitions _≈_ + module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) - +ᴹ-identityˡ : LeftIdentity _≈_ 0# _+_ → LeftIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityˡ : ≈.LeftIdentity 0# _+_ → ≈ᴹ.LeftIdentity (0ᴹ {n}) _+ᴹ_ +ᴹ-identityˡ +-identityˡ xs i = +-identityˡ (xs i) - +ᴹ-identityʳ : RightIdentity _≈_ 0# _+_ → RightIdentity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identityʳ : ≈.RightIdentity 0# _+_ → ≈ᴹ.RightIdentity (0ᴹ {n}) _+ᴹ_ +ᴹ-identityʳ +-identityʳ xs is = +-identityʳ (xs is) - +ᴹ-identity : Identity _≈_ 0# _+_ → Identity _≈ᴹ_ (0ᴹ {n}) _+ᴹ_ + +ᴹ-identity : ≈.Identity 0# _+_ → ≈ᴹ.Identity (0ᴹ {n}) _+ᴹ_ +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ module GroupProperties (rawGroup : RawGroup a ℓ) where open VecGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) open MonoidProperties rawMonoid public + private + module ≈ = ADefinitions _≈_ + module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) - -ᴹ‿inverseˡ : LeftInverse _≈_ 0# -_ _+_ → LeftInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseˡ : ≈.LeftInverse 0# -_ _+_ → ≈ᴹ.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) - -ᴹ‿inverseʳ : RightInverse _≈_ 0# -_ _+_ → RightInverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseʳ : ≈.RightInverse 0# -_ _+_ → ≈ᴹ.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) - -ᴹ‿inverse : Inverse _≈_ 0# -_ _+_ → Inverse _≈ᴹ_ (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverse : ≈.Inverse 0# -_ _+_ → ≈ᴹ.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ - -ᴹ‿cong : Congruent₁ _≈_ -_ → Congruent₁ _≈ᴹ_ (-ᴹ_ {n}) + -ᴹ‿cong : ≈.Congruent₁ -_ → ≈ᴹ.Congruent₁ (-ᴹ_ {n}) -ᴹ‿cong -‿cong xs i = -‿cong (xs i) module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where open VecSemiring rawSemiring - module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n = n}) - - *ₗ-cong : Congruent₂ _≈_ _*_ → LD.Congruent _≈_ (_*ₗ_ {n}) + private + module LD≈ = LeftDefs Carrier _≈_ + module RD≈ = RightDefs Carrier _≈_ + module BD≈ = BiDefs Carrier Carrier _≈_ + module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n = n}) + module RD {n} = RightDefs Carrier (_≈ᴹ_ {n = n}) + module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n = n}) + module ≈ = ADefinitions _≈_ + module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) + + *ₗ-cong : ≈.Congruent₂ _*_ → LD.Congruent _≈_ (_*ₗ_ {n}) *ₗ-cong *-cong x≈y u≈v i = *-cong x≈y (u≈v i) - *ₗ-zeroˡ : LeftZero _≈_ 0# _*_ → LD.LeftZero 0# 0ᴹ (_*ₗ_ {n}) + *ₗ-zeroˡ : ≈.LeftZero 0# _*_ → LD.LeftZero 0# 0ᴹ (_*ₗ_ {n}) *ₗ-zeroˡ zeroˡ xs i = zeroˡ (xs i) + *ₗ-distribʳ : _*_ ≈.DistributesOverʳ _+_ → _*ₗ_ LD.DistributesOverʳ _+_ ⟶ _+ᴹ_ {n} + *ₗ-distribʳ distribʳ xs m n i = distribʳ (xs i) m n --- *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_ --- *ₗ-zeroˡ xs i = zeroˡ (xs i) - --- *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n}) --- *ₗ-distribʳ xs m n i = distribʳ (xs i) m n - --- *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n}) --- *ₗ-identityˡ xs i = *-identityˡ (xs i) + *ₗ-identityˡ : ≈.LeftIdentity 1# _*_ → LD.LeftIdentity 1# (_*ₗ_ {n}) + *ₗ-identityˡ *-identityˡ xs i = *-identityˡ (xs i) --- *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n}) --- *ₗ-assoc m n xs i = *-assoc m n (xs i) + *ₗ-assoc : ≈.Associative _*_ → LD.Associative _*_ (_*ₗ_ {n}) + *ₗ-assoc *-assoc m n xs i = *-assoc m n (xs i) --- *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_ --- *ₗ-zeroʳ m _ = zeroʳ m + *ₗ-zeroʳ : ≈.RightZero 0# _*_ → LD.RightZero (0ᴹ {n}) _*ₗ_ + *ₗ-zeroʳ zeroʳ m _ = zeroʳ m --- *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) --- *ₗ-distribˡ m xs ys i = distribˡ m (xs i) (ys i) + *ₗ-distribˡ : _*_ ≈.DistributesOverˡ _+_ → _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n}) + *ₗ-distribˡ distribˡ m xs ys i = distribˡ m (xs i) (ys i) --- *ᵣ-cong : RD.Congruent SR._≈_ (_*ᵣ_ {n}) --- *ᵣ-cong x≈y u≈v i = *-cong (x≈y i) u≈v + *ᵣ-cong : RD≈.Congruent _≈_ _*_ → RD.Congruent _≈_ (_*ᵣ_ {n}) + *ᵣ-cong *-cong x≈y u≈v i = *-cong (x≈y i) u≈v --- *ᵣ-distribˡ : _*ᵣ_ RD.DistributesOverˡ SR._+_ ⟶ (_+ᴹ_ {n}) --- *ᵣ-distribˡ xs m n i = distribˡ (xs i) m n + *ᵣ-distribˡ : _*_ RD≈.DistributesOverˡ _+_ ⟶ _+_ → _*ᵣ_ RD.DistributesOverˡ _+_ ⟶ (_+ᴹ_ {n}) + *ᵣ-distribˡ distribˡ xs m n i = distribˡ (xs i) m n --- *ᵣ-zeroˡ : RD.LeftZero (0ᴹ {n}) _*ᵣ_ --- *ᵣ-zeroˡ xs i = zeroˡ xs + *ᵣ-zeroˡ : RD≈.LeftZero 0# _*_ → RD.LeftZero (0ᴹ {n}) _*ᵣ_ + *ᵣ-zeroˡ zeroˡ xs i = zeroˡ xs --- *ᵣ-identityʳ : RD.RightIdentity SR.1# (_*ᵣ_ {n}) --- *ᵣ-identityʳ xs i = *-identityʳ (xs i) + *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) + *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) --- *ᵣ-assoc : RD.Associative SR._*_ (_*ᵣ_ {n}) --- *ᵣ-assoc xs m n i = *-assoc (xs i) m n + *ᵣ-assoc : RD≈.Associative _*_ _*_ → RD.Associative _*_ (_*ᵣ_ {n}) + *ᵣ-assoc *-assoc xs m n i = *-assoc (xs i) m n --- *ᵣ-zeroʳ : RD.RightZero SR.0# (0ᴹ {n}) _*ᵣ_ --- *ᵣ-zeroʳ xs i = zeroʳ (xs i) + *ᵣ-zeroʳ : RD≈.RightZero 0# 0# _*_ → RD.RightZero 0# (0ᴹ {n}) _*ᵣ_ + *ᵣ-zeroʳ zeroʳ xs i = zeroʳ (xs i) --- *ᵣ-distribʳ : _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) --- *ᵣ-distribʳ xs m n i = distribʳ xs (m i) (n i) + *ᵣ-distribʳ : _*_ RD≈.DistributesOverʳ _+_ → _*ᵣ_ RD.DistributesOverʳ (_+ᴹ_ {n}) + *ᵣ-distribʳ distribʳ xs m n i = distribʳ xs (m i) (n i) --- *ₗ-*ᵣ-assoc : BD.Associative (_*ₗ_ {n}) _*ᵣ_ --- *ₗ-*ᵣ-assoc m xs n i = *-assoc m (xs i) n + *ₗ-*ᵣ-assoc : BD≈.Associative _*_ _*_ → BD.Associative (_*ₗ_ {n}) _*ᵣ_ + *ₗ-*ᵣ-assoc *-assoc m xs n i = *-assoc m (xs i) n --- *ᴹ-zeroˡ : AD'.LeftZero (0ᴹ {n}) _*ᴹ_ --- *ᴹ-zeroˡ xs i = zeroˡ (xs i) + *ᴹ-zeroˡ : ≈.LeftZero 0# _*_ → ≈ᴹ.LeftZero (0ᴹ {n}) _*ᴹ_ + *ᴹ-zeroˡ zeroˡ xs i = zeroˡ (xs i) --- *ᴹ-zeroʳ : AD'.RightZero (0ᴹ {n}) _*ᴹ_ --- *ᴹ-zeroʳ xs i = zeroʳ (xs i) + *ᴹ-zeroʳ : ≈.RightZero 0# _*_ → ≈ᴹ.RightZero (0ᴹ {n}) _*ᴹ_ + *ᴹ-zeroʳ zeroʳ xs i = zeroʳ (xs i) --- *ᴹ-zero : AD'.Zero (0ᴹ {n}) _*ᴹ_ --- *ᴹ-zero = *ᴹ-zeroˡ , *ᴹ-zeroʳ + *ᴹ-zero : ≈.Zero 0# _*_ → ≈ᴹ.Zero (0ᴹ {n}) _*ᴹ_ + *ᴹ-zero (*-zeroˡ , *-zeroʳ) = *ᴹ-zeroˡ *-zeroˡ , *ᴹ-zeroʳ *-zeroʳ --- *ᴹ-+ᴹ-distribˡ : (_*ᴹ_ {n}) AD'.DistributesOverˡ _+ᴹ_ --- *ᴹ-+ᴹ-distribˡ xs ys zs i = distribˡ (xs i) (ys i) (zs i) + *ᴹ-+ᴹ-distribˡ : _*_ ≈.DistributesOverˡ _+_ → (_*ᴹ_ {n}) ≈ᴹ.DistributesOverˡ _+ᴹ_ + *ᴹ-+ᴹ-distribˡ distribˡ xs ys zs i = distribˡ (xs i) (ys i) (zs i) --- *ᴹ-+ᴹ-distribʳ : (_*ᴹ_ {n}) AD'.DistributesOverʳ _+ᴹ_ --- *ᴹ-+ᴹ-distribʳ xs ys zs i = distribʳ (xs i) (ys i) (zs i) + *ᴹ-+ᴹ-distribʳ : _*_ ≈.DistributesOverʳ _+_ → (_*ᴹ_ {n}) ≈ᴹ.DistributesOverʳ _+ᴹ_ + *ᴹ-+ᴹ-distribʳ distribʳ xs ys zs i = distribʳ (xs i) (ys i) (zs i) --- *ᴹ-+ᴹ-distrib : (_*ᴹ_ {n}) AD'.DistributesOver _+ᴹ_ --- *ᴹ-+ᴹ-distrib = *ᴹ-+ᴹ-distribˡ , *ᴹ-+ᴹ-distribʳ + *ᴹ-+ᴹ-distrib : _*_ ≈.DistributesOver _+_ → (_*ᴹ_ {n}) ≈ᴹ.DistributesOver _+ᴹ_ + *ᴹ-+ᴹ-distrib (*-+-distribˡ , *-+-distribʳ) = *ᴹ-+ᴹ-distribˡ *-+-distribˡ , *ᴹ-+ᴹ-distribʳ *-+-distribʳ -- module MultiplicationProperties (_*_ : Op₂ A) where -- _*ᴹ_ : Op₂ $ Vector A n From 62b0af2d68ebdc1f75c7590b7280497fc0f746bb Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 25 May 2023 22:34:21 -0300 Subject: [PATCH 17/25] added monoid properties --- .../Vec/Functional/Algebra/Properties.agda | 80 +++++++++---------- 1 file changed, 36 insertions(+), 44 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 3fb1d6a39e..6b7b018805 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -50,12 +50,31 @@ module MagmaProperties (rawMagma : RawMagma a ℓ) where +ᴹ-comm : ≈.Commutative _+_ → ≈ᴹ.Commutative (_+ᴹ_ {n}) +ᴹ-comm +-comm xs ys i = +-comm (xs i) (ys i) + isMagma : IsMagma _≈_ _+_ → IsMagma _≈ᴹ_ (_+ᴹ_ {n}) isMagma isMagma = record { isEquivalence = ≈ᴹ-isEquivalence isEquivalence ; ∙-cong = +ᴹ-cong ∙-cong } where open IsMagma isMagma + isCommutativeMagma : IsCommutativeMagma _≈_ _+_ → IsCommutativeMagma _≈ᴹ_ (_+ᴹ_ {n}) + isCommutativeMagma isCMagma = record + { isMagma = isMagma CM.isMagma + ; comm = +ᴹ-comm CM.comm + } where module CM = IsCommutativeMagma isCMagma + + isSemigroup : IsSemigroup _≈_ _+_ → IsSemigroup _≈ᴹ_ (_+ᴹ_ {n}) + isSemigroup isSemigroup = record + { isMagma = isMagma SG.isMagma + ; assoc = +ᴹ-assoc SG.assoc + } where module SG = IsSemigroup isSemigroup + + isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _+_ → IsCommutativeSemigroup _≈ᴹ_ (_+ᴹ_ {n}) + isCommutativeSemigroup isCommutativeSemigroup = record + { isSemigroup = isSemigroup SG.isSemigroup + ; comm = +ᴹ-comm SG.comm + } where module SG = IsCommutativeSemigroup isCommutativeSemigroup + module MonoidProperties (rawMonoid : RawMonoid a ℓ) where open VecMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) @@ -74,6 +93,19 @@ module MonoidProperties (rawMonoid : RawMonoid a ℓ) where +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ + isMonoid : IsMonoid _≈_ _+_ 0# → IsMonoid _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ + isMonoid isMonoid = record + { isSemigroup = isSemigroup M.isSemigroup + ; identity = +ᴹ-identity M.identity + } where module M = IsMonoid isMonoid + + isCommutativeMonoid : IsCommutativeMonoid _≈_ _+_ 0# → IsCommutativeMonoid _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ + isCommutativeMonoid isCommutativeMonoid = record + { isMonoid = isMonoid CM.isMonoid + ; comm = +ᴹ-comm CM.comm + } where module CM = IsCommutativeMonoid isCommutativeMonoid + + module GroupProperties (rawGroup : RawGroup a ℓ) where open VecGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) open MonoidProperties rawMonoid public @@ -169,69 +201,29 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᴹ-+ᴹ-distrib : _*_ ≈.DistributesOver _+_ → (_*ᴹ_ {n}) ≈ᴹ.DistributesOver _+ᴹ_ *ᴹ-+ᴹ-distrib (*-+-distribˡ , *-+-distribʳ) = *ᴹ-+ᴹ-distribˡ *-+-distribˡ , *ᴹ-+ᴹ-distribʳ *-+-distribʳ --- module MultiplicationProperties (_*_ : Op₂ A) where --- _*ᴹ_ : Op₂ $ Vector A n --- _*ᴹ_ {n = n} = AB._*ᴹ_ {n = n} _*_ - - -- *ᴹ-cong : Congruent₂ _≈_ _*_ → Congruent₂ _≈ᴹ_ (_*ᴹ_ {n = n}) - -- *ᴹ-cong *-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) + *ᴹ-cong : ≈.Congruent₂ _*_ → ≈ᴹ.Congruent₂ (_*ᴹ_ {n = n}) + *ᴹ-cong *-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) - -- *ᴹ-assoc : Associative (_*ᴹ_ {n}) - -- *ᴹ-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) + *ᴹ-assoc : ≈.Associative _*_ → ≈ᴹ.Associative (_*ᴹ_ {n}) + *ᴹ-assoc *-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) -- ------------------------------------------------------------------------ -- -- Structures --- *ᴹ-isMagma : IsMagma (_*ᴹ_ {n}) --- *ᴹ-isMagma = record --- { isEquivalence = ≋-isEquivalence _ --- ; ∙-cong = *ᴹ-cong --- } - --- isCommutativeMagma : IsCommutativeMagma (_+ᴹ_ {n}) --- isCommutativeMagma = record --- { isMagma = isMagma --- ; comm = +ᴹ-comm --- } - --- isSemigroup : IsSemigroup (_+ᴹ_ {n}) --- isSemigroup = record --- { isMagma = isMagma --- ; assoc = +ᴹ-assoc --- } - -- *ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) -- *ᴹ-isSemigroup = record -- { isMagma = *ᴹ-isMagma -- ; assoc = *ᴹ-assoc -- } --- isCommutativeSemigroup : IsCommutativeSemigroup (_+ᴹ_ {n}) --- isCommutativeSemigroup = record --- { isSemigroup = isSemigroup --- ; comm = +ᴹ-comm --- } - --- isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ --- isMonoid = record --- { isSemigroup = isSemigroup --- ; identity = +ᴹ-identity --- } - -- *ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ -- *ᴹ-isMonoid = record -- { isSemigroup = *ᴹ-isSemigroup -- ; identity = *ᴹ-identity -- } --- isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ --- isCommutativeMonoid = record --- { isMonoid = isMonoid --- ; comm = +ᴹ-comm --- } - -- isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ -- isGroup = record -- { isMonoid = isMonoid From 651c31617feba1bf27a48894b5472138ba6a79e0 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 00:24:51 -0300 Subject: [PATCH 18/25] added isGroup and isAbGroup --- .../Vec/Functional/Algebra/Properties.agda | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 6b7b018805..d4f2f1a322 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -126,6 +126,19 @@ module GroupProperties (rawGroup : RawGroup a ℓ) where -ᴹ‿cong -‿cong xs i = -‿cong (xs i) + isGroup : IsGroup _≈_ _+_ 0# -_ → IsGroup _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ -ᴹ_ + isGroup isGroup = record + { isMonoid = isMonoid G.isMonoid + ; inverse = -ᴹ‿inverse G.inverse + ; ⁻¹-cong = -ᴹ‿cong G.⁻¹-cong + } where module G = IsGroup isGroup + + isAbelianGroup : IsAbelianGroup _≈_ _+_ 0# -_ → IsAbelianGroup _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ -ᴹ_ + isAbelianGroup isAbelianGroup = record + { isGroup = isGroup AG.isGroup + ; comm = +ᴹ-comm AG.comm + } where module AG = IsAbelianGroup isAbelianGroup + module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where open VecSemiring rawSemiring private @@ -208,7 +221,6 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᴹ-assoc *-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) - -- ------------------------------------------------------------------------ -- -- Structures @@ -224,18 +236,7 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where -- ; identity = *ᴹ-identity -- } --- isGroup : IsGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ --- isGroup = record --- { isMonoid = isMonoid --- ; inverse = -ᴹ‿inverse --- ; ⁻¹-cong = -ᴹ‿cong --- } --- isAbelianGroup : IsAbelianGroup (_+ᴹ_ {n}) 0ᴹ -ᴹ_ --- isAbelianGroup = record --- { isGroup = isGroup --- ; comm = +ᴹ-comm --- } -- isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ -- isPreleftSemimodule = record From 1c520d17136298c6d32c703a709dcd1972b1fe06 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 01:07:53 -0300 Subject: [PATCH 19/25] added semiring properties --- .../Vec/Functional/Algebra/Properties.agda | 89 ++++++++++--------- 1 file changed, 47 insertions(+), 42 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index d4f2f1a322..c561a3efe8 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -141,6 +141,7 @@ module GroupProperties (rawGroup : RawGroup a ℓ) where module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where open VecSemiring rawSemiring + open MonoidProperties +-rawMonoid public private module LD≈ = LeftDefs Carrier _≈_ module RD≈ = RightDefs Carrier _≈_ @@ -220,6 +221,52 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᴹ-assoc : ≈.Associative _*_ → ≈ᴹ.Associative (_*ᴹ_ {n}) *ᴹ-assoc *-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) +module SemiringProperties (semiring : Semiring a ℓ) where + open Semiring semiring + open VecSemiring rawSemiring + open VecSemiRingProperties rawSemiring + + isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ + isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong *-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ *-identityˡ + ; *ₗ-assoc = *ₗ-assoc *-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ distribˡ + } + + isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ + isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong *-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ *-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc *-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ distribʳ + } + + isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ + isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + ; isPrerightSemimodule = isPrerightSemimodule + } + + isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ + isBisemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimodule + ; isPrerightSemimodule = isPrerightSemimodule + ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc *-assoc + } + + isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ + isLeftSemimodule = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimodule + } -- ------------------------------------------------------------------------ -- -- Structures @@ -238,42 +285,6 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where --- isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ --- isPreleftSemimodule = record --- { *ₗ-cong = *ₗ-cong --- ; *ₗ-zeroˡ = *ₗ-zeroˡ --- ; *ₗ-distribʳ = *ₗ-distribʳ --- ; *ₗ-identityˡ = *ₗ-identityˡ --- ; *ₗ-assoc = *ₗ-assoc --- ; *ₗ-zeroʳ = *ₗ-zeroʳ --- ; *ₗ-distribˡ = *ₗ-distribˡ --- } - --- isPrerightSemimodule : IsPrerightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ --- isPrerightSemimodule = record --- { *ᵣ-cong = *ᵣ-cong --- ; *ᵣ-zeroʳ = *ᵣ-zeroʳ --- ; *ᵣ-distribˡ = *ᵣ-distribˡ --- ; *ᵣ-identityʳ = *ᵣ-identityʳ --- ; *ᵣ-assoc = *ᵣ-assoc --- ; *ᵣ-zeroˡ = *ᵣ-zeroˡ --- ; *ᵣ-distribʳ = *ᵣ-distribʳ --- } - --- isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ --- isRightSemimodule = record --- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid --- ; isPrerightSemimodule = isPrerightSemimodule --- } - --- isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ --- isBisemimodule = record --- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid --- ; isPreleftSemimodule = isPreleftSemimodule --- ; isPrerightSemimodule = isPrerightSemimodule --- ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc --- } - -- isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ -- isRightModule = record -- { isRightSemimodule = isRightSemimodule @@ -288,12 +299,6 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where -- ; -ᴹ‿inverse = -ᴹ‿inverse -- } --- isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ --- isLeftSemimodule = record --- { +ᴹ-isCommutativeMonoid = isCommutativeMonoid --- ; isPreleftSemimodule = isPreleftSemimodule --- } - -- isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ -- isLeftModule = record -- { isLeftSemimodule = isLeftSemimodule From 2f9e635cc7fc991db9da04a9797823082c205a27 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 01:23:24 -0300 Subject: [PATCH 20/25] added Ring Properties --- .../Vec/Functional/Algebra/Properties.agda | 53 +++++++++++-------- 1 file changed, 31 insertions(+), 22 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index c561a3efe8..478cb8d510 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -224,7 +224,7 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where module SemiringProperties (semiring : Semiring a ℓ) where open Semiring semiring open VecSemiring rawSemiring - open VecSemiRingProperties rawSemiring + open VecSemiRingProperties rawSemiring public isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isPreleftSemimodule = record @@ -268,6 +268,36 @@ module SemiringProperties (semiring : Semiring a ℓ) where ; isPreleftSemimodule = isPreleftSemimodule } +module RingProperties (ring : Ring a ℓ) where + open Ring ring + open VecRing rawRing + open VecSemiRingProperties rawSemiring + open Group +-group using (rawGroup) + open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse) + open SemiringProperties semiring public + + isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ + isRightModule = record + { isRightSemimodule = isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + isBimodule = record + { isBisemimodule = isBisemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ + isLeftModule = record + { isLeftSemimodule = isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + -- ------------------------------------------------------------------------ -- -- Structures @@ -285,27 +315,6 @@ module SemiringProperties (semiring : Semiring a ℓ) where --- isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ --- isRightModule = record --- { isRightSemimodule = isRightSemimodule --- ; -ᴹ‿cong = -ᴹ‿cong --- ; -ᴹ‿inverse = -ᴹ‿inverse --- } - --- isBimodule : IsBimodule ring ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ --- isBimodule = record --- { isBisemimodule = isBisemimodule --- ; -ᴹ‿cong = -ᴹ‿cong --- ; -ᴹ‿inverse = -ᴹ‿inverse --- } - --- isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ --- isLeftModule = record --- { isLeftSemimodule = isLeftSemimodule --- ; -ᴹ‿cong = -ᴹ‿cong --- ; -ᴹ‿inverse = -ᴹ‿inverse --- } - -- isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ -- isModule = record -- { isBimodule = isBimodule From 9fc26328c2d0a4953c4c7d4c527b8c6bb5e83464 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 18:37:16 -0300 Subject: [PATCH 21/25] changed back to espilon and dot definition --- src/Data/Vec/Functional/Algebra/Base.agda | 26 ++-- .../Vec/Functional/Algebra/Properties.agda | 145 ++++++++++-------- 2 files changed, 97 insertions(+), 74 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 69eb74b861..ea4bdd01d5 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -28,9 +28,9 @@ module EqualityVecFunc (_≈_ : Rel A ℓ) where _≈ᴹ_ : Rel (Vector A n) ℓ _≈ᴹ_ = Pointwise _≈_ -module VecAddition (_+_ : Op₂ A) where - _+ᴹ_ : Op₂ $ Vector A n - _+ᴹ_ = zipWith _+_ +module VecAddition (_∙_ : Op₂ A) where + _∙ᴹ_ : Op₂ $ Vector A n + _∙ᴹ_ = zipWith _∙_ module VecMagma (rawMagma : RawMagma a ℓ) where open RawMagma rawMagma public @@ -41,8 +41,8 @@ module VecMonoid (rawMonoid : RawMonoid a ℓ) where open RawMonoid rawMonoid using (rawMagma; ε) public open VecMagma rawMagma public - 0ᴹ : Vector Carrier n - 0ᴹ = replicate ε + εᴹ : Vector Carrier n + εᴹ = replicate ε module VecGroup (rawGroup : RawGroup a ℓ) where open RawGroup rawGroup using (rawMonoid; _⁻¹) public @@ -53,15 +53,8 @@ module VecGroup (rawGroup : RawGroup a ℓ) where module VecNearSemiring (rawNearSemiring : RawNearSemiring a ℓ) where open RawNearSemiring rawNearSemiring using (+-rawMonoid; *-rawMagma) public - open VecMonoid +-rawMonoid renaming (ε to 0#; _∙_ to _+_) public - open VecMagma *-rawMagma public renaming (_+ᴹ_ to _*ᴹ_; _∙_ to _*_) using () - -module VecSemiring (rawSemiring : RawSemiring a ℓ) where - open RawSemiring rawSemiring using (rawNearSemiring; 1#) public - open VecNearSemiring rawNearSemiring public - - 1ᴹ : Vector Carrier n - 1ᴹ = replicate 1# + open VecMonoid +-rawMonoid renaming (ε to 0#; εᴹ to 0ᴹ; _∙ᴹ_ to _+ᴹ_; _∙_ to _+_) public + open VecMagma *-rawMagma public renaming (_∙ᴹ_ to _*ᴹ_; _∙_ to _*_) using () _*ₗ_ : Opₗ Carrier (Vector Carrier n) _*ₗ_ r = map (r *_) @@ -69,6 +62,11 @@ module VecSemiring (rawSemiring : RawSemiring a ℓ) where _*ᵣ_ : Opᵣ Carrier (Vector Carrier n) _*ᵣ_ xs r = map (_* r) xs +module VecSemiring (rawSemiring : RawSemiring a ℓ) where + open RawSemiring rawSemiring using (rawNearSemiring; 1#; *-rawMonoid) public + open VecNearSemiring rawNearSemiring public + open VecMonoid *-rawMonoid public renaming (εᴹ to 1ᴹ) using () + module VecRing (rawRing : RawRing a ℓ) where open RawRing rawRing using (+-rawGroup; rawSemiring) public open VecGroup +-rawGroup public using (-ᴹ_) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 478cb8d510..ff5786c30f 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -32,7 +32,7 @@ private variable -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ module MagmaProperties (rawMagma : RawMagma a ℓ) where - open VecMagma rawMagma renaming (_∙_ to _+_) + open VecMagma rawMagma open IsEquivalence private module ≈ = ADefinitions _≈_ @@ -41,107 +41,119 @@ module MagmaProperties (rawMagma : RawMagma a ℓ) where ≈ᴹ-isEquivalence : IsEquivalence _≈_ → IsEquivalence (_≈ᴹ_ {n = n}) ≈ᴹ-isEquivalence = flip Pointwise.isEquivalence _ - +ᴹ-cong : ≈.Congruent₂ _+_ → ≈ᴹ.Congruent₂ (_+ᴹ_ {n = n}) - +ᴹ-cong +-cong x≈y u≈v i = +-cong (x≈y i) (u≈v i) + ∙ᴹ-cong : ≈.Congruent₂ _∙_ → ≈ᴹ.Congruent₂ (_∙ᴹ_ {n = n}) + ∙ᴹ-cong ∙-cong x≈y u≈v i = ∙-cong (x≈y i) (u≈v i) - +ᴹ-assoc : ≈.Associative _+_ → ≈ᴹ.Associative (_+ᴹ_ {n}) - +ᴹ-assoc +-assoc xs ys zs i = +-assoc (xs i) (ys i) (zs i) + ∙ᴹ-assoc : ≈.Associative _∙_ → ≈ᴹ.Associative (_∙ᴹ_ {n}) + ∙ᴹ-assoc ∙-assoc xs ys zs i = ∙-assoc (xs i) (ys i) (zs i) - +ᴹ-comm : ≈.Commutative _+_ → ≈ᴹ.Commutative (_+ᴹ_ {n}) - +ᴹ-comm +-comm xs ys i = +-comm (xs i) (ys i) + ∙ᴹ-comm : ≈.Commutative _∙_ → ≈ᴹ.Commutative (_∙ᴹ_ {n}) + ∙ᴹ-comm ∙-comm xs ys i = ∙-comm (xs i) (ys i) - isMagma : IsMagma _≈_ _+_ → IsMagma _≈ᴹ_ (_+ᴹ_ {n}) + isMagma : IsMagma _≈_ _∙_ → IsMagma _≈ᴹ_ (_∙ᴹ_ {n}) isMagma isMagma = record { isEquivalence = ≈ᴹ-isEquivalence isEquivalence - ; ∙-cong = +ᴹ-cong ∙-cong + ; ∙-cong = ∙ᴹ-cong ∙-cong } where open IsMagma isMagma - isCommutativeMagma : IsCommutativeMagma _≈_ _+_ → IsCommutativeMagma _≈ᴹ_ (_+ᴹ_ {n}) + isCommutativeMagma : IsCommutativeMagma _≈_ _∙_ → IsCommutativeMagma _≈ᴹ_ (_∙ᴹ_ {n}) isCommutativeMagma isCMagma = record { isMagma = isMagma CM.isMagma - ; comm = +ᴹ-comm CM.comm + ; comm = ∙ᴹ-comm CM.comm } where module CM = IsCommutativeMagma isCMagma - isSemigroup : IsSemigroup _≈_ _+_ → IsSemigroup _≈ᴹ_ (_+ᴹ_ {n}) + isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) isSemigroup isSemigroup = record { isMagma = isMagma SG.isMagma - ; assoc = +ᴹ-assoc SG.assoc + ; assoc = ∙ᴹ-assoc SG.assoc } where module SG = IsSemigroup isSemigroup - isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _+_ → IsCommutativeSemigroup _≈ᴹ_ (_+ᴹ_ {n}) + isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ → IsCommutativeSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) isCommutativeSemigroup isCommutativeSemigroup = record { isSemigroup = isSemigroup SG.isSemigroup - ; comm = +ᴹ-comm SG.comm + ; comm = ∙ᴹ-comm SG.comm } where module SG = IsCommutativeSemigroup isCommutativeSemigroup module MonoidProperties (rawMonoid : RawMonoid a ℓ) where - open VecMonoid rawMonoid renaming (_∙_ to _+_; ε to 0#) + open VecMonoid rawMonoid open MagmaProperties rawMagma public private module ≈ = ADefinitions _≈_ module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) - +ᴹ-identityˡ : ≈.LeftIdentity 0# _+_ → ≈ᴹ.LeftIdentity (0ᴹ {n}) _+ᴹ_ - +ᴹ-identityˡ +-identityˡ xs i = +-identityˡ (xs i) + ∙ᴹ-identityˡ : ≈.LeftIdentity ε _∙_ → ≈ᴹ.LeftIdentity (εᴹ {n}) _∙ᴹ_ + ∙ᴹ-identityˡ ∙-identityˡ xs i = ∙-identityˡ (xs i) - +ᴹ-identityʳ : ≈.RightIdentity 0# _+_ → ≈ᴹ.RightIdentity (0ᴹ {n}) _+ᴹ_ - +ᴹ-identityʳ +-identityʳ xs is = +-identityʳ (xs is) + ∙ᴹ-identityʳ : ≈.RightIdentity ε _∙_ → ≈ᴹ.RightIdentity (εᴹ {n}) _∙ᴹ_ + ∙ᴹ-identityʳ ∙-identityʳ xs is = ∙-identityʳ (xs is) - +ᴹ-identity : ≈.Identity 0# _+_ → ≈ᴹ.Identity (0ᴹ {n}) _+ᴹ_ - +ᴹ-identity (+-identityˡ , +-identityʳ) = +ᴹ-identityˡ +-identityˡ , +ᴹ-identityʳ +-identityʳ + ∙ᴹ-identity : ≈.Identity ε _∙_ → ≈ᴹ.Identity (εᴹ {n}) _∙ᴹ_ + ∙ᴹ-identity (∙-identityˡ , ∙-identityʳ) = ∙ᴹ-identityˡ ∙-identityˡ , ∙ᴹ-identityʳ ∙-identityʳ - isMonoid : IsMonoid _≈_ _+_ 0# → IsMonoid _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ + isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ isMonoid isMonoid = record { isSemigroup = isSemigroup M.isSemigroup - ; identity = +ᴹ-identity M.identity + ; identity = ∙ᴹ-identity M.identity } where module M = IsMonoid isMonoid - isCommutativeMonoid : IsCommutativeMonoid _≈_ _+_ 0# → IsCommutativeMonoid _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ + isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε → IsCommutativeMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ isCommutativeMonoid isCommutativeMonoid = record { isMonoid = isMonoid CM.isMonoid - ; comm = +ᴹ-comm CM.comm + ; comm = ∙ᴹ-comm CM.comm } where module CM = IsCommutativeMonoid isCommutativeMonoid module GroupProperties (rawGroup : RawGroup a ℓ) where - open VecGroup rawGroup renaming (_∙_ to _+_; ε to 0#; _⁻¹ to -_) + open VecGroup rawGroup renaming (_⁻¹ to -_) open MonoidProperties rawMonoid public private module ≈ = ADefinitions _≈_ module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) - -ᴹ‿inverseˡ : ≈.LeftInverse 0# -_ _+_ → ≈ᴹ.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseˡ : ≈.LeftInverse ε -_ _∙_ → ≈ᴹ.LeftInverse (εᴹ {n}) -ᴹ_ _∙ᴹ_ -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) - -ᴹ‿inverseʳ : ≈.RightInverse 0# -_ _+_ → ≈ᴹ.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverseʳ : ≈.RightInverse ε -_ _∙_ → ≈ᴹ.RightInverse (εᴹ {n}) -ᴹ_ _∙ᴹ_ -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) - -ᴹ‿inverse : ≈.Inverse 0# -_ _+_ → ≈ᴹ.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_ + -ᴹ‿inverse : ≈.Inverse ε -_ _∙_ → ≈ᴹ.Inverse (εᴹ {n}) -ᴹ_ _∙ᴹ_ -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ -ᴹ‿cong : ≈.Congruent₁ -_ → ≈ᴹ.Congruent₁ (-ᴹ_ {n}) -ᴹ‿cong -‿cong xs i = -‿cong (xs i) - isGroup : IsGroup _≈_ _+_ 0# -_ → IsGroup _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ -ᴹ_ + isGroup : IsGroup _≈_ _∙_ ε -_ → IsGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ isGroup isGroup = record { isMonoid = isMonoid G.isMonoid ; inverse = -ᴹ‿inverse G.inverse ; ⁻¹-cong = -ᴹ‿cong G.⁻¹-cong } where module G = IsGroup isGroup - isAbelianGroup : IsAbelianGroup _≈_ _+_ 0# -_ → IsAbelianGroup _≈ᴹ_ (_+ᴹ_ {n}) 0ᴹ -ᴹ_ + isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε -_ → IsAbelianGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ isAbelianGroup isAbelianGroup = record { isGroup = isGroup AG.isGroup - ; comm = +ᴹ-comm AG.comm + ; comm = ∙ᴹ-comm AG.comm } where module AG = IsAbelianGroup isAbelianGroup +module VecNearSemiringProperties (rawNearSemiring : RawNearSemiring a ℓ) where + open VecNearSemiring rawNearSemiring + open MonoidProperties +-rawMonoid public renaming + ( ∙ᴹ-comm to +ᴹ-comm + ; ∙ᴹ-identity to +ᴹ-identity + ) + + module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where open VecSemiring rawSemiring - open MonoidProperties +-rawMonoid public + open VecNearSemiringProperties rawNearSemiring public + open MonoidProperties *-rawMonoid public using () renaming + ( ∙ᴹ-comm to *ᴹ-comm + ; ∙ᴹ-identity to *ᴹ-identity + ) private module LD≈ = LeftDefs Carrier _≈_ module RD≈ = RightDefs Carrier _≈_ @@ -164,6 +176,9 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ₗ-identityˡ : ≈.LeftIdentity 1# _*_ → LD.LeftIdentity 1# (_*ₗ_ {n}) *ₗ-identityˡ *-identityˡ xs i = *-identityˡ (xs i) + *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) + *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) + *ₗ-assoc : ≈.Associative _*_ → LD.Associative _*_ (_*ₗ_ {n}) *ₗ-assoc *-assoc m n xs i = *-assoc m n (xs i) @@ -182,9 +197,6 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᵣ-zeroˡ : RD≈.LeftZero 0# _*_ → RD.LeftZero (0ᴹ {n}) _*ᵣ_ *ᵣ-zeroˡ zeroˡ xs i = zeroˡ xs - *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) - *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) - *ᵣ-assoc : RD≈.Associative _*_ _*_ → RD.Associative _*_ (_*ᵣ_ {n}) *ᵣ-assoc *-assoc xs m n i = *-assoc (xs i) m n @@ -221,6 +233,11 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᴹ-assoc : ≈.Associative _*_ → ≈ᴹ.Associative (_*ᴹ_ {n}) *ᴹ-assoc *-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) +module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) where + open NearSemiring nearSemiring + open VecNearSemiringProperties rawNearSemiring public + + module SemiringProperties (semiring : Semiring a ℓ) where open Semiring semiring open VecSemiring rawSemiring @@ -271,9 +288,8 @@ module SemiringProperties (semiring : Semiring a ℓ) where module RingProperties (ring : Ring a ℓ) where open Ring ring open VecRing rawRing - open VecSemiRingProperties rawSemiring open Group +-group using (rawGroup) - open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse) + open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse; isAbelianGroup) open SemiringProperties semiring public isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ @@ -297,6 +313,36 @@ module RingProperties (ring : Ring a ℓ) where ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse } + +ᴹ-*-isRing : IsRing _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isRing = record + { +-isAbelianGroup = isAbelianGroup +-isAbelianGroup + ; *-cong = *ᴹ-cong *-cong + ; *-assoc = *ᴹ-assoc *-assoc + ; *-identity = *ᴹ-identity *-identity + ; distrib = *ᴹ-+ᴹ-distrib distrib + ; zero = *ᴹ-zero (Ring.zero ring) + } + +module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where + open CommutativeRing commutativeRing + open VecRing rawRing + open RingProperties ring public + -- open Group +-group using (rawGroup) + -- open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse) + -- open SemiringProperties semiring public + + + +ᴹ-*-isCommutativeRing : IsCommutativeRing _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isCommutativeRing = record + { isRing = +ᴹ-*-isRing + ; *-comm = *ᴹ-comm *-comm + } + + isModule : IsModule commutativeRing (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + isModule = record + { isBimodule = isBimodule + } + -- ------------------------------------------------------------------------ -- -- Structures @@ -315,11 +361,6 @@ module RingProperties (ring : Ring a ℓ) where --- isModule : IsModule cring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ --- isModule = record --- { isBimodule = isBimodule --- } - -- +ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ -- +ᴹ-*-isNearSemiring = record -- { +-isMonoid = isMonoid @@ -374,22 +415,6 @@ module RingProperties (ring : Ring a ℓ) where -- ; zero = *ᴹ-zero -- } --- +ᴹ-*-isRing : IsRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ --- +ᴹ-*-isRing = record --- { +-isAbelianGroup = isAbelianGroup --- ; *-cong = *ᴹ-cong --- ; *-assoc = *ᴹ-assoc --- ; *-identity = *ᴹ-identity --- ; distrib = *ᴹ-+ᴹ-distrib --- ; zero = *ᴹ-zero --- } - --- +ᴹ-*-isCommutativeRing : IsCommutativeRing (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ --- +ᴹ-*-isCommutativeRing = record --- { isRing = +ᴹ-*-isRing --- ; *-comm = *ᴹ-comm --- } - -- ------------------------------------------------------------------------ -- -- Bundles From e39e20e447b5ef9680c0bf835c0e9562a45a7c39 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 19:27:43 -0300 Subject: [PATCH 22/25] added magma definitions --- .../Vec/Functional/Algebra/Properties.agda | 106 +++++++++++------- 1 file changed, 63 insertions(+), 43 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index ff5786c30f..6141c1df73 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -141,19 +141,15 @@ module GroupProperties (rawGroup : RawGroup a ℓ) where module VecNearSemiringProperties (rawNearSemiring : RawNearSemiring a ℓ) where open VecNearSemiring rawNearSemiring + open MagmaProperties *-rawMagma public using () renaming + ( ∙ᴹ-comm to *ᴹ-comm + ; ∙ᴹ-assoc to *ᴹ-assoc + ; ∙ᴹ-cong to *ᴹ-cong + ) open MonoidProperties +-rawMonoid public renaming ( ∙ᴹ-comm to +ᴹ-comm ; ∙ᴹ-identity to +ᴹ-identity ) - - -module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where - open VecSemiring rawSemiring - open VecNearSemiringProperties rawNearSemiring public - open MonoidProperties *-rawMonoid public using () renaming - ( ∙ᴹ-comm to *ᴹ-comm - ; ∙ᴹ-identity to *ᴹ-identity - ) private module LD≈ = LeftDefs Carrier _≈_ module RD≈ = RightDefs Carrier _≈_ @@ -173,12 +169,6 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ₗ-distribʳ : _*_ ≈.DistributesOverʳ _+_ → _*ₗ_ LD.DistributesOverʳ _+_ ⟶ _+ᴹ_ {n} *ₗ-distribʳ distribʳ xs m n i = distribʳ (xs i) m n - *ₗ-identityˡ : ≈.LeftIdentity 1# _*_ → LD.LeftIdentity 1# (_*ₗ_ {n}) - *ₗ-identityˡ *-identityˡ xs i = *-identityˡ (xs i) - - *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) - *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) - *ₗ-assoc : ≈.Associative _*_ → LD.Associative _*_ (_*ₗ_ {n}) *ₗ-assoc *-assoc m n xs i = *-assoc m n (xs i) @@ -227,16 +217,70 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᴹ-+ᴹ-distrib : _*_ ≈.DistributesOver _+_ → (_*ᴹ_ {n}) ≈ᴹ.DistributesOver _+ᴹ_ *ᴹ-+ᴹ-distrib (*-+-distribˡ , *-+-distribʳ) = *ᴹ-+ᴹ-distribˡ *-+-distribˡ , *ᴹ-+ᴹ-distribʳ *-+-distribʳ - *ᴹ-cong : ≈.Congruent₂ _*_ → ≈ᴹ.Congruent₂ (_*ᴹ_ {n = n}) - *ᴹ-cong *-cong x≈y u≈v i = *-cong (x≈y i) (u≈v i) - *ᴹ-assoc : ≈.Associative _*_ → ≈ᴹ.Associative (_*ᴹ_ {n}) - *ᴹ-assoc *-assoc xs ys zs i = *-assoc (xs i) (ys i) (zs i) +module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where + open VecSemiring rawSemiring + open VecNearSemiringProperties rawNearSemiring public + open MonoidProperties *-rawMonoid public using () renaming + ( ∙ᴹ-identity to *ᴹ-identity + ) + private + module LD≈ = LeftDefs Carrier _≈_ + module RD≈ = RightDefs Carrier _≈_ + module BD≈ = BiDefs Carrier Carrier _≈_ + module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n = n}) + module RD {n} = RightDefs Carrier (_≈ᴹ_ {n = n}) + module BD {n} = BiDefs Carrier Carrier (_≈ᴹ_ {n = n}) + module ≈ = ADefinitions _≈_ + module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) + + *ₗ-identityˡ : ≈.LeftIdentity 1# _*_ → LD.LeftIdentity 1# (_*ₗ_ {n}) + *ₗ-identityˡ *-identityˡ xs i = *-identityˡ (xs i) + + *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) + *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) where open NearSemiring nearSemiring + open VecNearSemiring rawNearSemiring open VecNearSemiringProperties rawNearSemiring public + +ᴹ-*-isNearSemiring : IsNearSemiring _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isNearSemiring = record + { +-isMonoid = isMonoid +-isMonoid + ; *-cong = *ᴹ-cong *-cong + ; *-assoc = *ᴹ-assoc *-assoc + ; distribʳ = *ᴹ-+ᴹ-distribʳ distribʳ + ; zeroˡ = *ᴹ-zeroˡ zeroˡ + } + +module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) where + open SemiringWithoutOne semiringWithoutOne + open VecNearSemiring rawNearSemiring + open NearSemiringProperties nearSemiring public + + +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isSemiringWithoutOne = record + { +-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + ; *-cong = *ᴹ-cong *-cong + ; *-assoc = *ᴹ-assoc *-assoc + ; distrib = *ᴹ-+ᴹ-distrib distrib + ; zero = *ᴹ-zero (SemiringWithoutOne.zero semiringWithoutOne) + } + + +module CommutativeSemiringWithoutOneProperties + (commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne a ℓ) where + + open CommutativeSemiringWithoutOne commutativeSemiringWithoutOne + open VecNearSemiring rawNearSemiring + open SemiringWithoutOneProperties semiringWithoutOne public + + +ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ + +ᴹ-*-isCommutativeSemiringWithoutOne = record + {isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne + ; *-comm = *ᴹ-comm *-comm + } module SemiringProperties (semiring : Semiring a ℓ) where open Semiring semiring @@ -361,30 +405,6 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where --- +ᴹ-*-isNearSemiring : IsNearSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ --- +ᴹ-*-isNearSemiring = record --- { +-isMonoid = isMonoid --- ; *-cong = *ᴹ-cong --- ; *-assoc = *ᴹ-assoc --- ; distribʳ = *ᴹ-+ᴹ-distribʳ --- ; zeroˡ = *ᴹ-zeroˡ --- } - --- +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ --- +ᴹ-*-isSemiringWithoutOne = record --- { +-isCommutativeMonoid = isCommutativeMonoid --- ; *-cong = *ᴹ-cong --- ; *-assoc = *ᴹ-assoc --- ; distrib = *ᴹ-+ᴹ-distrib --- ; zero = *ᴹ-zero --- } - --- +ᴹ-*-isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ --- +ᴹ-*-isCommutativeSemiringWithoutOne = record --- {isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne --- ; *-comm = *ᴹ-comm --- } - -- +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ -- +ᴹ-*-isSemiringWithoutAnnihilatingZero = record -- { +-isCommutativeMonoid = isCommutativeMonoid From 59e693e421340952b62489262e77e58a18d6ae19 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 20:28:16 -0300 Subject: [PATCH 23/25] added some more groups --- .../Vec/Functional/Algebra/Properties.agda | 96 ++++++++++++------- 1 file changed, 61 insertions(+), 35 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 6141c1df73..6ae22b9aad 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -282,10 +282,26 @@ module CommutativeSemiringWithoutOneProperties ; *-comm = *ᴹ-comm *-comm } +module SemiringWithoutAnnihilatingZeroProperties + (semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ) where + + open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero + open VecSemiring rawSemiring + open VecSemiRingProperties rawSemiring public + + +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + ; *-cong = *ᴹ-cong *-cong + ; *-assoc = *ᴹ-assoc *-assoc + ; *-identity = *ᴹ-identity *-identity + ; distrib = *ᴹ-+ᴹ-distrib distrib + } + module SemiringProperties (semiring : Semiring a ℓ) where open Semiring semiring open VecSemiring rawSemiring - open VecSemiRingProperties rawSemiring public + open SemiringWithoutAnnihilatingZeroProperties semiringWithoutAnnihilatingZero public isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isPreleftSemimodule = record @@ -329,6 +345,50 @@ module SemiringProperties (semiring : Semiring a ℓ) where ; isPreleftSemimodule = isPreleftSemimodule } + +ᴹ-*-isSemiring : IsSemiring _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isSemiring = record + { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero + ; zero = *ᴹ-zero (Semiring.zero semiring) + } + +module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring a ℓ) where + open CommutativeSemiring commutativeSemiring + open VecSemiring rawSemiring + open SemiringProperties semiring + + +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ + +ᴹ-*-isCommutativeSemiring = record + { isSemiring = +ᴹ-*-isSemiring + ; *-comm = *ᴹ-comm *-comm + } + +module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) where + open RingWithoutOne ringWithoutOne + + rawNearSemiring : RawNearSemiring a ℓ + rawNearSemiring = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + } + + open Group +-group renaming (rawGroup to +-rawGroup) using () + open VecGroup +-rawGroup using (-ᴹ_) + open GroupProperties +-rawGroup using (isAbelianGroup) public + open VecNearSemiring rawNearSemiring + open VecNearSemiringProperties rawNearSemiring public + + +ᴹ-*-isRingWithoutOne : IsRingWithoutOne _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ + +ᴹ-*-isRingWithoutOne = record + { +-isAbelianGroup = isAbelianGroup +-isAbelianGroup + ; *-cong = *ᴹ-cong *-cong + ; *-assoc = *ᴹ-assoc *-assoc + ; distrib = *ᴹ-+ᴹ-distrib distrib + ; zero = *ᴹ-zero (RingWithoutOne.zero ringWithoutOne) + } + module RingProperties (ring : Ring a ℓ) where open Ring ring open VecRing rawRing @@ -371,10 +431,6 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where open CommutativeRing commutativeRing open VecRing rawRing open RingProperties ring public - -- open Group +-group using (rawGroup) - -- open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse) - -- open SemiringProperties semiring public - +ᴹ-*-isCommutativeRing : IsCommutativeRing _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ +ᴹ-*-isCommutativeRing = record @@ -405,36 +461,6 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where --- +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ --- +ᴹ-*-isSemiringWithoutAnnihilatingZero = record --- { +-isCommutativeMonoid = isCommutativeMonoid --- ; *-cong = *ᴹ-cong --- ; *-assoc = *ᴹ-assoc --- ; *-identity = *ᴹ-identity --- ; distrib = *ᴹ-+ᴹ-distrib --- } - --- +ᴹ-*-isSemiring : IsSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ --- +ᴹ-*-isSemiring = record --- { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero --- ; zero = *ᴹ-zero --- } - --- +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ --- +ᴹ-*-isCommutativeSemiring = record --- { isSemiring = +ᴹ-*-isSemiring --- ; *-comm = *ᴹ-comm --- } - --- +ᴹ-*-isRingWithoutOne : IsRingWithoutOne (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ --- +ᴹ-*-isRingWithoutOne = record --- { +-isAbelianGroup = isAbelianGroup --- ; *-cong = *ᴹ-cong --- ; *-assoc = *ᴹ-assoc --- ; distrib = *ᴹ-+ᴹ-distrib --- ; zero = *ᴹ-zero --- } - -- ------------------------------------------------------------------------ -- -- Bundles From 967be038307fe20d05228ab57306c883f811476c Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 22:24:21 -0300 Subject: [PATCH 24/25] added structures inside --- .../Vec/Functional/Algebra/Properties.agda | 214 +++++++++++++----- 1 file changed, 154 insertions(+), 60 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index 6ae22b9aad..ad02999b16 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -31,7 +31,7 @@ private variable ------------------------------------------------------------------------ -- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_ -module MagmaProperties (rawMagma : RawMagma a ℓ) where +module RawMagmaProperties (rawMagma : RawMagma a ℓ) where open VecMagma rawMagma open IsEquivalence private @@ -51,34 +51,33 @@ module MagmaProperties (rawMagma : RawMagma a ℓ) where ∙ᴹ-comm ∙-comm xs ys i = ∙-comm (xs i) (ys i) - isMagma : IsMagma _≈_ _∙_ → IsMagma _≈ᴹ_ (_∙ᴹ_ {n}) - isMagma isMagma = record - { isEquivalence = ≈ᴹ-isEquivalence isEquivalence - ; ∙-cong = ∙ᴹ-cong ∙-cong - } where open IsMagma isMagma - - isCommutativeMagma : IsCommutativeMagma _≈_ _∙_ → IsCommutativeMagma _≈ᴹ_ (_∙ᴹ_ {n}) - isCommutativeMagma isCMagma = record - { isMagma = isMagma CM.isMagma - ; comm = ∙ᴹ-comm CM.comm - } where module CM = IsCommutativeMagma isCMagma + -- isMagma : IsMagma _≈_ _∙_ → IsMagma _≈ᴹ_ (_∙ᴹ_ {n}) + -- isMagma isMagma = record + -- { isEquivalence = ≈ᴹ-isEquivalence isEquivalence + -- ; ∙-cong = ∙ᴹ-cong ∙-cong + -- } where open IsMagma isMagma - isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) - isSemigroup isSemigroup = record - { isMagma = isMagma SG.isMagma - ; assoc = ∙ᴹ-assoc SG.assoc - } where module SG = IsSemigroup isSemigroup + -- isCommutativeMagma : IsCommutativeMagma _≈_ _∙_ → IsCommutativeMagma _≈ᴹ_ (_∙ᴹ_ {n}) + -- isCommutativeMagma isCMagma = record + -- { isMagma = isMagma CM.isMagma + -- ; comm = ∙ᴹ-comm CM.comm + -- } where module CM = IsCommutativeMagma isCMagma - isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ → IsCommutativeSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) - isCommutativeSemigroup isCommutativeSemigroup = record - { isSemigroup = isSemigroup SG.isSemigroup - ; comm = ∙ᴹ-comm SG.comm - } where module SG = IsCommutativeSemigroup isCommutativeSemigroup + -- isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) + -- isSemigroup isSemigroup = record + -- { isMagma = isMagma SG.isMagma + -- ; assoc = ∙ᴹ-assoc SG.assoc + -- } where module SG = IsSemigroup isSemigroup + -- isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ → IsCommutativeSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) + -- isCommutativeSemigroup isCommutativeSemigroup = record + -- { isSemigroup = isSemigroup SG.isSemigroup + -- ; comm = ∙ᴹ-comm SG.comm + -- } where module SG = IsCommutativeSemigroup isCommutativeSemigroup -module MonoidProperties (rawMonoid : RawMonoid a ℓ) where +module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) where open VecMonoid rawMonoid - open MagmaProperties rawMagma public + open RawMagmaProperties rawMagma public private module ≈ = ADefinitions _≈_ module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) @@ -93,22 +92,22 @@ module MonoidProperties (rawMonoid : RawMonoid a ℓ) where ∙ᴹ-identity (∙-identityˡ , ∙-identityʳ) = ∙ᴹ-identityˡ ∙-identityˡ , ∙ᴹ-identityʳ ∙-identityʳ - isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ - isMonoid isMonoid = record - { isSemigroup = isSemigroup M.isSemigroup - ; identity = ∙ᴹ-identity M.identity - } where module M = IsMonoid isMonoid + -- isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ + -- isMonoid isMonoid = record + -- { isSemigroup = isSemigroup M.isSemigroup + -- ; identity = ∙ᴹ-identity M.identity + -- } where module M = IsMonoid isMonoid - isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε → IsCommutativeMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ - isCommutativeMonoid isCommutativeMonoid = record - { isMonoid = isMonoid CM.isMonoid - ; comm = ∙ᴹ-comm CM.comm - } where module CM = IsCommutativeMonoid isCommutativeMonoid + -- isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε → IsCommutativeMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ + -- isCommutativeMonoid isCommutativeMonoid = record + -- { isMonoid = isMonoid CM.isMonoid + -- ; comm = ∙ᴹ-comm CM.comm + -- } where module CM = IsCommutativeMonoid isCommutativeMonoid -module GroupProperties (rawGroup : RawGroup a ℓ) where +module RawGroupProperties (rawGroup : RawGroup a ℓ) where open VecGroup rawGroup renaming (_⁻¹ to -_) - open MonoidProperties rawMonoid public + open RawMonoidProperties rawMonoid public private module ≈ = ADefinitions _≈_ module ≈ᴹ {n} = ADefinitions (_≈ᴹ_ {n = n}) @@ -126,27 +125,27 @@ module GroupProperties (rawGroup : RawGroup a ℓ) where -ᴹ‿cong -‿cong xs i = -‿cong (xs i) - isGroup : IsGroup _≈_ _∙_ ε -_ → IsGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ - isGroup isGroup = record - { isMonoid = isMonoid G.isMonoid - ; inverse = -ᴹ‿inverse G.inverse - ; ⁻¹-cong = -ᴹ‿cong G.⁻¹-cong - } where module G = IsGroup isGroup +-- isGroup : IsGroup _≈_ _∙_ ε -_ → IsGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ +-- isGroup isGroup = record +-- { isMonoid = isMonoid G.isMonoid +-- ; inverse = -ᴹ‿inverse G.inverse +-- ; ⁻¹-cong = -ᴹ‿cong G.⁻¹-cong +-- } where module G = IsGroup isGroup - isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε -_ → IsAbelianGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ - isAbelianGroup isAbelianGroup = record - { isGroup = isGroup AG.isGroup - ; comm = ∙ᴹ-comm AG.comm - } where module AG = IsAbelianGroup isAbelianGroup +-- isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε -_ → IsAbelianGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ +-- isAbelianGroup isAbelianGroup = record +-- { isGroup = isGroup AG.isGroup +-- ; comm = ∙ᴹ-comm AG.comm +-- } where module AG = IsAbelianGroup isAbelianGroup module VecNearSemiringProperties (rawNearSemiring : RawNearSemiring a ℓ) where open VecNearSemiring rawNearSemiring - open MagmaProperties *-rawMagma public using () renaming + open RawMagmaProperties *-rawMagma public using () renaming ( ∙ᴹ-comm to *ᴹ-comm ; ∙ᴹ-assoc to *ᴹ-assoc ; ∙ᴹ-cong to *ᴹ-cong ) - open MonoidProperties +-rawMonoid public renaming + open RawMonoidProperties +-rawMonoid public renaming ( ∙ᴹ-comm to +ᴹ-comm ; ∙ᴹ-identity to +ᴹ-identity ) @@ -221,7 +220,7 @@ module VecNearSemiringProperties (rawNearSemiring : RawNearSemiring a ℓ) where module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where open VecSemiring rawSemiring open VecNearSemiringProperties rawNearSemiring public - open MonoidProperties *-rawMonoid public using () renaming + open RawMonoidProperties *-rawMonoid public using () renaming ( ∙ᴹ-identity to *ᴹ-identity ) private @@ -240,14 +239,106 @@ module VecSemiRingProperties (rawSemiring : RawSemiring a ℓ) where *ᵣ-identityʳ : RD≈.RightIdentity 1# _*_ → RD.RightIdentity 1# (_*ᵣ_ {n}) *ᵣ-identityʳ *-identityʳ xs i = *-identityʳ (xs i) +module MagmaProperties (magma : Magma a ℓ) where + open Magma magma + open VecMagma rawMagma + open RawMagmaProperties rawMagma public + + ∙ᴹ-isMagma : IsMagma _≈ᴹ_ (_∙ᴹ_ {n}) + ∙ᴹ-isMagma = record + { isEquivalence = ≈ᴹ-isEquivalence isEquivalence + ; ∙-cong = ∙ᴹ-cong ∙-cong + } + +module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) where + open CommutativeMagma commutativeMagma + open VecMagma rawMagma + open MagmaProperties magma public + + ∙ᴹ-isCommutativeMagma : IsCommutativeMagma _≈ᴹ_ (_∙ᴹ_ {n}) + ∙ᴹ-isCommutativeMagma = record + { isMagma = ∙ᴹ-isMagma + ; comm = ∙ᴹ-comm comm + } + +module SemiRawGroupProperties (semigroup : Semigroup a ℓ) where + open Semigroup semigroup + open VecMagma rawMagma + open MagmaProperties magma public + + ∙ᴹ-isSemigroup : IsSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) + ∙ᴹ-isSemigroup = record + { isMagma = ∙ᴹ-isMagma + ; assoc = ∙ᴹ-assoc assoc + } + +module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigroup a ℓ) where + open CommutativeSemigroup commutativeSemigroup + open VecMagma rawMagma + open SemiRawGroupProperties semigroup public + + ∙ᴹ-isCommutativeSemigroup : IsCommutativeSemigroup _≈ᴹ_ (_∙ᴹ_ {n}) + ∙ᴹ-isCommutativeSemigroup = record + { isSemigroup = ∙ᴹ-isSemigroup + ; comm = ∙ᴹ-comm comm + } + +module MonoidProperties (monoid : Monoid a ℓ) where + open Monoid monoid + open VecMonoid rawMonoid + open RawMonoidProperties rawMonoid public using (∙ᴹ-identity) + open SemiRawGroupProperties semigroup public + + ∙ᴹ-isMonoid : IsMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ + ∙ᴹ-isMonoid = record + { isSemigroup = ∙ᴹ-isSemigroup + ; identity = ∙ᴹ-identity identity + } + +module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) where + open CommutativeMonoid commutativeMonoid + open VecMonoid rawMonoid + open MonoidProperties monoid public + + ∙ᴹ-isCommutativeMonoid : IsCommutativeMonoid _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ + ∙ᴹ-isCommutativeMonoid = record + { isMonoid = ∙ᴹ-isMonoid + ; comm = ∙ᴹ-comm comm + } + +module GroupProperties (group : Group a ℓ) where + open Group group + open VecGroup rawGroup + open RawGroupProperties rawGroup public using (-ᴹ‿inverse; -ᴹ‿cong) + open MonoidProperties monoid public + + ∙ᴹ-isGroup : IsGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ + ∙ᴹ-isGroup = record + { isMonoid = ∙ᴹ-isMonoid + ; inverse = -ᴹ‿inverse inverse + ; ⁻¹-cong = -ᴹ‿cong ⁻¹-cong + } + +module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) where + open AbelianGroup abelianGroup + open VecGroup rawGroup + open GroupProperties group public + + ∙ᴹ-isAbelianGroup : IsAbelianGroup _≈ᴹ_ (_∙ᴹ_ {n}) εᴹ -ᴹ_ + ∙ᴹ-isAbelianGroup = record + { isGroup = ∙ᴹ-isGroup + ; comm = ∙ᴹ-comm comm + } + module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) where open NearSemiring nearSemiring open VecNearSemiring rawNearSemiring open VecNearSemiringProperties rawNearSemiring public + open MonoidProperties +-monoid public using (∙ᴹ-isMonoid) +ᴹ-*-isNearSemiring : IsNearSemiring _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ +ᴹ-*-isNearSemiring = record - { +-isMonoid = isMonoid +-isMonoid + { +-isMonoid = ∙ᴹ-isMonoid ; *-cong = *ᴹ-cong *-cong ; *-assoc = *ᴹ-assoc *-assoc ; distribʳ = *ᴹ-+ᴹ-distribʳ distribʳ @@ -258,10 +349,11 @@ module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a open SemiringWithoutOne semiringWithoutOne open VecNearSemiring rawNearSemiring open NearSemiringProperties nearSemiring public + open CommutativeMonoidProperties +-commutativeMonoid public using (∙ᴹ-isCommutativeMonoid) +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ +ᴹ-*-isSemiringWithoutOne = record - { +-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + { +-isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid ; *-cong = *ᴹ-cong *-cong ; *-assoc = *ᴹ-assoc *-assoc ; distrib = *ᴹ-+ᴹ-distrib distrib @@ -288,10 +380,11 @@ module SemiringWithoutAnnihilatingZeroProperties open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero open VecSemiring rawSemiring open VecSemiRingProperties rawSemiring public + open CommutativeMonoidProperties +-commutativeMonoid public using (∙ᴹ-isCommutativeMonoid) +ᴹ-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ 0ᴹ 1ᴹ +ᴹ-*-isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + { +-isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid ; *-cong = *ᴹ-cong *-cong ; *-assoc = *ᴹ-assoc *-assoc ; *-identity = *ᴹ-identity *-identity @@ -327,13 +420,13 @@ module SemiringProperties (semiring : Semiring a ℓ) where isRightSemimodule : IsRightSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ᵣ_ isRightSemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + { +ᴹ-isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid ; isPrerightSemimodule = isPrerightSemimodule } isBisemimodule : IsBisemimodule semiring semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ isBisemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + { +ᴹ-isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid ; isPreleftSemimodule = isPreleftSemimodule ; isPrerightSemimodule = isPrerightSemimodule ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc *-assoc @@ -341,7 +434,7 @@ module SemiringProperties (semiring : Semiring a ℓ) where isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_ isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid +-isCommutativeMonoid + { +ᴹ-isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid ; isPreleftSemimodule = isPreleftSemimodule } @@ -376,13 +469,13 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) where open Group +-group renaming (rawGroup to +-rawGroup) using () open VecGroup +-rawGroup using (-ᴹ_) - open GroupProperties +-rawGroup using (isAbelianGroup) public + open AbelianGroupProperties +-abelianGroup using (∙ᴹ-isAbelianGroup) public open VecNearSemiring rawNearSemiring open VecNearSemiringProperties rawNearSemiring public +ᴹ-*-isRingWithoutOne : IsRingWithoutOne _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ +ᴹ-*-isRingWithoutOne = record - { +-isAbelianGroup = isAbelianGroup +-isAbelianGroup + { +-isAbelianGroup = ∙ᴹ-isAbelianGroup ; *-cong = *ᴹ-cong *-cong ; *-assoc = *ᴹ-assoc *-assoc ; distrib = *ᴹ-+ᴹ-distrib distrib @@ -393,7 +486,8 @@ module RingProperties (ring : Ring a ℓ) where open Ring ring open VecRing rawRing open Group +-group using (rawGroup) - open GroupProperties rawGroup public using (-ᴹ‿cong; -ᴹ‿inverse; isAbelianGroup) + open AbelianGroupProperties +-abelianGroup public + using (∙ᴹ-isAbelianGroup; -ᴹ‿cong; -ᴹ‿inverse) open SemiringProperties semiring public isRightModule : IsRightModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ @@ -419,7 +513,7 @@ module RingProperties (ring : Ring a ℓ) where +ᴹ-*-isRing : IsRing _≈ᴹ_ (_+ᴹ_ {n}) _*ᴹ_ -ᴹ_ 0ᴹ 1ᴹ +ᴹ-*-isRing = record - { +-isAbelianGroup = isAbelianGroup +-isAbelianGroup + { +-isAbelianGroup = ∙ᴹ-isAbelianGroup ; *-cong = *ᴹ-cong *-cong ; *-assoc = *ᴹ-assoc *-assoc ; *-identity = *ᴹ-identity *-identity From 4dccb0e32a573b063240936b568907da20a31604 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 26 May 2023 22:40:15 -0300 Subject: [PATCH 25/25] added the bundles --- .../Vec/Functional/Algebra/Properties.agda | 234 ++++++++---------- 1 file changed, 99 insertions(+), 135 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index ad02999b16..c65a91e2c3 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -250,6 +250,11 @@ module MagmaProperties (magma : Magma a ℓ) where ; ∙-cong = ∙ᴹ-cong ∙-cong } + ∙ᴹ-magma : ℕ → Magma _ _ + ∙ᴹ-magma n = record + { isMagma = ∙ᴹ-isMagma {n} + } + module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) where open CommutativeMagma commutativeMagma open VecMagma rawMagma @@ -261,6 +266,11 @@ module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) wh ; comm = ∙ᴹ-comm comm } + ∙ᴹ-commutativeMagma : ℕ → CommutativeMagma _ _ + ∙ᴹ-commutativeMagma n = record { + isCommutativeMagma = ∙ᴹ-isCommutativeMagma {n} + } + module SemiRawGroupProperties (semigroup : Semigroup a ℓ) where open Semigroup semigroup open VecMagma rawMagma @@ -272,6 +282,11 @@ module SemiRawGroupProperties (semigroup : Semigroup a ℓ) where ; assoc = ∙ᴹ-assoc assoc } + ∙ᴹ-semigroup : ℕ → Semigroup _ _ + ∙ᴹ-semigroup n = record + { isSemigroup = ∙ᴹ-isSemigroup {n} + } + module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigroup a ℓ) where open CommutativeSemigroup commutativeSemigroup open VecMagma rawMagma @@ -283,6 +298,11 @@ module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigro ; comm = ∙ᴹ-comm comm } + ∙ᴹ-commutativeSemigroup : ℕ → CommutativeSemigroup _ _ + ∙ᴹ-commutativeSemigroup n = record + { isCommutativeSemigroup = ∙ᴹ-isCommutativeSemigroup {n} + } + module MonoidProperties (monoid : Monoid a ℓ) where open Monoid monoid open VecMonoid rawMonoid @@ -295,6 +315,11 @@ module MonoidProperties (monoid : Monoid a ℓ) where ; identity = ∙ᴹ-identity identity } + -- *ᴹ-monoid : ℕ → Monoid _ _ + -- *ᴹ-monoid n = record + -- { isMonoid = *ᴹ-isMonoid {n} + -- } + module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) where open CommutativeMonoid commutativeMonoid open VecMonoid rawMonoid @@ -306,6 +331,11 @@ module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) ; comm = ∙ᴹ-comm comm } + ∙ᴹ-commutativeMonoid : ℕ → CommutativeMonoid _ _ + ∙ᴹ-commutativeMonoid n = record + { isCommutativeMonoid = ∙ᴹ-isCommutativeMonoid {n} + } + module GroupProperties (group : Group a ℓ) where open Group group open VecGroup rawGroup @@ -319,6 +349,11 @@ module GroupProperties (group : Group a ℓ) where ; ⁻¹-cong = -ᴹ‿cong ⁻¹-cong } + ∙ᴹ-group : ℕ → Group _ _ + ∙ᴹ-group n = record + { isGroup = ∙ᴹ-isGroup {n} + } + module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) where open AbelianGroup abelianGroup open VecGroup rawGroup @@ -345,6 +380,11 @@ module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) where ; zeroˡ = *ᴹ-zeroˡ zeroˡ } + +ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ + +ᴹ-*-nearSemiring n = record + { isNearSemiring = +ᴹ-*-isNearSemiring {n} + } + module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) where open SemiringWithoutOne semiringWithoutOne open VecNearSemiring rawNearSemiring @@ -360,6 +400,11 @@ module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ; zero = *ᴹ-zero (SemiringWithoutOne.zero semiringWithoutOne) } + +ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ + +ᴹ-*-semiringWithoutOne n = record + { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne {n} + } + module CommutativeSemiringWithoutOneProperties (commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne a ℓ) where @@ -374,6 +419,11 @@ module CommutativeSemiringWithoutOneProperties ; *-comm = *ᴹ-comm *-comm } + +ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ + +ᴹ-*-commutativeSemiringWithoutOne n = record + { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne {n} + } + module SemiringWithoutAnnihilatingZeroProperties (semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ) where @@ -391,6 +441,11 @@ module SemiringWithoutAnnihilatingZeroProperties ; distrib = *ᴹ-+ᴹ-distrib distrib } + +ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ + +ᴹ-*-semiringWithoutAnnihilatingZero n = record + { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero {n} + } + module SemiringProperties (semiring : Semiring a ℓ) where open Semiring semiring open VecSemiring rawSemiring @@ -444,6 +499,16 @@ module SemiringProperties (semiring : Semiring a ℓ) where ; zero = *ᴹ-zero (Semiring.zero semiring) } + leftSemimodule : ℕ → LeftSemimodule _ _ _ + leftSemimodule n = record + { isLeftSemimodule = isLeftSemimodule {n} + } + + +ᴹ-*-semiring : ℕ → Semiring _ _ + +ᴹ-*-semiring n = record + { isSemiring = +ᴹ-*-isSemiring {n} + } + module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring a ℓ) where open CommutativeSemiring commutativeSemiring open VecSemiring rawSemiring @@ -455,6 +520,11 @@ module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring ; *-comm = *ᴹ-comm *-comm } + +ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ + +ᴹ-*-commutativeSemiring n = record + { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring {n} + } + module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) where open RingWithoutOne ringWithoutOne @@ -482,6 +552,11 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) where ; zero = *ᴹ-zero (RingWithoutOne.zero ringWithoutOne) } + +ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ + +ᴹ-*-ringWithoutOne n = record + { isRingWithoutOne = +ᴹ-*-isRingWithoutOne {n} + } + module RingProperties (ring : Ring a ℓ) where open Ring ring open VecRing rawRing @@ -521,6 +596,26 @@ module RingProperties (ring : Ring a ℓ) where ; zero = *ᴹ-zero (Ring.zero ring) } + leftModule : ℕ → LeftModule _ _ _ + leftModule n = record + { isLeftModule = isLeftModule {n} + } + + bisemimodule : ℕ → Bisemimodule _ _ _ _ + bisemimodule n = record + { isBisemimodule = isBisemimodule {n} + } + + rightModule : ℕ → RightModule _ _ _ + rightModule n = record + { isRightModule = isRightModule {n} + } + + bimodule : ℕ → Bimodule _ _ _ _ + bimodule n = record + { isBimodule = isBimodule {n} + } + module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where open CommutativeRing commutativeRing open VecRing rawRing @@ -537,138 +632,7 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) where { isBimodule = isBimodule } - --- ------------------------------------------------------------------------ --- -- Structures - --- *ᴹ-isSemigroup : IsSemigroup (_*ᴹ_ {n}) --- *ᴹ-isSemigroup = record --- { isMagma = *ᴹ-isMagma --- ; assoc = *ᴹ-assoc --- } - --- *ᴹ-isMonoid : IsMonoid (_*ᴹ_ {n}) 1ᴹ --- *ᴹ-isMonoid = record --- { isSemigroup = *ᴹ-isSemigroup --- ; identity = *ᴹ-identity --- } - - - --- ------------------------------------------------------------------------ --- -- Bundles - --- magma : ℕ → Magma _ _ --- magma n = record --- { isMagma = isMagma {n} --- } - --- *ᴹ-magma : ℕ → Magma _ _ --- *ᴹ-magma n = record --- { isMagma = *ᴹ-isMagma {n} --- } - --- commutativeMagma : ℕ → CommutativeMagma _ _ --- commutativeMagma n = record { --- isCommutativeMagma = isCommutativeMagma {n} --- } - --- semigroup : ℕ → Semigroup _ _ --- semigroup n = record --- { isSemigroup = isSemigroup {n} --- } - --- *ᴹ-semigroup : ℕ → Semigroup _ _ --- *ᴹ-semigroup n = record --- { isSemigroup = *ᴹ-isSemigroup {n} --- } - --- commutativeSemigroup : ℕ → CommutativeSemigroup _ _ --- commutativeSemigroup n = record --- { isCommutativeSemigroup = isCommutativeSemigroup {n} --- } - --- monoid : ℕ → Monoid _ _ --- monoid n = record --- { isMonoid = isMonoid {n} --- } - --- *ᴹ-monoid : ℕ → Monoid _ _ --- *ᴹ-monoid n = record --- { isMonoid = *ᴹ-isMonoid {n} --- } - --- commutativeMonoid : ℕ → CommutativeMonoid _ _ --- commutativeMonoid n = record --- { isCommutativeMonoid = isCommutativeMonoid {n} --- } - --- group : ℕ → Group _ _ --- group n = record --- { isGroup = isGroup {n} --- } - --- leftSemimodule : ℕ → LeftSemimodule _ _ _ --- leftSemimodule n = record --- { isLeftSemimodule = isLeftSemimodule {n} --- } - --- leftModule : ℕ → LeftModule _ _ _ --- leftModule n = record --- { isLeftModule = isLeftModule {n} --- } - --- bisemimodule : ℕ → Bisemimodule _ _ _ _ --- bisemimodule n = record --- { isBisemimodule = isBisemimodule {n} --- } - --- rightModule : ℕ → RightModule _ _ _ --- rightModule n = record --- { isRightModule = isRightModule {n} --- } - --- bimodule : ℕ → Bimodule _ _ _ _ --- bimodule n = record --- { isBimodule = isBimodule {n} --- } - --- module' : ℕ → Module _ _ _ --- module' n = record --- { isModule = isModule {n} --- } - --- +ᴹ-*-nearSemiring : ℕ → NearSemiring _ _ --- +ᴹ-*-nearSemiring n = record --- { isNearSemiring = +ᴹ-*-isNearSemiring {n} --- } - --- +ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _ --- +ᴹ-*-semiringWithoutOne n = record --- { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne {n} --- } - --- +ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _ --- +ᴹ-*-commutativeSemiringWithoutOne n = record --- { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne {n} --- } - --- +ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _ --- +ᴹ-*-semiringWithoutAnnihilatingZero n = record --- { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero {n} --- } - --- +ᴹ-*-semiring : ℕ → Semiring _ _ --- +ᴹ-*-semiring n = record --- { isSemiring = +ᴹ-*-isSemiring {n} --- } - --- +ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _ --- +ᴹ-*-commutativeSemiring n = record --- { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring {n} --- } - --- +ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _ --- +ᴹ-*-ringWithoutOne n = record --- { isRingWithoutOne = +ᴹ-*-isRingWithoutOne {n} --- } + module' : ℕ → Module _ _ _ + module' n = record + { isModule = isModule {n} + }