diff options
Diffstat (limited to 'Data/Matrix')
| -rw-r--r-- | Data/Matrix/FreeSemimodule.agda | 86 | ||||
| -rw-r--r-- | Data/Matrix/Transform.agda | 17 |
2 files changed, 102 insertions, 1 deletions
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 |