Free differential modalities

TL;DR

This paper demonstrates that in well-structured symmetric monoidal categories, every coalgebra modality can be extended to a differential modality, introducing new models for differential linear logic and exploring algebraically-free monoids.

Contribution

It establishes the existence of a free construction from coalgebra to differential modalities and introduces the concept of algebraically-free commutative monoids in this context.

Findings

Every coalgebra modality can be freely completed to a differential modality.

Existence of an initial monoidal differential modality in certain categories.

New models of differential linear logic are obtained even in simple settings like sets and relations.

Abstract

Categorical models of the exponential modality of linear logic will often, but not always, support an operation of differentiation. When they do, we speak of a monoidal differential modality; when they do not, we have merely a monoidal coalgebra modality. More generally, there are notions of differential modality and coalgebra modality which stand in the same relation, but which move outside the realm of linear logic; they model important structures such as smooth differentiation on Euclidean space. In this paper, we show that, in a suitably well-behaved k-linear symmetric monoidal category, each (monoidal) coalgebra modality can be freely completed to a (monoidal) differential modality. In particular, we prove the existence of an initial monoidal differential modality, which, even in simple examples such as the category of sets and relations, yields new models of differential linear logic. Key to our proofs is the concept of an algebraically-free commutative monoid in a symmetric monoidal category. A commutative monoid $M$ is said to be algebraically-free on an object $X$ if actions by the monoid $M$ correspond to self-commuting actions by the mere object $X$. Along the way, we study the theory of algebraically-free commutative monoids and self-commuting actions, and their interplay with differential modality structure.