From 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Aug 2026 19:08:47 -0500 Subject: Show category of maps is monoidal --- Category/Dagger/Semiadditive.agda | 253 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 253 insertions(+) (limited to 'Category/Dagger/Semiadditive.agda') diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index a5b03ab..424f8df 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -5,11 +5,21 @@ open import Categories.Category using (Category) module Category.Dagger.Semiadditive {o β„“ e : Level} (π’ž : Category o β„“ e) where +import Categories.Morphism as Morphism import Categories.Morphism.Reasoning π’ž as β‡’-Reasoning +import Category.Semiadditive.Monoidal as SemiadditiveMonoidal open import Categories.Category.Dagger using (HasDagger) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.Morphism using (Iso) +open import Categories.Morphism.Properties π’ž using (Iso-resp-β‰ˆ; Iso-swap) +open import Category.Dagger.2-Poset using (Dagger-2-Poset; Map; Maps; unitary-isMap) open import Category.Semiadditive using (Semiadditive) +open import Data.Product using (_,_) open import Relation.Binary using (Rel) +open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo) record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where @@ -41,6 +51,42 @@ record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where Ξ” † † β‰ˆβŸ¨ †-involutive Ξ” ⟩ Ξ” ∎ + i₁† : {A B : Obj} β†’ i₁ {A} {B} † β‰ˆ π₁ + i₁† = begin + i₁ † β‰ˆβŸ¨ ⟨ π₁† βŸ©β€  ⟨ + π₁ † † β‰ˆβŸ¨ †-involutive π₁ ⟩ + π₁ ∎ + + i₂† : {A B : Obj} β†’ iβ‚‚ {A} {B} † β‰ˆ Ο€β‚‚ + i₂† = begin + iβ‚‚ † β‰ˆβŸ¨ ⟨ π₂† βŸ©β€  ⟨ + Ο€β‚‚ † † β‰ˆβŸ¨ †-involutive Ο€β‚‚ ⟩ + Ο€β‚‚ ∎ + + module _ {A B C : Obj} where + + α⇒† : assocΛ‘ {A} {B} {C} † β‰ˆ assocΚ³ + α⇒† = begin + ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩ † β‰ˆβŸ¨ ⟨⟩-† ⟩ + [ (π₁ ∘ π₁) † , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ † ] β‰ˆβŸ¨ []-congβ‚‚ †-homomorphism ⟨⟩-† ⟩ + [ π₁ † ∘ π₁ † , [ (Ο€β‚‚ ∘ π₁) † , Ο€β‚‚ † ] ] β‰ˆβŸ¨ []-congΛ‘ ([]-congΚ³ †-homomorphism) ⟩ + [ π₁ † ∘ π₁ † , [ π₁ † ∘ Ο€β‚‚ † , Ο€β‚‚ † ] ] β‰ˆβŸ¨ []-congβ‚‚ (π₁† ⟩∘⟨ π₁†) ([]-congβ‚‚ (π₁† ⟩∘⟨ π₂†) π₂†) ⟩ + [ i₁ ∘ i₁ , [ i₁ ∘ iβ‚‚ , iβ‚‚ ] ] β‰ˆβŸ¨ assocΚ³β‰ˆ+-assocΚ³ ⟨ + assocΚ³ ∎ + + α⇐† : assocΚ³ {A} {B} {C} † β‰ˆ assocΛ‘ + α⇐† = begin + assocΚ³ † β‰ˆβŸ¨ ⟨ α⇒† βŸ©β€  ⟨ + assocΛ‘ † † β‰ˆβŸ¨ †-involutive assocΛ‘ ⟩ + assocΛ‘ ∎ + + swap† : {A B : Obj} β†’ swap {A} {B} † β‰ˆ swap {B} {A} + swap† {A} {B} = begin + ⟨ Ο€β‚‚ , π₁ ⟩ † β‰ˆβŸ¨ ⟨⟩-† ⟩ + [ Ο€β‚‚ † , π₁ † ] β‰ˆβŸ¨ []-congβ‚‚ π₂† π₁† ⟩ + [ iβ‚‚ , i₁ ] β‰ˆβŸ¨ swapβ‰ˆ+-swap ⟨ + ⟨ Ο€β‚‚ , π₁ ⟩ ∎ + †-resp-×₁ : {A B C D : Obj} {f : A β‡’ B} {g : C β‡’ D} β†’ (f ×₁ g) † β‰ˆ (f †) ×₁ (g †) †-resp-×₁ {f = f} {g} = begin ⟨ f ∘ π₁ , g ∘ Ο€β‚‚ ⟩ † β‰ˆβŸ¨ ⟨⟩-† ⟩ @@ -77,6 +123,21 @@ record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where id ∘ f ∘ h + id ∘ g ∘ h β‰ˆβŸ¨ +-cong (pullΛ‘ identityΛ‘) (pullΛ‘ identityΛ‘) ⟩ f ∘ h + g ∘ h ∎ + open SemiadditiveMonoidal semiadditive using (monoidal; symmetric) + + monoidalCategory : MonoidalCategory o β„“ e + monoidalCategory = record + { U = π’ž + ; monoidal = monoidal + } + + symmetricMonoidalCategory : SymmetricMonoidalCategory o β„“ e + symmetricMonoidalCategory = record + { U = π’ž + ; monoidal = monoidal + ; symmetric = symmetric + } + record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where field @@ -127,6 +188,41 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where (f + h) + (g + i) β‰ˆβŸ¨ +-cong f≀h g≀i ⟩ h + i ∎ + Ξ”-βŠ• : {X Y : Obj} β†’ Ξ” {X βŠ• Y} β‰ˆ σ₂₃ ∘ Ξ” ×₁ Ξ” + Ξ”-βŠ• {X} {Y} = begin + ⟨ id , id ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ id×₁id id×₁id ⟨ + ⟨ id ×₁ id , id ×₁ id ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (×₁-congβ‚‚ project₁ project₁) (×₁-congβ‚‚ projectβ‚‚ projectβ‚‚) ⟨ + ⟨ (π₁ ∘ Ξ”) ×₁ (π₁ ∘ Ξ”) , (Ο€β‚‚ ∘ Ξ”) ×₁ (Ο€β‚‚ ∘ Ξ”) ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ Γ—β‚βˆ˜Γ—β‚ Γ—β‚βˆ˜Γ—β‚ ⟨ + ⟨ π₁ ×₁ π₁ ∘ Ξ” ×₁ Ξ” , Ο€β‚‚ ×₁ Ο€β‚‚ ∘ Ξ” ×₁ Ξ” ⟩ β‰ˆβŸ¨ ⟨⟩∘ ⟨ + σ₂₃ ∘ Ξ” ×₁ Ξ” ∎ + + βˆ‡-βŠ• : {X Y : Obj} β†’ βˆ‡ {X βŠ• Y} β‰ˆ βˆ‡ ×₁ βˆ‡ ∘ σ₂₃ + βˆ‡-βŠ• {X} {Y} = begin + [ id , id ] β‰ˆβŸ¨ []-congβ‚‚ id×₁id id×₁id ⟨ + [ id ×₁ id , id ×₁ id ] β‰ˆβŸ¨ []-congβ‚‚ (×₁-congβ‚‚ inject₁ inject₁) (×₁-congβ‚‚ injectβ‚‚ injectβ‚‚) ⟨ + [ (βˆ‡ ∘ i₁) ×₁ (βˆ‡ ∘ i₁) , (βˆ‡ ∘ iβ‚‚) ×₁ (βˆ‡ ∘ iβ‚‚) ] β‰ˆβŸ¨ []-congβ‚‚ Γ—β‚βˆ˜Γ—β‚ Γ—β‚βˆ˜Γ—β‚ ⟨ + [ βˆ‡ ×₁ βˆ‡ ∘ i₁ ×₁ i₁ , βˆ‡ ×₁ βˆ‡ ∘ iβ‚‚ ×₁ iβ‚‚ ] β‰ˆβŸ¨ ∘[] ⟨ + βˆ‡ ×₁ βˆ‡ ∘ [ i₁ ×₁ i₁ , iβ‚‚ ×₁ iβ‚‚ ] β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-unique (∘[] β—‹ []-congβ‚‚ Ο€β‚βˆ˜Γ—β‚ Ο€β‚βˆ˜Γ—β‚) (∘[] β—‹ []-congβ‚‚ Ο€β‚‚βˆ˜Γ—β‚ Ο€β‚‚βˆ˜Γ—β‚) ⟨ + βˆ‡ ×₁ βˆ‡ ∘ ⟨ π₁ +₁ π₁ , Ο€β‚‚ +₁ Ο€β‚‚ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (×₁-+₁ π₁ π₁) (×₁-+₁ Ο€β‚‚ Ο€β‚‚) ⟨ + βˆ‡ ×₁ βˆ‡ ∘ σ₂₃ ∎ + + ≀-resp-×₁ + : {A B C D : Obj} + {f h : A β‡’ B} + {g i : C β‡’ D} + β†’ f ≀ h + β†’ g ≀ i + β†’ (f ×₁ g) ≀ (h ×₁ i) + ≀-resp-×₁ {f = f} {h} {g} {i} f≀h g≀i = begin + βˆ‡ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ Ξ”-βŠ• ⟩ + βˆ‡ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Ξ” ×₁ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ σ₂₃-×₁ ⟩ + βˆ‡ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Ξ” ×₁ Ξ” β‰ˆβŸ¨ pushΛ‘ βˆ‡-βŠ• ⟩ + βˆ‡ ×₁ βˆ‡ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Ξ” ×₁ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ cancelΛ‘ σ₂₃-σ₂₃ ⟩ + βˆ‡ ×₁ βˆ‡ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Ξ” ×₁ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ Γ—β‚βˆ˜Γ—β‚ ⟩ + βˆ‡ ×₁ βˆ‡ ∘ (f ×₁ h ∘ Ξ”) ×₁ (g ×₁ i ∘ Ξ”) β‰ˆβŸ¨ Γ—β‚βˆ˜Γ—β‚ ⟩ + (βˆ‡ ∘ f ×₁ h ∘ Ξ”) ×₁ (βˆ‡ ∘ g ×₁ i ∘ Ξ”) β‰ˆβŸ¨ ×₁-congβ‚‚ f≀h g≀i ⟩ + h ×₁ i ∎ + ≀-resp-∘ : {A B C : Obj} {f h : B β‡’ C} @@ -156,3 +252,160 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where βˆ‡ ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ introΛ‘ id×₁id ⟩ βˆ‡ ∘ id ×₁ id ∘ Ξ” β‰ˆβŸ¨ idempotent ⟩ id ∎ + + dagger-2-poset : Dagger-2-Poset + dagger-2-poset = record + { 2-poset = record + { Obj = Obj + ; hom = Ξ» A B β†’ record + { Carrier = A β‡’ B + ; _β‰ˆ_ = _β‰ˆ_ + ; _≀_ = _≀_ + ; isPartialOrder = record + { isPreorder = record + { isEquivalence = equiv + ; reflexive = Ξ» xβ‰ˆy β†’ Equiv.trans (+-congΚ³ xβ‰ˆy) ≀-refl + ; trans = ≀-trans + } + ; antisym = ≀-antisym + } + } + ; id = mkPosetHomo _ _ (Ξ» _ β†’ id) (Ξ» _ β†’ ≀-refl) + ; ⊚ = mkPosetHomo _ _ (Ξ» (f , g) β†’ f ∘ g) (Ξ» (≀₁ , ≀₂) β†’ ≀-resp-∘ ≀₁ ≀₂) + ; ⊚-assoc = assoc + ; unitΛ‘ = identityΛ‘ + ; unitΚ³ = identityΚ³ + } + ; hasDagger = record + { _† = _† + ; †-identity = †-identity + ; †-homomorphism = †-homomorphism + ; †-resp-β‰ˆ = ⟨_βŸ©β€  + ; †-involutive = †-involutive + } + ; †-resp-≀ = †-resp-≀ + } + + maps : Category o (β„“ βŠ” e) e + maps = Maps dagger-2-poset + + open Dagger-2-Poset dagger-2-poset using (category) + open SemiadditiveMonoidal semiadditive using (monoidal) + + module M = Monoidal monoidal + + ×₁-functional + : {A B C D : Obj} + {f : A β‡’ B} + {g : C β‡’ D} + β†’ (f ∘ f †) ≀ id + β†’ (g ∘ g †) ≀ id + β†’ (f ×₁ g ∘ (f ×₁ g) †) ≀ id + ×₁-functional {f = f} {g} f∘f†≀id g∘g†≀id = begin + f ×₁ g ∘ (f ×₁ g) † + id β‰ˆβŸ¨ +-congΚ³ (refl⟩∘⟨ †-resp-×₁) ⟩ + f ×₁ g ∘ (f †) ×₁ (g †) + id β‰ˆβŸ¨ +-cong Γ—β‚βˆ˜Γ—β‚ (Equiv.sym id×₁id) ⟩ + (f ∘ f †) ×₁ (g ∘ g †) + id ×₁ id β‰ˆβŸ¨ ≀-resp-×₁ f∘f†≀id g∘g†≀id ⟩ + id ×₁ id β‰ˆβŸ¨ id×₁id ⟩ + id ∎ + + ×₁-entire + : {A B C D : Obj} + {f : A β‡’ B} + {g : C β‡’ D} + β†’ id ≀ (f † ∘ f) + β†’ id ≀ (g † ∘ g) + β†’ id ≀ ((f ×₁ g) † ∘ f ×₁ g) + ×₁-entire {f = f} {g} id≀fβ€ βˆ˜f id≀gβ€ βˆ˜g = begin + id + (f ×₁ g) † ∘ (f ×₁ g) β‰ˆβŸ¨ +-congΛ‘ (†-resp-×₁ ⟩∘⟨refl) ⟩ + id + (f †) ×₁ (g †) ∘ f ×₁ g β‰ˆβŸ¨ +-cong (Equiv.sym id×₁id) Γ—β‚βˆ˜Γ—β‚ ⟩ + id ×₁ id + (f † ∘ f) ×₁ (g † ∘ g) β‰ˆβŸ¨ ≀-resp-×₁ id≀fβ€ βˆ˜f id≀gβ€ βˆ˜g ⟩ + (f † ∘ f) ×₁ (g † ∘ g) β‰ˆβŸ¨ Γ—β‚βˆ˜Γ—β‚ ⟨ + (f †) ×₁ (g †) ∘ f ×₁ g β‰ˆβŸ¨ †-resp-×₁ ⟩∘⟨refl ⟨ + (f ×₁ g) † ∘ f ×₁ g ∎ + + open Map + + βŠ— : Bifunctor maps maps maps + βŠ— = record + { Fβ‚€ = M.βŠ—.β‚€ + ; F₁ = Ξ» (f , g) β†’ record + { map = map f M.βŠ—β‚ map g + ; isMap = record + { functional = ×₁-functional (functional f) (functional g) + ; entire = ×₁-entire (entire f) (entire g) + } + } + ; identity = M.βŠ—.identity + ; homomorphism = M.βŠ—.homomorphism + ; F-resp-β‰ˆ = M.βŠ—.F-resp-β‰ˆ + } + + open Morphism maps using (_β‰…_) + open Equiv + + Ξ»β‡’-unitary : {X : Obj} β†’ Iso category (Ο€β‚‚ {𝟘} {X}) (Ο€β‚‚ †) + Ξ»β‡’-unitary = record { Iso (Iso-resp-β‰ˆ M.unitorΛ‘.iso refl (sym π₂†)) } + + λ⇐-unitary : {X : Obj} β†’ Iso category (iβ‚‚ {𝟘} {X}) (iβ‚‚ †) + λ⇐-unitary = record { Iso (Iso-swap (Iso-resp-β‰ˆ M.unitorΛ‘.iso (sym i₂†) refl)) } + + ρ⇒-unitary : {X : Obj} β†’ Iso category (π₁ {X} {𝟘}) (π₁ †) + ρ⇒-unitary = record { Iso (Iso-resp-β‰ˆ M.unitorΚ³.iso refl (sym π₁†)) } + + ρ⇐-unitary : {X : Obj} β†’ Iso category (i₁ {X} {𝟘}) (i₁ †) + ρ⇐-unitary = record { Iso (Iso-swap (Iso-resp-β‰ˆ M.unitorΚ³.iso (sym i₁†) refl)) } + + Ξ±β‡’-unitary : {X Y Z : Obj} β†’ Iso category (assocΛ‘ {X} {Y} {Z}) (assocΛ‘ †) + Ξ±β‡’-unitary = record { Iso (Iso-resp-β‰ˆ M.associator.iso refl (sym α⇒†)) } + + α⇐-unitary : {X Y Z : Obj} β†’ Iso category (assocΚ³ {X} {Y} {Z}) (assocΚ³ †) + α⇐-unitary = record { Iso (Iso-swap (Iso-resp-β‰ˆ M.associator.iso (sym α⇐†) refl)) } + + unitorΛ‘ : {X : Obj} β†’ 𝟘 M.βŠ—β‚€ X β‰… X + unitorΛ‘ = record + { from = record + { map = M.unitorΛ‘.from + ; isMap = unitary-isMap dagger-2-poset Ξ»β‡’-unitary + } + ; to = record + { map = M.unitorΛ‘.to + ; isMap = unitary-isMap dagger-2-poset λ⇐-unitary + } + ; iso = record { M.unitorΛ‘ } + } + + unitorΚ³ : {X : Obj} β†’ X M.βŠ—β‚€ 𝟘 β‰… X + unitorΚ³ = record + { from = record + { map = M.unitorΚ³.from + ; isMap = unitary-isMap dagger-2-poset ρ⇒-unitary + } + ; to = record + { map = M.unitorΚ³.to + ; isMap = unitary-isMap dagger-2-poset ρ⇐-unitary + } + ; iso = record { M.unitorΚ³ } + } + + associator : {X Y Z : Obj} β†’ (X M.βŠ—β‚€ Y) M.βŠ—β‚€ Z β‰… X M.βŠ—β‚€ (Y M.βŠ—β‚€ Z) + associator = record + { from = record + { map = M.associator.from + ; isMap = unitary-isMap dagger-2-poset Ξ±β‡’-unitary + } + ; to = record + { map = M.associator.to + ; isMap = unitary-isMap dagger-2-poset α⇐-unitary + } + ; iso = record { M.associator } + } + + maps-monoidal : Monoidal maps + maps-monoidal = record + { βŠ— = βŠ— + ; unit = 𝟘 + ; unitorΛ‘ = unitorΛ‘ + ; unitorΚ³ = unitorΚ³ + ; associator = associator + ; M + } -- cgit v1.2.3