Cartesian differential categories as skew enriched categories (Q825992): Difference between revisions

This paper proves an embedding theorem for cartesian differential categories which is of interest in the area of intuitionistic differential linear logic. The technique is to show that cartesian differential categories are categories enriched in a skew monoidal base so that it is possible to make use of an enriched Yoneda embedding. Apart from advancing our understanding of differential categories, this work widens the scope and applications of skew monoidal categories and enrichment over them. Modules over a commutative rig \(k\) are considered but I shall discuss the indicative case \(k = \mathbb{N}\). The category \(\mathrm{CMon}\) of commutative monoids is closed: the internal hom is the homset with the addition operation taken pointwise. Categories enriched in \(\mathrm{CMon}\) are occasionally called additive categories: they share with usual additive categories the fact that any finite product is a direct sum. With this in mind, \textit{R. F. Blute} et al. [Theory Appl. Categ. 22, 622--672 (2009; Zbl 1262.18004)] define a category to be left additive when each hom is a commutative monoid but only composition on the left with a morphism is required to preserve the addition. Yet \(\mathrm{CMon}\) also has a skew closed structure: the internal hom \([A,B]_w\) is the set of all functions from \(A\) to \(B\) with pointwise addition. In 2012, Cockett and Lack pointed out that left additive categories are categories enriched (in the sense of \textit{R. Street} [J. Pure Appl. Algebra 217, No. 6, 973--988 (2013; Zbl 1365.18008)]) in this skew closed category \(\mathrm{CMon}_w\). Indeed, \(\mathrm{CMon}_w\) is a skew warping (in the sense of \textit{S. Lack} and \textit{R. Street} [Theory Appl. Categ. 26, 385--402 (2012; Zbl 1252.18016)] of the monoidal closed category \(\mathrm{CMon}\) by the monoidal comonad generated by the underlying functor into \(\mathrm{CMon}\to \mathrm{Set}\) and its left adjoint. Cartesian differential categories \(\mathcal{A}\) are left-additive categories admitting finite products and equipped with the extra structure of a derivative \(D(f) : A\times A \to B\) for each morphism \(f : A\to B\), subject to axioms expressing the formulas of multivariable calculus. The paper under review shows that such \(\mathcal{A}\) too are enriched in a warping of \(\mathrm{CMon}\). They are precisely the enriched categories admitting finite products, meaning what you might expect plus the condition that the projections are \(\mathcal{V}\)-linear (in a sense the authors define for morphisms in enriched categories over a general skew monoidal \(\mathcal{V}\)). Here the monoidal comonad \(Q\) on \(\mathrm{CMon}\) providing the warping is a monoidal differential modality. Showing that it is the initial such modality is left for a future paper.