Abstract
Following work of Ehrhard and Regnier, we introduce the notion of a
differential category: a (semi-)additive symmetric monoidal
category with a comonad (a "coalgebra modality") and a differential
combinator, satisfying a number of coherence conditions. In such a
category, one should imagine the morphisms in the base category as
being linear maps and the morphisms in the coKleisli category as being
smooth (infinitely differentiable). Although such categories do not
necessarily arise from models of linear logic, one should think of
this as replacing the usual dichotomy of linear vs. stable maps
established for coherence spaces.
After establishing the basic axioms, we give a number of examples. The
most important example arises from a general construction, a comonad
on the category of vector spaces. This comonad and associated
differential operators fully capture the usual notion of derivatives of
smooth maps. Finally, we derive additional properties of differential
categories in certain special cases, especially when the differential
comonad is a storage modality, as in linear logic. In particular, we
introduce the notion of categorical model of the differential
calculus, and show that it captures the not-necessarily-closed fragment
of Ehrhard-Regnier differential lambda-calculus.