Categorical semantics
(→Modeling IMLL) |
|||
Line 39: | Line 39: | ||
for every objects <math>A</math> and <math>B</math>. |
for every objects <math>A</math> and <math>B</math>. |
||
}} |
}} |
||
+ | |||
+ | {{Definition|title=Closed monoidal category| |
||
+ | A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor |
||
+ | :<math>B\mapsto A\otimes B</math> |
||
+ | has a right adjoint, written |
||
+ | :<math>B\mapsto(A\limp B)</math> |
||
+ | This means that there exists a bijection |
||
+ | :<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(A,B\limp C)</math> |
||
+ | which is natural in <math>B</math> and <math>C</math>. |
||
+ | Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of |
||
+ | * an object <math>A\limp B</math>, |
||
+ | * a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'', |
||
+ | 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> |
||
+ | commute. |
||
+ | |||
+ | Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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''. |
||
== Modeling the additives == |
== Modeling the additives == |
Revision as of 18:58, 23 March 2009
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.
TODO: why categories? how to extract categorical models? etc.
See [1]for a more detailed introduction to category theory.
Contents |
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 diagrams
commute.
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
- UNIQ5607d479223b9843-math-00000011-QINU
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 Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)):
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.
Modeling the additives
Definition (Product)
Definition (Monoid)
Property
Categories with products vs monoidal categories.
Modeling IMALL
Modeling negation
Definition (*-autonomous category)
TODO
References
- ↑ MacLane, Saunders. Categories for the Working Mathematician.