Cartesian differential categories as skew enriched categories

DOI10.1007/S10485-021-09649-7MaRDI QIDQ825992zbMATH OpenOpenAlexFDO

Authors Richard Garner, Jean-Simon Pacaud Lemay

Publication date 18 December 2021

Published in Applied Categorical Structures (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2002.02554

zbMATH Keywords

cartesian differential category differential category differential modality enriched category skew monoidal category

Mathematics Subject Classification ID

Enriched categories (over closed or monoidal categories) (18D20)

Abstract: We exhibit the cartesian differential categories of Blute, Cockett and Seely as a particular kind of enriched category. The base for the enrichment is the category of commutative monoids -- or in a straightforward generalisation, the category of modules over a commutative rig

k

. However, the tensor product on this category is not the usual one, but rather a warping of it by a certain monoidal comonad

Q

. Thus the enrichment base is not a monoidal category in the usual sense, but rather a skew monoidal category in the sense of Szlach'anyi. Our first main result is that cartesian differential categories are the same as categories with finite products enriched over this skew monoidal base. The comonad

Q

involved is, in fact, an example of a differential modality. Differential modalities are a kind of comonad on a symmetric monoidal

k

-linear category with the characteristic feature that their co-Kleisli categories are cartesian differential categories. Using our first main result, we are able to prove our second one: that every small cartesian differential category admits a full, structure-preserving embedding into the cartesian differential category induced by a differential modality (in fact, a monoidal differential modality on a monoidal closed category -- thus, a model of intuitionistic differential linear logic). This resolves an important open question in this area.

Review text

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.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Cartesian differential categories as skew enriched categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q825992)