From 1e73f2658f6d8d1559649b2cd97040f494dc1c96 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 5 Aug 2026 17:50:02 -0500 Subject: Show matrix change of base functor is cartesian --- Data/Matrix/SemiadditiveDagger.agda | 228 +----------------------------------- 1 file changed, 3 insertions(+), 225 deletions(-) (limited to 'Data/Matrix/SemiadditiveDagger.agda') diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index 3e13383..017f05f 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -1,7 +1,7 @@ {-# OPTIONS --without-K --safe #-} open import Algebra.Bundles using (CommutativeSemiring) -open import Level using (Level) +open import Level using (Level; 0ℓ; _⊔_) module Data.Matrix.SemiadditiveDagger {c ℓ : Level} (R : CommutativeSemiring c ℓ) where @@ -12,6 +12,7 @@ import Data.Nat.Properties as ℕ-Props import Data.Vec.Relation.Binary.Pointwise.Inductive as PW import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) open import Categories.Category.Cocartesian using (Cocartesian) open import Categories.Category.Dagger using (HasDagger) open import Categories.Object.Biproduct using (Biproduct) @@ -26,6 +27,7 @@ open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; · open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) +open import Data.Matrix.Semiadditive R.semiring using (Mat-Semiadditive) open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ) open import Data.Nat using (ℕ) open import Data.Product using (_,_; Σ-syntax) @@ -112,191 +114,6 @@ opaque where open ≡-Reasoning -inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M -inj₁ {A} {C} M N = begin - (M ∥ N) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ M N I 𝟎 ⟩ - (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-Iʳ (·-𝟎ʳ N) ⟩ - M [+] 𝟎 ≈⟨ [+]-𝟎ʳ M ⟩ - M ∎ - where - open ≈-Reasoning (Matrixₛ A C) - -inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N -inj₂ {A} {C} {B} M N = begin - (M ∥ N) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ M N 𝟎 I ⟩ - (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-Iʳ ⟩ - 𝟎 [+] N ≈⟨ [+]-𝟎ˡ N ⟩ - N ∎ - where - open ≈-Reasoning (Matrixₛ B C) - -opaque - - unfolding Matrix _∷ᵥ_ - - split-∥ : (A : ℕ) (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M - split-∥ zero M = []ᵥ , M , []ᵥ-∥ M - split-∥ (suc A) M′ - rewrite ≡.sym (head-∷-tailₕ M′) - using M₀ ← headₕ M′ - using M ← tailₕ M′ - with split-∥ A M - ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin - (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨ - M₀ ∷ₕ M₁ ∥ M₂ ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩ - M₀ ∷ₕ M ∎) - where - open ≡-Reasoning - - split-≑ : (B : ℕ) (M : Matrix A (B ℕ.+ C)) → Σ[ M₁ ∈ Matrix A B ] Σ[ M₂ ∈ Matrix A C ] M₁ ≑ M₂ ≡ M - split-≑ zero M = []ₕ , M , []ₕ-≑ M - split-≑ (suc B) (M₀ ∷ M) with split-≑ B M - ... | M₁ , M₂ , M₁≑M₂≡M = M₀ ∷ᵥ M₁ , M₂ , (begin - (M₀ ∷ᵥ M₁) ≑ M₂ ≡⟨ ∷ᵥ-≑ M₀ M₁ M₂ ⟨ - M₀ ∷ᵥ M₁ ≑ M₂ ≡⟨ ≡.cong (M₀ ∷ᵥ_) M₁≑M₂≡M ⟩ - M₀ ∷ᵥ M ∎) - where - open ≡-Reasoning - -∥-uniq - : (H : Matrix (A ℕ.+ B) C) - (M : Matrix A C) - (N : Matrix B C) - → H · (I ≑ 𝟎) ≋ M - → H · (𝟎 ≑ I) ≋ N - → M ∥ N ≋ H -∥-uniq {A} {B} {C} H M N eq₁ eq₂ - with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H - rewrite ≡.sym H₁∥H₂≡H = begin - M ∥ N ≈⟨ ∥-cong eq₁ eq₂ ⟨ - (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩ - (H₁ ∥ H₂) ∎ - where - open ≈-Reasoning (Matrixₛ (A ℕ.+ B) C) - -proj₁ : (M : Matrix A B) (N : Matrix A C) → (I ∥ 𝟎) · (M ≑ N) ≋ M -proj₁ {A} {B} M N = begin - (I ∥ 𝟎) · (M ≑ N) ≈⟨ ∥-·-≑ I 𝟎 M N ⟩ - (I · M) [+] (𝟎 · N) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ N) ⟩ - M [+] 𝟎 ≈⟨ [+]-𝟎ʳ M ⟩ - M ∎ - where - open ≈-Reasoning (Matrixₛ A B) - -proj₂ : (M : Matrix A B) (N : Matrix A C) → (𝟎 ∥ I) · (M ≑ N) ≋ N -proj₂ {A} {_} {C} M N = begin - (𝟎 ∥ I) · (M ≑ N) ≈⟨ ∥-·-≑ 𝟎 I M N ⟩ - (𝟎 · M) [+] (I · N) ≈⟨ [+]-cong (·-𝟎ˡ M) ·-Iˡ ⟩ - 𝟎 [+] N ≈⟨ [+]-𝟎ˡ N ⟩ - N ∎ - where - open ≈-Reasoning (Matrixₛ A C) - -≑-uniq - : (H : Matrix A (B ℕ.+ C)) - (M : Matrix A B) - (N : Matrix A C) - → (I ∥ 𝟎) · H ≋ M - → (𝟎 ∥ I) · H ≋ N - → M ≑ N ≋ H -≑-uniq {A} {B} {C} H M N eq₁ eq₂ - with (H₁ , H₂ , H₁≑H₂≡H) ← split-≑ B H - rewrite ≡.sym H₁≑H₂≡H = begin - M ≑ N ≈⟨ ≑-cong eq₁ eq₂ ⟨ - (I {B} ∥ 𝟎) · (H₁ ≑ H₂) ≑ (𝟎 ∥ I) · (H₁ ≑ H₂) ≈⟨ ≑-cong (proj₁ H₁ H₂) (proj₂ H₁ H₂) ⟩ - H₁ ≑ H₂ ∎ - where - open ≈-Reasoning (Matrixₛ A (B ℕ.+ C)) - - -isCoproduct : IsCoproduct Mat (I {A} ≑ 𝟎) (𝟎 ≑ I {B}) -isCoproduct {A} {B} = record - { [_,_] = _∥_ - ; inject₁ = λ {a} {b} {c} → inj₁ b c - ; inject₂ = λ {a} {b} {c} → inj₂ b c - ; unique = λ eq₁ eq₂ → ∥-uniq _ _ _ eq₁ eq₂ - } - -isProduct : IsProduct Mat (I {A} ∥ 𝟎) (𝟎 ∥ I {B}) -isProduct {A} {B} = record - { ⟨_,_⟩ = _≑_ - ; project₁ = λ {a} {b} {c} → proj₁ b c - ; project₂ = λ {a} {b} {c} → proj₂ b c - ; unique = λ eq₁ eq₂ → ≑-uniq _ _ _ eq₁ eq₂ - } - -opaque - - unfolding Matrix - - π₁∘i₁ : (I {A} ∥ 𝟎 {B}) · (I ≑ 𝟎) ≋ I - π₁∘i₁ {A} = begin - (I ∥ 𝟎) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩ - (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩ - I [+] 𝟎 ≈⟨ [+]-𝟎ʳ I ⟩ - I ∎ - where - open ≈-Reasoning (Matrixₛ A A) - - π₂∘i₂ : (𝟎 {A} {B} ∥ I) · (𝟎 ≑ I) ≋ I - π₂∘i₂ {A} {B} = begin - (𝟎 ∥ I) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩ - (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ ⟩ - 𝟎 [+] I ≈⟨ [+]-𝟎ˡ I ⟩ - I ∎ - where - open ≈-Reasoning (Matrixₛ B B) - - π₁∘i₂ : (I {A} ∥ 𝟎 {B}) · (𝟎 ≑ I) ≋ 𝟎 {B} {A} - π₁∘i₂ {A} {B} = begin - (I ∥ 𝟎) · (𝟎 ≑ I) ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩ - (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ - 𝟎 ∎ - where - open ≈-Reasoning (Matrixₛ B A) - - π₂∘i₁ : (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎) ≋ 𝟎 {A} {B} - π₂∘i₁ {A} {B} = begin - (𝟎 ∥ I) · (I ≑ 𝟎) ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩ - (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩ - 𝟎 [+] 𝟎 ≈⟨ [+]-𝟎ʳ 𝟎 ⟩ - 𝟎 ∎ - where - open ≈-Reasoning (Matrixₛ A B) - - permute - : (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) - ≋ (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) - permute {A} {B} = begin - (I ≑ 𝟎) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟨ - (I ≑ 𝟎) · ((I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I)) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₁∘i₂ ≋.refl) ⟩ - (I ≑ 𝟎) · 𝟎 {B} {A} · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (𝟎 ∥ I)) ⟩ - (I ≑ 𝟎 {A} {B}) · 𝟎 ≈⟨ ·-𝟎ʳ (I ≑ 𝟎) ⟩ - 𝟎 ≈⟨ ·-𝟎ʳ (𝟎 ≑ I) ⟨ - (𝟎 {B} {A} ≑ I) · 𝟎 ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (I ∥ 𝟎)) ⟨ - (𝟎 ≑ I) · 𝟎 {A} {B} · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₂∘i₁ ≋.refl) ⟨ - (𝟎 {B} {A} ≑ I) · ((𝟎 ∥ I) · (I ≑ 𝟎 {A} {B})) · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟩ - (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎) ∎ - where - open ≈-Reasoning (Matrixₛ (A ℕ.+ B) (A ℕ.+ B)) - -biproduct : Biproduct Mat A B -biproduct {A} {B} = record - { A⊕B = A ℕ.+ B - ; π₁ = I ∥ 𝟎 - ; π₂ = 𝟎 ∥ I - ; i₁ = I ≑ 𝟎 - ; i₂ = 𝟎 ≑ I - ; isBiproduct = record - { isCoproduct = isCoproduct - ; isProduct = isProduct - ; π₁∘i₁≈id = π₁∘i₁ - ; π₂∘i₂≈id = π₂∘i₂ - ; permute = permute - } - } - [I∥𝟎]ᵀ : (I ∥ 𝟎 {B} {A}) ᵀ ≋ I ≑ 𝟎 [I∥𝟎]ᵀ {B} {A} = begin (I ∥ 𝟎) ᵀ ≡⟨ ∥-ᵀ I 𝟎 ⟩ @@ -313,45 +130,6 @@ biproduct {A} {B} = record where open ≈-Reasoning (Matrixₛ B (A ℕ.+ B)) -opaque - - unfolding _≋_ - - ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E - ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) - - !-unique : (E : Matrix A 0) → []ₕ ≋ E - !-unique E = ≋.reflexive (≡.sym ([]ₕ-! E)) - -isInitial : IsInitial Mat 0 -isInitial = record - { ¡ = []ᵥ - ; ¡-unique = ¡-unique - } - -isTerminal : IsTerminal Mat 0 -isTerminal = record - { ! = []ₕ - ; !-unique = !-unique - } - -zeroObj : Zero Mat -zeroObj = record - { 𝟘 = 0 - ; isZero = record - { isInitial = isInitial - ; isTerminal = isTerminal - } - } - -Mat-Semiadditive : Semiadditive Mat -Mat-Semiadditive = record - { zero = zeroObj - ; biproducts = record - { biproduct = biproduct - } - } - Mat-HasDagger : HasDagger Mat Mat-HasDagger = record { _† = λ M → M ᵀ -- cgit v1.2.3