Coherent differentiation

Abstract

The categorical models of differential linear logic (LL) are additive categories and those of the differential lambda-calculus are left-additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential LL are concerned, these models feature finite nondeterminism and indeed these languages are essentially non-deterministic. We introduce a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces.

1. Introduction

The differential $\lambda$ -calculus has been introduced in Ehrhard and Regnier (2003), starting from earlier investigations on the semantics of linear logic ( ${\textsf{LL}}$ ) in models based on various kinds of topological vector spaces; see Ehrhard (2002, 2005). Later on, we proposed in Ehrhard and Regnier (2004), and Ehrhard (2018) an extension of ${\textsf{LL}}$ featuring differential operations which appear as an additional structure of the exponentials (the resource modalities of ${\textsf{LL}}$ ), offering a perfect duality to the standard rules of dereliction, weakening, and contraction. The differential $\lambda$ -calculus and differential ${\textsf{LL}}$ are about computing formal derivatives of programs and from this point of view are deeply connected to the kind of formal differentiation of programs used in machine learning for propagating gradients (i.e., differentials viewed as vectors of partial derivatives) within formal neural networks. As shown by the recent Brunel et al. (2020) and Mazza and Pagani (2021), formal transformations of programs related to the differential $\lambda$ -calculus can be used for efficiently implementing gradient back-propagation in a purely functional framework. The differential $\lambda$ -calculus and the differential ${\textsf{LL}}$ are also useful as the foundation for an approach to finite approximations of programs based on the Taylor expansion – see Ehrhard and Regnier (2008) and Barbarossa and Manzonetto (2020) – which provides a precise analysis of the use of resources during the execution of a functional program deeply related with implementations of the $\lambda$ -calculus in abstract machines such as the Krivine Machine, as explained in Ehrhard and Regnier (2006).

One should insist on the fact that in the differential $\lambda$ -calculus, derivatives are not taken with respect to a ground type of real numbers as in Brunel et al. (2020) and Mazza and Pagani (2021) but can be computed with respect to elements of all types. For instance, it makes sense to compute the derivative of a function $M:{({\iota}\Rightarrow{\iota})}\to\iota$ with respect to its argument which is a function from $\iota$ , the type of integers, to itself, thus suggesting the possibility of using this formalism for optimization purposes in a model such as the probabilistic coherence spaces (PCSs) of Danos and Ehrhard (2011) where a program of type $\iota\to\iota$ is seen as an analytic function transforming probability distributions on the integers. In Ehrhard (2019), it is also shown how such derivatives can be used to compute the expectation of the number of steps in the execution of a program. A major obstacle on the extension of programming languages with such derivatives is the fact that PCSs are not a model of the differential $\lambda$ -calculus in spite of the fact that the morphisms, being analytic, are obviously differentiable. The main goal of this paper is to circumvent this obstacle, and let us first understand it better.

These differential extensions of the $\lambda$ -calculus and of ${\textsf{LL}}$ require the possibility of adding terms of the same type. For instance, to define the operational semantics of the differential $\lambda$ -calculus, given a term t such that ${x:A}\vdash{t}:{B}$ and a term u such that ${\Gamma}\vdash{ }:{u}A$ one has to define a term $\frac{\partial{t}}{\partial{x}}\cdot{u}$ such that ${\Gamma,x:A}\vdash{\frac{\partial{t}}{\partial{x}}\cdot{u}}:{B}$ which can be understood as a linear substitution of u for x in t and is actually a formal differentiation: x has no reason to occur linearly in t, so this operation involves the creation of linear occurrences of x in t, and this is done applying the rules of ordinary differential calculus. The most important case is when t is an application $t=\left({t_1}\right){t_2}$ where ${\Gamma,x:A}\vdash{t_1}:{{C}\Rightarrow{B}}$ and ${\Gamma,x:A}\vdash{t_2}:{C}$ . In that case, we set

\begin{align*} \frac{\partial{\left({t_1}\right){t_2}}}{\partial{x}}\cdot{u} =\left({\frac{\partial{t_1}}{\partial{x}}\cdot{u}}\right){t_2} +\left({\mathrm D_{}{t_1}\cdot{\left(\frac{\partial{t_2}}{\partial{x}}\cdot{u}\right)}}\right){t_2}\end{align*}

where we use differential application which is a syntactic construct of the language: given ${\Gamma}\vdash{ }:{s}{{C}\Rightarrow{B}}$ and ${\Gamma}\vdash{ }:{v}C$ , we have ${\Gamma}\vdash{\mathrm D_{}{s}\cdot{v}}:{{C}\Rightarrow{B}}$ . This crucial definition involves a sum corresponding to the fact that x can appear free in $t_1$ and in $t_2$ : this is the essence of the “Leibniz rule” $(fg)'=f'g+fg'$ which has nothing to do with multiplication but everything with the fact that both f and g can have nonzero derivatives with respect to a common variable they share (logically this sharing is implemented by a contraction rule).

For this reason, the syntax of the differential $\lambda$ -calculi and ${\textsf{LL}}$ features an addition operation on terms of the same type, and accordingly the categorical models of these formalisms are based on additive categories. Operationally, such sums correspond to a form of finite nondeterminism: for instance, if the language has a ground type of integers $\iota$ with constants $\underline{n}$ such that ${\Gamma}\vdash{\underline{n}}:{\iota}$ for each $n\in{\mathbb{N}}$ , we are allowed to consider sums such as $\underline{42}+\underline{57}$ corresponding to the nondeterministic superposition of the two integers (and not at all to their sum $\underline{99}$ in the usual sense!). This can be considered as a weakness of this approach since, even if one has nothing against nondeterminism per se, it is not satisfactory to be obliged to enforce it for allowing differential operations which have nothing to do with it a priori. So the fundamental question is:

Does every logical approach to differentiation require nondeterminism?

We ground our negative answer to this question on the observation made in Ehrhard (2019) that, in the category of PCS, morphisms of the associated cartesian closed category are analytic functions and therefore admit all iterated derivatives (at least in the “interior” of the domain where they are defined). Consider for instance in this category an analytic $f:1\to1$ where 1 (the $\otimes$ unit of ${\textsf{LL}}$ ) is the [0,1] interval, meaning that $f(x)=\sum_{n=0}^\infty a_nx^n$ with coefficient $a_n\in\mathbb{R}_{\geq 0}$ such that $\sum_{n=0}^\infty a_n\leq 1$ . The derivative $f'(x)=\sum_{n=0}^\infty (n+1)a_{n+1}x^n$ has no reason to map [0,1] to [0,1] and can even be unbounded on [0,1) and undefined at $x=1$ (and there are programs whose interpretation behaves in that way). Though, if $(x,u)\in[0,1]^2$ satisfy $x+u\in[0,1]$ , then $f(x)+f'(x)u\leq f(x+u)\in[0,1]$ . This is true actually of any analytic morphism f between two PCSs X and Y: we can see the differential of f as mapping a summable pair (x,u) of elements of X to the summable pair $(f(x),f'(x)\cdot u)$ of elements of Y. Seeing the differential as such a pair of functions is central in differential geometry as it allows one, thanks to the chain rule, to turn it into a functor mapping a smooth map $f:X\to Y$ (where X and Y are now manifolds) to the function $\mathsf Tf:\mathsf TX\to\mathsf TY$ which maps (x,u) to $(f(x),f'(x)\cdot u)$ where $\mathsf TX$ is the tangent bundle of X, a manifold whose elements are the pairs (x,u) of a point x of X and of a vector u tangent to X at x. The concept of tangent category has been introduced in Rosický (1984), see also Cockett and Cruttwell (2014), precisely to describe categorically this construction and its properties.

Content. We base our approach on a concept of summable pair that we axiomatize as a general categorical notion in Section 3: a summable category is a category $\mathcal{L}$ with 0-morphisms ¹ together with a functor $\mathsf S:\mathcal{L}\to\mathcal{L}$ equipped with three natural transformations from $\mathsf S X$ to X: two projections and a sum operation. The first projection also exists in the “tangent bundle” functor of a tangent category, but the two other morphisms do not. Such a summability structure induces a monad structure on $\mathsf S$ (a similar phenomenon occurs in tangent categories). In Section 4, we consider the case where the category is a cartesian SMC (symmetric monoidal category) equipped with a resource comonad $\ !{\_}$ in the sense of ${\textsf{LL}}$ . In this setting, we present differentiation as a distributive law between the monad $\mathsf S$ and the comonad $!{\_}$ . This allows us to extend $\mathsf S$ to a strong monad $\widetilde{\mathsf D}$ on the Kleisli category ${\mathcal {L}}_!$ which implements differentiation of nonlinear maps. We choose the notation $\widetilde{\mathsf D}$ and not simply $\mathsf D$ to avoid a clash of notation with cartesian differential categories where $\mathsf D$ is used for a different, though related, operator. See Cockett and Cruttwell (2014), Section 4.

This functor $\widetilde{\mathsf D}$ acting on ${\mathcal L}_!$ is formally similar to the functor $\mathsf T$ of a tangent category, but it is important to notice that these two notions cannot be compared in terms of generality:

first because, in a tangent bundle, when $(x,u)\in\mathsf TX$ , it makes no sense to add x and u or to consider u alone (independently of x), and hence our summability-based framework is not more general than tangent categories.

And second because, given $(x,u_0),(x,u_1)\in\mathsf TX$ , the local sum $(x,u_0+u_1)\in\mathsf TX$ is always defined in a tangent bundle, whereas in our summability setting, when $(x,u_0),(x,u_1)\in\widetilde{\mathsf D} X$ , $u_0$ and $u_1$ are elements of X which are not necessarily summable. ² So tangent categories are not more general than our summability structures.

In Section 5, we study the case where the functor $\mathsf S$ can be defined using a more basic structure of $\mathcal{L}$ based on the object ${1}\mathrel{\&}{1}$ where $\mathrel{\&}$ is the cartesian product and 1 is the unit of $\otimes$ : this is actually what happens in the concrete situations we have in mind. Then, the existence of the summability structure becomes a property of $\mathcal{L}$ and not an additional structure. We also study the differential structure in this setting, showing that it boils down to a simple $\ !$ -coalgebra structure on ${1}\mathrel{\&}{1}$ satisfying a few simple equations which automatically hold when the exponential is free; this is the case in many standard models of ${\textsf{LL}}$ .

As a running example along the presentation of our categorical constructions, we use the category of coherence spaces, the first model of ${\textsf{LL}}$ historically, introduced in Girard (1987). There are three main reasons for this choice.

• It is one of the most popular models of ${\textsf{LL}}$ and of functional languages.

• It is a typical example of a model of ${\textsf{LL}}$ which is not an additive category, in contrast with the relational model or the models based on profunctors.

• It does not a priori exhibit the usual features of a model of the differential calculus (no coefficients, no vector spaces, etc), and it strongly suggests that our coherent approach to the differential $\lambda$ -calculus might be applied to programming languages which have nothing to do with probabilities, deep learning, or nondeterminism.

In Section 6, we describe the differential structure of the coherence space model, showing that it provides an example of an elementarily summable differential category. We observe that, in the uniform setting of Girard’s coherence space, our differentiation does not satisfy the Taylor formula, but that this formula will hold if we use instead nonuniform coherence spaces of which we describe the differential structure.

In Section 7, we consider the situation where the underlying SMC is closed, that is, it has internal hom objects. In that case, an additional condition on the summability structure is required, expressing intuitively that two morphisms are summable iff they are summable pointwise.

Related works. As already mentioned our approach has strong similarities with tangent categories which have been a major source of inspiration, we explained above the differences. There are also strong connections with differential categories; see Blute et al. (2020). The main difference again is that differential categories are left-additive which is generally not the case of ${\mathcal L}_!$ in our case, we explained why. There are also interesting similarities with Cockett et al. (2020) (still in an additive setting): our distributive law $\partial_X$ might play a role similar to the one of the distributive law introduced in the Section 5 of that paper. This needs further investigations.

The summable categories introduced here have strong similarities with the partially additive categories introduced in Arbib and Manes (1980); see Remark 26 for a discussion about the connections between these two notions: although conveying very close intuitions, summable categories seem more general than partially additive categories.

In Kerjean and Pédrot (2020), a striking connection between Gödel’s Dialectica interpretation and the differential $\lambda$ -calculus and differential ${\textsf{LL}}$ has been exhibited, with applications to gradient back-propagation in differential programming. One distinctive feature of Pédrot’s approach to Dialectica in Pédrot (2015) is to use a “multiset parameterized type” $\mathfrak M$ whose purpose is apparently to provide some control on the summations allowed when performing Pédrot’s analog of the Leibniz rule (under the Dialectica/differential correspondence of Kerjean and Pédrot 2020) and might therefore play a role similar to our summability functor $\mathsf S$ . The precise technical connection is not clear at all, but we believe that this analogy will lead to a unified framework for Dialectica interpretation and coherent differentiation of programs and proofs involving denotational semantics, proof theory, and differential programming.

Change of terminology and notation. Following suggestions by the reviewers of this article, some important terminology and notation have been changed with respect to earlier versions of this work available online.

• We use now the expression elementary summable category instead of canonical summable category as the adjective “canonical” is somehow too generic and could also be misleading in a differential setting because of its use in differential geometry. This choice is motivated by the fact that in the setting of Section 5, the summability and differential structures boil down to very elementary properties of one specific object in the considered category, namely ${1}\mathrel{\&}{1}$ .

• We use now the notation $\mathbb D$ instead of $\mathsf I$ for the object ${1}\mathrel{\&}{1}$ in the elementary summable setting because the notation $\mathsf I$ is already way too overloaded, especially in homotopy theory for denoting the interval object, ³ and also in category theory for denoting the unit of the monoidal product in a monoidal category (our object 1). Moreover, the letter $\mathbb D$ suggests that this object has a kind of differential structure and that it is can be understood as an object of dual numbers; see for instance Section 1.1.3 of Rosenfeld (2013) (two reasons for using this letter) a bit like in synthetic differential geometry (SDG) and see Kock (2010). There is a little discrepancy here: our object $\mathbb D$ seems closer to the line object R than to the object of infinitesimals D of SDG which consists of the $x\in R$ such that $x^2=0$ , but using a notation like $\mathsf R$ or $\mathbb R$ for ${1}\mathrel{\&}{1}$ would have been even more misleading, suggesting an analogy with the real line. See also Remark 42.

2. Preliminary Notions and Results

This section provides some more or less standard technical material useful to understand the paper. It can be skipped and used in a call-by-need manner.

2.1 Finite multisets

A finite multiset on a set A is a function $m:A\to{\mathbb{N}}$ such that the set $\operatorname{\mathsf{supp}}({m})=\{a\in A\mid m(a)\not=0\}$ is finite, and we use $\mathcal M_{{\mathrm{fin}}}({A})$ for the set of all finite multisets of elements of A. The cardinality of m is $\#{m}=\sum_{a\in A}m(a)$ . We use $[\,]$ for the empty multiset (so that $\operatorname{\mathsf{supp}}({[\,]})=\emptyset$ where $\operatorname{\mathsf{supp}}({m})=\{a\in A\mid m(a)\not=0\}$ is the support of m) and if $m_0,m_1\in\mathcal M_{{\mathrm{fin}}}({A})$ then $m_0+m_1\in\mathcal M_{{\mathrm{fin}}}({A})$ is defined by $(m_0+m_1)(a)=m_0(a)+m_1(a)$ . If $a_{1},\dots,a_{n}\in A$ , we use $[{a_{1},\dots,a_{n}}]$ for the $m\in\mathcal M_{{\mathrm{fin}}}({A})$ such that m(a) is the number of $i\in\{1,\dots,n\}$ such that $a_i=a$ . If $m=[{a_{1},\dots,a_{n}}]\in\mathcal M_{{\mathrm{fin}}}({A})$ and $p=[{b_{1},\dots,b_{p}}]\in\mathcal M_{{\mathrm{fin}}}({B})$ , then $m\times p=[{(a_i,b_j)\mid i\in\{1,\dots ,n\}\text{ and }j\in\{1,\dots,p\}}]\in\mathcal M_{{\mathrm{fin}}}({A\times B})$ . If $M=[{m_{0},\dots,m_{n}}]\in\mathcal M_{{\mathrm{fin}}}({\mathcal M_{{\mathrm{fin}}}({A})})$ we set $\Sigma{M}=\sum_{i=0}^nm_i\in\mathcal M_{{\mathrm{fin}}}({A})$ .

2.2 The SMCC of pointed sets

Let $\mathbf{Set}_0$ be the category of pointed sets. We use $0_X$ or simply 0 for the distinguished point of the object X. A morphism $f\in\mathbf{Set}_0(X,Y)$ is a function $f:X\to Y$ such that $f(0_X)=0_Y$ . The terminal object is the singleton $\{0\}$ . The cartesian product ${X}\mathrel{\&}{Y}$ is the ordinary cartesian product, with $0_{{X}\mathrel{\&}{Y}}=(0_X,0_Y)$ . The tensor product ${X}\otimes{Y}$ is defined as:

\begin{align*} {X}\otimes{Y}=\{(x,y)\in X\times Y\mid x=0\Leftrightarrow y=0\}\end{align*}

with $0_{{X}\otimes{Y}}=(0_X,0_Y)$ . The unit of the tensor product is the object $1=\{0,\ast\}$ of $\mathbf{Set}_0$ . This category is enriched over itself, the distinguished point of $\mathbf{Set}_0(X,Y)$ being the constantly $0_Y$ function. Actually, it is monoidal closed with ${X}\multimap{Y}=\mathbf{Set}_0(X,Y)$ and $0_{{X}\multimap{Y}}$ defined by $0_{{X}\multimap{Y}}(x)=0_Y$ for all $x\in X$ . A mono in $\mathbf{Set}_0$ is a morphism of $\mathbf{Set}_0$ which is injective as a function.

Unless explicitly stipulated, all the categories $\mathcal{L}$ we consider in this paper are enriched over pointed sets, so this assumption will not be mentioned any more. In the case of symmetric monoidal categories, this also means that the tensor product of morphisms is “bilinear” with respect to the pointed structure, that is, if $f\in\mathcal{L}(X_0,Y_0)$ then ${f}\otimes{0}=0\in\mathcal{L}({X_0}\otimes{X_1},{Y_0}\otimes{Y_1})$ and by symmetry we have ${0}\otimes{f}=0$ .

2.3 Monoidal and resource categories

Following a well-established tradition, if X is an object of a category $\mathcal{L}$ we use X to denote the identity morphism at X in $\mathcal{L}$ .

A symmetric monoidal category (SMC) is a category $\mathcal{L}$ equipped with a bifunctor $\mathcal{L}^2\to\mathcal{L}$ denoted as $\otimes$ , a monoidal unit 1 which is an object of $\mathcal{L}$ and $\lambda_X\in\mathcal{L}({1}\otimes{ }X,X)$ , $\rho_X\in\mathcal{L}({X}\otimes{1},X)$ , $\alpha_{X_0,X_1,X_2}\in\mathcal{L}({({X_0}\otimes{X_1})}\otimes{X_2},{X_0}\otimes{({X_1}\otimes{X_2})})$ and $\gamma_{X_0,X_1}\in\mathcal{L}({X_0}\otimes{X_1},{X_1}\otimes{X_0})$ as associated isomorphisms satisfying the usual McLane coherence commutations. Given objects $X_{0},\dots,X_{n-1}$ and $i<j$ in $\{0,\dots,n-1\}$ , we use $\gamma_{i,j}$ for the canonical swapping iso in $\mathcal{L}(X_0\otimes\cdots\otimes X_{n-1},X_0\otimes\cdots\otimes X_{i-1}\otimes X_j\otimes X_{i+1}\cdots \otimes X_{j-1}\otimes X_i\otimes X_{j+1}\otimes\cdots\otimes X_{n-1})$ .

2.3.1 Commutative comonoids

Definition 1. In a SMC $\mathcal{L}$ (with the usual notations), a commutative comonoid is a tuple $C=(\underline{C},\mathsf w_{C},\mathsf c_{C})$ where $\underline{C}\in\mathcal{L}$ , $\mathsf w_{C}\in\mathcal{L}(\underline{C},1)$ and $\mathsf c_{C}\in\mathcal{L}(\underline{C},{\underline{C}}\otimes{\underline{C}})$ are such that the following diagrams commute.

The category ${\mathcal {L}}^{\otimes}$ of commutative comonoids has these tuples as objects, and an element of ${\mathcal {L}}^{\otimes}(C,D)$ is an $f\in\mathcal{L}(\underline{C},\underline{D})$ such that the two following diagrams commute

Theorem 1. For any SMC $\mathcal{L}$ the category ${\mathcal {L}}^{\otimes}$ is cartesian. The terminal object is $(1,\operatorname{\mathsf{Id}}_1,({\lambda_1})^{-1})$ (remember that $\lambda_1=\rho_1$ ) simply denoted as 1 and for any object C the unique morphism $C\to1$ is $\mathsf w_{C}$ . The cartesian product of $C_0,C_1\in{\mathcal {L}}^{\otimes}$ is the object ${C_0}\otimes{C_1}$ of ${\mathcal {L}}^{\otimes}$ such that $\underline{{C_0}\otimes{C_1}}={\underline{C_0}}\otimes{\underline{C_1}}$ and the structure maps are defined as:

The projections $\mathsf{pr}_{i}^\otimes\in{\mathcal {L}}^{\otimes}({C_0}\otimes{C_1},C_i)$ are given by:

The proof is straightforward. In a commutative monoid M, multiplication is a monoid morphism $M\times M\to M$ . The following is in the vein of this simple observation.

Lemma 2. If $C\in{\mathcal {L}}^{\otimes}$ , then $\mathsf w_{C}\in{\mathcal {L}}^{\otimes}(C,1)$ and $\mathsf c_{C}\in{\mathcal {L}}^{\otimes}(C,{C}\otimes{C})$ .

Proof. The second statement amounts to the following commutation

which results from the commutativity of C. The first statement is similarly trivial.

2.3.2 Resource categories

The notion of resource category is more general than that of a Seely category in the sense of Melliès (2009). We keep only the part of the structure and axioms that we need to define our notion of differential structure and keep our setting as general as possible.

An object X of an SMC $\mathcal{L}$ is exponentiable if the functor ${\_}\otimes{ }X$ has a right adjoint, denoted as ${X}\multimap{\_}$ . In that case, we use $\operatorname{\mathsf{ev}}\in\mathcal{L}({\left({X}\multimap{Y}\right)}\otimes{X},Y)$ for the counit of the adjunction and, given $f\in\mathcal{L}({Z}\otimes{X},Y)$ we use $\operatorname{\mathsf{cur}} f$ for the associated morphism $\operatorname{\mathsf{cur}} f\in\mathcal{L}(Z,{X}\multimap{Y})$ .

We say that the SMC $\mathcal{L}$ is closed (is an SMCC) if any object of $\mathcal{L}$ is exponentiable.

A category $\mathcal{L}$ is a resource category if

• $\mathcal{L}$ is an SMC;

• $\mathcal{L}$ is cartesian with terminal object $\top$ (so that 0 is the unique element of $\mathcal{L}(X,\top)$ ) and cartesian product of $X_0$ , $X_1$ denoted $({X_0}\mathrel{\&}{X_1},\mathsf{pr}_{0},\mathsf{pr}_{1})$ and pairing of morphisms $(f_i\in\mathcal{L}(Y,X_i))_{i=0,1}$ denoted $\langle{f_0,f_1}\rangle\in\mathcal{L}(Y,{X_0}\mathrel{\&}{X_1})$ ;

• and $\mathcal{L}$ is equipped with a resource comonad, that is a tuple $(\ !{\_},\operatorname{\mathsf{der}}_{},\operatorname{\mathsf{dig}}_{},\mathsf m^0,\mathsf m^2)$ where $\ !{\_}$ is a functor $\mathcal{L}\to\mathcal{L}$ which is a comonad with counit $\operatorname{\mathsf{der}}_{}$ (dereliction) and comultiplication $\operatorname{\mathsf{dig}}_{}$ (digging), and $\mathsf m^0\in\mathcal{L}(1,\ !{\top})$ and $\mathsf m^2\in\mathcal{L}({\ !{X}}\otimes{\ !{Y}},\ !{({X}\mathrel{\&}{Y})})$ are the Seely isomorphisms subject to conditions that we do not recall here; see for instance Melliès (2009) apart for the following which explains how $\operatorname{\mathsf{dig}}_{}$ interacts with $\mathsf m^2$ .

(1)

Then $\ !{\_}$ inherits a lax symmetric monoidality $\mu^0,\mu^2$ on $\mathcal{L}$ (considered as an SMC). This means that one can define $\mu^0\in\mathcal{L}(1,\ !{1})$ and $\mu^2_{X_0,X_1}\in\mathcal{L}({\ !{X_0}}\otimes{\ !{X_1}},\ !{({X_0}\otimes{X_1})})$ satisfying suitable coherence commutations. Explicitly these morphisms are given by:

Lemma 3. The following diagram commutes:

Proof. This results from the definition of $\mu^2$ and from the following commutation

which results from the observation that $\ !{0}\in\mathcal{L}(\ !\ !{X},\ !{0})$ can be written $\ !{0}=\ !({0\,\operatorname{\mathsf{der}}_{X}})$ .

For any $X\in\mathcal{L}$ , it is possible to define a contraction morphism $\operatorname{\mathsf{contr}}_{X}\in\mathcal{L}(\ !{X},{\ !{X}}\otimes{\ !{X}})$ and a weakening morphism $\operatorname{\mathsf{weak}}_{X}\in\mathcal{L}(\ !{X},1)$ turning $\ !{X}$ into a commutative comonoid. These morphisms are defined as follows:

Lemma 4. The two following diagrams commute in any resource category $\mathcal{L}$ .

Proof. For the first diagram, we have

and

For the second diagram, we compute

\begin{align*} f_1 &=\ !{\langle{{\mathsf{pr}_{0}}\otimes{Y},{\mathsf{pr}_{1}}\otimes{Y}}\rangle} \,\mu^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &=\ !{\langle{{\mathsf{pr}_{0}}\otimes{Y},{\mathsf{pr}_{1}}\otimes{Y}}\rangle} \,\ !{({\operatorname{\mathsf{der}}_{{X_0}\mathrel{\&}{X_1}}}\otimes{\operatorname{\mathsf{der}}_{Y}})} \,\ !{({\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}})^{-1}} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &\hspace{10em}\text{by definition of }\mu^2\\ &=\ !({{({\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}})}\mathrel{\&}{({\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}})}}) \,\ !{\langle{{\ !{\mathsf{pr}_{0}}}\otimes{\ !{Y}}, {\ !{\mathsf{pr}_{1}}}\otimes{\ !{Y}}}\rangle}\\ &\hspace{10em}\,\ !{({\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}})^{-1}} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \text{ by naturality of }\operatorname{\mathsf{der}}_{}\\ &=\ !({{({\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}})}\mathrel{\&}{({\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}})}}) \, f_2 \end{align*}

where

\begin{align*} f_2 &=\ !{\langle{{\ !{\mathsf{pr}_{0}}}\otimes{\ !{Y}}, {\ !{\mathsf{pr}_{1}}}\otimes{\ !{Y}}}\rangle} \,\ !{({\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}})^{-1}} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &=\ !({{({\mathsf m^2_{X_0,Y}})^{-1}}\mathrel{\&}{({\mathsf m^2_{X_1,Y}})^{-1}}}) \,\ !{\langle{\ !{\mathsf{pr}_{0}},\ !{\mathsf{pr}_{1}}}\rangle} \,\ !\ !{q} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \end{align*}

by naturality of $\mathsf m^2$ . In that expression, $\mathsf{pr}_{i}\in\mathcal{L}(X_0\mathrel{\&} Y\mathrel{\&} X_1\mathrel{\&} Y,{X_i}\mathrel{\&}{Y})$ and $q=\langle{\mathsf{pr}_{0},\mathsf{pr}_{2},\mathsf{pr}_{1},\mathsf{pr}_{2}}\rangle \in\mathcal{L}(X_0\mathrel{\&} X_1\mathrel{\&} Y,X_0\mathrel{\&} Y\mathrel{\&} X_1\mathrel{\&} Y)$ . We have used the commutation of the following diagram

which is easily proved by post-composing the two equated morphisms with $\mathsf{pr}_{i}\in\mathcal{L}({({\ !{X_0}}\otimes{\ !{Y}})}\mathrel{\&}{({\ !{X_1}}\otimes{\ !{Y}})},({\ !{X_i}}\otimes{\ !{Y}}))$ for $i=0,1$ .

Observe that

\begin{align*} &\ !({{({\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}})}\mathrel{\&}{({\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}})}})\\ &\hspace{8em}=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,{({\ !({{\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}\otimes{}) {\ !({{\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}} \, ({\mathsf m^2_{{\ !{X_0}}\otimes{\ !{Y}},{\ !{X_1}}\otimes{\ !{Y}}}})^{-1} \end{align*}

by naturality of $\mathsf m^2$ . For the same reason, the following diagram commutes:

and hence

\begin{align*} f_1 &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,{({\ !({{\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}\otimes{}) {\ !({{\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}} \, ({\mathsf m^2_{{\ !{X_0}}\otimes{\ !{Y}},{\ !{X_1}}\otimes{\ !{Y}}}})^{-1}\\ &\hspace{8em} \,\ !({{({\mathsf m^2_{X_0,Y}})^{-1}}\mathrel{\&}{({\mathsf m^2_{X_1,Y}})^{-1}}}) \,\ !{\langle{\ !{\mathsf{pr}_{0}},\ !{\mathsf{pr}_{1}}}\rangle} \,\ !\ !{q} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \\ &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,{({\ !({{\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}\otimes{}) {\ !({{\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}} \,({\ !{({\mathsf m^2_{X_0,Y}})^{-1}}}\otimes{\ !{({\mathsf m^2_{X_1,Y}})^{-1}}})\\ &\hspace{8em} \,({\mathsf m^2_{\ !{\left({X_0}\mathrel{\&}{Y}\right)},\ !{\left({X_1}\mathrel{\&}{Y}\right)}}})^{-1} \,\ !{\langle{\ !{\mathsf{pr}_{0}},\ !{\mathsf{pr}_{1}}}\rangle} \, f_3 \end{align*}

where, by naturality of $\operatorname{\mathsf{dig}}_{}$ ,

\begin{align*} f_3 &=\ !\ !{q} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} X_1\mathrel{\&} Y} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &=\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} Y\mathrel{\&} X_1\mathrel{\&} Y} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \in\mathcal{L}({\ !{\left({X_0}\mathrel{\&}{X_1}\right)}}\otimes{\ !{Y}}, \ !\ !{(X_0\mathrel{\&} Y\mathrel{\&} X_1\mathrel{\&} Y)}) \end{align*}

and hence, by the diagram (1)

\begin{align*} \ !{\langle{\ !{\mathsf{pr}_{0}},\ !{\mathsf{pr}_{1}}}\rangle}\, f_3 &=\ !{\langle{\ !{\mathsf{pr}_{0}},\ !{\mathsf{pr}_{1}}}\rangle} \,\operatorname{\mathsf{dig}}_{X_0\mathrel{\&} Y\mathrel{\&} X_1\mathrel{\&} Y} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &={\mathsf m^2_{\ !({{X_0}\mathrel{\&}{Y}}),\ !({{X_1}\mathrel{\&}{Y}})}} \,({\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{Y}}}\otimes{\operatorname{\mathsf{dig}}_{{X_1}\mathrel{\&}{Y}}}) \,({\mathsf m^2_{{X_0}\mathrel{\&}{Y},{X_1}\mathrel{\&}{Y}}})^{-1} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\,. \end{align*}

It follows that

\begin{align*} f_1 &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,{({\ !({{\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}\otimes{}) {\ !({{\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}} \,({\ !{({\mathsf m^2_{X_0,Y}})^{-1}}}\otimes{}) {\ !{({\mathsf m^2_{X_1,Y}})^{-1}}}\\ &\hspace{4em} ({\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{Y}}}\otimes{\operatorname{\mathsf{dig}}_{{X_1}\mathrel{\&}{Y}}}) \,({\mathsf m^2_{{X_0}\mathrel{\&}{Y},{X_1}\mathrel{\&}{Y}}})^{-1} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,{({\ !({{\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}\otimes{}) {\ !({{\operatorname{\mathsf{der}}_{X_1}}\otimes{\operatorname{\mathsf{der}}_{Y}}})}} \,({\ !{({\mathsf m^2_{X_0,Y}})^{-1}}}\otimes{}) {\ !{({\mathsf m^2_{X_1,Y}})^{-1}}}\\ &\hspace{4em} ({\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{Y}}}\otimes{\operatorname{\mathsf{dig}}_{{X_1}\mathrel{\&}{Y}}}) \,({\mathsf m^2_{X_0,Y}}\otimes{\mathsf m^2_{X_1,Y}})\\ &\hspace{4em} ({({\mathsf m^2_{X_0,Y}})^{-1}}\otimes{({\mathsf m^2_{X_1,Y}})^{-1}}) \,({\mathsf m^2_{{X_0}\mathrel{\&}{Y},{X_1}\mathrel{\&}{Y}}})^{-1} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y}\\ &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,({\mu^2_{X_0,Y}}\otimes{\mu^2_{X_1,Y}}) \,({({\mathsf m^2_{X_0,Y}})^{-1}}\otimes{({\mathsf m^2_{X_1,Y}})^{-1}}) \,({\mathsf m^2_{{X_0}\mathrel{\&}{Y},{X_1}\mathrel{\&}{Y}}})^{-1} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \end{align*}

hence,

\begin{align*} f_1\,({\mathsf m^2_{X_0,X_1}}\otimes{\ !{Y}}) &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,({\mu^2_{X_0,Y}}\otimes{\mu^2_{X_1,Y}}) \,({({\mathsf m^2_{X_0,Y}})^{-1}}\otimes{({\mathsf m^2_{X_1,Y}})^{-1}}) \,({\mathsf m^2_{{X_0}\mathrel{\&}{Y},{X_1}\mathrel{\&}{Y}}})^{-1}\\ &\hspace{4em} \,\ !{q} \,\mathsf m^2_{{X_0}\mathrel{\&}{X_1},Y} \,({\mathsf m^2_{X_0,X_1}}\otimes{\ !{Y}})\\ &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,({\mu^2_{X_0,Y}}\otimes{\mu^2_{X_1,Y}}) \,({\mathsf m^4_{X_0,Y,X_1,Y}})^{-1} \,\ !{q} \,\mathsf m^3_{X_0,X_1,Y}\\ &=\mathsf m^2_{{X_0}\otimes{Y},{X_1}\otimes{Y}} \,({\mu^2_{X_0,Y}}\otimes{\mu^2_{X_1,Y}}) \,\gamma_{2,3} \,(\ !{X_0}\otimes\ !{X_1}\otimes\operatorname{\mathsf{contr}}_{Y}\ !) \end{align*}

by the monoidality properties of the Seely isomorphisms, where we have used $\mathsf m^k$ for their k-ary version.

2.3.3 Coalgebras of the resource comonad

A $\ !$ -coalgebra is a pair $P=(\underline{P},h_{P})$ where $\underline{P}$ is an object of $\mathcal{L}$ and $h_{P}\in\mathcal{L}(\underline{P},\ !{\underline{P}})$ satisfies

Given coalgebras P and Q, a coalgebra morphism from P to Q is an $f\in\mathcal{L}(\underline{P},\underline{Q})$ such that the following square commutes

The category so defined is the Eilenberg–Moore category ${\mathcal {L}}^!$ associated with the comonad $\ !{\_}$ . We will use the following standard result for which we refer to Melliès (2009).

Theorem 2. The Eilenberg–Moore category ${\mathcal{L}}^!$ of a resource category $\mathcal{L}$ is cartesian with final object $(1,\mu^0)$ simply denoted as 1 and cartesian product of $P_0,P_1$ the coalgebra $({\underline{P_0}}\otimes{\underline{P_1}},\mu^2_{\underline{P_0},\underline{P_1}} \,({h_{P_0}}\otimes{h_{P_1}}))$ denoted as ${P_0}\otimes{P_1}$ with projection $\mathsf{pr}_{0}^\otimes\in{\mathcal{L}}^!({P_0}\otimes{P_1},P_0)$ defined as the following composition of morphisms

and similarly for $\mathsf{pr}_{1}^\otimes\in{\mathcal{L}}^!({P_0}\otimes{P_1},P_1)$ . And given $f_i\in{\mathcal{L}}^!(Q,P_i)$ for $i=0,1$ , the unique morphism $\langle{f_0,f_1}\rangle^\otimes\in{\mathcal{L}}^!(Q,{P_0}\otimes{P_1})$ such that $\mathsf{pr}_{i}^\otimes\,\langle{f_0,f_1}\rangle^\otimes=f_i$ is defined as the following composition of morphisms

Last, the unique morphism $P\to1$ in ${\mathcal{L}}^!$ is

An immediate consequence of this theorem is the following observation.

Proposition 5. Let P be an object of ${\mathcal{L}}^!$ , $u\in{\mathcal{L}}^!(P,1)$ and $d\in{\mathcal{L}}^!(P,{P}\otimes{P})$ be such that

commute. Then, $u=\operatorname{\mathsf{weak}}_{P}\,h_{P}$ and $d=\langle{\underline{P},\underline{P}}\rangle^\otimes =({\operatorname{\mathsf{der}}_{\underline{P}}}\otimes{\operatorname{\mathsf{der}}_{\underline{P}}}) \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}$ and the following diagram commutes in $\mathcal{L}$ .

Proof. The first equation results from the universal property of the terminal object. The second one results from the universal property of the cartesian product and from the commutation of

since $ \mathsf{pr}_{0}^\otimes\, d =\lambda_{\underline{P}} \,({\operatorname{\mathsf{weak}}_{\underline{P}}}\otimes{\underline{P}}) \,({h_{P}}\otimes{\underline{P}}) \, d =\lambda_{\underline{P}} \,({u}\otimes{\underline{P}}) \, d=\operatorname{\mathsf{Id}}_{\underline{P}} $ and similarly for $\mathsf{pr}_{1}^\otimes$ .

For the last commutation, we have

2.3.4 Lafont categories and the free exponential

In many interesting models of ${\textsf{LL}}$ , the exponential resource modality is completely determined by the tensor product; in that case, one says that the exponential is free. We provide the precise definition of such categories and give some of their properties that we will use in the paper.

Let $\mathcal{L}$ be an SMC. Remember from Melliès (2009) that $\mathcal{L}$ is a Lafont category if the forgetful functor $U:{\mathcal {L}}^{\otimes}\to\mathcal{L}$ has a right adjoint $E:\mathcal{L}\to{\mathcal {L}}^{\otimes}$ . We use $(\ !{X},\operatorname{\mathsf{weak}}_{X},\operatorname{\mathsf{contr}}_{X})$ for the commutative comonoid EX. In that case, we use $(\ !{\_},\operatorname{\mathsf{der}}_{},\operatorname{\mathsf{dig}}_{})$ for the associated comonad UE called the free exponential of the SMC $\mathcal{L}$ .

More explicitly, this means that for any object X of $\mathcal{L}$ , for any commutative comonoid $C=(\underline{C},\mathsf w_{C}:\underline{C}\to1, \mathsf c_{C}:\underline{C}\to{\underline{C}}\otimes{\underline{C}})$ and any $f\in\mathcal{L}(\underline{C},X)$ , there is exactly one morphism $f^\otimes\in\mathcal{L}/X((\underline{C},f),(\ !{X},\operatorname{\mathsf{der}}_{X}\ !))$ which is a comonoid morphism. In other words, there is exactly one morphism $f^\otimes\in\mathcal{L}(\underline{C},\ !{X})$ such that the three following diagrams commute.

Lemma 6. Let $\mathcal{L}$ be a Lafont category. For any commutative comonoid C, there is exactly one morphism $\delta_C\in\mathcal{L}(\underline{C},\ !{\underline{C}})$ such that the following diagrams commute.

Moreover $(\underline{C},\delta_C)$ is a $\ !$ -coalgebra.

Proof. The first part of the statement is just a special case of the universal property with $X=\underline{C}$ and $f=\operatorname{\mathsf{Id}}_X$ . For the second part, we only have to prove

Setting $f_1=\ !{\delta_C}\,\delta_C$ and $f_2=\operatorname{\mathsf{dig}}_{\underline{C}}\,\delta_C$ , observe first that $f_1,f_2\in{\mathcal {L}}^{\otimes}(C,(\ !\ !{\underline{C}},\mathsf c_{\ !{\underline{C}}},\mathsf w_{\ !{\underline{C}}}))$ because both are defined by composing morphisms in that category. The equation $f_1=f_2$ follows by universality, observing that

for $i=1,2$ , which readily results from the naturality of $\operatorname{\mathsf{der}}_{}$ and from the definition of a comonad.

Here are two important special cases of the above. First, there is exactly one morphism $\mu^0\in\mathcal{L}(1,\ !{1})$ such that

Next, there is exactly one morphism $\mu^2_{X,Y}\in\mathcal{L}({\ !{X}}\otimes{\ !{Y}},\ !({{X}\otimes{Y}}))$ such that

These two morphisms turn $\ !{\_}$ into a lax monoidal comonad on the SMC $\mathcal{L}$ .

The correspondence $C\mapsto(\underline{C},\delta_C)$ can be turned into a functor $\mathsf A:{\mathcal {L}}^{\otimes}\to{\mathcal{L}}^!$ acting as the identity on morphisms. Let indeed $f\in{\mathcal {L}}^{\otimes}(C,D)$ , it suffices to prove that $\delta_D\, f=\ !{f}\,\delta_C\in\mathcal{L}(\underline{C},\ !{\underline{D}})$ . Let $f_0=\delta_D\, f$ and $f_1=\ !{f}\,\delta_C$ . By the universal property, it suffices to prove that the three following diagrams commute for $i=0,1$ :

These commutations follow from the commutations satisfied by $\delta_C$ and $\delta_D$ and from the fact that $f\in{\mathcal {L}}^{\otimes}(C,D)$ . As an example of these computations, we have

\begin{align*} \operatorname{\mathsf{contr}}_{\underline{D}}\, f_0 &=\operatorname{\mathsf{contr}}_{\underline{D}}\,\delta_D\, f\\[2pt] &=({\delta_D}\otimes{\delta_D})\,\mathsf c_{D}\, f\\[2pt] &=({\delta_D}\otimes{\delta_D})\,({f}\otimes{f})\,\mathsf c_{C}\\[2pt] &=({f_0}\otimes{f_0})\,\mathsf c_{C}\end{align*}

and

\begin{align*} \operatorname{\mathsf{contr}}_{\underline{D}}\, f_1 &=\operatorname{\mathsf{contr}}_{\underline{D}}\,\ !{f}\,\delta_C\\[2pt] &=({\ !{f}}\otimes{\ !{f}})\,\operatorname{\mathsf{contr}}_{\underline{C}}\, \delta_C\\[2pt] &=({\ !{f}}\otimes{\ !{f}}) \,({\delta_C}\otimes{\delta_C})\,\mathsf c_{C}\\[2pt] &=({f_1}\otimes{f_1})\,\mathsf c_{C} \,.\end{align*}

Conversely given a $\ !$ -coalgebra $P=(\underline{P},h_{P})$ , one can define a commutative comonoid structure on $\underline{P}$ by the following two morphisms:

that we respectively denote as $\mathsf w_{P}$ and $\mathsf c_{P}$ . This correspondence $P\mapsto\mathsf M(P)=(\underline{P},\mathsf w_{P},\mathsf c_{P})$ can be turned into a functor $\mathsf M:{\mathcal{L}}^!\to{\mathcal {L}}^{\otimes}$ acting as the identity on morphisms.

Theorem 3. For any Lafont SMC $\mathcal{L}$ , the functors $\mathsf A$ and $\mathsf M$ define an isomorphism of categories between ${\mathcal {L}}^{\otimes}$ and ${\mathcal{L}}^!$ .

Proof. Let $C\in{\mathcal {L}}^{\otimes}$ and let $P=\mathsf A(C)$ so that $\underline{P}=\underline{C}$ and $h_{P}=\delta_C$ . Let $D=\mathsf M(P)$ so that $\underline{D}=\underline{C}$ ,

\begin{align*} \mathsf w_{D}&=\operatorname{\mathsf{weak}}_{\underline{P}}\,h_{P} =\operatorname{\mathsf{weak}}_{\underline{C}}\,\delta_C=\mathsf w_{C}\\[2pt] \mathsf c_{D}&=({\operatorname{\mathsf{der}}_{\underline{P}}}\otimes{\operatorname{\mathsf{der}}_{\underline{P}}}) \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}\\[2pt] &=({\operatorname{\mathsf{der}}_{\underline{C}}}\otimes{\operatorname{\mathsf{der}}_{\underline{C}}}) \,\operatorname{\mathsf{contr}}_{\underline{C}} \,\delta_C\\[2pt] &=({\operatorname{\mathsf{der}}_{\underline{C}}}\otimes{\operatorname{\mathsf{der}}_{\underline{C}}}) ({\delta_C}\otimes{\delta_C}) \,\operatorname{\mathsf{contr}}_{\underline{C}}\\[2pt] &=\operatorname{\mathsf{contr}}_{\underline{C}}. \end{align*}

Conversely let $P\in{\mathcal{L}}^!$ . Let $C=\mathsf M(P)$ so that $\underline{C}=\underline{P}$ , $\mathsf w_{C}=\operatorname{\mathsf{weak}}_{\underline{P}}\,h_{P}$ and $\mathsf c_{C}=({\operatorname{\mathsf{der}}_{\underline{P}}}\otimes{\operatorname{\mathsf{der}}_{\underline{P}}})$ $ \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}$ . Let $Q=\mathsf A(C)=(\underline{P},\delta_C)$ . To prove that $\delta_C=h_{P}$ , it suffices to show that the following diagrams commute

which results from the definition of C and from the fact that P is a coalgebra. Let us check for instance the last one:

\begin{align*} ({h_{P}}\otimes{h_{P}}) \,\mathsf c_{C} &=({h_{P}}\otimes{h_{P}}) \,({\operatorname{\mathsf{der}}_{\underline{P}}}\otimes{\operatorname{\mathsf{der}}_{\underline{P}}}) \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}\\ &=({\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}\otimes{\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}) \,({\ !{h_{P}}}\otimes{\ !{h_{P}}}) \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}\\ &=({\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}\otimes{\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}) \,\operatorname{\mathsf{contr}}_{\ !{\underline{P}}} \,\ !{h_{P}} \,h_{P}\\ &=({\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}\otimes{\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}) \,\operatorname{\mathsf{contr}}_{\ !{\underline{P}}} \,\operatorname{\mathsf{dig}}_{\underline{P}} \,h_{P}\\ &=({\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}\otimes{\operatorname{\mathsf{der}}_{\ !{\underline{P}}}}) ({\operatorname{\mathsf{dig}}_{\underline{P}}}\otimes{\operatorname{\mathsf{dig}}_{\underline{P}}}) \,\operatorname{\mathsf{contr}}_{\underline{P}} \,h_{P}\\ &=\,\operatorname{\mathsf{contr}}_{\underline{C}} \,h_{P} \end{align*}

where we have used in particular the fact that for any $X\in\mathcal{L}$ , one has $\operatorname{\mathsf{dig}}_{X}\in{\mathcal {L}}^{\otimes}(E(X),E(\ !{X}))$ by the fact that the comonad $\ !{\_}$ is induced by the adjunction $U\mathrel{\dashv} E$ .

This shows that $\mathsf M$ and $\mathsf A$ define a bijective correspondence on objects and since both functors act as the identity on morphisms, our contention is proven.

In that way, we retrieve the fact that ${\mathcal{L}}^!$ is cartesian since ${\mathcal {L}}^{\otimes}$ is always cartesian by Theorem 1 (even if $\mathcal{L}$ is not Lafont). Remember that in the general (not necessarily Lafont) case the fact that ${\mathcal{L}}^!$ is cartesian could be proven under the additional assumption that $\mathcal{L}$ is a resource category. Remember also that a cartesian Lafont SMC is automatically a resource category; see Melliès (2009).

Lemma 7. Let $C_0,C_1\in{\mathcal {L}}^{\otimes}$ . Remember that we use ${C_0}\otimes{C_1}$ for the cartesian product of $C_0$ and $C_1$ in ${\mathcal {L}}^{\otimes}$ (see Theorem 1). Then, we have

\begin{align*} \delta_1=\mu^0 \delta_{{C_0}\otimes{C_1}} =\mu^2_{{\underline{C_0}},{\underline{C_1}}} \,({\delta_{C_0}}\otimes{\delta_{C_1}}) \in\mathcal{L}({\underline{C_0}}\otimes{\underline{C_1}}, \ !({{\underline{C_0}}\otimes{\underline{C_1}}}))\,. \end{align*}

Proof. One just checks that the right-hand morphisms satisfy the three diagrams of Lemma 6.

Theorem 4. Let $\mathcal{L}$ be a Lafont category and let $C\in{\mathcal {L}}^{\otimes}$ . Then the following diagrams commute

Proof. We deal with the second diagram, the argument for the first one being completely similar. By Lemma 2 we have $\mathsf c_{C}\in{\mathcal {L}}^{\otimes}(C,{C}\otimes{C})$ and hence (since $\mathsf A$ is the identity on morphisms) we have $\mathsf c_{C}\in{\mathcal{L}}^!(\mathsf A(C),\mathsf A({C}\otimes{C}))$ which is exactly the diagram under consideration by Lemma 7.

2.3.5 Resource Lafont categories

A resource Lafont category is a resource category $\mathcal{L}$ where the exponential arises in the way explained above; in that case one says that $\ !{\_}$ is the free exponential (it is unique up to unique iso since it is defined by a universal property). This is equivalent to requiring that

• $\mathcal{L}$ is a Lafont SMC

• and $\mathcal{L}$ is cartesian.

Indeed when these conditions hold, the Seely isomorphisms are uniquely defined by the universal property of the Lafont SMC $\mathcal{L}$ . The lax monoidality $(\mu^0,\mu^2)$ induced by these Seely isomorphisms coincide with the one which is directly induced by the Lafont property (again by universality). This is why we used the same notations for both.

2.4 The category of sets and relations

This category is a well-known categorical model of classical ${\textsf{LL}}$ that we briefly recall here. It is perhaps the simplest example of a Lafont resource category.

The category $\operatorname{\mathbf{Rel}}$ has sets as objects and $\operatorname{\mathbf{Rel}}(X,Y)={\mathcal P}\left({X\times Y}\right)$ , that is, a morphism from the set X to the set Y is a relation from X to Y. The identity morphism $\operatorname{\mathsf{Id}}_X$ is the diagonal relation on X and composition is the usual composition of relations. An iso in $\operatorname{\mathbf{Rel}}$ is a relation which is (the graph of) a bijection.

The category $\operatorname{\mathbf{Rel}}$ is monoidal with monoidal product ${X_0}\otimes{X_1}=X_0\times X_1$ and monoidal unit $1=\{\ast\}$ . Given $s_i\in\operatorname{\mathbf{Rel}}(X_i,Y_i)$ for $i=0,1$ , the relation ${s_0}\otimes{s_1}\in\operatorname{\mathbf{Rel}}({X_0}\otimes{X_1},{Y_0}\otimes{Y_1})$ is defined as:

\begin{align*} {s_0}\otimes{s_1} =\{((a_0,a_1),(b_0,b_1))\mid (a_i,b_i)\in s_i\text{ for }i=0,1\}\end{align*}

which turns $\otimes$ into a functor and $\operatorname{\mathbf{Rel}}$ into a SMC (with obvious symmetric monoidality isos). It is also closed with ${X}\multimap{Y}=X\times Y$ as internal hom object and evaluation morphism:

\begin{align*} \operatorname{\mathsf{ev}}=\{(((a,b),a),b)\mid a\in X\text{ and }b\in Y\} \in\operatorname{\mathbf{Rel}}({\left({X}\multimap{Y}\right)}\otimes{X},Y)\,.\end{align*}

With dualizing object ${\mathord{\perp}}=1$ , this category is $\ast$ -autonomous.

The category $\operatorname{\mathbf{Rel}}$ is not complete, but it is cartesian. Given a family $(X_i)_{i\in I}$ of sets, their product is

\begin{align*} (\mathop{\&}_{i\in I}X_i,(\mathsf{pr}_{i})_{i\in I})\end{align*}

where $\mathop{\&}_{i\in I}X_i=\bigcup_{i\in I}\{i\}\times X_i$ and the projections are $\mathsf{pr}_{i}=\{((i,a),a)\mid i\in I\text{ and }a\in X_i\}\in\operatorname{\mathbf{Rel}}(\ !\mathop{\&}_{j\in I}X_j,X_i)$ . Given a family of morphisms $(s_i\in\operatorname{\mathbf{Rel}}(Y,X_i))_{i\in I}$ , the unique morphism $\langle{s_i}\rangle_{i\in I}\in\operatorname{\mathbf{Rel}}(Y,\mathop{\&}_{i\in I}X_i)$ such that $\mathsf{pr}_{i}\,\langle{s_j}\rangle_{j\in I}=s_i$ is

\begin{align*} \langle{s_i}\rangle_{i\in I}= \{(b,(i,a))\mid i\in I\text{ and }(b,a)\in s_i\}\,.\end{align*}

The terminal object is $\top=\emptyset$ .

As an SMC, $\operatorname{\mathbf{Rel}}$ is a Lafont category. The associated resource comonad $(\ !,\operatorname{\mathsf{der}}_{},\operatorname{\mathsf{dig}}_{}\ !)$ on $\operatorname{\mathbf{Rel}}$ is given by $\ !{X}=\mathcal M_{{\mathrm{fin}}}({X})$ (see Section 2.1) with functorial action given by:

\begin{align*} \ !{s}=\{([{a_{1},\dots,a_{n}}],[{b_{1},\dots,b_{n}}]) \mid n\in{\mathbb{N}}\text{ and }\forall i\ (a_i,b_i)\in s\} \in\operatorname{\mathbf{Rel}}(\ !{X},\ !{Y})\end{align*}

for $s\in\operatorname{\mathbf{Rel}}(X,Y)$ . The counit is $\operatorname{\mathsf{der}}_{X}=\{([{a}],a)\mid a\in X\}\in\operatorname{\mathbf{Rel}}(\ !{X},X)$ and the comultiplication is $\operatorname{\mathsf{dig}}_{X} =\{(m_1+\cdots+m_k,[{m_{1},\dots,m_{k}}])\mid k\in{\mathbb{N}} \text{ and}m_{1},\dots,m_{k}\in\ !{X}\}$ . Its strong symmetric monoidality from the SMC $(\operatorname{\mathbf{Rel}},\mathrel{\&},\top)$ to the SMC $(\operatorname{\mathbf{Rel}},\otimes,1)$ is given by the isos $\mathsf m^0\in\operatorname{\mathbf{Rel}}(1,\ !{\top})$ and $\mathsf m^2_{X_0,X_1}\in\operatorname{\mathbf{Rel}}({\ !{X_0}}\otimes{\ !{X_1}},\ !{\left({X_0}\mathrel{\&}{X_1}\right)})$ given by $\mathsf m^0=\{(\ast,[]\,)\}$ and

3. Summable Categories

Let $\mathcal{L}$ be a category. We develop a categorical axiomatization of a concept of finite summability in $\mathcal{L}$ which will induce an enrichment of $\mathcal{L}$ over partial commutative monoids, in the sense of Poinsot et al. (2010). The main idea is to equip $\mathcal{L}$ with a functor $\mathsf S$ which has the flavor of a monad ⁴ and intuitively maps an object X to the object $\mathsf S X$ of all pairs $(x_0,x_1)$ of elements of X whose sum $x_0+x_1$ is well defined. This is another feature of our approach which is to give a crucial role to such pairs, which are the values on which derivatives are computed, very much in the spirit of dual numbers. However, contrarily to dual numbers, our structures also axiomatize the actual summation of such pairs.

▸ Example 3.1. In order to illustrate the definitions and constructions of the paper, we will use the category $\mathbf{Coh}$ of coherence spaces of Girard (1987) as a running example. An object of this category is a pair where ${}|{E}{}|$ is a set (the web of E) and is a symmetric and reflexive relation on ${}|{E}{}|$ . The set of cliques of a coherence space E is

Equipped with $\subseteq$ as order relation, $\mathsf{Cl}({E})$ is a complete partial order (cpo). Given coherence spaces E and F, we define the coherence space ${E}\multimap{F}$ by ${}|{{E}\multimap{F}}{}|={}|{E}{}|\times{}|{F}{}|$ and

Lemma 8. If $s\in\mathsf{Cl}({{E}\multimap{F}})$ and $t\in\mathsf{Cl}({{F}\multimap{G}})$ , then $t\, s$ (the relational composition of t and s) belongs to $\mathsf{Cl}({{E}\multimap{G}})$ and the diagonal relation $\operatorname{\mathsf{Id}}_E$ belongs to $\mathsf{Cl}({{E}\multimap{E}})$ .

In that way, we have turned the class of coherence spaces into a category $\mathbf{Coh}$ with $\mathbf{Coh}(E,F)=\mathsf{Cl}({{E}\multimap{F}})$ and $\mathbf{Coh}$ is enriched over pointed sets, with $0=\emptyset$ . This category is cartesian with ${E_0}\mathrel{\&}{E_1}$ given by ${}|{{E_0}\mathrel{\&}{E_1}}{}|=\{0\}\times{}|{E_0}{}|\cup\{1\}\times{}|{E_1}{}|$ , if and $\mathsf{pr}_{i}=\{((i,a),a)\mid a\in{}|{E_i}{}|\}$ for $i=0,1$ and, given $s_i\in\mathbf{Coh}(F,E_i)$ (for $i=0,1$ ),

\begin{align*} \langle{s_0,s_1}\rangle=\{(b,(i,a))\mid i\in\{0,1\}\text{ and }(b,a)\in s_i\}\,.\end{align*}

Given $s\in\mathbf{Coh}(E,F)$ and $x\in\mathsf{Cl}({E})$ , one defines ${s}\cdot{x}\in\mathsf{Cl}({F})$ by ${s}\cdot{x}=\{b\in{}|{F}{}|\mid a\in x\text{ and }(a,b)\in s\}$ . Given $x_0,x_1\in\mathsf{Cl}({E})$ , we use $x_0+x_1$ to denote $x_0\cup x_1$ if $x_0\cup x_1\in\mathsf{Cl}({E})$ and $x_0\cap x_1=\emptyset$ . Notice that the use of the notation $x_0+x_1$ means in particular that these conditions (disjointedness and compatibility) hold for $x_0$ and $x_1$ . This notation is justified by the following observation by Girard in Girard (1995).

Lemma 9. Let E and F be coherence spaces and let $s\subseteq{}|{E}{}|\times{}|{F}{}|$ . Then $s\in\mathsf{Cl}({{E}\multimap{F}})$ iff

\begin{align*} {s}\cdot{\emptyset}=\emptyset \text{ and } \forall x_0,x_1\in\mathsf{Cl}({E}) \ {s}\cdot{(x_0+x_1)}={s}\cdot{x_0}+{s}\cdot{x_1}\in\mathsf{Cl}({F})\,,\end{align*}

the second statement meaning that if $x_0,x_1\in\mathsf{Cl}({E})$ are disjoint and satisfy $x_0\cup x_1\in\mathsf{Cl}({E})$ then ${s}\cdot{x_0},{s}\cdot{x_1}$ are disjoint and satisfy ${s}\cdot{x_0}\cup{s}\cdot{x_1}={s}\cdot{(x_0\cup x_1)}\in\mathsf{Cl}({F})$ .

This lemma expresses that the linear maps between coherence spaces are exactly those which preserve these partially defined “sums.”

Definition 10. A pre-summability structure on $\mathcal{L}$ is a tuple $(\mathsf S,\pi_{0},\pi_{1},\sigma)$ where $\mathsf S:\mathcal{L}\to\mathcal{L}$ is a functor which preserves the enrichment of $\mathcal{L}$ over $\mathbf{Set}_0$ (that is $\mathsf S 0=0$ ) and $\pi_{0},\pi_{1}$ and $\sigma$ are natural transformation from $\mathsf S$ to the identity functor such that for any two morphisms $f,g\in\mathcal{L}(Y,\mathsf S X)$ , if $\pi_{i}\, f=\pi_{i}\, g$ for $i=0,1$ , then $f=g$ . In other words, $\pi_{0}$ and $\pi_{1}$ are jointly monic.

▸ Example 3.2. We give a pre-summability structure on coherence spaces. Given a coherence space E, the coherence space $\mathsf S(E)$ is defined by ${}|{\mathsf S(E)}{}|=\{0,1\}\times{}|{E}{}|$ and if $i=i'$ and , or $i\not=i'$ and . Remember that means that and $a\not=a'$ (strict coherence relation). Notice that $\mathsf S E=\left({{1}\mathrel{\&}{1}}\multimap{E}\right)$ where 1 is the coherence space whose web is a chosen singleton $\{^\ast\}$ . We will see in Section 5 that it is often possible to define $\mathsf S$ in that particular way.

Lemma 11. The cpo $(\mathsf{Cl}({\mathsf S E}),\subseteq)$ is isomorphic to the poset of all pairs $(x_0,x_1)\in\mathsf{Cl}({E})^2$ such that $x_0+ x_1$ is defined (that is $x_0\cap x_1=\emptyset$ and $x_0\cup x_1\in\mathsf{Cl}({E})$ ), equipped with the product order.

Given $s\in\mathbf{Coh}(E,F)$ , we define $\mathsf S s\subseteq{}|{{\mathsf S E}\multimap{\mathsf S F}}{}|$ by:

\begin{align*} \mathsf S s=\{((i,a),(i,b))\mid i\in\{0,1\}\text{ and }(a,b)\in s\}\,.\end{align*}

Then it is easy to check that $\mathsf S s\in\mathbf{Coh}(\mathsf S E,\mathsf S F)$ and that $\mathsf S$ is a functor. This is due to the definition of s which entails ${s}\cdot{(x_0+x_1)}={s}\cdot{x_0}+{s}\cdot{x_1}$ .

The additional structure is defined as follows:

\begin{align*} \pi_{i}=\{((i,a),a)\mid a\in{}|{E}{}|\}\text{ and } \sigma=\{((i,a),a)\mid i\in\{0,1\}\text{ and }a\in{}|{E}{}|\}\end{align*}

which are easily seen to belong to $\mathbf{Coh}(\mathsf S E,E)$ . Notice that $\sigma=\pi_{0}+\pi_{1}$ . Of course ${\pi_{i}}\cdot{(x_0,x_1)}=x_i$ and ${\sigma}\cdot{(x_0,x_1)}=x_0+x_1$ .

From now on, we assume that we are given such a structure. We say that $f_i\in\mathcal{L}(X,Y)$ (for $i=0,1$ ) are summable if there is a morphism $g\in\mathcal{L}(X,\mathsf S Y)$ such that

for

$i=0,1$ . By definition of a pre-summability structure, there is only one such g if it exists, we denote it as $\langle{f_0,f_1}\rangle_{\mathsf S}$ . When this is the case we set $f_0+f_1=\sigma\,\langle{f_0,f_1}\rangle_{\mathsf S}\in\mathcal{L}(X,Y)$ . We sometimes call $\langle{f_0,f_1}\rangle_{\mathsf S}$ the witness of the summability of $f_0$ and $f_1$ and $f_0+f_1$ their sum.

▸ Example 3.3. In the case of coherence spaces, saying that $s_0,s_1\in\mathbf{Coh}(E,F)$ are summable simply means that $s_0\cap s_1=\emptyset$ and $s_0\cup s_1\in\mathbf{Coh}(E,F)$ . This property is equivalent to

\begin{align*} \forall x\in\mathsf{Cl}({X}) ({s_0}\cdot{x},{s_1}\cdot{x})\in\mathsf{Cl}({\mathsf S E}) \end{align*}

and in that case the witness is defined exactly in the same way as $\langle{s_0,s_1}\rangle\in\mathbf{Coh}(E,{F}\mathrel{\&}{F})$ .

Lemma 12. Assume that $f_0,f_1\in\mathcal{L}(X,Y)$ are summable and that $g\in\mathcal{L}(U,X)$ and $h\in\mathcal{L}(Y,Z)$ . Then $h\, f_0\, g$ and $h\, f_1\, g$ are summable with witness $(\mathsf S h)\,\langle{f_0,f_1}\rangle_{\mathsf S}\, g\in\mathcal{L}(U,\mathsf S Z)$ and sum $h\,(f_0+f_1)\, g\in\mathcal{L}(U,Z)$ .

The proof boils down to the naturality of $\pi_{i}$ and $\sigma$ . An easy consequence is that the application of $\mathsf S$ to a morphism can be written as a witness.

Lemma 13. If $f\in\mathcal{L}(X,Y)$ , then $f\,\pi_{0},f\,\pi_{1}\in\mathcal{L}(\mathsf S X,Y)$ are summable with witness $\mathsf S f$ and sum $f\,\sigma$ . That is, $\mathsf S f=\langle{f\,\pi_{0},f\,\pi_{1}}\rangle_{\mathsf S}$ .

Now using this notion of pre-summability structure, we start introducing additional conditions to define a summability structure. As a general principle, and unless specified otherwise, each time we introduce an axiom, we assume that it holds in the considerations which follow.

Notice that by definition, $\pi_{0}$ and $\pi_{1}$ are summable with $\operatorname{\mathsf{Id}}$ as witness and $\sigma$ as sum. Here is our first axiom.

(S-com) $\pi_{1}$ and $\pi_{0}$ are summable and the witness $\langle{\pi_{1},\pi_{0}}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S X,\mathsf S X)$ satisfies $\sigma\,\langle{\pi_{1},\pi_{0}}\rangle_{\mathsf S}=\sigma$ .

Notice that this witness is an involutive iso since $\pi_{i}\,\langle{\pi_{1},\pi_{0}}\rangle_{\mathsf S}\,\langle{\pi_{1},\pi_{0}}\rangle_{\mathsf S}=\pi_{i}$ for $i=0,1$ .

Lemma 14. If $f_0,f_1\in\mathcal{L}(X,Y)$ are summable, then $f_1,f_0$ are summable with witness $\langle{\pi_{1},\pi_{0}}\rangle_{\mathsf S}$ $\,\langle{f_0,f_1}\rangle_{\mathsf S}$ and we have $f_0+f_1=f_1+f_0$ .

Our next axiom expresses that the 0-morphisms are neutral for this partially defined addition. (S-zero) For any $f\in\mathcal{L}(X,Y)$ , the morphisms f and $0\in\mathcal{L}(X,Y)$ are summable and their sum is f, that is $\sigma\,\langle{f,0}\rangle=f$ .

By (S-com), this implies that 0 and f are summable with $0+f=f$ .

Notice that we have four morphisms $\pi_{0}\pi_{0},\pi_{1}\pi_{1},\pi_{0}\pi_{1},\pi_{1}\pi_{0}\in\mathcal{L}(\mathsf S^2X,X)$ .

Lemma 15. If $f,f'\in\mathcal{L}(X,\mathsf S^2Y)$ satisfy $\pi_{i}\,\pi_{j}\, f=\pi_{i}\,\pi_{j}\, f'$ for all $i,j\in\{0,1\}$ , then $f=f'$ , that is, the $\pi_{i}\,\pi_{j}$ are jointly monic.

This is an easy consequence of the fact that $\pi_{0},\pi_{1}$ are jointly monic.

The next axiom will allow us in particular to show that our partially defined addition is associative.

(S-witness) Let $f_{0},f_{1}\in\mathcal{L}(X,\mathsf S Y)$ . If $\sigma\, f_0,\sigma\, f_1$ are summable, then $f_0,f_1$ are summable.

Notice that the converse implication holds by Lemma 12. This axiom means that the summability of witnesses boils down to that of the associated sums.

Lemma 17 requires a little preparation. By Lemma 12, the pairs of morphisms $(\pi_{0}\pi_{0},\pi_{0}\pi_{1})$ and $(\pi_{1}\pi_{0},\pi_{1}\pi_{1})$ are summable with sums $\pi_{0}\,\sigma$ and $\pi_{1}\,\sigma$ , respectively. By the same lemma, these two morphisms are summable (with sum $\sigma\,\sigma\in\mathcal{L}(\mathsf S^2X,X)$ ). By Axiom (S-witness), it follows that the witnesses $\langle{\pi_{0}\pi_{0},\pi_{0}\pi_{1}}\rangle_{\mathsf S},\langle{\pi_{1}\pi_{0},\pi_{1}\pi_{1}}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S^2X,\mathsf S X)$ are summable, let $\mathsf c_X=\langle{\langle{\pi_{0}\pi_{0},\pi_{0}\pi_{1}}\rangle_{\mathsf S},\langle{\pi_{1}\pi_{0},\pi_{1}\pi_{1}}\rangle_{\mathsf S}}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S^2X,\mathsf S^2X)$ be the corresponding witness.

Lemma 16. The morphism $\mathsf c_X=\langle{\langle{\pi_{0}\pi_{0},\pi_{0}\pi_{1}}\rangle_{\mathsf S},\langle{\pi_{1}\pi_{0},\pi_{1}\pi_{1}}\rangle_{\mathsf S}}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S^2X,\mathsf S^2X)$ is an involutive natural iso in $\mathcal{L}$ .

The proof is easy, using Lemma 15. Notice that $\mathsf c$ (which is similar to the flip of a tangent bundle functor) is completely characterized by:

\begin{align*} \forall i,j\in\{0,1\} \pi_{i}\,\pi_{j}\,\mathsf c =\pi_{j}\,\pi_{i}\,.\end{align*}

It will be called the standard flip on $\mathsf S^2X$ .

Lemma 17. The following diagram commutes:

Proof. For $i\in\{0,1\}$ , we have $\pi_{i}\,\mathsf S{\sigma_X}=\sigma_X\,\pi_{i}$ by naturality of $\pi_{i}$ and $\pi_{i}\,\sigma_{\mathsf S X}=\sigma_X\,\mathsf S{\pi_{i}}$ by naturality of $\sigma$ . So by the fact that $\pi_{0},\pi_{1}$ are jointly monic it suffices to prove that the following diagram commutes:

We use again the fact that $\pi_{0},\pi_{1}$ are jointly monic. Let $j\in\{0,1\}$ , we have $\pi_{j}\,\mathsf S\pi_{i}=\pi_{i}\,\pi_{j}$ by naturality of $\pi_{j}$ . The required commutation follows from $\pi_{i}\,\pi_{j}\,\mathsf c=\pi_{j}\,\pi_{i}$ .

Notice that if $f_0,f_1\in\mathcal{L}(X,\mathsf S Y)$ are summable, then

(2) \begin{align} \pi_{i}\,(f_0+f_1)=\pi_{i}\, f_0+\pi_{i}\, f_1 \text{ for }i=0,1\end{align}

by Lemma 12, that is, if we set $f_{ij}=\pi_{j}\, f_i$ for $i,j\in\{0,1\}$ , so that $f_i=\langle{f_{i0},f_{i1}}\rangle_{\mathsf S}$ for $i=0,1$ , Equations (2) mean that

\begin{align*} \langle{f_{00},f_{01}}\rangle_{\mathsf S}+\langle{f_{10},f_{11}}\rangle_{\mathsf S} =\langle{f_{00}+f_{10},f_{01}+f_{11}}\rangle_{\mathsf S}\,.\end{align*}

In other words, addition of summable witnesses is performed componentwise.

Lemma 18. Let $f_0,f_1\in\mathcal{L}(Y,\mathsf S X)$ be summable. Then the morphisms $(f'_i=\pi_{i}\,\mathsf c\,\langle{f_0,f_1}\rangle_{\mathsf S} \in\mathcal{L}(Y,\mathsf S X))_{i=0,1}$ are summable and satisfy

\begin{align*} \sigma_X\, f'_0+\sigma_X\, f'_1 =\sigma_X\, f_0+\sigma_X\, f_1\,, \end{align*}

the two sums being well defined by Lemma 12.

Proof. The morphisms $f'_0,f'_1$ are summable with witness $\langle{f'_0,f'_1}\rangle_{\mathsf S}=\mathsf c\,\langle{f_0,f_1}\rangle_{\mathsf S}\in\mathcal{L}(Y,\mathsf S^2X)$ by their very definition. We have

Let us explain what this means. Setting $f_{ij}=\pi_{j}\, f_i$ for $i,j\in\{0,1\}$ , we have $f_i=\langle{f_{i0},f_{i1}}\rangle_{\mathsf S}$ for $i=0,1$ , so $\langle{f_0,f_1}\rangle_{\mathsf S}=\angle{\langle{f_{00},f_{01}}\rangle_{\mathsf S},\langle{f_{10},f_{11}}\rangle_{\mathsf S}}\rangle_{\mathsf S}$ and $\langle{f'_0,f'_1}\rangle_{\mathsf S} =\mathsf c\,\langle{f_0,f_1}\rangle_{\mathsf S}=\langle{\langle{f_{00},f_{10}}\rangle_{\mathsf S},\langle{f_{01},f_{11}}\rangle_{\mathsf S}}\rangle_{\mathsf S}$ . The lemma tells us that

\begin{align*} (f_{00}+f_{10})+(f_{01}+f_{11}) =(f_{00}+f_{01})+(f_{10}+f_{11})\,.\end{align*}

Lemma 19. Let $f_0,f_1,f_2\in\mathcal{L}(X,Y)$ be such that $(f_0,f_1)$ is summable and $(f_0+f_1,f_2)$ is summable. Then, $(f_1,f_2)$ is summable and $(f_0,f_1+f_2)$ is summable, and we have $(f_0+f_1)+f_2=f_0+(f_1+f_2)$ .

Proof. By (S-zero) we know that $0,f_2$ are summable and $0+f_2=f_2$ . So by (S-witness), we have that $\langle{f_0,f_1}\rangle_{\mathsf S}$ and $\langle{0,f_2}\rangle_{\mathsf S}$ are summable. Hence, by Lemma 18, $\langle{f_0,0}\rangle_{\mathsf S},\langle{f_1,f_2}\rangle_{\mathsf S}$ are summable and we have $(f_0+f_1)+f_2=f_0+(f_1+f_2)$ .

▸ Example 3.4. All these properties are easy to check in coherence spaces and boil down to the standard algebraic properties of set unions.

Definition 20. A summability structure on $\mathcal{L}$ is a pre-summability structure which satisfies axioms (S-com), (S-zero), and (S-witness). We call summable category a tuple $(\mathcal{L},\mathsf S,\pi_{0},\pi_{1},\sigma)$ consisting of a category $\mathcal{L}$ equipped with a summability structure.

We define a general notion of summable family of morphisms $(f_i)_{i=1}^n$ in $\mathcal{L}(X,Y)$ together with its sum $f_1+\cdots+f_n$ by induction on n:

• if $n=0$ then $(f_i)_{i=1}^n$ if summable with sum 0;

• if $n>0$ then $(f_i)_{i=1}^n$ is summable if $(f_i)_{i=1}^{n-1}$ is summable and $f_1+\cdots+f_{n-1},f_n$ are summable, and then $f_1+\cdots+f_n=(f_1+\cdots+f_{n-1})+f_n$ .

Of course we use the standard notation $\sum_{i=1}^nf_i$ for $f_1+\cdots+f_n$ .

Lemma 21. If $(f_i)_{i=1}^n$ is summable with $n>0$ then $(f_i)_{i=2}^n$ is summable and $f_1,\sum_{i=2}^nf_i$ are summable and $f_1+\sum_{i=2}^nf_i=\sum_{i=1}^nf_i$ .

Proof. By induction on n. If $n=0$ , there is nothing to prove so assume $n>0$ . If $n=1$ the statement results from (S-zero), so we assume that $n\geq 2$ . By definition, we know that $f_{1},\dots,f_{n-1}$ is summable and $\sum_{i=1}^{n-1}f_i+f_n=\sum_{i=1}^nf_i$ . So by inductive hypothesis $f_{2},\dots,f_{n-1}$ is summable, $f_1,\sum_{i=2}^{n-1}f_i$ are summable and $f_1+\sum_{i=2}^{n-1}f_i=\sum_{i=1}^{n-1}f_i$ . So we can apply Lemma 19 to $f_1,\sum_{i=2}^{n-1}f_i,f_n$ and hence $\sum_{i=2}^{n-1}f_i,f_n$ are summable which by definition means that $f_{2},\dots,f_{n}$ is summable and $\sum_{i=2}^nf_i=\sum_{i=2}^{n-1}f_i+f_n$ , and moreover $f_1,\sum_{i=2}^nf_i$ are summable and $f_1+\sum_{i=2}^nf_i=\sum_{i=1}^{n-1}f_i+f_n=\sum_{i=1}^nf_i$ as contended.

Now we prove that summability is invariant by permutations. For this, we consider first a circular permutation and then a transposition.

Lemma 22. If $f_{1},\dots,f_{n}$ are summable, then $f_{2},\dots,f_{n},f_1$ is summable and $\sum_{i=1}^nf_i=f_2+\cdots+f_{n}+f_1$ .

Proof. This is obvious if $n\leq 1$ , so we can assume $n\geq 2$ . By Lemma 21 $f_{2},\dots,f_{n}$ are summable and $f_1,\sum_{i=2}^nf_i$ are summable with $f_1+\sum_{i=2}^nf_i=\sum_{i=1}^nf_i$ . So $\sum_{i=2}^nf_i,f_1$ are summable by Lemma 14 and hence $f_2,\dots,f_n,f_1$ is summable (by definition) with sum equal to $\sum_{i=1}^nf_i$ .

Lemma 23. If the family $f_{1},\dots,f_{n}$ is summable, with $n\geq 2$ , then $f_{1},\dots,f_{n-2},f_n,f_{n-1}$ is summable with the same sum.

Proof. By our assumption, $f_{1},\dots,f_{n-2}$ is summable (let us call g its sum), $g,f_{n-1}$ are summable and $g+f_{n-1},f_n$ are summable. Moreover $(g+f_{n-1})+f_n=\sum_{i=1}^nf_i$ . It follows by Lemma 19 that $f_{n-1},f_n$ are summable and hence $f_n,f_{n-1}$ are summable with $f_n+f_{n-1}=f_{n-1}+f_n$ by Lemma 14. So we know by Lemma 19 that $g,f_n+f_{n-1}$ are summable and hence by the same lemma that $g,f_n$ are summable and that $g+f_n,f_{n-1}$ are summable with $(g+f_n)+f_{n-1}=g+(f_n+f_{n-1})=\sum_{i=1}^nf_i$ . By definition, it follows that $f_{1},\dots,f_{n-2},f_n$ is a summable family whose sum is $g+f_n$ , and then that $f_{1},\dots,f_{n-2},f_n,f_{n-1}$ is a summable family whose sum is $\sum_{i=1}^nf_i$ , as announced.

Proposition 24. For any $p\in\mathfrak S_{n}$ (the symmetric group) and any family of morphisms $(f_i)_{i=1}^n$ , the family $(f_i)_{i=1}^n$ is summable iff the family $(f_{p(i)})_{i=1}^n$ is summable and then $\sum_{i\in I}f_i=\sum_{i\in I}f_{p(i)}$ .

Proof. Remember that $\mathfrak S_{n}$ is generated by the permutations $(1,\dots,n-2,n,n-1)$ (transposition) and $(2,\dots,n,1)$ (circular permutation) and apply Lemmas 23 and 22.

So we define a finite family $(f_i)_{i\in I}$ (where I is an arbitrary finite set) to be summable if any of its enumerations $(f_{i_1},\dots,f_{i_n})$ is summable and then we set $\sum_{i\in I}f_i=\sum_{k=1}^nf_{i_k}$ .

Theorem 5. A finite family of morphisms $(f_i)_{i\in I}$ in $\mathcal{L}(X,Y)$ is summable iff for any family of pairwise disjoint sets $(I_j)_{j\in J}$ such that $\cup_{j\in J}I_j=I$ :

• for each $j\in J$ the restricted family $(f_i)_{i\in I_j}$ is summable with sum $\sum_{i\in I_j}f_i\in\mathcal{L}(X,Y)$

• the family $(\sum_{i\in I_j}f_i)_{j\in J}$ is summable

and then we have $\sum_{i\in I}f_i=\sum_{j\in J}\sum_{i\in I_j}f_i$ .

Proof. By induction on $k=\#{J}\geq 1$ . If $k=1$ , the property trivially holds so assume $k>1$ . Upon choosing enumerations, we can assume that $I=\{1,\dots,n\}$ and $J=\{1,\dots,k\}$ , with $n,k\in{\mathbb{N}}$ . Thanks to Proposition 24, we can choose these enumerations in such a way that $I_k=\{l+1,\dots,n\}$ for some $l\in\{1,\dots,n\}$ . Then by an iterated application of the definition of summability and of Lemma 19, we know that the families $f_{1},\dots,f_{l}$ and $f_{l+1},\dots,f_{k}$ are summable and that $(\sum_{i=1}^lf_i)+(\sum_{j=l+1}^kf_i)=\sum_{i=1}^nf_i$ . We conclude the proof by applying the inductive hypothesis to $(I_j)_{j=1}^{k-1}$ which satisfies $\bigcup_{j=1}^{k-1}I_j=\{1,\dots,l\}$ .

Remark 25. These properties strongly suggest to consider summability as an n-ary notion, axiomatized in an operadic way. However, in the sequel, we will see that the differential operations use $\mathsf S X$ as a space of pairs, and there it is not clear that such an operadic approach would be so convenient. This is why we stick (at least for the time being) to this “binary” axiomatization.

Remark 26. Theorem 5 expresses exactly that $\mathcal{L}(X,Y)$ is a partial commutative monoid ⁵ in the sense of Arbib and Manes (1980). And actually $\mathcal{L}$ is enriched over partial commutative monoids by Lemma 12. Contrarily to what we suggested in an earlier version of this article, it does not seem always possible to describe $\mathcal{L}$ as a partially additive category in the sense of Arbib and Manes (1980) Section 3 (even restricting this notion to finite sums) for the first obvious reason that we do not need $\mathcal{L}$ to have coproducts. More fundamentally, assuming now that $\mathcal{L}$ has coproducts, we can read Theorem 9 of Arbib and Manes (1980) as expressing that if $\mathcal{L}$ is partially additive then it has a summability structure (in our sense) given by the endofunctor $\mathsf S X={X}\oplus{X}$ (where ${X}\oplus{Y}$ is the coproduct of X and Y) equipped with $\pi_{0}=\left[{X,0}\right]$ , $\pi_{1}=\left[{0,X}\right]$ and $\sigma=\left[{X,X}\right]$ where $\left[{f_0,f_1}\right]\in\mathcal{L}({X_0}\oplus{X_1},Y)$ is the copairing of the $(f_i\in\mathcal{L}(X_i,Y))_{i=0,1}$ . So, as far as we understand partially additive categories, the cocartesian category $\mathbf{Coh}$ seems to be an example of a summable category which is not partially additive, since $\mathsf S E$ and ${E}\oplus{E}$ are very far from being isomorphic in general. Indeed $\mathsf{Cl}({{E}\oplus{E}})=\{(x,\emptyset),(\emptyset,x)\mid x\in\mathsf{Cl}({E})\}$ to be compared with $\mathsf{Cl}({\mathsf S E})$ which contains many more elements in general, see Lemma 11.

Another interesting consequence of Lemma 17 is that $\mathsf S$ preserves summability.

Theorem 6. Let $f_0,f_1\in\mathcal{L}(X,Y)$ be summable. Then, $\mathsf S f_0,\mathsf S f_1\in\mathcal{L}(\mathsf S X,\mathsf S Y)$ are summable, with witness $\langle{\mathsf S f_0,\mathsf S f_1}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S X,\mathsf S^2Y)$ given by $\langle{\mathsf S f_0,\mathsf S f_1}\rangle_{\mathsf S}=$ $\mathsf c\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S}$ . And one has $\mathsf S f_0+\mathsf S f_1=\mathsf S(f_0+f_1)$ .

Proof. This could be derived from Lemme 13, we prefer to give a direct argument. We must prove that $\pi_{i}\,\mathsf c\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S}=\mathsf S f_i$ . For this, we use the fact that $\pi_{0},\pi_{1}\in\mathcal{L}(\mathsf S Y,Y)$ are jointly monic. We have

\begin{align*} \pi_{j}\,\pi_{i}\,\mathsf c\,\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S} &=\pi_{i}\,\pi_{j}\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S}\\[3pt] &=\pi_{i}\,\langle{f_0,f_1}\rangle_{\mathsf S}\,\pi_{j}\text{ by naturality}\\[3pt] &=f_i\,\pi_{j}=\pi_{j}\,\mathsf S f_i\text{ by naturality.} \end{align*}

This shows that $\pi_{i}\,\mathsf c\,\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S}=\mathsf S f_i$ for $i=0,1$ and hence $\mathsf S f_0,\mathsf S f_1$ are summable with witness $\mathsf c\,\,\mathsf S\langle{f_0,f_1}\rangle_{\mathsf S}$ . And we have

Notice that taking $X=\mathsf S Y$ and $f_i=\pi_{i}$ for $i=0,1$ , this result gives us another expression for the standard flip:

\begin{align*} \mathsf c=\langle{\mathsf S{\pi_{0}},\mathsf S{\pi_{1}}}\rangle_{\mathsf S}\,.\end{align*}

We will use the notations $\iota_{0}=\langle{X,0}\rangle_{\mathsf S}\in\mathcal{L}(X,\mathsf S X)$ and $\iota_{1}=\langle{0,X}\rangle_{\mathsf S}\in\mathcal{L}(X,\mathsf S X)$ .

Lemma 27. The morphisms $\iota_{0},\iota_{1}\in\mathcal{L}(X,\mathsf S X)$ are natural in X.

Proof. Let $f\in\mathcal{L}(X,Y)$ . For $i=0,1$ , we have $\pi_{i}\,\mathsf S f\,\langle{\operatorname{\mathsf{Id}},0}\rangle_{\mathsf S} =f\,\pi_{i}\,\langle{\operatorname{\mathsf{Id}},0}\langle_{\mathsf S}$ which is equal to f if $i=0$ and to 0 if $i=1$ since $f\, 0=0$ . On the other hand, $\pi_{i}\,\langle{\operatorname{\mathsf{Id}},0}\rangle_{\mathsf S}\, f$ is equal to f if $i=0$ and to 0 if $i=1$ since $0\, f=0$ . The naturality follows by the fact that $\pi_{0},\pi_{1}$ are jointly monic.

Notice that if $\mathcal{L}$ has products ${X}\mathrel{\&}{Y}$ and coproducts ${X}\oplus{Y}$ , then we have

where $\left[{\iota_{0},\iota_{1}}\right]$ is the co-pairing of $\iota_{0}$ and $\iota_{1}$ , locating $\mathsf S X$ somewhere in between the coproduct and the product of X with itself. In many cases, as in coherence spaces, $\mathsf S X$ is neither the product ${X}\mathrel{\&}{X}$ nor the coproduct ${X}\oplus{X}$ .

In contrast, if $\mathcal{L}$ has biproducts, then we necessarily have $\mathsf S X={X}\mathrel{\&}{X}={X}\oplus{X}$ with obvious structural morphisms, and $\mathcal{L}$ is additive. Of course, this is not the situation we are primarily interested in!

3.1 A monad structure on $\mathsf S$

We already noticed that there is a natural transformation $\iota_{0}\in\mathcal{L}(X,\mathsf S X)$ . As also mentioned the morphisms $\pi_{i}\,\pi_{j}\in\mathcal{L}(\mathsf S^2 X,X)$ (for all $i,j\in\{0,1\}$ ) are summable so that the morphisms $\pi_{0}\,\pi_{0},\pi_{1}\,\pi_{0}+\pi_{0}\,\pi_{1}\in\mathcal{L}(\mathsf S^2X,\mathsf S X)$ are summable by Theorem 5, let $\tau=\langle{\pi_{0}\,\pi_{0},\pi_{1} \,\pi_{0}+\pi_{0} \,\pi_{1}}\rangle_{\mathsf S}\in\mathcal{L}(\mathsf S^2X,\mathsf S X)$ be the witness of this summability.

Theorem 7. The tuple $(\mathsf S,\iota_{0},\tau)$ is a monad on $\mathcal{L}$ , and we have $\tau\,\mathsf c=\tau$ .

Proof. The proof is easy and uses the fact that $\pi_{0},\pi_{1}$ are jointly monic. Let us prove that $\tau$ is natural so let $f\in\mathcal{L}(X,Y)$ , we have $\pi_{0}\,(\mathsf S f)\,\tau_{X} = f\,\pi_{0}\tau_X$ by naturality of $\pi_{0}$ and hence $\pi_{0}\,(\mathsf S f)\,\tau_{X}=f\,\pi_{0}\,\pi_{0}$ , and $\pi_{0}\,\tau_Y\,(\mathsf S^2f)= \pi_{0}\,\pi_{0}\,(\mathsf S^2f)=f\,\pi_{0}\,\pi_{0}$ by naturality of $\pi_{0}$ .

Similarly, using the naturality of $\pi_{1}$ , we have $\pi_{1}\,(\mathsf S f)\,\tau_{X} =f\,\pi_{1}\tau_X =f\,(\pi_{0}\,\pi_{1}+\pi_{1}\,\pi_{0}) =f\,\pi_{0}\,\pi_{1}+f\,\pi_{1}\,\pi_{0}$ and $\pi_{1}\,\tau_Y\,(\mathsf S^2f) =(\pi_{0}\,\pi_{1}+\pi_{1}\,\pi_{0})\,(\mathsf S^2f) =\pi_{0}\,\pi_{1}\,(\mathsf S^2f)+\pi_{1}\,\pi_{0}\,(\mathsf S^2f) =f\,\pi_{0}\,\pi_{1}+$ $f\,\pi_{1}\,\pi_{0}$ . The other naturalities are proved in the same way.

One proves $\tau_X\,\tau_{\mathsf S X}=\tau_X\,\mathsf S\tau_X$ by showing in the same manner that $\pi_{0}\,\tau_X\,\tau_{\mathsf S X}=\pi_{0}\,\pi_{0}\,\pi_{0} =\pi_{0}\,\tau_X\,\mathsf S\tau_X $ and that $\pi_{1}\,\tau_X\,\tau_{\mathsf S X}=\pi_{0}\,\pi_{0}\,\pi_{1} +\pi_{0}\,\pi_{1}\,\pi_{0} +\pi_{1}\,\pi_{0}\,\pi_{0} =\pi_{1}\,\tau_X\,\mathsf S\tau_X$ . The commutations involving $\tau$ and $\iota_{0}$ are proved in the same way. The last equation results from $\pi_{i}\,\pi_{j}\,\mathsf c=\pi_{j}\,\pi_{i}$

▸ Example 3.5. In our coherence space running example, we have ${\iota_{0}}\cdot{x}=(x,\emptyset)$ and ${\tau}\cdot{((x,u),(y,v))}=(x,u+y)$ ; notice indeed that since $((x,u),(y,v))\in\mathsf{Cl}({\mathsf S^2 E})$ we have $x+u+y+v\in\mathsf{Cl}({E})$ .

Just as in tangent categories, this monad structure will be crucial for expressing that the differential is a linear morphism.

3.2 Summable symmetric monoidal category

We assume now that $\mathcal{L}$ is a SMC, with monoidal product $\otimes$ , unit 1 and isomorphisms $\rho_X\in\mathcal{L}({X}\otimes{1},X)$ , $\lambda_X\in\mathcal{L}({1}\otimes{ }X,X)$ , $\alpha_{X_0,X_1,X_2}\in\mathcal{L}({({X_0}\otimes{X_1})}\otimes{X_2},{X_0}\otimes{({X_1}\otimes{X_2})})$ and $\gamma_{X_0,X_1}\in\mathcal{L}({X_0}\otimes{X_1},{X_1}\otimes{X_0})$ . Most often these isos will be kept implicit to simplify the presentation.

Assume that $\mathcal{L}$ is also equipped with a summability structure. We assume now that the following property holds, which expresses that the tensor distributes over the (partially defined) sum.

(S $\otimes$ -dist) If $(f_{00},f_{01})$ is a summable pair of morphisms in $\mathcal{L}(X_0,Y_0)$ and $f_1\in\mathcal{L}(X_1,Y_1)$ , then $({f_{00}}\otimes{f_1},{f_{01}}\otimes{f_1})$ is a summable pair of morphisms in $\mathcal{L}({X_0}\otimes{X_1},{Y_0}\otimes{Y_1})$ , and moreover

\begin{align*} {f_{00}}\otimes{f_1}+{f_{01}}\otimes{f_1}={(f_{00}+f_{01})}\otimes{f_1}\end{align*}

As a consequence, using the symmetry of $\otimes$ , if $(f_{00},f_{01})$ is summable in $\mathcal{L}(X_0,Y_0)$ and $(f_{10},f_{11})$ is summable in $\mathcal{L}(X_1,Y_1)$ , the family $({f_{00}}\otimes{f_{10}},{f_{00}}\otimes{f_{11}},{f_{01}}\otimes{f_{10}},{f_{01}}\otimes{f_{11}})$ is summable in $\mathcal{L}({X_0}\otimes{X_1},{Y_0}\otimes{Y_1})$ and we have

\begin{align*} {(f_{00}+f_{01})}\otimes{(f_{10}+f_{11})} ={f_{00}}\otimes{f_{10}}+{f_{00}}\otimes{f_{11}}+{f_{01}}\otimes{f_{10}}+{f_{01}}\otimes{f_{11}}\,.\end{align*}

We can define a natural transformation $\phi^1_{X_0,X_1}\in\mathcal{L}({X_0}\otimes{\mathsf S X_1},\mathsf S({X_0}\otimes{X_1}))$ by setting $\phi^1_{X_0,X_1}=\langle{{X_0}\otimes{\pi_{0}},{X_0}\otimes{\pi_{1}}}\rangle_{\mathsf S}$ which is well defined by (S $\otimes$ -dist). We use $\phi^0_{X_0,X_1}\in\mathcal{L}({\mathsf S X_0}\otimes{X_1},\mathsf S({X_0}\otimes{X_1}))$ for the natural transformation defined from $\phi^1$ using the symmetry isomorphism of the SMC, that is, $\phi^0_{X_0,X_1}=\phi^1_{X_1,X_0}\,\gamma=\langle{{\pi_{0}}\otimes{X_1},{\pi_{1}}\otimes{X_1}}\rangle_{\mathsf S}\in\mathcal{L}({\mathsf S X_0}\otimes{X_1},\mathsf S({X_0}\otimes{X_1}))$ .

Lemma 28. $\sigma\,\phi^1_{{X_0},{X_1}}={X_0}\otimes{\sigma_{X_1}}$ .

Proof. We have $\sigma\,\phi^1_{{X_0},{X_1}}={X_0}\otimes{\pi_{0}}+{X_0}\otimes{\pi_{1}}={X_0}\otimes{(\pi_{0}+\pi_{1})}$ by (S $\otimes$ -dist), and we have $\pi_{0}+\pi_{1}=\sigma_{X_1}$ .

Theorem 8. The natural transformation $\phi^1$ is a strength for the monad $(\mathsf S,\iota_{0},\tau)$ and the following diagram commutes:

Therefore, equipped with the strength $\phi^1$ , the monad $(\mathsf S,\iota_{0},\tau)$ is commutative.

Proof. The fact that $\phi^1$ is a strength means that the following two diagrams commute:

Let us prove for instance the second one. We have

The fact that $(\mathsf S,\iota_{0},\tau,\phi^1)$ is a commutative monad means that, moreover, the following diagram commutes:

which results from a stronger property, namely that, as announced, the following diagram commutes:

and from Theorem 7. This commutation is proved as follows:

We set

\begin{align*} \mathsf L_{X_0,X_1} &=\tau\,(\mathsf S\phi^0_{X_0,X_1})\,\phi^1_{\mathsf S X_0,X_1}\\ &=\tau\,(\mathsf S\phi^1_{X_0,X_1})\,\phi^0_{X_0,\mathsf S X_1}\\ &=\langle{{\pi_{0}}\otimes{\pi_{0}}, {\pi_{1}}\otimes{\pi_{0}}+{\pi_{0}}\otimes{\pi_{1}}}\rangle_{\mathsf S}\\ &\in\mathcal{L}({\mathsf S X_0}\otimes{\mathsf S X_1},\mathsf S({X_0}\otimes{X_1}))\,.\end{align*}

It is well known that in such a commutative monad situation, the associated tuple $(\mathsf S,\iota_{0},\tau,\mathsf L)$ is a symmetric monoidal monad on the SMC $\mathcal{L}$ . In particular, we will use the following equation:

(3) \begin{equation} \mathsf L\,({\mathsf S X_0}\otimes{\iota_{0}}) =\phi^0_{X_0,X_1}=\langle{{\pi_{0}}\otimes{X_1},{\pi_{1}}\otimes{X_1}}\rangle_{\mathsf S} \in\mathcal{L}({\mathsf S X_0}\otimes{X_1},\mathsf S({X_0}\otimes{X_1}))\end{equation}

and symmetrically for $\mathsf L\,({\iota_{0}}\otimes{\mathsf S X_1})$ .

Definition 29. When the summability structure of the SMC $\mathcal{L}$ satisfies (S $\otimes$ -dist), we say that $\mathcal{L}$ is a summable SMC.

4. Differentiation in a Summable Resource Category

We have now enough material about our summability structures to be able to introduce coherent differentiation. As in differential ${\textsf{LL}}$ , differentiation will be associated with a resource modality we assume our category to be equipped with.

4.1 Differential structure

Definition 30. A resource category $\mathcal{L}$ (see Section 2.3) is a summable resource category if it is a summable SMC and satisfies the following additional condition of compatibility with the cartesian product.

(S $\mathrel{\&}$ -pres) The functor $\mathsf S$ preserves all finite cartesian products. In other words, the morphisms $0\in\mathcal{L}(\mathsf S\top,\top)$ and $\langle{\mathsf S{\mathsf{pr}_{0}},\mathsf S{\mathsf{pr}_{1}}}\rangle\in\mathcal{L}(\mathsf S({X_0}\mathrel{\&}{X_1}), {\mathsf S{X_0}}\mathrel{\&}{\mathsf S{X_1}})$ are isos.

A differential structure on a summable resource category $\mathcal{L}$ consists of a natural transformation $\partial_X\in\mathcal{L}(\ !{\mathsf S X},\mathsf S\ !{X})$ which satisfies the following conditions:

Remark 31. This condition is required only for $\pi_{0}$ and not for $\pi_{1}$ . In some sense, it is only with the differential structure that we start breaking the symmetry between the “two sides” of the $\mathsf S$ functor. Notice that the definition of the monad structure of $\mathsf S$ in Section 3.1 has the same kind of asymmetry, but it is not a condition on the categorical structure, just a construction.

It is standard that this condition allows one to extend (in the sense of Power and Watanabe 2002, Definition 4.5) the functor $\ !{\_}$ to the Kleisli category $\mathcal{L}_{\mathsf S}$ of the monad $\mathsf S$ . In this Kleisli category, a morphism $X\to Y$ can be seen as a pair $(f_0,f_1)$ of two summable morphisms in $\mathcal{L}(X,Y)$ , and composition is defined by $g\mathrel\circ f=(g_0\, f_0,g_1\, f_0+g_0\, f_1)$ , a definition which is very reminiscent of the multiplication of dual numbers.

This condition allows us to extend the functor $\mathsf S$ to the Kleisli category ${\mathcal L}_!$ . We obtain in that way the functor $\widetilde{\mathsf D}:{\mathcal L}_!\to{\mathcal L}_!$ defined as follows: on objects, we set $\widetilde{\mathsf D} X=\mathsf S X$ . Next, given $f\in{\mathcal L}_!(X,Y)=\mathcal{L}(\ !{X},Y)$ , the morphism $\widetilde{\mathsf D} f\in{\mathcal L}_!(\mathsf S X,\mathsf S Y)=\mathcal{L}(\ !{\mathsf S X},\mathsf S Y)$ is defined by $\widetilde{\mathsf D} f=(\mathsf S f)\,\partial_X$ . The purpose of the two commutations is precisely to make this operation functorial, and this functoriality is a categorical version of the chain rule of calculus, exactly as in tangent categories since, as we will see, this functor $\widetilde{\mathsf D}$ essentially computes the derivative of f.

In other words, we have explicit expressions for $\partial_\top$ and $\partial_{{X_0}\mathrel{\&}{X_1}}$ :

(4)

(5)

Theorem 9. (Leibniz rule). If ( $\partial$ - $\mathord{\mathrel{\&}}$ ) holds then the following diagrams commute.

Proof. This is an easy consequence of the naturality of $\partial$ and of the definition of $\operatorname{\mathsf{weak}}_{X}$ and $\operatorname{\mathsf{contr}}_{X}$ which is based on the cartesian products and on the Seely isomorphisms.

This diagram, involves the canonical flip $\mathsf c$ and expresses a kind of commutativity of the second derivative.

Definition 32. A differentiation in a summable resource category $\mathcal{L}$ is a natural transformation $\partial_X\in\mathcal{L}(\ !{\mathsf S X},\mathsf S\ !{X})$ which satisfies ( $\partial$ -local), ( $\partial$ -lin), ( $\partial$ -chain), ( $\partial$ - $\mathord{\mathrel{\&}}$ ), and ( $\partial$ -Schwarz). A summable resource category given together with a differentiation is a differential summable resource category.

We assume that $\mathcal{L}$ is a differential summable resource category.

4.2 Derivatives and partial derivatives in the Kleisli category

The Kleisli category ${\mathcal L}_!$ of the comonad $(\ !{},\operatorname{\mathsf{der}}_{},\operatorname{\mathsf{dig}}_{}\ !)$ is well known to be cartesian, where we use “ $\mathrel\circ$ ” for the composition of morphisms. In general, it is not a differential cartesian category in the sense of Alvarez-Picallo and Lemay (2020) because it is not required to be left additive. We postpone the precise axiomatization of this kind of partially additive ⁶ Our running example of coherence spaces is an example of such a category which is not a differential category.

There is an inclusion functor $\operatorname{\mathsf{Der}}:\mathcal{L}\to{\mathcal L}_!$ which maps X to X and $f\in\mathcal{L}(X,Y)$ to $f\,\operatorname{\mathsf{der}}_{X}\in{\mathcal L}_!(X,Y)$ , and it is faithful but not full in general and allows us to see any morphism of $\mathcal{L}$ as a “linear morphism” of ${\mathcal L}_!$ .

We have already mentioned the functor $\widetilde{\mathsf D}:{\mathcal L}_!\to{\mathcal L}_!$ , remember that $\widetilde{\mathsf D} X=\mathsf S X$ and $\widetilde{\mathsf D} f=(\mathsf S f)\,\partial_X$ when $f\in{\mathcal L}_!(X,Y)$ . Then we have $\widetilde{\mathsf D}\mathrel\circ\operatorname{\mathsf{Der}}=\operatorname{\mathsf{Der}}\mathrel\circ\mathsf S$ which allows us to extend simply the monad structure of $\mathsf S$ to $\widetilde{\mathsf D}$ by setting $\zeta_X=\operatorname{\mathsf{Der}}{\iota_{0}}\in{\mathcal L}_!(X,\widetilde{\mathsf D} X)$ and $\theta_X=\operatorname{\mathsf{Der}}{\tau}\in{\mathcal L}_!(\widetilde{\mathsf D}^2 X,\widetilde{\mathsf D} X)$ .

Theorem 10. The morphisms $\zeta_X\in{\mathcal L}_!(X,\widetilde{\mathsf D} X)$ and $\theta_X\in{\mathcal L}_!(\widetilde{\mathsf D}^2X,\widetilde{\mathsf D} X)$ are natural and turn the functor $\widetilde{\mathsf D}$ into a monad on ${\mathcal L}_!$ .

Proof. This result can be seen as a consequence of Corollary 4.9 of Power and Watanabe (2002), we provide the proof for convenience. The only non-obvious property is naturality, the monadic diagram commutations resulting from those of $(\mathsf S,\iota_{0},\sigma)$ on $\mathcal{L}$ and of the functoriality of $\operatorname{\mathsf{Der}}$ . Let $f\in{\mathcal L}_!(X,Y)$ , that is, $f\in\mathcal{L}(\ !{X},Y)$ . We must first prove that $\widetilde{\mathsf D} f\mathrel\circ\zeta_X=\zeta_Y\mathrel\circ f$ . We have

Similarly,

Since $\mathsf S$ preserves cartesian products, we can equip easily this monad $(\widetilde{\mathsf D},\zeta,\theta)$ on ${\mathcal L}_!$ with a commutative strength $\psi^1_{X_0,X_1}\in{\mathcal L}_!({X_0}\mathrel{\&}{\widetilde{\mathsf D}{X_1}},\widetilde{\mathsf D}{\left({X_0}\mathrel{\&}{X_1}\right)})$ which is the following composition in $\mathcal{L}$ :

where $\eta={\langle{\mathsf S{\mathsf{pr}_{0}},\mathsf S{\mathsf{pr}_{1}}}\rangle}^{-1}$ is the canonical iso of (S $\mathrel{\&}$ -pres).

Given $f\in{\mathcal L}_!({X_0}\mathrel{\&}{X_1},Y)$ , we can define the partial derivatives $\widetilde{\mathsf D}_0f\in{\mathcal L}_!({\widetilde{\mathsf D} X_0}\mathrel{\&}{X_1},\widetilde{\mathsf D} Y)$ and $\widetilde{\mathsf D}_1f\in{\mathcal L}_!({X_0}\mathrel{\&}{\widetilde{\mathsf D} X_1},\widetilde{\mathsf D} Y)$ as $\widetilde{\mathsf D} f\mathrel\circ\psi^0$ and $\widetilde{\mathsf D} f\mathrel\circ\psi^1$ where we use $\psi^0$ for the strength ${\widetilde{\mathsf D} X_0}\mathrel{\&}{X_1}\to\widetilde{\mathsf D}\left({X_0}\mathrel{\&}{X_1}\right)$ defined from $\psi^1$ using the symmetry of $\mathrel{\&}$ . We have

In other words, $\widetilde{\mathsf D}_0f$ is fully characterized by the two following equations:

(6)

(7)

and of course there are symmetric equations characterizing $\widetilde{\mathsf D}_1f$ .

Remark 33. (Connection with differential categories) Not surprisingly, any resource category which is a model of differential ${\textsf{LL}}$ (see Blute et al. 2020; Ehrhard 2018; Fiore 2007) and is therefore additive and has biproducts is a differential summable category (in the sense of Definition 32). It suffices to take $\mathsf S X={X}\mathrel{\&}{X}={X}\oplus{X}$ (identifying products and coproducts to the biproduct) with morphisms $\pi_{0},\pi_{1},\sigma$ defined in the obvious way and to define

\begin{align*} \partial_X=\langle{d_0,d_1}\rangle:\ !{\left({X}\mathrel{\&}{X}\right)}\to{\ !{X}}\mathrel{\&}{\ !{X}}\end{align*}

where $d_0=\ !{\mathsf{pr}_{0}}$ and $d_1$ is the following composition of morphisms:

where $\operatorname{\overline{\mathsf{der}}}_{X}:X\to\ !{X}$ is the codereliction morphism and $\operatorname{\overline{\mathsf{contr}}}_{X}$ is the cocontraction morphism of the differential ${\textsf{LL}}$ model structure.

This fact has been proven in Spring 2021 by Aymeric Walch during his Master Internship and the proof will be made available soon.

4.3 Deciphering the diagrams

After this rather terse list of categorical axioms, it is fair to provide the reader with intuitions about their mathematical meaning; this is the purpose of this section.

One should think of the objects of $\mathcal{L}$ as partial commutative monoids (with additional structures depending on the considered category), and $\mathsf S X$ as the object of pairs (x,u) of elements $x,u\in X$ such that $x+u\in X$ is defined. The morphisms in $\mathcal{L}$ are linear in the sense that they preserve 0 and these partially defined sums, whereas the morphisms of ${\mathcal L}_!$ should be thought of as functions which are not linear but admit a “derivative.” More precisely, $f\in{\mathcal L}_!(X,Y)$ can be seen as a function $X\to Y$ and, given $(x,u)\in\mathsf S X$ we have

\begin{align*} \widetilde{\mathsf D} f(x,u)=(f(x),\frac{d{f(x)}}{d{x}}\cdot{u})\in\mathsf S Y\,,\end{align*}

where $\frac{d{f(x)}}{d{x}}\cdot{u}$ is just a notation for the second component of the pair $\widetilde{\mathsf D} f(x,u)$ which, by construction, is such that the sum $f(x)+\frac{d{f(x)}}{d{x}}\cdot{u}$ is a well-defined element of Y. Now we assume that this derivative $\frac{d{f(x)}}{d{x}}\cdot{u}$ obeys the standard rules of differential calculus, and we will see that the above axioms about $\partial$ correspond to these rules.

Remark 34. The equations we are using in this section as intuitive justifications for the diagrams of Section 4.1 refer to the standard laws and properties of the differential calculus that we assume the reader to be acquainted with. They do hold exactly as written here in the model $\mathbf{Pcoh}$ where derivatives are computed as in calculus as we will show in a forthcoming paper.

Remark 35. We use the well-established notation $\frac{d{f(x)}}{d{x}}\cdot{u}$ which must be understood properly: in particular, the expression $\frac{d{f(x)}}{d{x}}\cdot{u}$ is a function of x (the point where the derivative is computed) and of u (the linear parameter of the derivative). When required we use $\frac{d{f(x)}}{d{x}}(x_0)\cdot{u}$ for the evaluation of this derivative at point $x_0\in X$ .

• ( $\partial$ -local) means that the first component of $\widetilde{\mathsf D} f(x,u)$ is f(x), justifying our intuitive notation:

  \begin{align*} \widetilde{\mathsf D} f(x,u)=(f(x),\frac{d{f(x)}}{d{x}}\cdot{u})\in\mathsf S Y. \end{align*}

• The first diagram of ( $\partial$ -chain) means that if $f\in{\mathcal L}_!(X,Y)$ is linear ⁷ in the sense that there is $g\in\mathcal{L}(X,Y)$ such that $f=g\,\operatorname{\mathsf{der}}_{X}=\operatorname{\mathsf{Der}} g$ , then $\frac{d{f(x)}}{d{x}}\cdot{u}=f(u)$ . Notice that it prevents differentiation from being trivial by setting $\frac{d{f(x)}}{d{x}}\cdot{u}=0$ for all f and all x,u. Consider now $f\in{\mathcal L}_!(X,Y)$ and $g\in{\mathcal L}_!(Y,Z)$ ; the second diagram means that $\widetilde{\mathsf D}(g\mathrel\circ f)=\widetilde{\mathsf D} g\mathrel\circ\widetilde{\mathsf D} f$ , which amounts to

  \begin{align*} \frac{d{g(f(x))}}{d{x}}\cdot{u}=\frac{d{g(y)}}{d{y}}(f(x))\cdot{(\frac{d{f(x)}}{d{x}}\cdot{u})} \end{align*}

  which is exactly the chain rule.

• The “second derivative” $\widetilde{\mathsf D}^2f\in{\mathcal L}_!(\mathsf S^2X,\mathsf S^2Y)$ of $f\in{\mathcal L}_!(X,Y)$ is $(\mathsf S^2f)\,(\mathsf S\partial_X)\,\partial_{\mathsf S X}$ . Remember that $\widetilde{\mathsf D} f(x,u)=(f(x),\frac{d{f(x)}}{d{x}}\cdot{u})$ , therefore applying the standard rules of differential calculus we have

  \begin{align*} \widetilde{\mathsf D}^2f((x,u),(x',u')) &=(\widetilde{\mathsf D} f(x,u),\frac{d{\widetilde{\mathsf D} f(x,u)}}{d{(x,u)}}\cdot{(x',u')})\\ &=((f(x),\frac{d{f(x)}}{d{x}}\cdot{u}),\frac{\partial{(f(x), \frac{d{f(x)}}{d{x}}\cdot{u})}}{\partial{x}}\cdot{x'}+\frac{\partial{(f(x), \frac{d{f(x)}}{d{x}}\cdot{u})}}{\partial{u}}\cdot{u'})\\ &=((f(x),\frac{d{f(x)}}{d{x}}\cdot{u}),(\frac{d{f(x)}}{d{x}}\cdot{x'}, \frac{d^{2}{f(x)}}{d{x}^{2}}\cdot{(u,x')}+\frac{d{f(x)}}{d{x}}\cdot{u'})) \end{align*}

  where we have used the fact that f(x) does not depend on u and that $\frac{d{f(x)}}{d{x}}\cdot{u}$ is linear in u. We have used ( $\partial$ -lin) to prove Theorem 10 whose main content is the naturality of $\zeta$ and $\theta$ . This second naturality means that $\widetilde{\mathsf D} f\mathrel\circ\theta_X=\theta_Y\mathrel\circ\widetilde{\mathsf D}^2f$ , that is, by the computation above $\frac{d{f(x)}}{d{x}}\cdot{(u+x')}=\frac{d{f(x)}}{d{x}}\cdot{u}+\frac{d{f(x)}}{d{x}}\cdot{x'}$ since, intuitively, $\theta_X((x,u),(x',u'))=(x,u+x')$ . Similarly, the naturality of $\zeta$ means that $\frac{d{f(x)}}{d{x}}\cdot{0}=0$ . So the condition ( $\partial$ -lin) means that the derivative is a function which is linear with respect to its second parameter.

• We have assumed that $\mathcal{L}$ is cartesian and hence ${\mathcal L}_!$ is also cartesian. Intuitively, ${X_0}\mathrel{\&}{X_1}$ is the space of pairs $(x_0,x_1)$ with $x_i\in X_i$ , and our assumption (S $\mathrel{\&}$ -pres) means that $\mathsf S\left({X_0}\mathrel{\&}{X_1}\right)$ is the space of pairs $((x_0,x_1),(u_0,u_1))$ such that $(x_i,u_i)\in\mathsf S X_i$ , and the sum of such a pair is $(x_0+u_0,x_1+u_1)\in {X_0}\mathrel{\&}{X_1}$ . Then, given $f\in{\mathcal L}_!({X_0}\mathrel{\&}{X_1},Y)$ the second diagram of ( $\partial$ - $\mathord{\mathrel{\&}}$ ) means that

  \begin{align*} \frac{d{f(x_0,x_1)}}{d{(x_0,x_1)}}\cdot{(u_0,u_1)} =\frac{\partial{f(x_0,x_1)}}{\partial{x_0}}\cdot{u_0}+\frac{\partial{f(x_0,x_1)}}{\partial{x_1}}\cdot{u_1} \end{align*}

  which can be seen by the following computation of $\pi_{1}\,\widetilde{\mathsf D} f$ :

  

  Then Theorem 9 means that $\frac{d{f(x,x)}}{d{x}}\cdot{u} =\frac{\partial{f(x_0,x_1)}}{\partial{x_0}}(x,x)\cdot{u}+\frac{\partial{f(x_0,x_1)}}{\partial{x_1}}(x,x)\cdot{u}$ which is the essence of the Leibniz rule of calculus.

• The object $\mathsf S^2 X$ consists of pairs ((x,u),(x’,u’)) such that x, u, x’ and u’ are globally summable. Then $\mathsf c\in\mathcal{L}(\mathsf S^2X,\mathsf S^2X)$ maps ((x,u),(x’,u’)) to ((x,x’),(u,u’)). Therefore, using the same computation of $\widetilde{\mathsf D}^2f((x,u),(x',u'))$ as in the case of ( $\partial$ -lin), we see that ( $\partial$ -Schwarz) expresses that $\frac{d^{2}{f(x)}}{d{x}^{2}}\cdot{(u,x')}=\frac{d^{2}{f(x)}}{d{x}^{2}}\cdot{(x',u)}$ (upon taking $u'=0$ ). So this diagram means that the second derivative is a symmetric bilinear function, a property of sufficiently regular differentiable functions often referred to as Schwarz Theorem.

4.4 A differentiation in coherence spaces

Now we exhibit such a differentiation in $\mathbf{Coh}$ . We define $\ !{E}$ as follows: ${}|{\ !{E}}{}|$ is the set of finite multisets ⁸ m of elements of ${}|{E}{}|$ such that $\operatorname{\mathsf{supp}}({m})\in\mathsf{Cl}({E})$ (such an m is called a finite multiclique). Given $m_0,m_1\in{}|{\ !{E}}{}|$ , we have if $m_0+ m_1\in{}|{\ !{E}}{}|$ . This operation is a functor $\mathbf{Coh}\to\mathbf{Coh}$ : given $s\in\mathbf{Coh}(E,F)$ one sets

\begin{align*} \ !{s}= \{([{a_{1},\dots,a_{n}}],[{b_{1},\dots,b_{n}}])\mid n\in{\mathbb{N}},\ (a_i,b_i)\in s \text{ for }i=1,\dots,n\text{ and }[{a_{1},\dots,a_{n}}]\in{}|{\ !{E}}{}|\}\end{align*}

which actually belongs to $\mathsf{Cl}({{\ !{E}}\multimap{\ !{F}}})$ because $s\in\mathsf{Cl}({{E}\multimap{F}})$ . The comonad structure of this functor and the associated commutative comonoid structure are given by:

• $\operatorname{\mathsf{der}}_{E}=\{([{a}],a)\mid a\in{}|{E}{}|\}$

• $\operatorname{\mathsf{dig}}_{E}=\{(m,[{m_1,\dots,m_n}])\in{}|{{\ !{E}}\multimap{\ !\ !{E}}}{}|\mid m=m_1+\cdots+ m_n\}$

• $\operatorname{\mathsf{weak}}_{E}=\{([\,],\ast)\}$

• and $\operatorname{\mathsf{contr}}_{E}=\{(m,(m_1,m_2))\in{}|{{\ !{E}}\multimap{({\ !{E}}\otimes{\ !{E}})}}{}|\mid m=m_1+ m_2\}$ .

Composition in ${\mathbf{Coh}}_!$ can be described directly as follows: let $s\in\mathsf{Cl}({{\ !{E}}\multimap{F}})$ and $t\in\mathsf{Cl}({{\ !{F}}\multimap{G}})$ , then $t\mathrel\circ s\in\mathcal{L}{\left({\ !{E}}\multimap{G}\right)}$ is $\{(m,c)\in{}|{{\ !{E}}\multimap{G}}{}|\mid\exists n\in{\mathbb{N}}\,\exists (m_1,b_1),\dots,(m_n,b_n)\in s\ m_1+\cdots+m_n=m\text{ and }([{b_{1},\dots,b_{n}}],c)\in t\}$ . A morphism $s\in{\mathbf{Coh}}_!(E,F)$ induces a function $\widehat{s}:\mathsf{Cl}({E})\to\mathsf{Cl}({F})$ by $\widehat{s}(x)=\{b\mid\exists m\in\mathcal M_{{\mathrm{fin}}}({x})\ (m,b)\in s\}$ . The functions $f:\mathsf{Cl}({E})\to\mathsf{Cl}({F})$ definable in that way are exactly the stable functions: f is stable if for any $x\in\mathsf{Cl}({E})$ and any $b\in f(x)$ there is exactly one minimal subset $x_0$ of x such that $b\in f(x_0)$ , and moreover this $x_0$ is finite. When moreover this $x_0$ is always a singleton f is said to be linear and such linear functions are in bijection with $\mathbf{Coh}(E,F)$ (given $t\in\mathbf{Coh}(E,F)$ , and the associated linear function $\mathsf{Cl}({E})\to\mathsf{Cl}({F})$ is the map $x\mapsto{t}\cdot{x}$ ).

Notice that for a given stable function $f:\mathsf{Cl}({E})\to\mathsf{Cl}({F})$ , there can be infinitely many $s\in{\mathbf{Coh}}_!(E,F)$ such that $f=\widehat{s}$ since the definition of $\widehat{s}$ does not take into account the multiplicities in the multisets m such that $(m,b)\in s$ . For instance, if $a\in{}|{E}{}|$ and $b\in{}|{F}{}|$ then $\{([{a}],b)\}$ and $\{([{a,a}],b)\}$ define exactly the same stable (actually linear) function.

Up to trivial iso we have ${}|{\ !{\mathsf S E}}{}|=\{(m_0,m_1)\in{}|{\ !{E}}{}|\mid \operatorname{\mathsf{supp}}({m_0})\cap\operatorname{\mathsf{supp}}({m_1})=\emptyset\text{ and }m_0+ m_1\in{}|{\ !{E}}{}|\}$ and if $m_{00}+ m_{01}+ m_{10}+ m_{11}\in{}|{\ !{X}}{}|$ and $\operatorname{\mathsf{supp}}({m_{00}+ m_{10}})\cap\operatorname{\mathsf{supp}}({m_{01}+ m_{11}})=\emptyset$ . With this identification, we define $\partial_E\subseteq{}|{{\ !{\mathsf S E}}\multimap{\mathsf S{\ !{E}}}}{}|$ as follows:

(8)

We think useful to check directly that $\partial_E\in\mathbf{Coh}(\ !{\mathsf S E},\mathsf S{\ !{E}})$ although this checking is not necessary since we will see in Section 5.6 that this property results from a much simpler one. Let $((m_{j0},m_{j1}),(i_j,m_j))\in\partial_E$ for $j=0,1$ and assume that

(9)

By symmetry, there are three cases to consider.

• If $i_0=i_1=0$ then, we have $m_{j1}=[\,]$ and $m_{j0}=m_j$ for $j=0,1$ . Then, we have by our assumption (9), and if $(0,m_0)=(0,m_1)$ then $(m_{00},m_{01})=(m_{10},m_{11})$ .

• Assume now that $i_0=i_1=1$ . We have $m_{j1}=[{a_j}]$ for $a_j\in{}|{E}{}|$ , with $a_j\notin \operatorname{\mathsf{supp}}({m_{j0}})$ and $m_{j}=m_{j0}+[{a_j}]$ . Our assumption (9) means that $m_{00}+ m_{10}+[{a_0,a_1}]\in{}|{\ !{E}}{}|$ and $\operatorname{\mathsf{supp}}({m_{00}+ m_{10}})\cap\{a_0,a_1\}=\emptyset$ . Therefore, $m_0+ m_1\in{}|{\ !{E}}{}|$ and hence . Assume moreover that $m_0=m_1$ , that is, $m_{00}+[{a_0}]=m_{10}+[{a_1}]$ . This implies $m_{00}=m_{10}$ and $a_0=a_1$ since we know that $a_1\notin \operatorname{\mathsf{supp}}({m_{00}})$ and $a_0\notin \operatorname{\mathsf{supp}}({m_{10}})$ .

• Last assume that $i_0=1$ and $i_1=0$ . So we have $m_{01}=[{a}]$ with $a\notin \operatorname{\mathsf{supp}}({m_{00}})$ and $m_0=m_{00}+[{a}]$ ; $m_{11}=[\,]$ and $m_1=m_{10}$ . By (9), we know that $\operatorname{\mathsf{supp}}({m_0+ m_1})\in\mathsf{Cl}({\ !{E}})$ . Coming back to the definition of the coherence in $\mathsf S F$ (for a coherence space F), we must also prove that $m_0\not=m_1$ : this results from (9) which entails that $a\notin \operatorname{\mathsf{supp}}({m_1})=m_{10}$ , whereas we know that $a\in \operatorname{\mathsf{supp}}({m_0})$ .

We do not prove the required commutations for the already mentioned reason that they will be reduced in Section 5.6 to a much simpler verification.

Given $x\in\mathsf{Cl}({E})$ , we can define a coherence space $E_x$ (the local sub-coherence space at x) as follows: ${}|{E_x}{}|=\{a\in{}|{E}{}|\setminus x\mid x\cup\{a\}\in\mathsf{Cl}({X})\}$ and if . Then, given $s\in{\mathbf{Coh}}_!(E,F)$ , we can define the differential of s at x as:

\begin{align*} \frac{d s(x)}{d x} =\{(a,b)\in{}|{E_x}{}|\times{}|{F}{}|\mid\exists m\in{}|{\ !{E}}{}|\ (m+[{a}],b)\in s\text{ and } \operatorname{\mathsf{supp}}({m})\subseteq x\} \subseteq{}|{{E_x}\multimap{Y}}{}|\,.\end{align*}

Theorem 11. Let $s\in{\mathbf{Coh}}_!(E,F)$ . Then $\widetilde{\mathsf D} s\in{\mathbf{Coh}}_!(\mathsf S E,\mathsf S F)$ satisfies

\begin{align*} \forall (x,u)\in\mathsf{Cl}({\mathsf S E}) \widehat{\widetilde{\mathsf D} s}(x,u)=(\widehat{s}(x),{\frac{d s(x)}{d x}}\cdot{u}) \end{align*}

Proof. Let $(x,u)\in\mathsf{Cl}({\mathsf S E})$ and $(i,b)\in{}|{\mathsf S F}{}|$ with $i\in\{0,1\}$ and $b\in{}|{F}{}|$ . We have $(i,b)\in\widehat{\widetilde{\mathsf D} s}(x,u)$ iff there is $(m_0,m_1)\in{}|{\ !{\mathsf S E}}{}|$ such that $\operatorname{\mathsf{supp}}({m_0})\subseteq x$ , $\operatorname{\mathsf{supp}}({m_1})\subseteq u$ and $((m_0,m_1),(i,b))\in\widetilde{\mathsf D} s=\partial_E\,\mathsf S s$ . This latter condition holds iff

either $i=0$ , $m_1=[\,]$ , and $(m_0,b)\in s$ ,

or $i=1$ , $m_1=[{a}]$ for some $a\in{}|{E}{}|\setminus\operatorname{\mathsf{supp}}({m_0})$ such that $m_0+[{a}]\in\mathsf{Cl}({E})$ , and $(m_0+[{a}],b)\in s$ .

Assume first that $(i,b)\in \widehat{\widetilde{\mathsf D} s}(x,u)$ and let $(m_0,m_1)$ be as above. If $i=0$ , we have $(m_0,b)\in s$ and $\operatorname{\mathsf{supp}}({m})_0\subseteq x$ and hence $b\in\widehat{s}(x)$ , that is $(i,b)\in(\widehat{s}(x),{\frac{d s(x)}{d x}}\cdot{u})$ . If $i=1$ let $a\in{}|{E}{}|\setminus\operatorname{\mathsf{supp}}({m_0})$ be such that $m_1=[{a}]$ , $m_0+[{a}]\in{}|{\ !{E}}{}|$ , $(m_0+[{a}],b)\in s$ and $\operatorname{\mathsf{supp}}({m_0,[{a}]})\subseteq(x,u)$ (remember that we consider the elements of $\mathsf{Cl}({\mathsf S E})$ as pairs of cliques), that is $\operatorname{\mathsf{supp}}({m_0})\subseteq x$ and $a\in u$ . Then we know that $a\in{}|{E_x}{}|$ since $x\cup u\in\mathsf{Cl}({E})$ and $x\cap u=\emptyset$ . Therefore, $(i,b)\in(\widehat{s}(x),{\frac{d s(x)}{d x}}\cdot{u})$ .

We have proven $\widehat{\widetilde{\mathsf D} s}(x,u)\subseteq(\widehat{s}(x),{\frac{d s(x)}{d x}}\cdot{u})$ , and we prove the converse inclusion. Let $(i,b)\in (\widehat{s}(x),{\frac{d s(x)}{d x}}\cdot{u})$ . If $i=0$ , we have $b\in \widehat{s}(x)$ , and hence there is a uniquely defined $m_0\in{}|{\ !{E}}{}|$ such that $\operatorname{\mathsf{supp}}({m_0})\subseteq x$ and $(m_0,b)\in s$ . It follows that $((m_0,[\,]),(0,b))\in\partial_E\,\mathsf S s$ and hence $(i,b)\in \widehat{\widetilde{\mathsf D} s}(x,u)$ . Assume now that $i=1$ so that $b\in{\frac{d s(x)}{d x}}\cdot{u}$ , and hence there is $a\in u$ (which implies $a\notin x$ ) such that $(a,b)\in\frac{d s(x)}{d x}$ . So there is $m_0\in{}|{\ !{E}}{}|$ such that $\operatorname{\mathsf{supp}}({m_0})\subseteq x$ and $(m_0+[{a}],b)\in s$ (notice that $a\notin\operatorname{\mathsf{supp}}({m_0})$ since $\operatorname{\mathsf{supp}}({m_0})\subseteq x$ and $a\notin x$ ). It follows that $((m_0,[{a}]),(1,m_0+[{a}]))\in\partial_E$ and hence $((m_0,[{a}]),(1,b))\in (\mathsf S s)\,\partial_E$ so that $(1,b)\in\widehat{\widetilde{\mathsf D} s}(x,u)$ .

Remark 36. The definition of $\widetilde{\mathsf D} s$ depends on s and not only on $\widehat{s}$ : for instance if $s=\{([{a}],b)\}$ then $\widetilde{\mathsf D} s=\{(([{a}],[\,]),(0,b)),(([\,],[{a}]),(1,b))\}$ and if $s'=\{([{a,a}],b)\}$ then $\widetilde{\mathsf D} s'=\{(([{a,a}],[\,]),(0,b))\}$ ; in that case the derivative vanishes, whereas $\widehat{s}=\widehat{s'}$ are the same function.

Remark 37. Theorem 11 shows in particular that $\frac{d s(x)}{d x}\in\mathbf{Coh}(E_x,F_{\widehat{s}(x)})$ since $\frac{d s(x)}{d x}=\pi_{1}\mathrel\circ\widetilde{\mathsf D} f\mathrel\circ\iota_{1}$ and also that this derivative is stable with respect to the point x where it is computed, and thus differentiation of stable functions can be iterated. However, Remark 36 indicates a peculiarity of this derivative which has as a consequence that the morphisms in ${\mathbf{Coh}}_!$ do not coincide with their Taylor expansion that one can define using this iteration of derivatives (the expansion of s is s whereas the expansion of s’ is $\emptyset$ ).

This is an effect of the uniformity of the construction $\ !{E}$ , that is, of the fact that for $m\in\mathcal M_{{\mathrm{fin}}}({{}|{E}{}|})$ to be in ${}|{\ !{E}}{}|$ , it is required that $\operatorname{\mathsf{supp}}({m})$ be a clique. Indeed, it is only because of this uniformity requirement in the definition of $\ !{E}$ that a coherence space E can be defined by means of a reflexive coherence relation (or an antireflexive strict coherence relation ) in the sense that one cannot define, in these coherence spaces, a resource modality $\ !{E}$ such that ${}|{\ !{E}}{}|=\mathcal M_{{\mathrm{fin}}}({{}|{E}{}|})$ . But an effect of this simplicity in the axiomatization of coherence is that the summability of two cliques requires their disjointedness, and a consequence of this is the slightly unsatisfactory behavior of differentiation explained in Remark 36. Do well notice however that this peculiarity does not prevent coherence spaces from satisfying all of our new axioms of summability and differentiation.

This can be remedied, without breaking the main feature of our construction, namely that it is compatible with the determinism ⁹ of the model, by using nonuniform coherence spaces instead, where it becomes possible to take ${}|{\ !{E}}{}|=\mathcal M_{{\mathrm{fin}}}({E})$ , see Bucciarelli and Ehrhard (2001), Boudes (2011), but where the coherence relation is no more necessarily reflexive (nor antireflexive), see Section 6.1.

5. Elementarily Summable Categories

The concept of summable category applies typically to models of ${\textsf{LL}}$ in the sense of Seely (see Melliès 2009): such a model is based on an SMC $\mathcal{L}$ whose morphisms are intuitively considered as linear, and the summability structure makes this linearity more explicit. In most known models of ${\textsf{LL}}$ featuring the above described coherent differential structure ¹⁰ – typically (probabilistic) coherence spaces, the summability structure boils down to a more basic structure which is always present in such a model: the functor $\mathsf S X$ is defined on objects by:

\[ \mathsf S X=\left({{1}\mathrel{\&}{1}}\multimap{X}\right),\]

and similarly for morphisms. A priori, given a categorical model of ${\textsf{LL}}$ $\mathcal{L}$ , this functor does not necessarily define a summability structure. The purpose of this section is to examine under which conditions this is the case and to express the differential structure introduced above in this particular and important setting.

Let $\mathcal{L}$ be a cartesian ¹¹ SMC where the object $\mathbb D={1}\mathrel{\&}{1}$ is exponentiable, that is, the functor $\overline{\mathsf S}_\mathbb D:X\mapsto{X}\otimes{\mathbb D}$ has a right adjoint $\mathsf S_{\mathbb D}:X\mapsto\left({\mathbb D}\multimap{X}\right)$ . We use $\operatorname{\mathsf{ev}}\in\mathcal{L}({({\mathbb D}\multimap{X})}\otimes{\mathbb D},X)$ for the corresponding evaluation morphism and, given $f\in\mathcal{L}({Y}\otimes{\mathbb D}, X)$ we use $\operatorname{\mathsf{cur}} f$ for the associated Curry transpose of f which satisfies $\operatorname{\mathsf{cur}} f\in\mathcal{L}(Y,{\mathbb D}\multimap{ }X)$ . Being a right adjoint, $\mathsf S_{\mathbb D}$ preserves all limits existing in $\mathcal{L}$ (and in particular the cartesian product).

We will use the construction provided by the following lemma.

Lemma 38. Let $\varphi\in\mathcal{L}(1,\mathbb D)$ . For any object X of $\mathcal{L}$ let $\mathsf{nt}(\varphi)_X\in\mathcal{L}({\mathbb D}\multimap{ }X,X)$ be the following composition of morphisms:

Then $(\mathsf{nt}(\varphi)_X)_{X\in\mathcal{L}}$ is a natural transformation.

Let $f\in\mathcal{L}({Y}\otimes{\mathbb D},X)$ , so that $\operatorname{\mathsf{cur}} f\in\mathcal{L}(Y,{\mathbb D}\multimap{ }X)$ . Then one has

\begin{align*} \mathsf{nt}(\varphi)_X\,(\operatorname{\mathsf{cur}} f)=f\,({Y}\otimes{\varphi})\,{\rho_Y}^{-1} \in\mathcal{L}(Y,X)\,. \end{align*}

Proof. Naturality results from the naturality of $\rho$ and functoriality of ${\mathbb D}\multimap{\_}$ . Let us prove the second part of the lemma, we have

For $i=0,1$ we have a morphism $\overline\pi_{i}\in\mathcal{L}(1,\mathbb D)$ given by $\overline\pi_{0}=\langle{\operatorname{\mathsf{Id}}_1,0}\rangle$ and $\overline\pi_{1}=\langle{0,\operatorname{\mathsf{Id}}_1}\rangle$ . We also have a diagonal morphism $\Delta=\langle{\operatorname{\mathsf{Id}}_1,\operatorname{\mathsf{Id}}_1}\rangle\in\mathcal{L}(1,\mathbb D)$ . Using these, we define the following natural transformations $\mathsf S_{\mathbb D} X\to X$ :

\begin{align*} \pi_{i}&=\mathsf{nt}(\overline\pi_{i})\text{ for }i=0,1\\ \sigma&=\mathsf{nt}(\Delta)\,.\end{align*}

Definition 39. The category $\mathcal{L}$ is elementarily summable if $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ is a summability structure.

Remark 40. Elementary summability is a property of $\mathcal{L}$ and not an additional structure, which is however defined in a rather implicit manner. We exhibit three elementary conditions that are necessary and sufficient for guaranteeing elementary summability.

Lemma 41. The following conditions are equivalent

• for any $X\in\mathcal{L}$ , the morphisms ${X}\otimes{\overline\pi_{0}},{X}\otimes{\overline\pi_{1}}$ are jointly epic

• $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ is a pre-summability structure on $\mathcal{L}$ .

Proof. Assume that ${X}\otimes{\overline\pi_{0}},{X}\otimes{\overline\pi_{1}}$ are jointly epic and let $f_j\in\mathcal{L}(X,\mathsf S_{\mathbb D} Y)$ for $j=0,1$ be such that $\pi_{i}\, f_0=\pi_{i}\, f_1$ for $i=0,1$ . Let $f'_j=\operatorname{\mathsf{ev}}\,({f_j}\otimes{\mathbb D})\in\mathcal{L}({X}\otimes{\mathbb D},Y)$ so that $f_j=\operatorname{\mathsf{cur}}{f'_j}$ , for $j=0,1$ . We have

\begin{align*} \pi_{i}\, f_j &=\mathsf{nt}(\overline\pi_{i})\,(\ !\operatorname{\mathsf{cur}}{f'_j})\\ &=f'_j \,({X}\otimes{\overline\pi_{j}}) \,{\rho_X}^{-1}\text{ by Lemma 38.} \end{align*}

So we have $f'_0=f'_1$ by our assumption on the $\overline\pi_{j}$ ’s and hence $f_0=f_1$ .

Assume conversely that $\pi_{0},\pi_{1}$ are jointly monic and let $f_0,f_1\in\mathcal{L}({X}\otimes{\mathbb D},Y)$ be such that $f_0\,({X}\otimes{\overline\pi_{i}})=f_1\,({X}\otimes{\overline\pi_{i}})$ for $i=0,1$ . By Lemma 38, again we have $f_j\,({X}\otimes{\overline\pi_{i}})=\pi_{i}\,(\operatorname{\mathsf{cur}}{f_j})\,\rho_X$ and hence $\operatorname{\mathsf{cur}}{f_0}=\operatorname{\mathsf{cur}}{f_1}$ and hence $f_0=f_1$ which proves that ${X}\otimes{\overline\pi_{0}},{X}\otimes{\overline\pi_{1}}$ are jointly epic.

Theorem 12. Let $\mathcal{L}$ be a cartesian SMC where the object $\mathbb D={1}\mathrel{\&}{1}$ is exponentiable. Setting $\pi_{i}=\mathsf{nt}(\overline\pi_{i})$ for $i=0,1$ and $\sigma=\mathsf{nt}(\Delta)$ , the two following statements are equivalent.

1. (1) For any $X\in\mathcal{L}$ , the morphisms ${X}\otimes{\overline\pi_{0}},{X}\otimes{\overline\pi_{1}}$ are jointly epic (we call (ES-epi) this condition) and $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ satisfies (S-witness), see Section 3.

2. (2) $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ is a summable category that is, $\mathcal{L}$ is elementarily summable.

Proof. The implication (2) $\Rightarrow$ (1) results immediately from Lemma 41 so let us prove the converse. We assume that (1) holds. By Lemma 41, we know that $\pi_{0},\pi_{1}$ are jointly monic, so we are left with proving (S-com), (S-zero), and (S $\otimes$ -dist).

$\triangleright$ (S-com). Let $f=\operatorname{\mathsf{cur}} g\in\mathcal{L}(\mathsf S_{\mathbb D} X,\mathsf S_{\mathbb D} X)$ where g is the following composition of morphisms:

We have

and similarly

\begin{align*} \sigma\, f =g\,({\left({\mathbb D}\multimap{ }\right)X}\otimes{\Delta})\,{\rho}^{-1} =\operatorname{\mathsf{ev}}\,({\left({\mathbb D}\multimap{ }\right)X}\otimes{\Delta})\,{\rho}^{-1}=\sigma. \end{align*}

$\triangleright$ (S-zero). Let $f\in\mathcal{L}(X,Y)$ . Let $h=\operatorname{\mathsf{cur}}(f\,\rho_X\,({X}\otimes{\mathsf{pr}_{0}}))\in\mathcal{L}(X,\mathsf S_{\mathbb D} Y)$ . We have

\begin{align*} \pi_{i}\, h &=f\,\rho_X\,({X}\otimes{\mathsf{pr}_{0}}) \,({X}\otimes{\overline\pi_{i}}) \,{\rho_X}^{-1} \text{ by Lemma 38}\\ &= \begin{cases} f & \text{if }i=0\\ 0 & \text{otherwise} \end{cases} \end{align*}

which shows that f,0 are summable with $\langle{f,0}\rangle_{\mathsf S}=h$ . Moreover,

\begin{align*} \sigma\, h=f\,\rho_X\,({X}\otimes{\mathsf{pr}_{0}}) \,({X}\otimes{\Delta}) \,{\rho_X}^{-1}=f. \end{align*}

$\triangleright$ (S $\otimes$ -dist). Let $(f_{00},f_{01})$ be a summable pair of morphisms in $\mathcal{L}(X_0,Y_0)$ so that we have the witness $\langle{f_{00},f_{01}}\rangle_{\mathsf S}\in\mathcal{L}(X_0,\mathsf S_{\mathbb D}{Y_0})$ , and let $f_1\in\mathcal{L}(X_1,Y_1)$ . Let $h=\operatorname{\mathsf{cur}}{h'}\in\mathcal{L}({X_0}\otimes{X_1},\mathsf S_{\mathbb D}({Y_0}\otimes{Y_1}))$ where h’ is the following composition of morphisms:

We have

\begin{align*} \pi_{i}\, h &=({\operatorname{\mathsf{ev}}}\otimes{f_1}) \,({\langle{f_{00},f_{01}}\rangle_{\mathsf S}}\otimes{\gamma_{X_1,\mathbb D}}) \,({{X_0}\otimes{X_1}}\otimes{\overline\pi_{i}}) \,{\rho_{{X_0}\otimes{X_1}}}^{-1} \text{ by Lemma 38}\\ &=({\operatorname{\mathsf{ev}}}\otimes{f_1}) \,({\langle{f_{00},f_{01}}\rangle_{\mathsf S}}\otimes{{\overline\pi_{i}}\otimes{X_1}}) \,({X_0}\otimes{\gamma_{X_1,1}}) \,{\rho_{{X_0}\otimes{X_1}}}^{-1}\\ &=({(\operatorname{\mathsf{ev}}\,({\langle{f_{00},f_{01}}\rangle_{\mathsf S}}\otimes{\overline\pi_{i}}))}\otimes{f_1}) \,({X_0}\otimes{\gamma_{X_1,1}}) \,{\rho_{{X_0}\otimes{X_1}}}^{-1}\\ &=({f_{0i}}\otimes{f_1}) \,({\rho_{X_0}}\otimes{X_1}) \,({X_0}\otimes{\gamma}) \,{\rho_{{X_0}\otimes{X_1}}}^{-1}\\ &={f_{0i}}\otimes{f_1}. \end{align*}

which shows that ${f_{00}}\otimes{f_1},{f_{01}}\otimes{f_1}$ are summable with

\begin{align*} \langle{{f_{00}}\otimes{f_1},{f_{01}}\otimes{f_1}}\rangle_{\mathsf S}=h. \end{align*}

We have by a similar computation:

There are cartesian SMC where $\mathbb D$ is exponentiable and which are not elementarily summable. The category $\mathbf{Set}_0$ provides probably the simplest example of that situation.

▸ Example 5.1. We refer to Section 2.2, we have $1=\{0,\ast\}$ and hence $\mathbb D=\{0,\ast\}^2$ with $0_\mathbb D=(0,0)$ . We have the functor $\mathsf S_{\mathbb D}:\mathbf{Set}_0\to\mathbf{Set}_0$ defined by $\mathsf S_{\mathbb D} X=({\mathbb D}\multimap{X})$ . An element of $\mathsf S_{\mathbb D} X$ is a function $z:\{0,\ast\}^2\to X$ such that $z(0,0)=0$ . The projections $\pi_{i}:\mathsf S_{\mathbb D} X\to X$ are characterized by $\pi_{0}(z)=z(\ast,0)$ and $\pi_{1}(z)=z(0,\ast)$ , so $\langle{\pi_{0},\pi_{1}}\rangle$ is not injective, since $\langle{\pi_{0},\pi_{1}}\rangle(z)=(z(\ast,0),z(0,\ast))$ does not depend on $z(\ast,\ast)$ which can take any value. So $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ is not even a presummability structure in $\mathbf{Set}_0$ . This failure of injectivity is due to the fact that $\mathbb D$ lacks an addition which would satisfy $(\ast,0)+(0,\ast)=(\ast,\ast)$ and, preserved by z, would enforce injectivity.

There are also cartesian SMC where $\mathbb D$ is exponentiable, where (ES-epi) holds but where $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ does not satisfy (S-witness).

▸ Example 5.2. Let $\mathcal{B}$ be the category whose objects are the finite-dimensional real Banach space. By this, we mean pairs $(V,\|{\_}\|_V)$ where V is a finite-dimensional real vector space and $\|{\_}\|_V$ is a norm on V. In $\mathcal{B}$ , a morphism $V\to W$ is a linear map such that $\forall v\in V\ \|{f(v)}\|_W\leq\|{v}\|_V$ . This category is a cartesian symmetric monoidal closed category with ${U}\multimap{V}$ defined as the space of all linear maps $f:U\to V$ and

\[ \|{f}\|_{{U}\multimap{V}}=\sup\{\|{f(u)}\|_V\mid u\in U\text{ and }\|{u}\|_U\leq 1\}\,. \]

Indeed since we consider only finite-dimensional spaces, all linear maps are continuous (for the product topology induced by any choice of basis, which is the same as the one induce by the norm) and hence bounded. The tensor product classifies bilinear maps (with norm defined by sups as for linear maps) and satisfies $\|{{u}\otimes{v}}\|_{{U}\otimes{V}}=\|{u}\|_U\|{v}\|_V$ for all $u\in U$ and $v\in V$ . The unit of this tensor product is $1=\mathbb{R}$ with $\|{a}\|_1=\left|{a}\right|$ for all $a\in\mathbb{R}$ . The cartesian product is the standard direct product of vector spaces with $\|{(u,v)}\|_{{U}\mathrel{\&}{V}}=\max(\|{u}\|_V,\|{v}\|_V)$ . Notice that there is also a coproduct ${U}\oplus{V}$ , with the same underlying vector space and $\|{(u,v)}\|_{{U}\oplus{V}}=\|{u}\|_U+\|{v}\|_V$ . So ${U}\mathrel{\&}{V}$ and ${U}\oplus{V}$ are not isomorphic in $\mathcal{B}$ which is not an additive category.

We have $\mathbb D={1}\mathrel{\&}{1}=\mathbb{R}^2$ with $\|{(a_0,a_1)}\|_\mathbb D=\max(\left|{a_0}\right|,\left|{a_1}\right|)$ . The functor $\mathsf S_{\mathbb D}:\mathcal{B}\to\mathcal{B}$ maps U to $V=\mathsf S_{\mathbb D} U=U\times U$ and

\[ \|{(u_0,u_1)}\|_V=\sup\{\|{a_0u_0+a_1u_1}\|_U\mid (a_0,a_1)\in[\ !-1,1]\times[\ !-1,1]\} \]

The natural transformations $\pi_{i}$ are the obvious projections and $\sigma(u_0,u_1)=u_0+u_1$ .

Then, taking $U=1=\mathbb{R}$ :

• $-1/2$ and $1/2$ are summable in 1 because $\left|{-\frac a2+\frac b2}\right|\leq 1$ for all $a,b\in[\ !-1,1]$

• $-1/2+1/2=0$ and 1 are summable in 1

• but $1/2$ and 1 are not summable in 1.

So $\mathcal{B}$ is not elementarily summable.

This example shows that the condition (S-witness) cannot be disposed of and speaks not only of associativity of partial sums but also of some kind of “positivity” of morphisms in $\mathcal{L}$ .

5.1 The comonoid structure of $\mathbb D$

We assume that $\mathcal{L}$ is an elementarily summable cartesian SMC. The morphisms $\overline\pi_{0},\overline\pi_{1}\in\mathcal{L}(1,\mathbb D)$ are summable with $\overline\pi_{0}+\overline\pi_{1}=\Delta$ , with witness $\operatorname{\mathsf{Id}}\in\mathcal{L}(\mathbb D,\mathbb D)$ . As a consequence of (S $\otimes$ -dist), the morphisms $({\overline\pi_{0}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}$ , $({\overline\pi_{0}}\otimes{\overline\pi_{1}})\,{\rho}^{-1}$ and $({\overline\pi_{1}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}$ are summable in $\mathcal{L}(1,{\mathbb D}\otimes{\mathbb D})$ . Therefore, $({\overline\pi_{0}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}$ and $({\overline\pi_{0}}\otimes{\overline\pi_{1}})\,{\rho}^{-1}+({\overline\pi_{1}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}$ are summable in $\mathcal{L}(1,{\mathbb D}\otimes{\mathbb D})$ , so there is a uniquely defined $\overline{\mathsf L}\in\mathcal{L}(\mathbb D,{\mathbb D}\otimes{\mathbb D})$ such that $ \overline{\mathsf L}\,\overline\pi_{0}=({\overline\pi_{0}}\otimes{\overline\pi_{0}})\,{\rho}^{-1} \text{ and } \overline{\mathsf L}\,\overline\pi_{1} =({\overline\pi_{0}}\otimes{\overline\pi_{1}})\,{\rho}^{-1} +({\overline\pi_{1}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}\,. $

Theorem 13. Equipped with $\mathsf{pr}_{0}\in\mathcal{L}(\mathbb D,1)$ as counit and $\overline{\mathsf L}\in\mathcal{L}(\mathbb D,{\mathbb D}\otimes{\mathbb D})$ as comultiplication, $\mathbb D$ is a cocommutative comonoid in the SMC $\mathcal{L}$ .

Proof. To prove the required commutations, we use (ES-epi). Here are two examples of these computations.

\begin{align*} \rho\,({\mathbb D}\otimes{\mathsf{pr}_{0}})\,\overline{\mathsf L}\,\overline\pi_{0} &=\rho\,({\mathbb D}\otimes{\mathsf{pr}_{0}}) \,({\overline\pi_{0}}\otimes{\overline\pi_{0}}) \,{{\rho}^{-1}} =\rho\,({\overline\pi_{0}}\otimes{1})\,{\rho}^{-1}=\overline\pi_{0} \end{align*}

and

\begin{align*} \rho\,({\mathbb D}\otimes{\mathsf{pr}_{0}})\,\overline{\mathsf L}\,\overline\pi_{1} &=\rho\,({\mathbb D}\otimes{\mathsf{pr}_{0}}) \,({\overline\pi_{0}}\otimes{\overline\pi_{1}}+{\overline\pi_{1}}\otimes{\overline\pi_{0}}) \,{{\rho}^{-1}} =\rho\,({\overline\pi_{1}}\otimes{1})\,{\rho}^{-1}=\overline\pi_{1} \end{align*}

since $\mathsf{pr}_{0}\,\overline\pi_{i}$ is equal to $\operatorname{\mathsf{Id}}_1$ if $i=0$ and to 0 otherwise. Hence, $\rho\,({\mathbb D}\otimes{\mathsf{pr}_{0}})\,\overline{\mathsf L}=\mathbb D$ . Next

\begin{align*} ({\mathbb D}\otimes{\overline{\mathsf L}})\,\overline{\mathsf L}\,\overline\pi_{0} &=({\mathbb D}\otimes{\overline{\mathsf L}})\,({\overline\pi_{0}}\otimes{\overline\pi_{0}})\,{\rho}^{-1} =({\overline\pi_{0}}\otimes{({\overline\pi_{0}}\otimes{\overline\pi_{0}})})\,({\mathbb D}\otimes{{\rho}^{-1}})\,{\rho}^{-1} \end{align*}

and

\begin{align*} ({\mathbb D}\otimes{\overline{\mathsf L}})\,\overline{\mathsf L}\,\overline\pi_{1} &=({\mathbb D}\otimes{\overline{\mathsf L}}) \,({\overline\pi_{0}}\otimes{\overline\pi_{1}}+{\overline\pi_{1}}\otimes{\overline\pi_{0}})\,{\rho}^{-1}\\ &=({\overline\pi_{0}}\otimes{({\overline\pi_{0}}\otimes{\overline\pi_{1}})} +{\overline\pi_{0}}\otimes{({\overline\pi_{1}}\otimes{\overline\pi_{0}})} +{\overline\pi_{1}}\otimes{({\overline\pi_{0}}\otimes{\overline\pi_{0}})}) \,({\mathbb D}\otimes{{\rho}^{-1}})\,{\rho}^{-1}\,. \end{align*}

Similar computations show that $ ({\overline{\mathsf L}}\otimes{\mathbb D})\,\overline{\mathsf L}\,\overline\pi_{0} =({({\overline\pi_{0}}\otimes{\overline\pi_{0}})}\otimes{\overline\pi_{0}}) \,({{\rho}^{-1}}\otimes{\mathbb D})\,{\rho}^{-1} $ and $ ({\overline{\mathsf L}}\otimes{\mathbb D})$ $\,\overline{\mathsf L}\,\overline\pi_{1} =({({\overline\pi_{0}}\otimes{\overline\pi_{0}})}\otimes{\overline\pi_{1}} +{({\overline\pi_{0}}\otimes{\overline\pi_{1}})}\otimes{\overline\pi_{0}} +{({\overline\pi_{1}}\otimes{\overline\pi_{0}})}\otimes{\overline\pi_{0}}) \,({{\rho}^{-1}}\otimes{\mathbb D})\,{\rho}^{-1}\,. $ Therefore $\alpha\,({\overline{\mathsf L}}\otimes{\mathbb D})\,\overline{\mathsf L}\,\overline\pi_{i} =({\mathbb D}\otimes{\overline{\mathsf L}})\,\overline{\mathsf L}\,\overline\pi_{i}$ for $i=0,1$ and $\overline{\mathsf L}$ is coassociative. Cocommutativity is proven similarly.

Remark 42. This comonoid structure of $\mathbb D$ has some similarity with the fact that the algebra $\mathbf k[X]/X^2$ of dual numbers (where $\mathbf k$ is a field) can be described as the vector space $\mathbf k\times\mathbf k$ equipped with the multiplication $(a_0,a_1)(b_0,b_1)=(a_0b_0,a_0b_1+a_1b_0)$ , with the difference that dual numbers are a commutative monoid in the category of $\mathbf k$ -vector spaces, whereas our $\mathbb D$ is a commutative comonoid. The analogy is strong because if $\mathcal{L}$ were a kind of SMC of vector spaces, then 1 would be the “field of coefficients” and $\mathbb D$ would be the direct (cartesian) product of this field with itself just as the algebra of dual numbers, with the same kind of meaning for the two components of this product.

5.2 Strong monad structure of $\mathsf S_{\mathbb D}$

Therefore, the functor $\overline{\mathsf S}_\mathbb D$ defined at the beginning of Section 5 has a canonical comonad structure given by $\rho\,({X}\otimes{\mathsf{pr}_{0}})\in\mathcal{L}(\overline{\mathsf S}_\mathbb D X,X)$ and $\alpha\,({X}\otimes{\overline{\mathsf L}})\in\mathcal{L}(\overline{\mathsf S}_\mathbb D X,\overline{\mathsf S}_\mathbb D^2X)$ . Through the adjunction $\overline{\mathsf S}_\mathbb D\mathrel{\dashv}\mathsf S_{\mathbb D}$ , the functor $\mathsf S_{\mathbb D}$ inherits a monad structure which is exactly the same as the monad structure of Section 3.1. This monad structure $(\iota_{0},\tau)$ can be described as the Curry transpose of the following morphisms (the monoidality isos are implicit):

Similarly, the trivial costrength $\alpha\in\mathcal{L}(\overline{\mathsf S}_\mathbb D({X}\otimes{Y}),{X}\otimes{\overline{\mathsf S}_\mathbb D Y})$ induces the strength $\phi^1\in\mathcal{L}({X}\otimes{\mathsf S_{\mathbb D} Y},\mathsf S_{\mathbb D}({X}\otimes{Y}))$ of $\mathsf S_{\mathbb D}$ (the same as the one defined in the general setting of Section 4). We have seen in Section 4 that equipped with this strength $\mathsf S_{\mathbb D}$ is a commutative monad and recalled that there is therefore an associated lax monoidality $\mathsf L_{X_0,X_1}\in\mathcal{L}({\mathsf S_{\mathbb D} X_0}\otimes{\mathsf S_{\mathbb D} X_1},\mathsf S_{\mathbb D}({X_0}\otimes{X_1}))$ which can be seen as arising from $\overline{\mathsf L}$ by transposing the following morphism (again we keep the monoidal isos implicit):

5.3 Elementarily summable SMCC

In a SMCC, the conditions of Theorem 12 admit a slightly simpler formulation.

Theorem 14. A cartesian SMCC is elementarily summable if and only if the condition (ECS-epi) $\overline\pi_{0}$ and $\overline\pi_{1}$ are jointly epic holds and $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ satisfies (S-witness).

▸ Example 5.3. The SMCC $\mathbf{Coh}$ is elementarily summable, actually the summability structure we have considered on this category is exactly its elementary summability structure. Let us check the three conditions.

The coherence space $\mathbb D={1}\mathrel{\&}{1}$ is given by ${}|{\mathbb D}{}|=\{0,1\}$ with . Then $\overline\pi_{i}=\{(\ast,i)\}$ and $\Delta=\{(\ast,0),(\ast,1)\}$ . If $s\in\mathbf{Coh}(\mathbb D,F)$ , then $(i,b)\in s\Leftrightarrow(\ast,b)\in s\,\overline\pi_{i}$ for $i=0,1$ and hence $\overline\pi_{0},\overline\pi_{1}$ are jointly epic so $\mathbf{Coh}$ satisfies (ECS-epi).

The functor $\mathsf S_{\mathbb D}$ defined by $\mathsf S_{\mathbb D} E=\left({\mathbb D}\multimap{ }\right)E$ (and similarly for morphisms) coincides exactly with the functor $\mathsf S$ described in Example 3.2. Therefore, the associated summability is the one described in Example 3.3.

We check that (S-witness) holds in $\mathbf{Coh}$ . Let $s_i\in\mathbf{Coh}(\mathbb D,E)$ for $i=0,1$ . Let $t_i=s_i\,\Delta=\{(\ast,a)\in{}|{{1}\multimap{} E}{}|\mid((0,a)\in s_i\text{ or }(1,a)\in s_i\}$ . Assume that $t_0$ and $t_1$ are summable, that is, $t_0\cap t_1=\emptyset$ and $t_0\cup t_1\in\mathbf{Coh}(1,E)$ , we must prove that $s_0\cap s_1=\emptyset$ and $s_0\cup s_1\in\mathbf{Coh}(\mathbb D, E)$ . Let $(j_i,a_i)\in s_i$ for $i=0,1$ . We have $(\ast,a_i)\in t_i$ and hence $a_0\not=a_1$ from which it follows that $(j_0,a_0)\not=(j_1,a_1)$ . Since and , we have . Hence, $s_0$ and $s_1$ are summable.

5.4 Differentiation in an elementarily summable category

Let $\mathcal{L}$ be a resource category (see the beginning of Section 4.1) which is elementarily summable. The next lemma is an instance of the general notion of mate in the general two-categorical theory of adjunctions; see Kelly and Street (2006). It relies only on the adjunction $\overline{\mathsf S}_\mathbb D\mathrel{\dashv}\mathsf S_{\mathbb D}$ and on the functoriality of $\ !{\_}$ . Let $\eta_X\in\mathcal{L}(X,\mathsf S_{\mathbb D}\overline{\mathsf S}_\mathbb D X)$ and $\epsilon_X\in\mathcal{L}(\overline{\mathsf S}_\mathbb D\mathsf S_{\mathbb D} X,X)$ be the unit and counit of this adjunction. Let $\varphi_X:\mathcal{L}(\ !{\mathsf S_{\mathbb D} X},\mathsf S_{\mathbb D}{\ !{X}})$ be a natural transformation, then we define a natural transformation ${\varphi}^{-}_X\in\overline{\mathsf S}_\mathbb D\ !{X}\to\ !{\overline{\mathsf S}_\mathbb D X}$ as the following composition of morphisms:

Conversely given a natural transformation $\psi_X\in\mathcal{L}(\overline{\mathsf S}_\mathbb D\ !{X},\ !{\overline{\mathsf S}_\mathbb D X})$ , we define a natural transformation ${\psi}^{+}_X\in\mathcal{L}(\ !{\mathsf S_{\mathbb D} X},\mathsf S_{\mathbb D}{\ !{X}})$ as the following composition of morphisms:

Lemma 43. With the notations above, ${{\varphi}^{-}}^{+}=\varphi$ and ${{\psi}^{+}}^{-}=\psi$ .

Proof. Simple computation using the basic properties of adjunctions and the naturality of the various morphisms involved.

Lemma 44. Let $\overline\partial_X\in\mathcal{L}(\overline{\mathsf S}_\mathbb D\ !{X},\ !{\overline{\mathsf S}_\mathbb D X})$ be a natural transformation. The associated natural transformation ${\overline\partial}^{+}_X\in\mathcal{L}(\ !{\mathsf S_{\mathbb D} X},\mathsf S_{\mathbb D}{\ !{X}})$ satisfies ( $\partial$ -chain) iff the two following diagrams commute (E $\partial$ -chain)

in other words $\overline\partial_X$ is a co-distributive law $\overline{\mathsf S}_\mathbb D\ !{X}\to\ !{\overline{\mathsf S}_\mathbb D X}$ .

Proof. Consists of computations using naturality and adjunction properties. As an example, assume the second commutation and let us prove the second diagram of ( $\partial$ -chain):

We have

The other computations are similar.

Let $\overline\partial_X\in\mathcal{L}({\ !{X}}\otimes{\mathbb D},\ !{({X}\otimes{\mathbb D})})$ satisfying (E $\partial$ -chain). We introduce additional conditions. We keep implicit some of the monoidal isos associated with $\otimes$ to increase readability.

Theorem 15. Let $\overline\partial_X\in\mathcal{L}({\ !{X}}\otimes{\mathbb D},\ !{({X}\otimes{\mathbb D})})$ be a natural transformation. The two following conditions are equivalent.

• $\overline\partial$ satisfies (E $\partial$ -chain), (E $\partial$ -local), (E $\partial$ -lin), (E $\partial$ - $\mathord{\mathrel{\&}}$ ) and (E $\partial$ -Schwarz).

• ${\overline\partial}^{+}$ is a differentiation in $(\mathcal{L},\mathsf S_{\mathbb D})$ (in the sense of Definition 32).

Proof. Simple categorical computations: there is a simple direct correspondence between the conditions (E $\partial$ -chain), (E $\partial$ -local), (E $\partial$ -lin), (E $\partial$ - $\mathord{\mathrel{\&}}$ ), and (E $\partial$ -Schwarz) on $\overline\partial$ and the conditions ( $\partial$ -chain), ( $\partial$ -local), ( $\partial$ -lin), ( $\partial$ - $\mathord{\mathrel{\&}}$ ), and ( $\partial$ -Schwarz) on ${\overline\partial}^{+}$ through the adjunction $\overline{\mathsf S}_\mathbb D\mathrel{\dashv}\mathsf S_{\mathbb D}$ .

Definition 45. A differential elementarily summable resource category is an elementarily summable resource category $\mathcal{L}$ equipped with a natural transformation $\overline\partial_X\in\mathcal{L}({\ !{X}}\otimes{\mathbb D},\ !{({X}\otimes{\mathbb D})})$ satisfying (E $\partial$ -chain), (E $\partial$ -local), (E $\partial$ -lin), (E $\partial$ - $\mathord{\mathrel{\&}}$ ), and (E $\partial$ -Schwarz). Then we set $\partial={\overline\partial}^{+}$ .

We show now that this differential structure boils down to a much simpler one.

5.5 A $\ !$ -coalgebra structure on $\mathbb D$ induced by an elementary differential structure

Let $\overline\partial_X\in\mathcal{L}({\ !{X}}\otimes{\mathbb D},\ !{({X}\otimes{\mathbb D})})$ be a natural transformation which satisfies the conditions of Definition 45.

Lemma 46. Given objects $X_0,X_1$ of $\mathcal{L}$ , the following diagram commutes:

where $q_0=\langle{\rho_{X_0}({\mathsf{pr}_{0}}\otimes{\mathsf{pr}_{0}}),{\mathsf{pr}_{1}}\otimes{\mathbb D}}\rangle \in\mathcal{L}({\left({X_0}\mathrel{\&}{X_1}\right)}\otimes{\mathbb D},{X_0}\mathrel{\&}{({X_1}\otimes{\mathbb D})})$ ; remember indeed that $\mathbb D={1}\mathrel{\&}{1}$ .

Proof. Observe first that $ q_0=\left({\rho_{X_0}\,({X_0}\otimes{\mathsf{pr}_{0}})}\mathrel{\&}{({X_1}\otimes{\mathbb D})}\right) \, \langle{{\mathsf{pr}_{0}}\otimes{\mathbb D},{{\mathsf{pr}_{1}}\otimes{\mathbb D}}}\rangle $ . We have

\begin{align*} \ !{q_0} \, \overline\partial_{{X_0}\mathrel{\&}{X_1}} &\, ({\mathsf m^2_{X_0,X_1}}\otimes{\mathbb D})\\ &=\ !({{\rho_{X_0}\,({X_0}\otimes{\mathsf{pr}_{0}})}\mathrel{\&}{({X_1}\otimes{\mathbb D})}}) \, \ !{\langle{{\mathsf{pr}_{0}}\otimes{\mathbb D},{{\mathsf{pr}_{1}}\otimes{\mathbb D}}}\rangle} \, \overline\partial_{{X_0}\mathrel{\&}{X_1}} \, ({\mathsf m^2_{X_0,X_1}}\otimes{\mathbb D})\\ &=\ !({{\rho_{X_0}\,({X_0}\otimes{\mathsf{pr}_{0}})}\mathrel{\&}{({X_1}\otimes{\mathbb D})}}) \,{\mathsf m^2_{{X_0}\otimes{\mathbb D},{X_1}\otimes{\mathbb D}}} \,({\overline\partial_{X_0}}\otimes{\overline\partial_{X_1}}) \,\gamma_{2,3} \,(\ !{X_0}\otimes\ !{X_1}\otimes\overline{\mathsf L}) \end{align*}

by (E $\partial$ - $\mathord{\mathrel{\&}}$ ), and notice that $\gamma_{2,3}\in\mathcal{L}(\ !{X_0}\otimes\ !{X_1}\otimes\mathbb D\otimes\mathbb D, \ !{X_0}\otimes\mathbb D\otimes\ !{X_1}\otimes\mathbb D)$ . So we have

The next result will be technically useful in the sequel and has also its own interest as it deals with differentiation with respect to a tensor product, showing essentially that it boils down to differentiation with respect to one of the components of the tensor product.

Theorem 16. The following diagram commutes, for all objects $X_0$ , $X_1$ of $\mathcal{L}$ .

Proof. We recall that $\mu^2_{X,Y}\in\mathcal{L}({\ !{X}}\otimes{\ !{Y}},\ !{({X}\otimes{Y})})$ is defined as the following composition of morphisms:

so that we have, starting to introduce notations $f_0,f_1\dots$ for subexpressions,

\begin{align*} \mu^2_{X_0,{X_1}\otimes{\mathbb D}}\,({\ !{X_0}}\otimes{\overline\partial_{X_1}}) &=\ !{({\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{{X_1}\otimes{\mathbb D}}})} \,\ !{({\mathsf m^2_{X_0,{X_1}\otimes{\mathbb D}}})^{-1}} \,\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{({X_1}\otimes{\mathbb D})}} \,\mathsf m^2_{X_0,{X_1}\otimes{\mathbb D}} \,({\ !{X_0}}\otimes{\overline\partial_{X_1}})\\ &=\ !{({\operatorname{\mathsf{der}}_{X_0}}\otimes{\operatorname{\mathsf{der}}_{{X_1}\otimes{\mathbb D}}})} \,\ !{({\mathsf m^2_{X_0,{X_1}\otimes{\mathbb D}}})^{-1}} \,\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{({X_1}\otimes{\mathbb D})}} \, f_0 \end{align*}

where, using by Lemma 46,

\begin{align*} f_0=\mathsf m^2_{X_0,{X_1}\otimes{\mathbb D}} \,({\ !{X_0}}\otimes{\overline\partial_{X_1}}) =\ !{q_0} \,\overline\partial_{{X_0}\mathrel{\&}{X_1}} \,({\mathsf m^2_{X_0,X_1}}\otimes{\mathbb D}) \end{align*}

where $q_0=\langle{\rho_{X_0}({\mathsf{pr}_{0}}\otimes{\mathsf{pr}_{0}}),{\mathsf{pr}_{1}}\otimes{\mathbb D}}\rangle \in\mathcal{L}({\left({X_0}\mathrel{\&}{X_1}\right)}\otimes{\mathbb D},{X_0}\mathrel{\&}{({X_1}\otimes{\mathbb D})})$ . Then

\begin{align*} f_1 =\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{({X_1}\otimes{\mathbb D})}}\, f_0 =\ !\ !{q_0} \,\operatorname{\mathsf{dig}}_{{\left({X_0}\mathrel{\&}{X_1}\right)}\otimes{\mathbb D}} \,\overline\partial_{{X_0}\mathrel{\&}{X_1}} \,({\mathsf m^2_{X_0,X_1}}\otimes{\mathbb D}) =\ !\ !{q_0} \, f_2 \,({\mathsf m^2_{X_0,X_1}}\otimes{\mathbb D})\,. \end{align*}

by naturality of $\operatorname{\mathsf{dig}}_{}$ . Next,

\begin{align*} f_2=\operatorname{\mathsf{dig}}_{{\left({X_0}\mathrel{\&}{X_1}\right)}\otimes{\mathbb D}} \,\overline\partial_{{X_0}\mathrel{\&}{X_1}} =\ !{\overline\partial_{{X_0}\mathrel{\&}{X_1}}} \,\overline\partial_{\ !{\left({X_0}\mathrel{\&}{X_1}\right)}} \,({\operatorname{\mathsf{dig}}_{{X_0}\mathrel{\&}{X_1}}}\otimes{\mathbb D}) \end{align*}

by (E $\partial$ -chain). By Lemma 46 again (applied under the functor $\ !{\_}$ ), we have

Finally, we have

by definition of $\mu^2_{X_0,X_1}$ .

We define $\widetilde\partial\in\mathcal{L}(\mathbb D,\ !{\mathbb D})$ as the following composition of morphisms:

Then the whole natural transformation $\overline\partial$ can be retrieved from this single morphism $\widetilde\partial$ .

Theorem 17. The following diagram commutes:

Proof. We have

\begin{align*} \mu^2_{X,\mathbb D} \,({\ !{X}}\otimes{\widetilde\partial}) &=\mu^2_{X,\mathbb D} \,({\ !{X}}\otimes{\ !{\lambda_\mathbb D}}) \,({\ !{X}}\otimes{\overline\partial_1}) \,({\ !{X}}\otimes{{\mu^0}\otimes{\mathbb D}}) \,({\ !{X}}\otimes{{\lambda_\mathbb D}^{-1}})\\ &=\ !({X\otimes\lambda_\mathbb D}) \,\mu^2_{X,{1}\otimes{\mathbb D}} \,({\ !{X}}\otimes{\overline\partial_1}) \,({\ !{X}}\otimes{{\mu^0}\otimes{\mathbb D}}) \,({\ !{X}}\otimes{{\lambda_\mathbb D}^{-1}})\\ &=\ !({X\otimes\lambda_\mathbb D}) \,\overline\partial_{{X}\otimes{1}} \,({\mu^2_{X,1}}\otimes{\mathbb D}) \,({\ !{X}}\otimes{{\mu^0}\otimes{\mathbb D}}) \,({\ !{X}}\otimes{{\lambda_\mathbb D}^{-1}}) \end{align*}

by Theorem 16. We obtain the announced equation by $\mu^2_{X,1}\,({\ !{X}}\otimes{\mu^0}) =\ !{({\rho_X})^{-1}}\,\rho_{\ !{X}}$ , the naturality of $\overline\partial$ and the fact that ${\rho_X}\otimes{Y} ={X}\otimes{\lambda_Y}\in\mathcal{L}(X\otimes1\otimes Y,{X}\otimes{Y})$ .

Theorem 18. The morphism $\widetilde\partial$ is a $\ !$ -coalgebra structure on $\mathbb D$ . Moreover, the following commutations hold.

In other words, $\overline\pi_{0}$ , $\mathsf{pr}_{0}$ , and $\overline{\mathsf L}$ are coalgebra morphisms.

Proof. We have, using the fact that $(1,\mu^0)$ is a $\ !$ -coalgebra,

and

and observe now that $\overline\partial_{1}\,({\mu^0}\otimes{\mathbb D}) =\ !{{\lambda}^{-1}}\,\widetilde\partial\,\lambda$ by definition of $\widetilde\partial$ . It follows that

We have proven that $(\mathbb D,\widetilde\partial)$ is a $\ !$ -coalgebra.

Let us prove that $\overline\pi_{0}\in{\mathcal{L}}^!((1,\mu^0),(\mathbb D,\widetilde\partial))$ . We have

since $\rho_1=\lambda_1$ .

Let us prove that

$\mathsf{pr}_{0}\in{\mathcal{L}}^!((\mathbb D,\widetilde\partial),(1,\mu^0))$ .

We have

Last we prove that $\overline{\mathsf L} \in{\mathcal{L}}^!((\mathbb D,\widetilde\partial),(\mathbb D,\widetilde\partial)\otimes(\mathbb D,\widetilde\partial))$ . We have

by standard properties of the lax monoidality structure $(\mu^0,\mu^2)$ of $\ !{\_}$ .

5.6 From a coalgebra structure on $\mathbb D$ to an elementary differential structure

Assume now conversely that $\mathcal{L}$ is an elementarily summable resource category (see Definition 45) where $\mathbb D$ is exponentiable and let $\widetilde\partial\in\mathcal{L}(\mathbb D,\ !{\mathbb D})$ . We can define a morphism $\overline\partial_X\in\mathcal{L}({\ !{X}}\otimes{\mathbb D},\ !({{X}\otimes{\mathbb D}}))$ as the following composition of morphisms:

This morphism is natural in X by the naturality of $\mu^2$ .

Theorem 19. If $\widetilde\partial$ satisfies the following properties:

1. (1) $(\mathbb D,\widetilde\partial)$ is a $\ !$ -coalgebra

2. (2) ( $\partial$ ca-local)

3. (3) and ( $\partial$ ca-lin)

4. then the natural transformation $\overline\partial$ satisfies (E $\partial$ -chain), (E $\partial$ -local), (E $\partial$ -lin), (E $\partial$ - $\mathord{\mathrel{\&}}$ ), and (E $\partial$ -Schwarz).

Proof. $\triangleright$ (E $\partial$ -chain). We have

and

as required.

$\triangleright$ (E $\partial$ -local). We have

by the properties of the lax monoidality $(\mu^2,\mu^0)$ .

$\triangleright$ (E $\partial$ -lin). We have

and

$\triangleright$ (E $\partial$ - $\mathord{\mathrel{\&}}$ ). By Proposition 5, we have $\mathsf{pr}_{0}=\operatorname{\mathsf{weak}}_{\mathbb D}\,\widetilde\partial$ and $\overline{\mathsf L}=({\operatorname{\mathsf{der}}_{\mathbb D}}\otimes{\operatorname{\mathsf{der}}_{\mathbb D}})\,\operatorname{\mathsf{contr}}_{\mathbb D}\,\widetilde\partial$ . We use these expressions in the next computations.

For the first diagram, we have

And the second one is proved by the following computation:

as required.

$\triangleright$ (E $\partial$ -Schwarz). We have

We can summarize the results obtained in this section as follows.

Theorem 20. Let $\mathcal{L}$ be an elementarily summable resource category. There is a bijective correspondence between

the differential structures $(\partial_X)_{X\in\mathcal{L}}$ on the elementary summability structure $(\mathsf S_{\mathbb D},\pi_{0},\pi_{1},\sigma)$ of $\mathcal{L}$

and the $\ !$ -coalgebra structures $\widetilde\partial$ on $\mathbb D$ which satisfy ( $\partial$ ca-local) and ( $\partial$ ca-lin).

In the second situation, the associated differentiation $\partial_X\in\mathcal{L}(\ !{\mathsf S_{\mathbb D} X},\mathsf S_{\mathbb D}{\ !{X}})$ is $\operatorname{\mathsf{cur}} d$ where d is the following composition of morphisms:

Remark 47. This correspondence can certainly be made functorial, and this is postponed to further work.

Now, we consider the case where $\mathcal{L}$ is Lafont; see Section 2.3.5. In this case, the situation is particularly simple.

Theorem 21. If $\mathcal{L}$ is a Lafont resource category which is elementarily summable, then there is exactly one differential structure on the elementary summability structure of $\mathcal{L}$ .

Proof. Since $(\mathbb D,\mathsf{pr}_{0},\overline{\mathsf L})$ is a commutative comonoid, we know by Lemma 6 that there is exactly one morphism $\widetilde\partial\in\mathcal{L}(\mathbb D,\ !{\mathbb D})$ such that the following diagrams commute:

By Theorem 4 $\widetilde\partial$ satisfies ( $\partial$ ca-lin) and hence we are left with proving ( $\partial$ ca-local). This readily follows from the bijective correspondence of Theorem 3 and from the fact that $\overline\pi_{0}\in{\mathcal {L}}^{\otimes}(1,(\mathbb D,\mathsf{pr}_{0},\overline{\mathsf L}))$ . Indeed $\mathsf{pr}_{0}\,\overline\pi_{0}=\operatorname{\mathsf{Id}}_1$ and $\overline{\mathsf L}\,\overline\pi_{0}={\overline\pi_{0}}\otimes{\overline\pi_{0}}$ .

Remark 48. Up to suitable applications of the ${\_}^{\mathsf{op}}$ operation on the involved categories, this result generalizes Theorem 3.4 of Blute et al. (2016) to the elementarily summable case. In that article, commutative monoids instead of comonoids are considered and, more importantly, the ambient category is additive.

6. The Differential Structure of Coherence Spaces

Equipped with the multiset exponential introduced in Section 4.4, it is well known that $\mathbf{Coh}$ is a Lafont resource category (see Section 2.3.5) as observed initially by Van de Wiele (unpublished, see Melliès 2009). Since $\mathbf{Coh}$ is elementarily summable as shown in Example 5.3, we already know that it has a unique differential structure by Theorem 21. We will show that we retrieve in that way the differential structure outlined in Section 4.4.

Remember that $\mathbb D={1}\mathrel{\&}{1}$ so that ${}|{\mathbb D}{}|=\{0,1\}$ with . The comonoid structure of $\mathbb D={1}\mathrel{\&}{1}$ is given by $\mathsf{pr}_{0}=\{(0,\ast)\}\in\mathbf{Coh}(\mathbb D,1)$ and $\overline{\mathsf L}=\{(0,(0,0)),(1,(1,0)),(1,(0,1))\}\in\mathbf{Coh}(\mathbb D,{\mathbb D}\otimes{\mathbb D})$ . The n-ary comultiplication of this comonoid is $\widetilde{\mathsf L}^{(n)}\in\mathbf{Coh}({\mathbb D},^{\mathord\otimes }D n)$ given by:

\begin{align*} \widetilde{\mathsf L}^{(n)} &=\{(0,(0,\dots,0))\}\cup \{(1,(\overbrace{0,\dots,0}^{k-1},1,\overbrace{0,\dots,0}^{n-k})) \mid k\in\{1,\dots,n\}\}\\ &=\{(i,(i_{1},\dots,i_{n}))\in{}|{\mathbb D}{}|\times{}|{\mathbb D}{}|^n\mid i=i_1+\cdots+i_n\}\,.\end{align*}

The unique $\widetilde\partial\in\mathbf{Coh}(\mathbb D,\ !{\mathbb D})$ specified by Theorem 21 is given by:

\begin{align*} \widetilde\partial =\{(i,[{i_{1},\dots,i_{k}}])\in{}|{\mathbb D}{}|\times\mathcal M_{{\mathrm{fin}}}({{}|{\mathbb D}{}|}) \mid k\in{\mathbb{N}}\text{ and }i=i_1+\cdots+i_n\}\,,\end{align*}

observe indeed that ${}|{\ !{\mathbb D}}{}|=\mathcal M_{{\mathrm{fin}}}({{}|{\mathbb D}{}|})$ due to the coherence relation of $\mathbb D$ . The associated natural transformation $\partial_E\in\mathbf{Coh}(\ !{\mathsf S_{\mathbb D} E},)$ is $\operatorname{\mathsf{cur}} d$ where d is the following composition of morphisms:

Since $\mu^2_{E_0,E_1}\in\mathbf{Coh}({\ !{E_0}}\otimes{\ !{E_1}},\ !({{E_0}\otimes{E_1}}))$ is given by:

and since for $\operatorname{\mathsf{ev}}\in\mathbf{Coh}({({\mathbb D}\multimap{ }E)}\otimes{\mathbb D},E)$ we have

\begin{align*} \ !{\mathsf{ev}} =\{([{((i_1,a_1),i_1),\dots,((i_n,a_n),i_n)}],[{a_{1},\dots,a_{n}}])\mid [{a_{1},\dots,a_{n}}]\in{}|{\ !{E}}{}|\text{ and }i_{1},\dots,i_{n}\in{}|{\mathbb D}{}|\}\end{align*}

it follows that

Upon identifying ${}|{\ !({{\mathbb D}\multimap{ }E})}{}|$ with

\begin{align*} \{(m_0,m_1)\in{}|{\ !{E}}{}|^2\mid m_0+m_1\in{}|{\ !{E}}{}| \text{ and }\operatorname{\mathsf{supp}}({m_0})\cap\operatorname{\mathsf{supp}}({m_1})=\emptyset\}\end{align*}

we get

which is exactly the definition announced in Equation (8). The proviso that $a\notin\operatorname{\mathsf{supp}}({m_0})$ in this expression of $\partial_E$ arises from the uniformity of the exponential since, setting $m_0=[{a_{1},\dots,a_{n}}]$ we must have $[{(0,a_1),\dots,(0,a_n),(1,a)}]\in{}|{\ !({{\mathbb D}\multimap{ }E})}{}|$ , that is, $\{0\}\times\{a_{1},\dots,a_{n}\}\cup\{(1,a)\}\in\mathsf{Cl}({{\mathbb D}\multimap{ }E})$ . The fact that this is a natural transformation satisfying all the commutations required to turn $\mathbf{Coh}$ into a differential summable category results from Theorem 15.

6.1 Differentiation in nonuniform coherence spaces

In Remark 37, we have pointed out that the uniform definition of $\ !{E}$ in coherence spaces makes our differentials “too thin” in general, although they are nontrivial and satisfy all the required rules of the differential calculus. We show briefly how this situation can be remedied using nonuniform coherence spaces.

A nonuniform coherence space (NUCS) is a triple where ${}|{E}{}|$ is a set and and are two disjoint binary symmetric relations on ${}|{E}{}|$ called strict coherence and strict incoherence. The important point of this definition is not what is written but what is not: contrarily to usual coherence spaces we do not require the complement of the union of these two relations to be the diagonal, it can be any (of course symmetric) binary relation on ${}|{E}{}|$ . We call this relation neutrality and denote it as $\equiv_{E}$ (warning: it needs not even be an equivalence relation!). Then we define coherence as and incoherence and any pair of relations among these five (with suitable relation between them such as ), apart from the two trivially complementary ones and , are sufficient to define such a structure.

Cliques are defined as usual: . Then, $(\mathsf{Cl}({E}),\mathord\subseteq)$ is a cpo (a dI-domain actually) but now there can be some $a\in{}|{E}{}|$ such that , and hence $\{a\}\notin\mathsf{Cl}({E})$ (we show below that this really happens). Given NUCS E and F, we define ${E}\multimap{F}$ by ${}|{{E}\multimap{F}}{}|={}|{E}{}|\times{}|{F}{}|$ and: if and $(a_0,b_0)\equiv_{{E}\multimap{F}}(a_1,b_1)$ if $a_0\equiv_{E}a_1$ and $b_0\equiv_{F}b_1$ . Then, we define a category $\mathbf{NCoh}$ by $\mathbf{NCoh}(E,F)=\mathsf{Cl}({{E}\multimap{F}})$ , taking the diagonal relations as identities and ordinary composition of relations as composition of morphisms.

This is a cartesian SMCC with tensor product given by ${}|{{E_0}\otimes{E_1}}{}|={}|{E_0}{}|\times{}|{E_1}{}|$ and if for $j=0,1$ , and $\equiv_{{E_0}\otimes{E_1}}$ is defined similarly; the unit is 1 with ${}|{1}{}|=\{\ast\}$ and $\ast\equiv_{1}\ast$ (so that $=^{{\mathord{\perp}}_{1}}1$ meaning that the model satisfies a strong form of the MIX rule of ${\textsf{LL}}$ ). The object of linear morphisms from E to F is of course ${E}\multimap{F}$ and $\mathbf{NCoh}$ is $\ast$ -autonomous with 1 as dualizing object. The dual $^{{\mathord{\perp}}_{E}}$ is given by $|{E}^\perp|=|{E}|$ ${}|{}^{{\mathord{\perp}}_{E}}{}|={}|{E}{}|$ , and . The cartesian product $\mathop{\&}_{i\in I}E_i$ of a family $(E_i)_{i\in I}$ of NUCS is given by ${}|{\mathop{\&}_{i\in I}E_i}{}|=\cup_{i\in I}\{i\}\times{}|{E_i}{}|$ with $(i_0,a_0)\equiv_{\mathop{\&}_{i\in I}E_i}(i_1,a_1)$ if $i_0=i_1=i$ and $a_0\equiv_{E_i}a_1$ , and if . We do not give the definition of the operations on morphisms as they are exactly the same as in $\operatorname{\mathbf{Rel}}$ (see Section 2.4). Notice that in the object $\mathbf{Bool}={1}\oplus{1}=^{{\mathord{\perp}}_{({1}\mathrel{\&}{1})}}$ , the two elements 0,1 of the web satisfy so that $\{0,1\}\notin\mathsf{Cl}({\mathbf{Bool}})$ which is expected in a model of deterministic computations.

We come to the most interesting feature of this model, which is the possibility of defining a nonuniform exponential $\ !{E}$ ; we choose here the one of Boudes (2011) which is the free exponential (so that $\mathbf{NCoh}$ is a Lafont resource category). One sets ${}|{\ !{E}}{}|=\mathcal M_{{\mathrm{fin}}}({{}|{E}{}|})$ (without any uniformity restrictions), if , and $m_0\equiv_{\ !{E}}m_1$ if and $m_j=[{a_{j1},\dots,a_{jn}}]$ (for $j=0,1$ ) with $\forall i\in\{1,\dots,n\}\ a_{0i}\equiv_{E}a_{1i}$ (in particular $m_0$ and $m_1$ must have the same size).

Remark 49. We have $[{0,1}]\in{}|{\ !\mathbf{Bool}}{}|$ and which illustrates the fact that is not antireflexive. This is an essential feature of this model because it is easy to write, in a suitable deterministic programming language functional language like PCF, a term of type $\mathbf{Bool}\to\mathbf{Bool}$ whose interpretation in $\mathbf{nCoh}$ is a clique t of ${\ !\mathbf{Bool}}\multimap{\mathbf{Bool}}$ which contains ([0,1],0) and ([0,1],1). So, since , it is only because that we can have , which is required since t must be a clique, being the interpretation of a term. Notice however that, as observed by Boudes, when we use the free exponential, we can assume that all NUCS E satisfy the property that $a\equiv_{E}b\Rightarrow a=b$ and that $\equiv_{E}$ is a partial equivalence relation, these properties being preserved by all constructions. The NUCS exponential described in Bucciarelli and Ehrhard (2001) is not compatible with these assumptions.

The action of the functor $\ !{\_}$ on morphisms is defined as in $\operatorname{\mathbf{Rel}}$ : if $s\in\mathbf{NCoh}(E,F)$ , then $\ !{s}=\{([{a_{1},\dots,a_{n}}],[{b_{1},\dots,b_{n}}])\mid n\in{\mathbb{N}}\text{ and }\forall i\ (a_i,b_i)\in s\}\in\mathbf{NCoh}(\ !{E},\ !{F})$ .

The object $\mathbb D={1}\mathrel{\&}{1}$ is characterized by ${}|{\mathbb D}{}|=\{0,1\}$ and , $ \equiv_{\mathbb D}ii$ for $i\in{}|{\mathbb D}{}|$ . The injections $\overline\pi_{0},\overline\pi_{1}\in\mathbf{NCoh}(1,\mathbb D)$ are given by $\overline\pi_{i}=\{(\ast,i)\}$ and are clearly jointly epic. Two cliques $x_0,x_1\in\mathsf{Cl}({E})$ are summable if there is $x\in\mathsf{Cl}({{\mathbb D}\multimap{ }E})$ such that $x_i=x\,\overline\pi_{i}$ , that is, if $\{0\}\times x_0\cup\{1\}\times x_1\in\mathsf{Cl}({{\mathbb D}\multimap{ }E})$ which means that

This implies $x_0\cup x_1\in\mathsf{Cl}({E})$ but not $x_0\cap x_1=\emptyset$ since we can have in a nonuniform coherence space.

The condition (S-witness) holds: let $x_{ij}\in\mathsf{Cl}({E})$ for $i,j\in\{0,1\}$ and assume that $x_{i0},x_{i1}$ are summable for $i=0,1$ and that moreover $x_{00}\cup x_{01},x_{10}\cup x_{11}$ are summable, we check that $\{0\}\times x_{00}\cup\{1\}\times x_{01}$ and $\{0\}\times x_{10}\cup\{1\}\times x_{11}$ are summable in ${\mathbb D}\multimap{ }E$ . Let $(i,a)\in\{0\}\times x_{00}\cup\{1\}\times x_{01}$ and $(j,b)\in\{0\}\times x_{10}\cup\{1\}\times x_{11}$ . If $i=j$ , then either $a,b\in x_{il}$ for some $l\in\{0,1\}$ and then , or $a\in x_{il}$ and $b\in x_{il'}$ with $l\not=l'$ and then since $x_{il},x_{il'}$ are summable. In both cases and hence . If $i=0$ and $j=1$ , then $a\in x_{00}\cup x_{01}$ and $b\in x_{10}\cup x_{11}$ and hence by our assumption that are $x_{00}\cup x_{01},x_{10}\cup x_{11}$ are summable. It follow that , as required.

The comonoid structure $(\mathsf{pr}_{0},\overline{\mathsf L})$ is exactly the same as in $\mathbf{Coh}$ and therefore the morphism $\widetilde\partial\in\mathbf{NCoh}(\mathbb D,\ !{\mathbb D})$ (whose existence and properties result from the fact that $\mathbf{NCoh}$ is Lafont) is defined exactly as in $\mathbf{Coh}$ :

\begin{align*} \widetilde\partial =\{(0,k[{0}])\mid k\in{\mathbb{N}}\}\cup\{(1,k[{0}]+[{1}])\mid k\in{\mathbb{N}}\}\,.\end{align*}

The functor $\mathsf S_{\mathbb D}$ can be described as follows: ${}|{\mathsf S_{\mathbb D} E}{}|=\{0,1\}\times{}|{E}{}|$ and $(i_0,a_0)\equiv_{\mathsf S_{\mathbb D} E}(i_1,a_1)$ if $i_0=i_1$ and $a_0\equiv_{E}a_1$ , and if ( and $a_0\equiv_{E}a_1\Rightarrow i_0=i_1$ ). Given $s\in\mathcal{L}(E,F)$ , we have $\mathsf S_{\mathbb D} s=\{((i,a),(i,b))\mid i\in\{0,1\}\text{ and }(a,b)\in s\}$ . By the same computation as in $\mathbf{Coh}$ (but now without the uniformity restrictions of $\mathbf{Coh}$ ), we get that

\begin{align*} \partial_E=\{((m_0,[\,]),(0,m_0))\mid m_0\in\mathcal M_{{\mathrm{fin}}}({{}|{E}{}|})\} \cup\{((m_0,[{a}]),(1,m_0+[{a}])) \mid m_0+[{a}]\in\mathcal M_{{\mathrm{fin}}}({{}|{E}{}|})\}\end{align*}

which is in $\mathbf{NCoh}(\ !{\mathsf S_{\mathbb D} E},\mathsf S_{\mathbb D}{\ !{E}})$ and satisfies all the required properties by Theorem 15.

Remark 50. This means that the issue with Girard’s uniform coherence spaces with respect to differentiation that we explained in Remarks 36 and 37 disappears in the nonuniform coherence space setting, at least if we use the exponentials introduced in Boudes (2011) ¹² . so that any morphism will coincide with its Taylor expansion in this model. This nonuniform model preserves the main feature of coherence spaces, namely that in the type $\mathbf{Bool}$ for instance, the only possible values are $\mathsf{true}$ and $\mathsf{false}$ (and not the nondeterministic superposition of these values as in the model $\operatorname{\mathbf{Rel}}$ shortly described in Section 2.4) as we have seen above with the description of ${1}\oplus{1}$ .

Remark 51. The category $\operatorname{\mathbf{Rel}}$ is a model of differential ${\textsf{LL}}$ because it is a Lafont additive category (see Remark 48) and therefore is also a differential summable resource category. That model is actually exactly the same as $\mathbf{nCoh}$ where objects are stripped from their coherence structure: the logical constructs in $\operatorname{\mathbf{Rel}}$ coincide with the constructs we perform on the webs of the objects of $\mathbf{nCoh}$ . For instance, given a set X, the object $\ !{X}$ in $\operatorname{\mathbf{Rel}}$ is simply $\mathcal M_{{\mathrm{fin}}}({X})$ . And similarly for the operation on morphisms: as constructions on relations, they are exactly the same as in $\mathbf{nCoh}$ . This identification extends even to $\widetilde\partial$ and hence to $\partial_X$ . So one of the outcomes of this paper is the fact that the constructions of differential ${\textsf{LL}}$ in $\operatorname{\mathbf{Rel}}$ are compatible with the coherence structure of $\mathbf{nCoh}$ , if we are careful enough with morphism addition. This is all the point of our categorical axiomatization to explain what this carefulness means.

7. Summability in a SMCC

Assume now that $\mathcal{L}$ is a summable resource category which is closed with respect to its monoidal product $\otimes$ so that ${\mathcal L}_!$ is cartesian closed. We use ${X}\multimap{Y}$ for the internal hom object and $\operatorname{\mathsf{ev}}\in\mathcal{L}({({X}\multimap{Y})}\otimes{X},Y)$ for the evaluation morphism. If $f\in\mathcal{L}({Z}\otimes{X},Y)$ , we use $\operatorname{\mathsf{cur}} f$ for its transpose $\in\mathcal{L}(Z,{X}\multimap{Y})$ .

We can define a natural morphism $\phi^{\multimap}=\operatorname{\mathsf{cur}}{((\mathsf S\operatorname{\mathsf{ev}})\,\phi^0_{{X}\multimap{Y},X}{})}\in\mathcal{L}(\mathsf S({X}\multimap{Y}),{X}\multimap{\mathsf S Y})$ where $\operatorname{\mathsf{ev}}\in\mathcal{L}({\left({X}\multimap{Y}\right)}\otimes{X},Y)$ .

Lemma 52. We have $\left({X}\multimap{\pi_{i}}\right)\,\phi^{\multimap}=\pi_{i}$ for $i=0,1$ and $\left({X}\multimap{\sigma_Y}\right)\,\phi^{\multimap}=\sigma_{{X}\multimap{Y}}$ .

Proof. The first two equations come from the fact that $\pi_{i}\,\phi^0={\pi_{i}}\otimes{X}$ . The last one results from Lemma 28.

Then we introduce a further axiom, required in the case where $\mathcal{L}$ is closed with respect to $\otimes$ . Its intuitive meaning is that two morphisms $f_0,f_1$ are summable if they map any element to a pair of summable elements, and that their sum is computed pointwise.

(S $\otimes$ -fun) The morphism $\phi^{\multimap}$ is an iso.

Lemma 53. If (S $\otimes$ -fun) holds, then $f_0,f_1\in\mathcal{L}({Z}\otimes{X},Y)$ are summable iff $\operatorname{\mathsf{cur}}{f_0}$ and $\operatorname{\mathsf{cur}}{f_1}$ are summable. Moreover when this property holds, we have $\operatorname{\mathsf{cur}}{(f_0+f_1)}=\operatorname{\mathsf{cur}}{f_0}+\operatorname{\mathsf{cur}}{f_1}$ .

Proof. Assume that $f_0,f_1$ are summable so that we have the witness $\langle{f_0,f_1}\rangle_{\mathsf S}\in\mathcal{L}({Z}\otimes{X},\mathsf S Y)$ and hence $\operatorname{\mathsf{cur}}\langle{f_0,f_1}\rangle_{\mathsf S}\in\mathcal{L}(Z,{X}\multimap{\mathsf S Y})$ , so let $h={(\phi^{\multimap})}^{-1}\,\operatorname{\mathsf{cur}}\langle{f_0,f_1}\rangle_{\mathsf S}\in\mathcal{L}(Z,\mathsf S{\left({X}\multimap{Y}\right)})$ . By Lemma 52, we have $\pi_{i}\, h=\left({\mathbb D}\multimap{\pi_{i}}\right)\,\operatorname{\mathsf{cur}}\langle{f_0,f_1}\rangle_{\mathsf S}=\operatorname{\mathsf{cur}}{f_i}$ for $i=0,1$ . Conversely if $\operatorname{\mathsf{cur}}{f_0},\operatorname{\mathsf{cur}}{f_1}$ are summable, we have the witness $\langle{\operatorname{\mathsf{cur}}{f_0},\operatorname{\mathsf{cur}}{f_1}}\rangle_{\mathsf S}\in\mathcal{L}(Z,\mathsf S\left({X}\multimap{Y}\right))$ and hence $\phi^{\multimap}\,\langle{\operatorname{\mathsf{cur}}{f_0},\operatorname{\mathsf{cur}}{f_1}}\rangle_{\mathsf S}\in\mathcal{L}(Z,{X}\multimap{\mathsf S Y})$ so that $g=\operatorname{\mathsf{ev}}({(\phi^{\multimap}\,\langle{\operatorname{\mathsf{cur}}{f_0},\operatorname{\mathsf{cur}}{f_1}}\rangle_{\mathsf S})}\otimes{X}) \in\mathcal{L}({Z}\otimes{X},\mathsf S Y)$ . Then by naturality of $\operatorname{\mathsf{ev}}$ and by Lemma 52, we get $\pi_{i}\, g=f_i$ for $i=0,1$ and hence $f_0,f_1$ are summable.

Assume that these equivalent properties hold so that $\langle{\operatorname{\mathsf{cur}}{f_0},\operatorname{\mathsf{cur}}{f_1}}\rangle_{\mathsf S} ={(\phi^{\multimap})}^{-1}\,\operatorname{\mathsf{cur}}{\langle{f_0,f_1}\rangle_{\mathsf S}}$ . Then,

Theorem 22. If $\mathcal{L}$ is elementarily summable, then the axiom (S $\otimes$ -fun) holds.

Proof. In this case, we know from Section 5.2 that $\phi^{\multimap}$ is the double transpose of the following morphism of $\mathcal{L}$

and therefore is an iso.

We know that ${\mathcal L}_!$ is a cartesian closed category, with internal hom-object $(X\Rightarrow Y,\operatorname{\mathsf{Ev}})$ (with $X\Rightarrow Y=\left({\ !{X}}\multimap{Y}\right)$ and $\operatorname{\mathsf{Ev}}$ defined using $\operatorname{\mathsf{ev}}$ ). Then if $\mathcal{L}$ is a differential summable resource category which is closed with respect to $\otimes$ and satisfies (S $\otimes$ -fun), we have a canonical iso between $\widetilde{\mathsf D}{(X\Rightarrow Y)}$ and $X\Rightarrow {\widetilde{\mathsf D} Y}$ and two morphisms $f_0,f_1\in{\mathcal L}_!({Z}\mathrel{\&}{X},Y)$ are summable (in $\mathcal{L}$ ) iff $\operatorname{\mathsf{Cur}}{f_0},\operatorname{\mathsf{Cur}}{f_1}\in{\mathcal L}_!(Z,X\Rightarrow Y)$ are summable and then $\operatorname{\mathsf{Cur}}{f_0}+\operatorname{\mathsf{Cur}}{f_1}=\operatorname{\mathsf{Cur}}{(f_0+f_1)}$ .

8. Conclusion

This work suggests a coherent setting for the formal differentiation of functional programs, allowing us to integrate differentiation as an ordinary construct in any functional programming language, without breaking the determinism of its evaluation, contrarily to the original differential $\lambda$ -calculus, whose operational meaning was unclear due essentially to its nondeterminism. Such a coherent differential extension of the standard language PCF of Scott and Plotkin is developed in Ehrhard (2022). Moreover, the coherent differential constructs feature commutative monadic structures suggesting to consider coherent differentiation as an effect, and this idea needs further investigations.

The fact that this differentiation is compatible with models such as (nonuniform) coherence spaces which have nothing to do with the ordinary “analytic” differentiation suggests that it could also be used for other operational goals, more internal to the scope of general purpose functional languages.