Differential categories

Abstract

Following work of Ehrhard and Regnier, we introduce the notion of a differential category: an 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 -calculus.