Cartesian differential storage categories

R. Blute ; J.R.B. Cockett ; R.A.G. Seely

Theory and applications of categories, Tome 30 (2015), pp. 620-686.

Résumé

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.

Détail

Publié le : 2015-05-06

Classification : 18D10, 18C20, 12H05, 32W99
Keywords: monoidal categories, differential categories, Kleisli categories, differential operators