#
Cartesian differential storage categories

##
R. Blute, J.R.B. Cockett, and R.A.G. Seely

Monoidal differential categories provide the framework for categorical models
of differential linear logic. The coKleisli category of any monoidal
differential category is always a Cartesian differential category. Cartesian
differential categories, besides arising in this manner as coKleisli
categories, occur in many different and quite independent ways. Thus, it was
not obvious how to pass from Cartesian differential categories back to monoidal
differential categories.

This paper provides natural conditions under which the linear maps of a
Cartesian differential category form a monoidal differential category. This is
a question of some practical importance as much of the machinery of modern
differential geometry is based on models which implicitly allow such a passage,
and thus the results and tools of the area tend to freely assume access to this
structure.

The purpose of this paper is to make precise the connection between the two
types of differential categories. As a prelude to this, however, it is
convenient to have available a general theory which relates the behaviour of
"linear" maps in Cartesian categories to the structure of Seely categories.
The latter were developed to provide the categorical semantics for (fragments
of) linear logic which use a "storage" modality. The general theory of
storage, which underlies the results mentioned above, is developed in the
opening sections of the paper and is then applied to the case of differential
categories.

Keywords:
monoidal categories, differential categories, Kleisli categories, differential
operators

2010 MSC:
18D10,18C20,12H05,32W99

*Theory and Applications of Categories,*
Vol. 30, 2015,
No. 18, pp 620-686.

Published 2015-05-06.

http://www.tac.mta.ca/tac/volumes/30/18/30-18.pdf

TAC Home