Cartesian differential categories

by R.F. Blute, J.R.B. Cockett and R.A.G. Seely


This paper revisits the authors' notion of a differential category from a different perspective. A differential category is an additive symmetric monoidal category with a comonad (a "coalgebra modality") and a differential combinator. The morphisms of a differential category should be thought of as the linear maps; the differentiable or smooth maps would then be morphisms of the coKleisli category. The purpose of the present paper is to directly axiomatize differentiable maps and thus to move the emphasis from the linear notion to structures resembling the coKleisli category. The result is a setting with a more evident and intuitive relationship to the familiar notion of calculus on smooth maps. Indeed a primary example is the category whose objects are Euclidean spaces and whose morphisms are smooth maps.

A Cartesian differential category is a Cartesian left additive category which possesses a Cartesian differential operator. The differential operator itself must satisfy a number of equations, which guarantee, in particular, that the differential of any map is "linear" in a suitable sense.

We present an analysis of the basic properties of Cartesian differential categories. We show that under modest and natural assumptions, the coKleisli category of a differential category is Cartesian differential. Finally we present a (sound and complete) term calculus for these categories which allows their structure to be analysed using essentially the same language one might use for traditional multi-variable calculus.