Functional vector module

CHANGELOG.md

@@ -3027,3 +3027,113 @@ 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 (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`
+```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 : LD.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})
+  *ᵣ-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}) _*ᵣ_
+  *ᴹ-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ᴹ _*ₗ_
+  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 _ _ _
+  bisemimodule : ℕ → Bisemimodule _ _ _ _
+  rightModule : ℕ → RightModule _ _ _
+  bimodule : ℕ → Bimodule _ _ _ _
+  module' : ℕ → Module _ _ _
+  +ᴹ-*-nearSemiring : ℕ → NearSemiring _ _
+  +ᴹ-*-semiringWithoutOne : ℕ → SemiringWithoutOne _ _
+  +ᴹ-*-commutativeSemiringWithoutOne : ℕ → CommutativeSemiringWithoutOne _ _
+  +ᴹ-*-semiringWithoutAnnihilatingZero : ℕ → SemiringWithoutAnnihilatingZero _ _
+  +ᴹ-*-semiring : ℕ → Semiring _ _
+  +ᴹ-*-commutativeSemiring : ℕ → CommutativeSemiring _ _
+  +ᴹ-*-ringWithoutOne : ℕ → RingWithoutOne _ _
+```

src/Data/Vec/Functional/Algebra/Base.agda

@@ -0,0 +1,73 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some Vector-related module Definitions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Functional.Algebra.Base where
+
+open import Level using (Level)
+open import Function using (_$_)
+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 using (Rel)
+open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
+
+private variable
+  a ℓ : Level
+  A : Set ℓ
+  n : ℕ
+
+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 public
+  open VecAddition _∙_ public
+  open EqualityVecFunc _≈_ public
+
+module VecMonoid (rawMonoid : RawMonoid a ℓ) where
+  open RawMonoid rawMonoid using (rawMagma; ε) public
+  open VecMagma rawMagma public
+
+  εᴹ : Vector Carrier n
+  εᴹ = replicate ε
+
+module VecGroup (rawGroup : RawGroup a ℓ) where
+  open RawGroup rawGroup using (rawMonoid; _⁻¹) public
+  open VecMonoid rawMonoid public
+
+  -ᴹ_ : Op₁ $ Vector Carrier n
+  -ᴹ_ = map $ _⁻¹
+
+module VecNearSemiring (rawNearSemiring : RawNearSemiring a ℓ) where
+  open RawNearSemiring rawNearSemiring using (+-rawMonoid; *-rawMagma) public
+  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 *_)
+
+  _*ᵣ_ : 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 (-ᴹ_)
+  open VecSemiring rawSemiring public