Projects per year
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ányi. 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 klinear
category with the characteristic feature that their coKleisli
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, structurepreserving 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.
Original language  English 

Pages (fromto)  10991150 
Number of pages  52 
Journal  Applied Categorical Structures 
Volume  29 
Issue number  6 
DOIs  
Publication status  Published  Dec 2021 
Bibliographical note
Copyright the Author(s) 2021. Version archived for private and noncommercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.Keywords
 Cartesian differential categories
 Skew monoidal categories
 Differential categories
Fingerprint
Dive into the research topics of 'Cartesian differential categories as skew enriched categories'. Together they form a unique fingerprint.

Working synthetically in higher categorical structures
Lack, S., Verity, D., Garner, R. & Street, R.
19/06/19 → 18/06/22
Project: Other