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.