Additive Enrichment from Coderelictions
Jean-Simon Pacaud Lemay
TL;DR
This work investigates the categorical semantics of differentiation beyond additive enrichment. It shows that a monoidal bialgebra modality equipped with a codereliction induces additive enrichment via convolution, even when the base category is not additively enriched, and provides a new equivalent axiomatization of differential linear categories as symmetric monoidal categories with a monoidal bialgebra modality and codereliction. The paper then proves the uniqueness of pre-coderelictions and coderelictions, connects to additive and Hopf structures to handle negatives, and establishes equivalences between monoidal coalgebra modalities and additive/monoidal bialgebra modalities in the additive setting. Overall, it clarifies the foundational role of additive enrichment in differentiation, unifies several modality notions, and extends the framework to Hopf (negative) contexts, yielding a comprehensive axiomatization of differential linear categories. The results have implications for modeling Differential Linear Logic and its exponential fragment within a canonical categorical structure.
Abstract
Differential linear categories provide the categorical semantics of the multiplicative and exponential fragments of Differential Linear Logic. Briefly, a differential linear category is a symmetric monoidal category that is enriched over commutative monoids (called additive enrichment) and has a monoidal coalgebra modality that is equipped with a codereliction. The codereliction is what captures the ability of differentiating non-linear proofs via linearization in Differential Linear Logic. The additive enrichment plays an important role since it allows one to express the famous Leibniz rule. However, the axioms of a codereliction can be expressed without any sums or zeros. Therefore, it is natural to ask if one can consider a possible non-additive enriched version of differential linear categories. In this paper, we show that even if a codereliction can be technically defined in an non-additive setting, it nevertheless induces an additive enrichment via bialgebra convolution. Thus we obtain a novel characterization of a differential linear category as a symmetric monoidal category with a monoidal bialgebra modality equipped with a codereliction. Moreover, we also show that coderelictions are, in fact, unique. We also introduce monoidal Hopf coalgebra modalities and discuss how antipodes relate to enrichment over Abelian groups.