module Cat.Monoidal.Base where
Monoidal categoriesπ
record Monoidal-category {o β} (C : Precategory o β) : Type (o β β) where no-eta-equality open Cr C
A monoidal category is a vertical categorification of the concept of monoid: We replace the identities in a monoid by isomorphisms. For this to make sense, a monoidal category must have an underlying precategory, rather than an underlying set; Similarly, the multiplication operation must be a multiplication functor, and we have to throw on some coherence data on top, to make sure everything works out.
We start with a category together with a chosen functor, the tensor product, , and a distinguished object , the tensor unit. These take the place of the multiplication operation and identity element, respectively.
field -β- : Functor (C ΓαΆ C) C Unit : Ob
private module -β- = Bifunctor -β- _β_ : Ob β Ob β Ob A β B = -β- .Functor.Fβ (A , B) _ββ_ : β {w x y z} β Hom w x β Hom y z β Hom (w β y) (x β z) f ββ g = -β- .Functor.Fβ (f , g)
We replace the associativity and unit laws by associativity and unitor morphisms, which are natural isomorphisms (in components)
The morphism is called the associator, and (resp. ) are the right unitor (resp. left unitor).
field unitor-l : Cr._β _ Cat[ C , C ] Id (-β-.Right Unit) unitor-r : Cr._β _ Cat[ C , C ] Id (-β-.Left Unit) associator : Cr._β _ Cat[ C ΓαΆ C ΓαΆ C , C ] (compose-assocΛ‘ {O = β€} {H = Ξ» _ _ β C} -β-) (compose-assocΚ³ {O = β€} {H = Ξ» _ _ β C} -β-)
Ξ»β : β {X} β Hom (Unit β X) X Ξ»β = unitor-l .Cr._β _.from .Ξ· _ Ξ»β : β {X} β Hom X (Unit β X) Ξ»β = unitor-l .Cr._β _.to .Ξ· _ Οβ : β {X} β Hom (X β Unit) X Οβ = unitor-r .Cr._β _.from .Ξ· _ Οβ : β {X} β Hom X (X β Unit) Οβ = unitor-r .Cr._β _.to .Ξ· _ Ξ±β : β A B C β Hom ((A β B) β C) (A β (B β C)) Ξ±β _ _ _ = associator .Cr._β _.to .Ξ· _ Ξ±β : β A B C β Hom (A β (B β C)) ((A β B) β C) Ξ±β _ _ _ = associator .Cr._β _.from .Ξ· _ -- whiskering on the right _βΆ_ : β A {B C} (g : Hom B C) β Hom (A β B) (A β C) _βΆ_ A f = id ββ f -- whiskering on the left _β_ : β {A B} (g : Hom A B) C β Hom (A β C) (B β C) _β_ f A = f ββ id
The final data we need are coherences relating the left and right unitors (the triangle identity; despite the name, nothing to do with adjunctions), and one for reducing sequences of associators, the pentagon identity. As for where the name βpentagonβ comes from, the path pentagon witnesses commutativity of the diagram
which we have drawn less like a regular pentagon and more like a childrenβs drawing of a house, so that it fits on the page horizontally.
field triangle : β {A B} β (Οβ β B) β Ξ±β A Unit B β‘ A βΆ Ξ»β pentagon : β {A B C D} β (Ξ±β A B C β D) β Ξ±β A (B β C) D β (A βΆ Ξ±β B C D) β‘ Ξ±β (A β B) C D β Ξ±β A B (C β D)
Deloopingsπ
Just as a monoid can be promoted to a 1-object category, with the underlying set of the monoid becoming the single -set, we can deloop a monoidal category into a bicategory with a single object, where the sole -category is given by the monoidal category.
Deloop : β {o β} {C : Precategory o β} β Monoidal-category C β Prebicategory lzero o β Deloop {C = C} mon = bi where open Prebicategory module M = Monoidal-category mon bi : Prebicategory _ _ _ bi .Ob = β€ bi .Hom _ _ = C bi .id = M.Unit bi .compose = M.-β- bi .unitor-l = M.unitor-l bi .unitor-r = M.unitor-r bi .associator = M.associator bi .triangle _ _ = M.triangle bi .pentagon _ _ _ _ = M.pentagon
This makes the idea that a monoidal category is βjustβ the categorified version of a monoid precisely, and itβs generally called the delooping hypothesis: A monoidal -category is the same as an -category with a single object.
Endomorphism categoriesπ
In the same way that, if you have a category , making a choice of object canonically gives you a monoid of endomorphisms , having a bicategory and choosing an object canonically gives you a choice of monoidal category, .
Endomorphisms : β {o β ββ²} (B : Prebicategory o β ββ²) β (a : Prebicategory.Ob B) β Monoidal-category (Prebicategory.Hom B a a) Endomorphisms B a = mon where open Monoidal-category module B = Prebicategory B mon : Monoidal-category (B.Hom a a) mon .-β- = B.compose mon .Unit = B.id mon .unitor-l = B.unitor-l mon .unitor-r = B.unitor-r mon .associator = to-natural-iso $ ni where open make-natural-iso open Cr ni : make-natural-iso _ _ ni .eta _ = B.Ξ±β _ _ _ ni .inv _ = B.Ξ±β _ _ _ ni .etaβinv _ = Cr.invl _ B.associator Ξ·β _ ni .invβeta _ = Cr.invr _ B.associator Ξ·β _ ni .natural x y f = sym $ Cr.to B.associator .is-natural _ _ _ mon .triangle = B.triangle _ _ mon .pentagon = B.pentagon _ _ _ _