Add free functor from rig-matrices to semimodulesmain

4 files changed, 182 insertions, 23 deletions

diff --git a/Category/Instance/Bisemimodules.agda b/Category/Instance/Bisemimodules.agda
index 7556a75..0b7b0b2 100644
--- a/Category/Instance/Bisemimodules.agda
+++ b/Category/Instance/Bisemimodules.agda
@@ -12,6 +12,7 @@ open import Algebra.Module using (Bisemimodule)
 open import Algebra.Module.Morphism.Structures using (IsBisemimoduleHomomorphism)
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary using (Rel; IsEquivalence)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
 record BisemimoduleHomomorphism (M N : Bisemimodule R S m ℓm) : Set (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) where
@@ -24,6 +25,8 @@ record BisemimoduleHomomorphism (M N : Bisemimodule R S m ℓm) : Set (c₁ ⊔
     ⟦_⟧ : M.Carrierᴹ → N.Carrierᴹ
     isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism M.rawBisemimodule N.rawBisemimodule ⟦_⟧
 
+  open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public
+
 id : (M : Bisemimodule R S m ℓm) → BisemimoduleHomomorphism M M
 id M = record
     { isBisemimoduleHomomorphism = Identity.isBisemimoduleHomomorphism M.rawBisemimodule M.≈ᴹ-refl
@@ -50,20 +53,46 @@ compose M N P f g = record
 
 open BisemimoduleHomomorphism
 
-Bisemimodules : Category (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ suc (m ⊔ ℓm)) (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) m
+_≈_ : {M N : Bisemimodule R S m ℓm} → Rel (BisemimoduleHomomorphism M N) (m ⊔ ℓm)
+_≈_ {M} {N} f g = (x : M.Carrierᴹ) → ⟦ f ⟧ x N.≈ᴹ ⟦ g ⟧ x
+  where
+    module M = Bisemimodule M
+    module N = Bisemimodule N
+
+≈-isEquiv : {M N : Bisemimodule R S m ℓm} → IsEquivalence (_≈_ {M} {N})
+≈-isEquiv {M} {N} = record
+    { refl = λ _ → N.≈ᴹ-refl
+    ; sym = λ f≈g x → N.≈ᴹ-sym (f≈g x)
+    ; trans = λ f≈g g≈h x → N.≈ᴹ-trans (f≈g x) (g≈h x)
+    }
+  where
+    module M = Bisemimodule M
+    module N = Bisemimodule N
+
+∘-resp-≈
+    : {M N P : Bisemimodule R S m ℓm}
+      {f h : BisemimoduleHomomorphism N P}
+      {g i : BisemimoduleHomomorphism M N}
+    → f ≈ h
+    → g ≈ i
+    → compose M N P f g ≈ compose M N P h i
+∘-resp-≈ {M} {N} {P} {f} {g} {h} {i} f≈h g≈i x = P.≈ᴹ-trans (f.⟦⟧-cong (g≈i x)) (f≈h (⟦ i ⟧ x))
+  where
+    module P = Bisemimodule P
+    module f = BisemimoduleHomomorphism f
+
+open Bisemimodule
+
+Bisemimodules : Category (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ suc (m ⊔ ℓm)) (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) (m ⊔ ℓm)
 Bisemimodules = categoryHelper record
     { Obj = Bisemimodule R S m ℓm
     ; _⇒_ = BisemimoduleHomomorphism
-    ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+    ; _≈_ = _≈_
     ; id = λ {M} → id M
     ; _∘_ = λ {M N P} f g → compose M N P f g
-    ; assoc = λ _ → ≡.refl
-    ; identityˡ = λ _ → ≡.refl
-    ; identityʳ = λ _ → ≡.refl
-    ; equiv = record
-        { refl = λ _ → ≡.refl
-        ; sym = λ f≈g x → ≡.sym (f≈g x)
-        ; trans = λ f≈g g≈h x → ≡.trans (f≈g x) (g≈h x)
-        }
-    ; ∘-resp-≈ = λ {f = f} {h g i} eq₁ eq₂ x → ≡.trans (≡.cong ⟦ f ⟧ (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+    ; assoc = λ {D = D} _ → ≈ᴹ-refl D
+    ; identityˡ = λ {B = B} _ → ≈ᴹ-refl B
+    ; identityʳ = λ {B = B} _ → ≈ᴹ-refl B
+    ; equiv = ≈-isEquiv
+    ; ∘-resp-≈ = λ {f = f} {g h i } → ∘-resp-≈ {f = f} {g} {h} {i}
     }
diff --git a/Category/Instance/Semimodules.agda b/Category/Instance/Semimodules.agda
index d8ab6f5..7b48cd9 100644
--- a/Category/Instance/Semimodules.agda
+++ b/Category/Instance/Semimodules.agda
@@ -12,6 +12,7 @@ open import Algebra.Module using (Semimodule)
 open import Algebra.Module.Morphism.Structures using (IsSemimoduleHomomorphism)
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary using (Rel; IsEquivalence)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
 record SemimoduleHomomorphism (M N : Semimodule R m ℓm) : Set (c ⊔ m ⊔ ℓm) where
@@ -24,6 +25,8 @@ record SemimoduleHomomorphism (M N : Semimodule R m ℓm) : Set (c ⊔ m ⊔ ℓ
     ⟦_⟧ : M.Carrierᴹ → N.Carrierᴹ
     isSemimoduleHomomorphism : IsSemimoduleHomomorphism M.rawSemimodule N.rawSemimodule ⟦_⟧
 
+  open IsSemimoduleHomomorphism isSemimoduleHomomorphism public
+
 id : (M : Semimodule R m ℓm) → SemimoduleHomomorphism M M
 id M = record
     { isSemimoduleHomomorphism = Identity.isSemimoduleHomomorphism M.rawSemimodule M.≈ᴹ-refl
@@ -50,20 +53,46 @@ compose M N P f g = record
 
 open SemimoduleHomomorphism
 
-Semimodules : Category (c ⊔ ℓ ⊔ suc (m ⊔ ℓm)) (c ⊔ m ⊔ ℓm) m
+_≈_ : {M N : Semimodule R m ℓm} → Rel (SemimoduleHomomorphism M N) (m ⊔ ℓm)
+_≈_ {M} {N} f g = (x : M.Carrierᴹ) → ⟦ f ⟧ x N.≈ᴹ ⟦ g ⟧ x
+  where
+    module M = Semimodule M
+    module N = Semimodule N
+
+≈-isEquiv : {M N : Semimodule R m ℓm} → IsEquivalence (_≈_ {M} {N})
+≈-isEquiv {M} {N} = record
+    { refl = λ _ → N.≈ᴹ-refl
+    ; sym = λ f≈g x → N.≈ᴹ-sym (f≈g x)
+    ; trans = λ f≈g g≈h x → N.≈ᴹ-trans (f≈g x) (g≈h x)
+    }
+  where
+    module M = Semimodule M
+    module N = Semimodule N
+
+∘-resp-≈
+    : {M N P : Semimodule R m ℓm}
+      {f h : SemimoduleHomomorphism N P}
+      {g i : SemimoduleHomomorphism M N}
+    → f ≈ h
+    → g ≈ i
+    → compose M N P f g ≈ compose M N P h i
+∘-resp-≈ {M} {N} {P} {f} {g} {h} {i} f≈h g≈i x = P.≈ᴹ-trans (f.⟦⟧-cong (g≈i x)) (f≈h (⟦ i ⟧ x))
+  where
+    module P = Semimodule P
+    module f = SemimoduleHomomorphism f
+
+open Semimodule
+
+Semimodules : Category (c ⊔ ℓ ⊔ suc (m ⊔ ℓm)) (c ⊔ m ⊔ ℓm) (m ⊔ ℓm)
 Semimodules = categoryHelper record
     { Obj = Semimodule R m ℓm
     ; _⇒_ = SemimoduleHomomorphism
-    ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+    ; _≈_ = _≈_
     ; id = λ {M} → id M
     ; _∘_ = λ {M N P} f g → compose M N P f g
-    ; assoc = λ _ → ≡.refl
-    ; identityˡ = λ _ → ≡.refl
-    ; identityʳ = λ _ → ≡.refl
-    ; equiv = record
-        { refl = λ _ → ≡.refl
-        ; sym = λ f≈g x → ≡.sym (f≈g x)
-        ; trans = λ f≈g g≈h x → ≡.trans (f≈g x) (g≈h x)
-        }
-    ; ∘-resp-≈ = λ {f = f} {h g i} eq₁ eq₂ x → ≡.trans (≡.cong ⟦ f ⟧ (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+    ; assoc = λ {D = D} _ → ≈ᴹ-refl D
+    ; identityˡ = λ {B = B} _ → ≈ᴹ-refl B
+    ; identityʳ = λ {B = B} _ → ≈ᴹ-refl B
+    ; equiv = ≈-isEquiv
+    ; ∘-resp-≈ = λ {f = f} {g h i } → ∘-resp-≈ {f = f} {g} {h} {i}
     }
diff --git a/Data/Matrix/FreeSemimodule.agda b/Data/Matrix/FreeSemimodule.agda
new file mode 100644
index 0000000..ae5822f
--- /dev/null
+++ b/Data/Matrix/FreeSemimodule.agda
@@ -0,0 +1,86 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CommutativeSemiring)
+open import Level using (Level; _⊔_)
+
+module Data.Matrix.FreeSemimodule {c ℓ : Level} (R : CommutativeSemiring c ℓ) where
+
+module R = CommutativeSemiring R
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Categories.Functor using (Functor)
+open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism)
+open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-[])
+open import Data.Matrix.Core R.setoid using (Matrix; module ≋; mapRows)
+open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕])
+open import Data.Nat using (ℕ)
+open import Data.Vec using (map)
+open import Data.Vec.Properties using (map-∘)
+open import Data.Vector.Bisemimodule R.semiring using (_⟨_⟩; ⟨_⟩_; _∙_; *-∙ˡ; *-∙ʳ; ∙-cong)
+open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; _≊_; module ≊)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⟨ε⟩)
+open import Data.Vector.Semimodule R using (Vector-Semimodule; ⟨-⟩-comm)
+
+open R
+
+opaque
+
+  unfolding _[_] _⟨_⟩
+
+  -[-⟨-⟩] : {A B : ℕ} (M : Matrix A B) (r : Carrier) (V : Vector A) → M [ r ⟨ V ⟩ ] ≊ r ⟨ M [ V ] ⟩
+  -[-⟨-⟩] {A} M r V = begin
+      map (λ x → x ∙ r ⟨ V ⟩) M ≈⟨ PW.map⁺ lemma {xs = M} ≋.refl ⟩
+      map (λ x → r * x ∙ V) M   ≡⟨ map-∘ (r *_) (_∙ V) M ⟩
+      map (r *_) (map (_∙ V) M) ∎
+    where
+      lemma : {X Y : Vector A} → X ≊ Y → X ∙ r ⟨ V ⟩ ≈ r * Y ∙ V
+      lemma {X} {Y} X≊Y = begin
+          X ∙ r ⟨ V ⟩ ≈⟨ ∙-cong ≊.refl (⟨-⟩-comm r V) ⟩
+          X ∙ ⟨ V ⟩ r ≈⟨ *-∙ʳ X V r ⟨
+          X ∙ V * r   ≈⟨ *-comm (X ∙ V) r ⟩
+          r * X ∙ V   ≈⟨ *-congˡ (∙-cong X≊Y ≊.refl) ⟩
+          r * Y ∙ V   ∎
+        where
+          open ≈-Reasoning R.setoid
+      open ≈-Reasoning (Vectorₛ _)
+
+  -[⟨-⟩-] : {A B : ℕ} (M : Matrix A B) (r : Carrier) (V : Vector A) → M [ ⟨ V ⟩ r ] ≊ ⟨ M [ V ] ⟩ r
+  -[⟨-⟩-] {A} {B} M r V = begin
+      map (λ x → x ∙ ⟨ V ⟩ r) M ≈⟨ PW.map⁺ (λ {W} ≊W → trans (*-∙ʳ W V r) (∙-cong ≊W ≊.refl)) {xs = M} ≋.refl ⟨
+      map (λ x → x ∙ V * r) M   ≡⟨ map-∘ (_* r) (_∙ V) M ⟩
+      map (_* r) (map (_∙ V) M) ∎
+    where
+      open ≈-Reasoning (Vectorₛ _)
+
+F₁  : {A B : ℕ}
+    → Matrix A B
+    → SemimoduleHomomorphism (Vector-Semimodule A) (Vector-Semimodule B)
+F₁ M = record
+    { ⟦_⟧ = M [_]
+    ; isSemimoduleHomomorphism = record
+        { isBisemimoduleHomomorphism = record
+            { +ᴹ-isMonoidHomomorphism = record
+                { isMagmaHomomorphism = record
+                    { isRelHomomorphism = record
+                        { cong = -[-]-cong M
+                        }
+                    ; homo = -[⊕] M
+                    }
+                ; ε-homo = -[⟨0⟩] M
+                }
+            ; *ₗ-homo = -[-⟨-⟩] M
+            ; *ᵣ-homo = -[⟨-⟩-] M
+            }
+        }
+    }
+
+Free : Functor Mat Semimodules
+Free = record
+    { F₀ = Vector-Semimodule
+    ; F₁ = F₁
+    ; identity = I[-]
+    ; homomorphism = λ {f = M} {N} V → ·-[] M N V
+    ; F-resp-≈ = -[-]-cong₁
+    }
diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda
index 671725f..87b8020 100644
--- a/Data/Matrix/Transform.agda
+++ b/Data/Matrix/Transform.agda
@@ -27,7 +27,7 @@ open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_)
 open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; ⟨⟩; module ≊; _≊_; _++_; ⟨⟩-++)
 open import Data.Vector.Vec using (zipWith-map; map-zipWith; zipWith-map-map)
 open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩)
-open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; ∙-distribʳ)
+open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; *-∙ʳ; ∙-distribˡ; ∙-distribʳ)
 
 open Vec
 open ℕ
@@ -55,6 +55,9 @@ opaque
     -[-]-cong : {x y : Vector n} (A : Matrix n m) → x ≊ y → A [ x ] ≊ A [ y ]
     -[-]-cong {x = x} {y} A ≋V = PW.map⁺ (λ ≋w → ∙-cong ≋w ≋V) {xs = A} ≋.refl
 
+    -[-]-cong₁ : {M M′ : Matrix n m} → M ≋ M′ → (V : Vector n) → M [ V ] ≊ M′ [ V ]
+    -[-]-cong₁ {n} {m} {M} {M′} ≋M V = PW.map⁺ (λ ≊V → ∙-cong ≊V ≊.refl) ≋M
+
     [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B
     [-]--cong ≋V A≋B = PW.map⁺ (∙-cong ≋V) (-ᵀ-cong A≋B)
 
@@ -74,6 +77,12 @@ opaque
       [-]-[]ₕ {zero} [] = ≡.refl
       [-]-[]ₕ {suc A} [] = ≡.cong (0# ∷_) ([-]-[]ₕ [])
 
+    opaque
+      unfolding _⊕_
+      -[⊕] : (M : Matrix A B) (V W : Vector A) → M [ V ⊕ W ] ≊ (M [ V ]) ⊕ (M [ W ])
+      -[⊕] [] V W = PW.[]
+      -[⊕] (x ∷ M) V W = ∙-distribˡ x V W PW.∷ -[⊕] M V W
+
 opaque
 
   unfolding Matrix Vector
@@ -296,3 +305,9 @@ opaque
       0# ∷ ⟨0⟩              ∎
     where
       open ≈-Reasoning (Vectorₛ _)
+
+opaque
+  unfolding _[_] ⟨0⟩
+  -[⟨0⟩] : (M : Matrix A B) → M [ ⟨0⟩ ] ≊ ⟨0⟩
+  -[⟨0⟩] {A} {B} [] = PW.[]
+  -[⟨0⟩] {A} {B} (M₀ ∷ M) = ∙-zeroʳ M₀ PW.∷ -[⟨0⟩] M