ﻻ يوجد ملخص باللغة العربية
Cartesian differential categories were introduced to provide an abstract axiomatization of categories of differentiable functions. The fundamental example is the category whose objects are Euclidean spaces and whose arrows are smooth maps. Tensor differential categories provide the framework for categorical models of differential linear logic. The coKleisli category of any tensor differential category is always a Cartesian differential category. Cartesian differential categories, besides arising in this manner as coKleisli categories, occur in many different and quite independent ways. Thus, it was not obvious how to pass from Cartesian differential categories back to tensor differential categories. This paper provides natural conditions under which the linear maps of a Cartesian differential category form a tensor differential category. This is a question of some practical importance as much of the machinery of modern differential geometry is based on models which implicitly allow such a passage, and thus the results and tools of the area tend to freely assume access to this structure. The purpose of this paper is to make precise the connection between the two types of differential categories. As a prelude to this, however, it is convenient to have available a general theory which relates the behaviour of linear maps in Cartesian categories to the structure of Seely categories. The latter were developed to provide the categorical semantics for (fragments of) linear logic which use a storage modality. The general theory of storage, which underlies the results mentioned above, is developed in the opening sections of the paper and is then applied to the case of differential categories.
We revisit the definition of Cartesian differential categories, showing that a slightly more general version is useful for a number of reasons. As one application, we show that these general differential categories are comonadic over Cartesian catego
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 modu
We prove that four different ways of defining Cartesian fibrations and the Cartesian model structure are all Quillen equivalent: On marked simplicial sets, on bisimplicial spaces, on bisimplicial sets, on marked simplicial spaces. The main way to pro
We prove that every locally Cartesian closed $infty$-category with subobject classifier has a strict initial object and disjoint and universal binary coproducts.
We combine two recent ideas: cartesian differential categories, and restriction categories. The result is a new structure which axiomatizes the category of smooth maps defined on open subsets of $R^n$ in a way that is completely algebraic. We also gi