Categorical semantics
(→Modeling negation) |
(→Compact closed categories) |
||
(42 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
− | Constructing denotational models of linear can be a tedious work. Categorical model are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models. |
+ | Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models. |
TODO: why categories? how to extract categorical models? etc. |
TODO: why categories? how to extract categorical models? etc. |
||
− | See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. |
+ | See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic. |
+ | |||
+ | == Basic category theory recalled == |
||
+ | {{Definition|title=Category| |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Functor| |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Natural transformation| |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Adjunction| |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Monad| |
||
+ | }} |
||
+ | |||
+ | == Overview == |
||
+ | |||
+ | In order to interpret the various [[fragment]]s of linear logic, we define incrementally what structure we need in a categorical setting. |
||
+ | |||
+ | * The most basic underlying structure are '''symmetric monoidal categories''' which model the symmetric tensor <math>\otimes</math> and its unit <math>1</math>. |
||
+ | * The <math>\otimes, \multimap</math> fragment ([[IMLL]]) is captured by so-called '''symmetric monoidal closed categories'''. |
||
+ | * Upgrading to [[ILL]], that is, adding the exponential <math>\oc</math> modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough '''adjunctions''', or with an ad-hoc definition of a well-behaved comonad which leads to '''linear categories''' and close relatives. |
||
+ | * Dealing with the additives <math>\with, \oplus</math> is quite easy, as they are plain '''cartesian product''' and '''coproduct''', usually defined through universal properties in category theory. |
||
+ | * Retrieving <math>\parr</math>, <math>\bot</math> and <math>\wn</math> is just a matter of dualizing <math>\otimes</math>, <math>1</math> and <math>\oc</math>, thus requiring the model to be a '''*-autonomous category''' for that purpose. |
||
== Modeling [[IMLL]] == |
== Modeling [[IMLL]] == |
||
Line 23: | Line 23: | ||
such that |
such that |
||
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram |
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | ((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\ |
||
+ | (A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D)) |
||
+ | } |
||
+ | </math> |
||
commutes, |
commutes, |
||
− | * for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagrams |
+ | * for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram |
− | commute. |
+ | :<math> |
+ | \xymatrix{ |
||
+ | (A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\ |
||
+ | &A\otimes B& |
||
+ | } |
||
+ | </math> |
||
+ | commutes. |
||
}} |
}} |
||
Line 32: | Line 38: | ||
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math> |
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math> |
||
called ''braiding'', such that the two diagrams |
called ''braiding'', such that the two diagrams |
||
− | :<math></math> |
+ | :<math> |
+ | \xymatrix{ |
||
+ | &A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\ |
||
+ | (A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\ |
||
+ | &(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\ |
||
+ | } |
||
+ | </math> |
||
+ | and |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | &(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\ |
||
+ | A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\ |
||
+ | &A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\ |
||
+ | } |
||
+ | </math> |
||
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>. |
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>. |
||
Line 53: | Line 59: | ||
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram |
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram |
||
:<math> |
:<math> |
||
− | TODO |
+ | \xymatrix{ |
+ | A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\ |
||
+ | A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B |
||
+ | } |
||
</math> |
</math> |
||
commute. |
commute. |
||
Line 64: | Line 70: | ||
== Modeling the additives == |
== Modeling the additives == |
||
{{Definition|title=Product| |
{{Definition|title=Product| |
||
+ | A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | &\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\ |
||
+ | &\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\ |
||
+ | B&&C |
||
+ | } |
||
+ | </math> |
||
+ | commute. |
||
}} |
}} |
||
+ | |||
+ | A category has ''finite products'' when it has products and a terminal object. |
||
{{Definition|title=Monoid| |
{{Definition|title=Monoid| |
||
+ | A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms |
||
+ | :<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math> |
||
+ | such that the diagrams |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | &(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\ |
||
+ | M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\ |
||
+ | M\tens M\ar[rr]_{\mu}&&M\\ |
||
+ | } |
||
+ | </math> |
||
+ | and |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\ |
||
+ | &M& |
||
+ | } |
||
+ | </math> |
||
+ | commute. |
||
}} |
}} |
||
Line 73: | Line 108: | ||
}} |
}} |
||
− | == Modeling [[IMLL]] == |
+ | == Modeling [[ILL]] == |
Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>. |
Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>. |
||
Line 80: | Line 115: | ||
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors |
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors |
||
:<math> |
:<math> |
||
− | (\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I) |
+ | \xymatrix{ |
+ | (\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I) |
||
+ | } |
||
</math> |
</math> |
||
in which the category <math>\mathcal{M}</math> has finite products. |
in which the category <math>\mathcal{M}</math> has finite products. |
||
+ | }} |
||
+ | |||
+ | :<math>\oc=L\circ M</math> |
||
+ | |||
+ | This section is devoted to defining the concepts necessary to define these adjunctions. |
||
+ | |||
+ | {{Definition|title=Monoidal functor| |
||
+ | A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of |
||
+ | * a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories, |
||
+ | * a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>, |
||
+ | * a morphism <math>f:J\to FI</math> |
||
+ | such that the diagrams |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | (FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\ |
||
+ | F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\ |
||
+ | &F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C)) |
||
+ | } |
||
+ | </math> |
||
+ | and |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\ |
||
+ | FA&\ar[l]^{F\rho_A}F(A\otimes I) |
||
+ | } |
||
+ | </math> and <math> |
||
+ | \xymatrix{ |
||
+ | J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\ |
||
+ | FB&\ar[l]^{F\lambda_B}F(I\otimes B) |
||
+ | } |
||
+ | </math> |
||
+ | commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''. |
||
+ | |||
+ | A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities. |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Monoidal natural transformation| |
||
+ | Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and |
||
+ | :<math> |
||
+ | (F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J) |
||
+ | </math> and <math> |
||
+ | (G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J) |
||
+ | </math> |
||
+ | are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\ |
||
+ | F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B) |
||
+ | } |
||
+ | </math> and <math> |
||
+ | \xymatrix{ |
||
+ | &\ar[dl]_{f}J\ar[dr]^{g}&\\ |
||
+ | FI\ar[rr]_{\theta_I}&&GI |
||
+ | } |
||
+ | </math> |
||
+ | commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>. |
||
+ | }} |
||
+ | |||
+ | {{Definition|title=Monoidal adjunction| |
||
+ | A ''monoidal adjunction'' between two monoidal functors |
||
+ | :<math> |
||
+ | (F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J) |
||
+ | </math> and <math> |
||
+ | (G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I) |
||
+ | </math> |
||
+ | is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit |
||
+ | :<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math> |
||
+ | induce monoidal natural transformations between the corresponding monoidal functors. |
||
}} |
}} |
||
Line 96: | Line 199: | ||
=== Compact closed categories === |
=== Compact closed categories === |
||
+ | |||
+ | {{Definition|title=Dual objects| |
||
+ | A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms |
||
+ | :<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math> |
||
+ | such that the diagrams |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | &A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\ |
||
+ | A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\ |
||
+ | A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\ |
||
+ | } |
||
+ | </math> |
||
+ | and |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | &(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\ |
||
+ | I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\ |
||
+ | B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\ |
||
+ | } |
||
+ | </math> |
||
+ | commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>). |
||
+ | }} |
||
+ | |||
+ | {{Lemma| |
||
+ | Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic. |
||
+ | }} |
||
{{Definition|title=Compact closed category| |
{{Definition|title=Compact closed category| |
||
− | A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual. |
+ | A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write |
+ | :<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math> |
||
+ | for the corresponding duality morphisms. |
||
}} |
}} |
||
+ | {{Lemma| |
||
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic. |
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic. |
||
+ | }} |
||
{{Property| |
{{Property| |
||
− | A compact closed category is monoidal closed. |
+ | A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by |
+ | :<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math> |
||
+ | }} |
||
+ | {{Proof| |
||
+ | To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\ |
||
+ | } |
||
+ | </math> |
||
+ | and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as |
||
+ | :<math> |
||
+ | \xymatrix{ |
||
+ | A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C |
||
+ | } |
||
+ | </math> |
||
+ | It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection. |
||
+ | }} |
||
+ | |||
+ | {{Property| |
||
+ | A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, <math>(A \otimes B)^* \cong A^*\otimes B^*</math>. |
||
+ | }} |
||
+ | |||
+ | {{Remark|The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify <math>\otimes</math> and <math>\parr</math> as well as <math>1</math> and <math>\bot</math>.}} |
||
+ | |||
+ | {{Proof| |
||
+ | The dualizing object <math>R</math> is simply <math>I^*</math>. |
||
+ | |||
+ | For any <math>A</math>, the reverse isomorphism <math>\delta_A : (A \multimap R)\multimap R \rightarrow A</math> is constructed as follows: |
||
+ | |||
+ | <math>\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)</math> |
||
+ | |||
+ | Identity on <math>A</math> is taken as the canonical morphism required. |
||
+ | |||
}} |
}} |
||
== Other categorical models == |
== Other categorical models == |
||
+ | |||
+ | === Lafont categories === |
||
+ | |||
+ | === Seely categories === |
||
+ | |||
+ | === Linear categories === |
||
== Properties of categorical models == |
== Properties of categorical models == |
Latest revision as of 00:29, 4 October 2011
Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.
TODO: why categories? how to extract categorical models? etc.
See [1]for a more detailed introduction to category theory. See [2]for a detailed treatment of categorical semantics of linear logic.
Contents |
[edit] Basic category theory recalled
Definition (Category)
Definition (Functor)
Definition (Natural transformation)
Definition (Adjunction)
Definition (Monad)
[edit] Overview
In order to interpret the various fragments of linear logic, we define incrementally what structure we need in a categorical setting.
- The most basic underlying structure are symmetric monoidal categories which model the symmetric tensor and its unit 1.
- The fragment (IMLL) is captured by so-called symmetric monoidal closed categories.
- Upgrading to ILL, that is, adding the exponential modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough adjunctions, or with an ad-hoc definition of a well-behaved comonad which leads to linear categories and close relatives.
- Dealing with the additives is quite easy, as they are plain cartesian product and coproduct, usually defined through universal properties in category theory.
- Retrieving , and is just a matter of dualizing , 1 and , thus requiring the model to be a *-autonomous category for that purpose.
[edit] Modeling IMLL
A model of IMLL is a closed symmetric monoidal category. We recall the definition of these categories below.
Definition (Monoidal category)
A monoidal category is a category equipped with
- a functor called tensor product,
- an object I called unit object,
- three natural isomorphisms α, λ and ρ, called respectively associator, left unitor and right unitor, whose components are
such that
- for every objects A,B,C,D in , the diagram
commutes,
- for every objects A and B in , the diagram
commutes.
Definition (Braided, symmetric monoidal category)
A braided monoidal category is a category together with a natural isomorphism of components
called braiding, such that the two diagrams
and
commute for every objects A, B and C.
A symmetric monoidal category is a braided monoidal category in which the braiding satisfies
for every objects A and B.
Definition (Closed monoidal category)
A monoidal category is left closed when for every object A, the functor
has a right adjoint, written
This means that there exists a bijection
which is natural in B and C. Equivalently, a monoidal category is left closed when it is equipped with a left closed structure, which consists of
- an object ,
- a morphism , called left evaluation,
for every objects A and B, such that for every morphism there exists a unique morphism making the diagram
commute.
Dually, the monoidal category is right closed when the functor admits a right adjoint. The notion of right closed structure can be defined similarly.
In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a closed symmetric monoidal category.
[edit] Modeling the additives
Definition (Product)
A product (X,π1,π2) of two coinitial morphisms and in a category is an object X of together with two morphisms and such that there exists a unique morphism making the diagram
commute.
A category has finite products when it has products and a terminal object.
Definition (Monoid)
A monoid (M,μ,η) in a monoidal category is an object M together with two morphisms
- and
such that the diagrams
and
commute.
Property
Categories with products vs monoidal categories.
[edit] Modeling ILL
Introduced in[3].
Definition (Linear-non linear (LNL) adjunction)
A linear-non linear adjunction is a symmetric monoidal adjunction between lax monoidal functors
in which the category has finite products.
This section is devoted to defining the concepts necessary to define these adjunctions.
Definition (Monoidal functor)
A lax monoidal functor (F,f) between two monoidal categories and consists of
- a functor between the underlying categories,
- a natural transformation f of components ,
- a morphism
such that the diagrams
and
- and
commute for every objects A, B and C of . The morphisms fA,B and f are called coherence maps.
A lax monoidal functor is strong when the coherence maps are invertible and strict when they are identities.
Definition (Monoidal natural transformation)
Suppose that and are two monoidal categories and
- and
are two monoidal functors between these categories. A monoidal natural transformation between these monoidal functors is a natural transformation between the underlying functors such that the diagrams
- and
commute for every objects A and B of .
Definition (Monoidal adjunction)
A monoidal adjunction between two monoidal functors
- and
is an adjunction between the underlying functors F and G such that the unit and the counit
- and
induce monoidal natural transformations between the corresponding monoidal functors.
[edit] Modeling negation
[edit] *-autonomous categories
Definition (*-autonomous category)
Suppose that we are given a symmetric monoidal closed category and an object R of . For every object A, we define a morphism
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism , we get a morphism , and thus a morphism by precomposing with the symmetry . The morphism is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object R is called dualizing when the morphism is a bijection for every object A of . A symmetric monoidal closed category is *-autonomous when it admits such a dualizing object.
[edit] Compact closed categories
Definition (Dual objects)
A dual object structure in a monoidal category is a pair of objects A and B together with two morphisms
- and
such that the diagrams
and
commute. The object A is called a left dual of B (and conversely B is a right dual of A).
Lemma
Two left (resp. right) duals of a same object B are necessarily isomorphic.
Definition (Compact closed category)
A symmetric monoidal category is compact closed when every object A has a right dual A * . We write
- and
for the corresponding duality morphisms.
Lemma
In a compact closed category the left and right duals of an object A are isomorphic.
Property
A compact closed category is monoidal closed, with closure defined by
Proof. To every morphism , we associate a morphism defined as
and to every morphism , we associate a morphism defined as
It is easy to show that and from which we deduce the required bijection.
Property
A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, .
Remark: The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify and as well as 1 and .
Proof. The dualizing object R is simply I * .
For any A, the reverse isomorphism is constructed as follows:
Identity on A is taken as the canonical morphism required.