A convenient differential category

TL;DR

This paper demonstrates that the category of convenient vector spaces, as introduced by Fr"olicher and Kriegl, forms a differential category, providing a new bornological perspective on models of differential linear logic.

Contribution

It offers a new bornological interpretation of convenient vector spaces as models of differential linear logic, expanding the understanding of their categorical structure.

Findings

The category of Mackey-complete, separated, topological convex bornological vector spaces is a differential category.

Provides a new interpretation of convenient vector spaces within differential linear logic.

Highlights the potential of bornological structures to model differential logics.

Abstract

In this paper, we show that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category. Such spaces were introduced by Fr\"olicher and Kriegl, where they were called convenient vector spaces. While much of the structure necessary to demonstrate this observation is already contained in Fr\"olicher and Kriegl's book, we here give a new interpretation of the category of convenient vector spaces as a model of the differential linear logic of Ehrhard and Regnier. Rather than base our proof on the abstract categorical structure presented by Fr\"olicher and Kriegl, we prefer to focus on the bornological structure of convenient vector spaces. We believe bornological structures will ultimately yield a wide variety of models of differential logics.