Additive Enrichment from Coderelictions

TL;DR

This paper explores the structure of differential linear categories, showing that even in non-additive settings, a codereliction induces additive enrichment, leading to a new characterization involving bialgebra modalities.

Contribution

It introduces a novel characterization of differential linear categories using monoidal bialgebra modalities with coderelictions, and proves the uniqueness of coderelictions.

Findings

Coderelictions induce additive enrichment via bialgebra convolution.

Differential linear categories can be characterized by monoidal bialgebra modalities with coderelictions.

Coderelictions are shown to be unique.

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 technically be defined in a 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.