An algebra modality admitting countably many deriving transformations
Jean-Baptiste Vienney
TL;DR
The paper addresses whether the uniqueness of deriving transformations for comonoidal algebra modalities in differential categories extends to arbitrary algebra modalities. It constructs a counterexample by building a free commutative rig with a self-map on $\mathsf{CMon}$, yielding a monad $F$ endowed with an algebra modality structure and a countable family $({}_{n}\mathsf{d})_{n\in\mathbb{N}}$ of deriving transformations. The main result shows that, for this $F$, the deriving transformations are pairwise distinct, proving that a single algebra modality may support multiple inequivalent notions of differentiation. This clarifies the limitations of uniqueness results outside differential linear logic and provides an explicit, general construction demonstrating non-uniqueness in differential categories. The work thus delineates the boundary between differentiation in differential categories and the stricter setting of differential linear logic, with implications for categorical models of smooth functions and differentiation.
Abstract
A differential category is an additive symmetric monoidal category, that is, a symmetric monoidal category enriched over commutative monoids, with an algebra modality, axiomatizing smooth functions, and a deriving transformation on this algebra modality, axiomatizing differentiation. Lemay proved that a comonoidal algebra modality has at most one deriving transformation, thus differentiation is unique in models of differential linear logic. It was then an open problem whether this result extends to arbitrary algebra modalities. We answer this question in the negative. We build a free "commutative rig with a self-map" algebra modality on the category of commutative monoids, where the self-map can be seen as an arbitrary smooth function. We then define a countable family of distinct deriving transformations $({}_{n}\mathsf{d})_{n \in \mathbb{N}}$ on this algebra modality where the parameter $n$ controls the derivative of the self-map. It shows that in a differential category, a single algebra modality may admit multiple, inequivalent notions of differentiation.