Differential categories revisited (Q2307523)

Differential categories were introduced to provide further insight into differential linear logic. The differential \(\lambda\)-calculus is an extension of (simply typed) \(\lambda\)-calculus in which there is an addition operation allowing for the differentiation of terms. This naturally led to examining models of linear logic in which there was, once again, a natural differential operator. Every model of linear logic comes equipped with storage comonad, !, which, in turn, defines a co-Kleisli category of coalgebras for ! which is important for the differential structure if one exists. One can abstract away from models of linear logic to study the comonad as the central feature. This leads to a model of differentiation operators on monoidal categories. The resulting definition of differential category was given by three of the authors of this paper in [Math. Struct. Comput. Sci. 16, No. 6, 1049--1083 (2006; Zbl 1115.03092)]. In this categorical approach. two methods of defining the differentiation were introduced. One uses a deriving transformation, and the other what is termed a codereliction. Coderelictions always give deriving transformations, and under certain circumstances the converse holds. For some time, it was not completely clear if the two notions might not lead to distinct notions of differentiation, but it was found that in the presence of a monoidal coalgebra modality, the two form coincide. This paper, as the title suggests, revisits the original definition of a differential category, and, following an exposition of the terminology (coalgebra modality, etc.), proves that, under the conditions mentioned above, the two approaches are equivalent. (Very extensive and effective use is made of the graphical calculus for monoidal categories, augmented as appropriate to handle extra structure.)