From 0000b8aee0c002bfdf0f0a310062a80c2c8ea94d Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 29 Mar 2026 16:59:17 -0500 Subject: Add bisemimodule of vectors over a rig --- Data/Vector/Bisemimodule.agda | 233 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 233 insertions(+) create mode 100644 Data/Vector/Bisemimodule.agda (limited to 'Data') diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda new file mode 100644 index 0000000..d895459 --- /dev/null +++ b/Data/Vector/Bisemimodule.agda @@ -0,0 +1,233 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (Semiring) +open import Level using (Level; _⊔_) + +module Data.Vector.Bisemimodule {c ℓ : Level} (R : Semiring c ℓ) where + +module R = Semiring R + +import Data.Vec.Relation.Binary.Pointwise.Inductive as PW +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (CommutativeMonoid) +open import Algebra.Module using (Bisemimodule) +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec; map) +open import Data.Vector.CommutativeMonoid R.+-commutativeMonoid using (Vectorₘ) +open import Data.Vector.Core R.setoid using (Vector; _≊_; module ≊) +open import Data.Vector.Monoid R.*-monoid using () renaming (_⊕_ to _⊗_; ⊕-cong to ⊗-cong) +open import Data.Vector.Monoid R.+-monoid using (sum; sum-cong; _⊕_; ⊕-cong; ⟨ε⟩; ⊕-identityˡ) +open import Function using (flip) + +open R +open Vec +open ℕ + +open ≈-Reasoning setoid + +private + variable + n : ℕ + +opaque + + unfolding Vector + + -- Scaling a vector from the left + _⟨_⟩ : Carrier → Vector n → Vector n + _⟨_⟩ r = map (r *_) + + -⟨-⟩-cong : {r r′ : Carrier} {V V′ : Vector n} → r ≈ r′ → V ≊ V′ → r ⟨ V ⟩ ≊ r′ ⟨ V′ ⟩ + -⟨-⟩-cong ≈r ≊V = PW.map⁺ (*-cong ≈r) ≊V + + -- Scaling a vector from the right + ⟨_⟩_ : Vector n → Carrier → Vector n + ⟨_⟩_ v r = map (_* r) v + + ⟨-⟩--cong : {r r′ : Carrier} {V V′ : Vector n} → V ≊ V′ → r ≈ r′ → ⟨ V ⟩ r ≊ ⟨ V′ ⟩ r′ + ⟨-⟩--cong ≊V ≈r = PW.map⁺ (flip *-cong ≈r) ≊V + + -- Scaling by one from the left + 1⟨-⟩ : (V : Vector n) → 1# ⟨ V ⟩ ≊ V + 1⟨-⟩ [] = PW.[] + 1⟨-⟩ (x ∷ V) = *-identityˡ x PW.∷ 1⟨-⟩ V + + -- Scaling by one from the right + ⟨-⟩1 : (V : Vector n) → ⟨ V ⟩ 1# ≊ V + ⟨-⟩1 [] = PW.[] + ⟨-⟩1 (x ∷ V) = *-identityʳ x PW.∷ ⟨-⟩1 V + + -- Associativity from left + -⟨-⟩-assoc : (r s : Carrier) (V : Vector n) → (r * s) ⟨ V ⟩ ≊ r ⟨ s ⟨ V ⟩ ⟩ + -⟨-⟩-assoc r s [] = PW.[] + -⟨-⟩-assoc r s (x ∷ V) = *-assoc r s x PW.∷ -⟨-⟩-assoc r s V + + -- Associativity from right + ⟨-⟩--assoc : (V : Vector n) (r s : Carrier) → ⟨ ⟨ V ⟩ r ⟩ s ≊ ⟨ V ⟩ (r * s) + ⟨-⟩--assoc [] r s = PW.[] + ⟨-⟩--assoc (x ∷ V) r s = *-assoc x r s PW.∷ ⟨-⟩--assoc V r s + + -- Scaling by left then right + ⟨-⟨-⟩⟩--assoc : (r : Carrier) (V : Vector n) (s : Carrier) → ⟨ r ⟨ V ⟩ ⟩ s ≊ r ⟨ ⟨ V ⟩ s ⟩ + ⟨-⟨-⟩⟩--assoc r [] s = PW.[] + ⟨-⟨-⟩⟩--assoc r (x ∷ V) s = *-assoc r x s PW.∷ ⟨-⟨-⟩⟩--assoc r V s + +infix 9 _⟨_⟩ ⟨_⟩_ + +opaque + + unfolding _⟨_⟩ ⟨_⟩_ ⟨ε⟩ + + -- Scaling by zero from the left + 0⟨-⟩ : (V : Vector n) → 0# ⟨ V ⟩ ≊ ⟨ε⟩ + 0⟨-⟩ [] = PW.[] + 0⟨-⟩ (x ∷ V) = zeroˡ x PW.∷ 0⟨-⟩ V + + -- Scaling by zero from the right + ⟨-⟩0 : (V : Vector n) → ⟨ V ⟩ 0# ≊ ⟨ε⟩ + ⟨-⟩0 [] = PW.[] + ⟨-⟩0 (x ∷ V) = zeroʳ x PW.∷ ⟨-⟩0 V + + -- scaling the zero vector from the left + -⟨ε⟩ : (r : Carrier) → r ⟨ ⟨ε⟩ ⟩ ≊ ⟨ε⟩ {n} + -⟨ε⟩ {zero} r = PW.[] + -⟨ε⟩ {suc n} r = zeroʳ r PW.∷ -⟨ε⟩ r + + -- scaling the zero vector from the right + ⟨ε⟩- : (r : Carrier) → ⟨ ⟨ε⟩ ⟩ r ≊ ⟨ε⟩ {n} + ⟨ε⟩- {zero} r = PW.[] + ⟨ε⟩- {suc n} r = zeroˡ r PW.∷ ⟨ε⟩- r + +opaque + + unfolding _⟨_⟩ ⟨_⟩_ _⊕_ + + -⟨-⟩-distribʳ : (V : Vector n) (r s : Carrier) → (r + s) ⟨ V ⟩ ≊ r ⟨ V ⟩ ⊕ s ⟨ V ⟩ + -⟨-⟩-distribʳ [] r s = PW.[] + -⟨-⟩-distribʳ (x ∷ V) r s = distribʳ x r s PW.∷ -⟨-⟩-distribʳ V r s + + -⟨-⟩-distribˡ : (r : Carrier) (V W : Vector n) → r ⟨ V ⊕ W ⟩ ≊ r ⟨ V ⟩ ⊕ r ⟨ W ⟩ + -⟨-⟩-distribˡ r [] [] = PW.[] + -⟨-⟩-distribˡ r (v ∷ V) (w ∷ W) = distribˡ r v w PW.∷ -⟨-⟩-distribˡ r V W + + ⟨-⟩--distribˡ : (V : Vector n) (r s : Carrier) → ⟨ V ⟩ (r + s) ≊ ⟨ V ⟩ r ⊕ ⟨ V ⟩ s + ⟨-⟩--distribˡ [] r s = PW.[] + ⟨-⟩--distribˡ (x ∷ V) r s = distribˡ x r s PW.∷ ⟨-⟩--distribˡ V r s + + ⟨-⟩--distribʳ : (r : Carrier) (V W : Vector n) → ⟨ V ⊕ W ⟩ r ≊ ⟨ V ⟩ r ⊕ ⟨ W ⟩ r + ⟨-⟩--distribʳ r [] [] = PW.[] + ⟨-⟩--distribʳ r (v ∷ V) (w ∷ W) = distribʳ r v w PW.∷ ⟨-⟩--distribʳ r V W + +opaque + + unfolding sum _⊗_ + + -- Dot product of two vectors + _∙_ : Vector n → Vector n → Carrier + _∙_ V W = sum (V ⊗ W) + + ∙-cong : {v₁ v₂ w₁ w₂ : Vector n} → v₁ ≊ v₂ → w₁ ≊ w₂ → v₁ ∙ w₁ ≈ v₂ ∙ w₂ + ∙-cong {n} ≊v ≊w = sum-cong (⊗-cong ≊v ≊w) + +infix 8 _∙_ + +opaque + + unfolding _∙_ ⟨ε⟩ + + ∙-identityˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0# + ∙-identityˡ [] = refl + ∙-identityˡ (x ∷ V) = begin + 0# * x + ⟨ε⟩ ∙ V  ≈⟨ +-congʳ (zeroˡ x) ⟩ + 0# + ⟨ε⟩ ∙ V  ≈⟨ +-congˡ (∙-identityˡ V) ⟩ + 0# + 0#  ≈⟨ +-identityˡ 0# ⟩ + 0# ∎ + + ∙-identityʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0# + ∙-identityʳ [] = refl + ∙-identityʳ (x ∷ V) = begin + x * 0# + V ∙ ⟨ε⟩ ≈⟨ +-congʳ (zeroʳ x) ⟩ + 0# + V ∙ ⟨ε⟩ ≈⟨ +-congˡ (∙-identityʳ V) ⟩ + 0# + 0# ≈⟨ +-identityˡ 0# ⟩ + 0# ∎ + +opaque + + unfolding _∙_ _⊕_ + + ∙-distribʳ : (A B C : Vector n) → (A ⊕ B) ∙ C ≈ A ∙ C + B ∙ C + ∙-distribʳ [] [] [] = sym (+-identityˡ 0#) + ∙-distribʳ (a ∷ A) (b ∷ B) (c ∷ C) = begin + (a + b) * c + ((A ⊕ B) ∙ C) ≈⟨ +-congˡ (∙-distribʳ A B C) ⟩ + (a + b) * c + (A ∙ C + B ∙ C) ≈⟨ +-congʳ (distribʳ c a b) ⟩ + a * c + b * c + (A ∙ C + B ∙ C) ≈⟨ +-assoc _ _ _ ⟩ + a * c + (b * c + (A ∙ C + B ∙ C)) ≈⟨ +-congˡ (+-assoc _ _ _) ⟨ + a * c + (b * c + A ∙ C + B ∙ C) ≈⟨ +-congˡ (+-congʳ (+-comm _ _)) ⟩ + a * c + (A ∙ C + b * c + B ∙ C) ≈⟨ +-congˡ (+-assoc _ _ _) ⟩ + a * c + (A ∙ C + (b * c + B ∙ C)) ≈⟨ +-assoc _ _ _ ⟨ + a * c + A ∙ C + (b * c + B ∙ C) ∎ + + ∙-distribˡ : (A B C : Vector n) → A ∙ (B ⊕ C) ≈ A ∙ B + A ∙ C + ∙-distribˡ [] [] [] = sym (+-identityˡ 0#) + ∙-distribˡ (a ∷ A) (b ∷ B) (c ∷ C) = begin + a * (b + c) + A ∙ (B ⊕ C) ≈⟨ +-congˡ (∙-distribˡ A B C) ⟩ + a * (b + c) + (A ∙ B + A ∙ C) ≈⟨ +-congʳ (distribˡ a b c) ⟩ + a * b + a * c + (A ∙ B + A ∙ C) ≈⟨ +-assoc _ _ _ ⟩ + a * b + (a * c + (A ∙ B + A ∙ C)) ≈⟨ +-congˡ (+-assoc _ _ _) ⟨ + a * b + (a * c + A ∙ B + A ∙ C) ≈⟨ +-congˡ (+-congʳ (+-comm _ _)) ⟩ + a * b + (A ∙ B + a * c + A ∙ C) ≈⟨ +-congˡ (+-assoc _ _ _) ⟩ + a * b + (A ∙ B + (a * c + A ∙ C)) ≈⟨ +-assoc _ _ _ ⟨ + a * b + A ∙ B + (a * c + A ∙ C) ∎ + +opaque + + unfolding _⟨_⟩ _∙_ + + *-∙ˡ : (r : Carrier) (A B : Vector n) → r * A ∙ B ≈ r ⟨ A ⟩ ∙ B + *-∙ˡ r [] [] = zeroʳ r + *-∙ˡ r (a ∷ A) (b ∷ B) = begin + r * (a * b + A ∙ B) ≈⟨ distribˡ r (a * b) (A ∙ B) ⟩ + r * (a * b) + r * A ∙ B ≈⟨ +-congʳ (*-assoc r a b) ⟨ + r * a * b + r * A ∙ B ≈⟨ +-congˡ (*-∙ˡ r A B )⟩ + r * a * b + r ⟨ A ⟩ ∙ B ∎ + + *-∙ʳ : (A B : Vector n) (r : Carrier) → A ∙ B * r ≈ A ∙ ⟨ B ⟩ r + *-∙ʳ [] [] r = zeroˡ r + *-∙ʳ (a ∷ A) (b ∷ B) r = begin + (a * b + A ∙ B) * r ≈⟨ distribʳ r (a * b) (A ∙ B) ⟩ + a * b * r + (A ∙ B) * r ≈⟨ +-congʳ (*-assoc a b r) ⟩ + a * (b * r) + (A ∙ B) * r ≈⟨ +-congˡ (*-∙ʳ A B r) ⟩ + a * (b * r) + A ∙ ⟨ B ⟩ r ∎ + +Vector-Bisemimodule : ℕ → Bisemimodule R R c (c ⊔ ℓ) +Vector-Bisemimodule n = record + { Carrierᴹ = Vector n + ; _≈ᴹ_ = _≊_ + ; _+ᴹ_ = _⊕_ + ; _*ₗ_ = _⟨_⟩ + ; _*ᵣ_ = ⟨_⟩_ + ; 0ᴹ = ⟨ε⟩ + ; isBisemimodule = record + { +ᴹ-isCommutativeMonoid = record { CommutativeMonoid (Vectorₘ n) } + ; isPreleftSemimodule = record + { *ₗ-cong = -⟨-⟩-cong + ; *ₗ-zeroˡ = 0⟨-⟩ + ; *ₗ-distribʳ = -⟨-⟩-distribʳ + ; *ₗ-identityˡ = 1⟨-⟩ + ; *ₗ-assoc = -⟨-⟩-assoc + ; *ₗ-zeroʳ = -⟨ε⟩ + ; *ₗ-distribˡ = -⟨-⟩-distribˡ + } + ; isPrerightSemimodule = record + { *ᵣ-cong = ⟨-⟩--cong + ; *ᵣ-zeroʳ = ⟨-⟩0 + ; *ᵣ-distribˡ = ⟨-⟩--distribˡ + ; *ᵣ-identityʳ = ⟨-⟩1 + ; *ᵣ-assoc = ⟨-⟩--assoc + ; *ᵣ-zeroˡ = ⟨ε⟩- + ; *ᵣ-distribʳ = ⟨-⟩--distribʳ + } + ; *ₗ-*ᵣ-assoc = ⟨-⟨-⟩⟩--assoc + } + } -- cgit v1.2.3