From 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 11 Oct 2026 22:59:21 -0700 Subject: Add hom-set addition to semiadditive record --- Data/Matrix/Category.agda | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) (limited to 'Data/Matrix/Category.agda') diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda index 717926a..e1a10ec 100644 --- a/Data/Matrix/Category.agda +++ b/Data/Matrix/Category.agda @@ -13,8 +13,8 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapₕ; mapᵥ; ∷ᵥⁿ; ∷ₕⁿ; columns-∷ₕⁿ; ∷ᵥⁿ-ᵀ) -open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋) -open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_) +open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋; ∥-cong; ≑-cong) +open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong) open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; map) @@ -176,6 +176,36 @@ opaque ·-𝟎ˡ {A} {B} {zero} M = PW.[] ·-𝟎ˡ {A} {B} {suc C} M = [⟨0⟩]- M PW.∷ ·-𝟎ˡ M +·-[+]ˡ + : (W : Matrix B C) + (Y Z : Matrix A B) + → W · (Y [+] Z) ≋ (W · Y) [+] (W · Z) +·-[+]ˡ {C = C} {A = A} W Y Z = begin + W · (Y [+] Z) ≈⟨ ·-resp-≋ ≋.refl ([+]-cong ·-Iˡ ·-Iˡ) ⟨ + W · ((I · Y) [+] (I · Z)) ≈⟨ ·-resp-≋ ≋.refl (∥-·-≑ I I Y Z) ⟨ + W · (I ∥ I) · (Y ≑ Z) ≈⟨ ·-assoc ⟨ + (W · (I ∥ I)) · (Y ≑ Z) ≡⟨ ≡.cong (_· (Y ≑ Z)) (·-∥ W I I) ⟩ + (W · I ∥ W · I) · (Y ≑ Z) ≈⟨ ·-resp-≋ (∥-cong ·-Iʳ ·-Iʳ) ≋.refl ⟩ + (W ∥ W) · (Y ≑ Z) ≈⟨ ∥-·-≑ W W Y Z ⟩ + (W · Y) [+] (W · Z) ∎ + where + open ≈-Reasoning (Matrixₛ A C) + +·-[+]ʳ + : (W : Matrix A B) + (Y Z : Matrix B C) + → (Y [+] Z) · W ≋ (Y · W) [+] (Z · W) +·-[+]ʳ {A = A} {C = C} W Y Z = begin + (Y [+] Z) · W ≈⟨ ·-resp-≋ ([+]-cong ·-Iʳ ·-Iʳ) ≋.refl ⟨ + ((Y · I) [+] (Z · I)) · W ≈⟨ ·-resp-≋ (∥-·-≑ Y Z I I) ≋.refl ⟨ + ((Y ∥ Z) · (I ≑ I)) · W ≈⟨ ·-assoc ⟩ + (Y ∥ Z) · ((I ≑ I) · W) ≡⟨ ≡.cong ((Y ∥ Z) ·_) (≑-· I I W) ⟩ + (Y ∥ Z) · ((I · W) ≑ (I · W)) ≈⟨ ·-resp-≋ ≋.refl (≑-cong ·-Iˡ ·-Iˡ) ⟩ + (Y ∥ Z) · (W ≑ W) ≈⟨ ∥-·-≑ Y Z W W ⟩ + (Y · W) [+] (Z · W) ∎ + where + open ≈-Reasoning (Matrixₛ A C) + -- The category of matrices over a rig Mat : Category 0ℓ c (c ⊔ ℓ) Mat = categoryHelper record -- cgit v1.2.3