Convenient Antiderivatives For Differential Linear Categories

TL;DR

This paper demonstrates that certain differential categories, including those of convenient vector spaces and relational models, possess antiderivatives, enabling a categorical formulation of integration and calculus fundamentals.

Contribution

It proves that convenient vector spaces and relational models are differential linear categories with antiderivatives, extending the categorical framework of calculus.

Findings

Convenient vector spaces have antiderivatives in this categorical setting.

Relational models can be equipped with antiderivatives.

Fundamental Theorems of Calculus hold in these models.

Abstract

Differential categories axiomatize the basics of differentiation and provide categorical models of differential linear logic. A differential category is said to have antiderivatives if a natural transformation $\mathsf{K}$, which all differential categories have, is a natural isomorphism. Differential categories with antiderivatives come equipped with a canonical integration operator such that generalizations of the Fundamental Theorems of Calculus hold. In this paper, we show that Blute, Ehrhard, and Tasson's differential category of convenient vector spaces has antiderivatives. To help prove this result, we show that a differential linear category -- which is a differential category with a monoidal coalgebra modality -- has antiderivatives if and only if one can integrate over the monoidal unit and such that the Fundamental Theorems of Calculus hold. We also show that generalizations of the relational model (which are biproduct completions of complete semirings) are also differential linear categories with antiderivatives.