From 29dacb01350879a1f94ca100aafc058298bcb8a1 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 29 Mar 2026 17:49:49 -0500
Subject: Add semimodule of vectors over a commutative rig

---
 Data/Vector/Semimodule.agda | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 Data/Vector/Semimodule.agda

(limited to 'Data/Vector/Semimodule.agda')

diff --git a/Data/Vector/Semimodule.agda b/Data/Vector/Semimodule.agda
new file mode 100644
index 0000000..f6fe2de
--- /dev/null
+++ b/Data/Vector/Semimodule.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CommutativeSemiring)
+open import Level using (Level; _⊔_)
+
+module Data.Vector.Semimodule {c ℓ : Level} (R : CommutativeSemiring c ℓ) where
+
+module R = CommutativeSemiring R
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+open import Algebra.Module using (Bisemimodule; Semimodule)
+open import Data.Nat using (ℕ)
+open import Data.Vector.Core R.setoid using (Vector; _≊_)
+open import Data.Vec using (Vec)
+open import Data.Vector.Bisemimodule R.semiring using (⟨_⟩_; _⟨_⟩; Vector-Bisemimodule)
+
+open R
+open Vec
+
+private
+  variable
+    n : ℕ
+
+opaque
+
+  unfolding ⟨_⟩_ _⟨_⟩
+
+  -- scaling on left equals scaling on right
+  ⟨-⟩-comm : (r : Carrier) (V : Vector n) → r ⟨ V ⟩ ≊ ⟨ V ⟩ r
+  ⟨-⟩-comm r [] = PW.[]
+  ⟨-⟩-comm r (x ∷ V) = *-comm r x PW.∷ ⟨-⟩-comm r V
+
+Vector-Semimodule : ℕ → Semimodule R c (c ⊔ ℓ)
+Vector-Semimodule n = record
+    { Bisemimodule (Vector-Bisemimodule n)
+    ; isSemimodule = record
+        { isBisemimodule = record { Bisemimodule (Vector-Bisemimodule n) }
+        ; *ₗ-*ᵣ-coincident = ⟨-⟩-comm
+        }
+    }
-- 
cgit v1.2.3