Theory and Applications of Categories, Vol. 30, No. 18, 2015, pp. 620–686.

CARTESIAN DIFFERENTIAL STORAGE CATEGORIES

R. BLUTE, J.R.B. COCKETT, AND R.A.G. SEELY

Abstract. Cartesian differential categories were introduced to provide an abstract axiomatization of categories of differentiable functions. The fundamental example is the category whose objects are Euclidean spaces and whose arrows are smooth maps.

Monoidal differential categories provide the framework for categorical models of differential linear logic. The coKleisli category of any monoidal differential category is always a Cartesian differential category. Cartesian differential categories, besides arising in this manner as coKleisli categories, occur in many different and quite independent ways. Thus, it was not obvious how to pass from Cartesian differential categories back to monoidal differential categories.

This paper provides natural conditions under which the linear maps of a Cartesian differential category form a monoidal differential category. This is a question of some practical importance as much of the machinery of modern differential geometry is based on models which implicitly allow such a passage, and thus the results and tools of the area tend to freely assume access to this structure.

The purpose of this paper is to make precise the connection between the two types of differential categories. As a prelude to this, however, it is convenient to have available a general theory which relates the behaviour of “linear” maps in Cartesian categories to the structure of Seely categories. The latter were developed to provide the categorical semantics for (fragments of) linear logic which use a “storage” modality. The general theory of storage, which underlies the results mentioned above, is developed in the opening sections of the paper and is then applied to the case of differential categories.

1. Introduction

A fundamental observation of Girard, [G87], which led to the development of linear logic, was that the hom-functor of stable domains could be decomposed as A ⇒ B := !A ⊸ B where the latter, X ⊸ Y, is the hom-functor of coherence spaces. This suggested that one might similarly be able to decompose differentiable maps between two spaces A and B as the “linear” maps from a constructed space S(A) to B. Ehrhard and Regnier’s work [ER04] on the differential λ-calculus was inspired by this analogy and in [E04] Ehrhard provided concrete examples which realized this analogy. This raised the question of how general a correspondence this was.

Research partially supported by NSERC and the Centre International de Recontres Mathématiques, and by FRQNT.

Received by the editors 2014-09-29 and, in revised form, 2015-05-05. Transmitted by Susan Niefield. Published on 2015-05-06. 2010 Mathematics Subject Classification: 18D10,18C20,12H05,32W99. Key words and phrases: monoidal categories, differential categories, Kleisli categories, differential

operators.

\begin{matrix}c \\ ◯ \end{matrix} R. Blute, J.R.B. Cockett, and R.A.G. Seely, 2015. Permission to copy for private use granted.

In [BCS06] the notion of a (monoidal) differential category was introduced as a minimal categorical doctrine in which differentiability could be studied. This generalized Ehrhard and Regnier’s ideas in various ways. It dispensed with the necessity that the setting be ∗-autonomous: the decomposition of the hom-functor was then handled through the presence of a comonad—or modality—satisfying a minimal set of coherences. Finally the differential was introduced satisfying a minimal set of identities. In this paper we shall, in fact, consider a slight strengthening of this basic notion by requiring, first, that the modality be a storage modality (i.e. the Seely isomorphisms 1 ≡ S(0) and S(A)⊗S(B) ≡ S(A × B) are present) and, second, that the differential satisfies an interchange law.

This maintained the perspective of linear logic, by providing a decomposition of differentiable functions through a comonad—or storage modality—on more basic “linear” functions. However, a rather unsatisfactory aspect of this perspective remained. Smooth functions (i.e. infinitely differentiable functions)—after all the main subject of calculus— appeared only indirectly as the maps of the coKleisli category. This left a veil between these settings and the direct understanding of these differentiable functions in the classical sense. It seemed, therefore, important to develop a more direct view of what a category of differentiable functions should look like. This caused us to examine more closely the coKleisli categories of differential categories and to seek a direct axiomatization for them.

To advance this aim we deployed (the dual of) Fuhrmann’s notion of an abstract Kleisli category [F99]. In the course of developing these ideas we stumbled on a much deeper sense in which the situation in linear logic can be read as mathematics. Thus a key result of this paper is a very general structural theorem about how “models of linear logic” arise. Rather than retrospectively remove our path to this result, we have centred the paper around the results on differential categories so that the motivation which brought us to this particular passage is not lost.

The “models of linear logic” we consider here are not, in fact, models of full linear logic, as the underlying categories are monoidal and not, in general, monoidal closed, let alone ∗-autonomous. These models were studied in depth by Gavin Bierman [B95]: he called them “Seely categories”. Given that these categories have now been the object of quite a number of studies, it is perhaps surprising that there is more to say about them. Our main rather general structural theorem points out that these categories arise in a rather natural mathematical way from the “linear maps” of Cartesian storage categories. As Cartesian storage categories have a rather natural mathematical genus, this helps to explain why “Seely categories” are such fundamental structures.

Our examination of the coKleisli categories of differential categories had led us to introduce the notion of a Cartesian differential category, [BCS09]. Cartesian differential categories are categories of “raw” differentiable maps with all the indirection—alluded to above—removed. Pleasingly these categories have a wide range of models. In particular, in [BCS09], we showed that the coKleisli category of a (monoidal) differential category— satisfying an additional interchange axiom—is a Cartesian differential category.

However, this had left open the issue of providing a converse for this result. In general, it is certainly not the case that a Cartesian differential category is the coKleisli category of a (monoidal) differential category—a basic counterexample is the category of finite dimensional real vector spaces with smooth maps. Thus, it is natural to ask what extra conditions are required on a Cartesian differential category to make it a coKleisli category of a (monoidal) differential category. This paper provides a rather natural (and appealing) answer to this question. However, lest the reader think we have completely resolved this question, we hasten to admit that it still does not answer the question in complete generality. Furthermore, it leaves some other rather natural questions open: for example it is natural to wonder whether every Cartesian differential category arises as a full subcategory of the coKleisli category of a (monoidal) differential category.

The motivation for developing Cartesian storage categories^{1} was that they provided an intermediate description of the coKleisli category of a (monoidal) differential category. These coKleisli categories were already proven to be Cartesian differential categories and, as such, had an obvious subcategory of linear maps—namely those which were linear in the natural differential sense. A Cartesian storage category uses the abstract properties of “linear maps” as the basis for its definition and is always the coKleisli category of its linear maps. In order for such a storage category to be the coKleisli category of a “Seely category”, a further ingredient was required: one must be able to represent bilinear maps with a monoidal product. The theory of these categories—which we have taken to thinking of as the theory of storage—provides the theoretical core of the paper and is described in Sections 2 and 3.

In Section 4 we apply this theory to Cartesian differential categories. Cartesian differential categories exhibit a notable further coincidence of structure. When one can classify the linear maps of a Cartesian differential category one also automatically has a transformation called a “codereliction”. Having a codereliction in any Cartesian storage category implies—assuming linear idempotents split—that one also has, for free, monoidal representation. Thus, to apply the theory of storage categories to Cartesian differential categories it suffices to know just that the linear maps are classified. Finally, but crucially for the coherence of the story, the linear maps then, with no further structural requirement, form a monoidal differential category. This provides the main result of the paper Theorem 4.3.1. Completing the circle then, at the end of the paper, we are in a position to point out that a closed Cartesian differential storage category is a model of Ehrhard and Regnier’s differential λ-calculus [ER04].

Considering that we have been discussing two types of differential category, it seemed a good idea to qualify each with an appropriate adjective, so as to distinguish between them in a balanced manner. So we shall (in this paper) refer to differential categories as “monoidal differential categories”, to contrast them with “Cartesian differential categories”. In parallel with this, we introduce other terminological pairings which are natural from the perspective of this paper, but are also structures which have received attention under different names: For example, “monoidal storage categories” are essentially “Seely categories” and “monoidal differential storage categories” are essentially what previously we called differential storage categories. Our purpose is not to precipitate any renaming of familiar structures but rather to emphasize the structural relationships which emerge from the story we tell here.

1In [Kock12] a closely related theory, based on commutative monads, is developed. Interestingly that work was motivated by probability distributions and so is related to abstracting integration rather than differentiation.

2. Cartesian Storage categories

In the discussion above two situations were described in which we selected from a Cartesian category certain maps, namely the coherent maps in stable domains and the linear maps among differentiable maps, and then used a classification of these maps to extract a Seely category. The aim of the next two sections is to show why this works as a general procedure and, moreover, can produce a monoidal storage (or “Seely”) category. In fact, our aim is to prove much more: namely that all “Seely categories” (with an exact modality) arise in this manner.

We start by defining what is meant by a system L of linear maps. One way to view a linear system is as a subfibration of the simple fibration. In a category equipped with a system of linear maps, we shall often suppress explicit mention of L, referring to maps belonging to this system as simply being linear. Such systems arise very naturally in Cartesian closed categories from exponentiable systems of maps and we make a detour to describe these connections.

Our initial aim is to characterize the categories in which there is a decomposition of maps analogous to that in linear logic. This eventually leads us to “Seely categories” as those in which all the “first-order” structural components of the logic are present.

Leaving definitions for later, the path will be the following: a “Cartesian storage category” is a category equipped with a system of linear maps which are “strongly and persistently classified”. We then prove that this is equivalent to demanding that the category is a “strong abstract coKleisli category”. This, in turn, is equivalent to being the coKleisli category of a category with a “forceful” comonad. Finally, to this story we add, in the next section, “monoidal representation”, which when present, ensures the linear maps forms a monoidal storage category—this is essentially a “Seely category”.

2.1. Systems of linear maps. By a system of maps of a category is meant a subcategory on the same objects: a Cartesian system of maps of a Cartesian category is just such a subcategory closed under the product structure. This means that projections, diagonal maps, and final map must be in the system and, furthermore, the pairing of any two maps in the system must be in the system. For a system L of maps to be linear it must determine a subfibration of the simple fibration.

The simple slice 𝕏[A] at A—that is the fiber over A of the simple fibration—of a Cartesian category 𝕏, has the same objects as 𝕏 but the homsets are modified 𝕏[A](X, Y) = 𝕏(A × X, Y). The composition in 𝕏[A] of two maps g: A × X ⟶ Y and h: A × Y ⟶ Z is ⟨π_{0}, g⟩h with identities given by projection π_{1}: A × X ⟶ X. The substitution functor between simple slices has the following effect on the maps of 𝕏. If f: A ⟶ B is any map of 𝕏, g: X ⟶ Y a map of 𝕏[B], (in 𝕏 this is a map g: B × X ⟶ Y), then 𝕏[f](g) = (f × 1)g: A × X ⟶ Y, which is a map of 𝕏[A].

2.1.1. Definition. A Cartesian category 𝕏 is said to have a system of linear maps, L, in case in each simple slice 𝕏[A] there is a system of maps L[A] ⊆ 𝕏[A], which we shall refer to as the L[A]-linear maps (or, when L is understood, simply as “linear” maps), satisfying:

[LS.1] for each X, Y, Z ∈ 𝕏[A], all of 1_{X}, π_{0}: X × Y ⟶ X, π_{1}: X × Y ⟶ Y are in L[A] and, furthermore, ⟨f, g⟩: X ⟶ Y × Z ∈ L[A] whenever f, g ∈ L[A];

[LS.2] in each 𝕏[A], L[A], as a system of maps, is closed under composition, furthermore, whenever g ∈ L[A] is a retraction and gh ∈ L[A] then h ∈ L[A];

[LS.3] all substitution functors

{A ⟶^{f} B \atop 𝕏[B] ⟶_{𝕏[f]} 𝕏[A]}

preserve linear maps.

Notice how a system of linear maps determines a subfibration:

\xymatrix{L[𝕏] \ar[d]^{∂_{L}} \ar[r]^{I[𝕏]} & 𝕏[𝕏] \ar[d]^{∂} \\ L \ar[r]_{I} & 𝕏}

where I is the obvious inclusion and L[𝕏] is the category:

[Objects:] (A, X) ∈ 𝕏_{0} × 𝕏_{0}

[Maps:] (f, g): (A, X) ⟶ (B, Y) where g: A ⟶ B is any map and f: A × X ⟶ Y is linear in its second argument.

Composition and identities are as in 𝕏[𝕏], where the maps are the same but with no linear restriction. Composition is defined by (f, g)(f′, g′) = (⟨π_{0}g, f⟩f′, gg′) and (π_{1}, 1) is the identity map. Cartesian maps are of the form (π_{1}, g): (A, X) ⟶ (B, X).

Furthermore we observe using [LS.2]:

2.1.2. Lemma. For any 𝕏 with a system of linear maps in any slice 𝕏[A]:

(i) if f is an linear map which is an isomorphism, then f^{−1} is linear;

(ii) if e is a linear idempotent which splits as a retraction r and a section i, and if r is linear, then i is also linear.

We shall need terminology which focuses on the linear argument rather than the context of that argument. Thus to say that a map f: X × A ⟶ Y is linear in its second argument is equivalent to saying that f is L[X]-linear. Similarly, a map, f, is linear in its first argument if c_{×}f is L[X]-linear.

2.1.3. Lemma. If L is a system of linear maps on a Cartesian category 𝕏 then if f: X ×A ⟶ B and g: Y × B ⟶ C are linear in their second arguments then (f × 1)g: Y × X × A ⟶ C is linear in its third argument.

Proof. As f is linear in 𝕏[X], 𝕏[π_{1}](f): Y × X × A ⟶ C is linear in 𝕏[Y × X]. Similarly as g is linear in 𝕏[Y], 𝕏[π_{0}](g) is linear in 𝕏[Y × X]. Now (1 × f)g = 𝕏[π_{1}](f)𝕏[π_{0}](g) which makes it a composite of linear maps and so itself linear.

The lemma means that to determine whether a composite is linear in a particular argument it suffices to know that each composition was at a linear argument.

If L is a system of linear maps then f: A × B ⟶ C is (L-)bilinear in case it is linear in each argument individually.

Finally we make the useful if immediate observation:

2.1.4. Lemma. If 𝕏 has a system of linear maps L then each simple slice, 𝕏[A], inherits a system of linear maps L[A].

2.2. Closed systems of maps. A system of linear maps induces a system of maps on 𝕏 itself, as 𝕏 ≅ 𝕏[1]. This class, which we shall denote by L[], will determine the whole system of linear maps when the category is Cartesian closed. However, clearly such an L[] must satisfy some special properties which we now outline.

2.2.1. Definition. A system of maps C ⊆ 𝕏 is an exponentiable system of maps in case:

[ES.1] for each X, Y, Z ∈ 𝕏, all of 1_{X}, π_{0}: X × Y ⟶ X, π_{1}: X × Y ⟶ Y, Δ: X ⟶ X × X are in C and, furthermore, ⟨f, g⟩: X ⟶ Y × Z ∈ C whenever f, g ∈ C;

[ES.2] C as a system of maps is closed under composition, moreover, whenever g ∈ C is a retraction and gh ∈ C then h ∈ C;

[ES.3] whenever f: A ⟶ B is in C and g: X ⟶ Y is any map, then g ⇒ f: Y ⇒ A ⟶ X ⇒ B is in C;

[ES.4] furthermore

η[X] = curry(π_{1}): A ⟶ X ⇒ A
μ[X] = curry((Δ × 1)(1 × eval)eval): X ⇒ (X ⇒ A) ⟶ X ⇒ A

are all in C.

Here we use the exponential correspondence in the following form:

{A × X ⟶^{f} B \atop X ⟶_{curry(f)} A ⇒ B}.

2.2.2. Definition. We shall say that a system of linear maps in a Cartesian closed category is closed in case

• each evaluation map is linear in its second (higher-order) argument.

• the system is closed under currying, that is if f: A × B × C ⟶ D is linear in its second argument (B) then curry(f): B ×C ⟶ A ⇒ D is linear in its first argument.

Equivalently, when 𝕏 is Cartesian closed, a system of linear maps is closed provided k: B × X ⟶ Y ∈ L[B] if and only if curry(k) ∈ L[].

2.2.3. Proposition. In a Cartesian closed category 𝕏, exponentiable systems of maps are in bijective correspondence with closed systems of linear maps.

Proof. Given an exponentiable system of maps C we define a system of linear maps C̃, by saying f: A × B ⟶ C is linear in 𝕏[A] if and only if curry(f): B ⟶ A ⇒ C is in C. This defines a system of linear maps since:

[LS.1] In 𝕏[A] the identity map is π_{1}: A × X ⟶ X which is linear as curry(π_{1}) is. For the remainder note that A × X ⟶^{π_{1}} X ⟶^{f} Y has curry(π_{1}f) = curry(π_{0})A ⇒ f so that whenever f is in C then curry(π_{1}f) will be in C. Finally note that curry(⟨f, g⟩) = ⟨curry(f), curry(g)⟩(⟨A ⇒ π_{0}, A ⇒ π_{1}⟩)^{−1}.

[LS.2] The curry of a composite in 𝕏[B] is given by

curry(⟨f, π_{1}⟩g) = curry(f)(B ⇒ curry(g))μ[B]

which is a composite of C-maps when f and g are.

Suppose now that g • h in 𝕏[B] and curry(g), curry(gh) ∈ C with g a retraction (with section g^{s}) then (B ⇒ curry(g^{s})μ[B] is right inverse to (B ⇒ curry(g))μ[B] where the latter is in C. Also

B ⇒ curry(gh))μ[B] = B ⇒ curry(g))μ[B]B ⇒ curry(h))μ[B]

so that B ⇒ curry(h))μ[B] ∈ C But this means η[B](B ⇒ curry(h))μ[B] = curry(h) is in C.

[LS.3] If curry(h) ∈ C then curry(𝕏[f](h)) = curry((1×f)h) = (f ⇒ B)curry(h) so that the substitution functors preserve C̃-maps.

We observe that as curry(eval) = 1 that in C̃ the evaluation map must necessarily be linear in its second (higher-order) argument.

For the converse, given a system of linear maps L in which evaluation maps are linear in their second argument, we now show that L[] is an exponential system of maps. The only difficulties are [ES.3] and [ES.4]. For the former note that f ⇒ g is obtained by currying:

A × (A′ ⇒ B′) ⟶^{f × 1} A′ × (A′ ⇒ B′) ⟶^{eval} B′ ⟶^{g} B

However observe that this is linear in its second argument so that currying preserves this establishing [ES.3]. For the latter the argument is similar as both η and μ are obtained by currying maps which are linear in the appropriate coordinates.

Finally we must argue that these transitions are inverse: that C̃[] = C is immediate. We show that L̃[] = L by showing L ⊆ L̃[] and the converse. Suppose f ∈ L[A] then curry(f) ∈ L[] so that f ∈ L̃[][A] as required. Conversely suppose f ∈ L̃[][A] then curry(f) ∈ L[] but this means f = (1 × curry(f))eval is in L[A].

We note that when L is an exponentiable system of linear maps, the notion of being (L-)bilinear becomes the requirement that both curry(f) and curry(c_{×}f) are linear in 𝕏.

2.3. Storage. A Cartesian storage category is a Cartesian category 𝕏 together with a system of linear maps, L, which is persistently and strongly classified,^{2} in the following sense.

2.3.1. Definition.

(i) A system of linear maps is classified if there is an object function S and a family of maps φ_{X}: X ⟶ S(X) such that for each f: X ⟶ Y, there is a unique linear map f^{♯} such that

\xymatrix{X \ar[r]^{f} \ar[d]_{φ_{X}} & Y \\ S(X) \ar@{.>}[ur]_{f^{♯}}}

commutes.

(ii) A system of linear maps is strongly classified if there is an object function S and maps X ⟶^{φ_{X}} S(X) such that for every f: A×X ⟶ Y there is a unique f^{♯}: A×S(X) ⟶ Y in L[A] (that is, f^{♯} is linear in its second argument) making

\xymatrix{A × X \ar[d]_{1×φ_{X}} \ar[r]^{f} & Y \\ A × S(X) \ar@{.>}[ur]_{f^{♯}}}

commute.

(iii) A strong classification is said to be persistent in case whenever f: A × B × X ⟶ Y is linear in its second argument B then f^{♯}: A × B × S(X) ⟶ Y is also linear in its second argument.

2The notion of classification might (by comparison with the notion of a subobject classifier in a topos, for example) be called coclassification—we shall not do that. Furthermore, we also use the term “represented”, especially in the sense that under the classification given by S and φ, f^{♯} represents f.

2.3.2. Remark. When the linear maps are classified this makes the inclusion of the linear maps into a right adjoint. A strong classification makes the inclusion of the linear maps into the simple fibration a fibred right adjoint. A strong persistent classification allows a powerful proof technique which we shall use extensively in what follows. To establish the equality of

f, g: A × \underbrace{S(X) × ...S(X)}_{n} ⟶ Y

when f and g are maps which are linear individually in their last n arguments, it suffices to show (1 × φ^{n})f = (1 × φ^{n})g. Note that the linearity precondition is vital!

Strong classification gives a morphism of fibrations defined by:

S[𝕏]: 𝕏[𝕏] ⟶ L[𝕏]; (f, g) ↦ ((fφ)^{♯}, g).

This is a functor on the total category. Identity maps are preserved because

\xymatrix{A × X \ar[d]_{1×φ} \ar[r]^{π_{1}} & X \ar[r]^{φ} & S(X) \\ A × S(X) \ar@{-->}[urr]_{π_{1}}}

commutes making (π_{1}φ)^{♯} = π_{1}. Composition is preserved as

\xymatrix{A × X \ar[d]_{1×φ} \ar[r]^{⟨π_{0}g,f⟩} & B × Y \ar[d]^{1×φ} \ar[r]^{f′} & Z \ar[r]^{φ} & S(Z) \\ A × S(X) \ar[r]_{⟨π_{0}g,(fφ)^{♯}⟩} & B × S(Y) \ar[urr]_{(f′φ)^{♯}}}

Finally S[𝕏] preserves Cartesian arrows as S[𝕏](π_{1}, g) = (π_{1}, g): (A, S(X)) ⟶ (B, S(X)).

Therefore the classification is the couniversal property for the inclusion of the linear maps into the simple fibration, and so S is a fibred right adjoint.

2.3.3. Remark. We recall some definitions dealing with the notion of strength.

A functor S: 𝕏 ⟶ 𝕐 between monoidal categories is strong if there is a natural transformation (“strength”) θ^{S}: X ⊗ S(Y) ⟶ S(X ⊗ Y) so that the following diagrams commute:

\xymatrix{⊤ ⊗ S(Y) \ar[dr]_{u_{⊗}^{L}} \ar[rr]^{θ} &  & S(⊤ ⊗ Y) \ar[dl]^{S(u_{⊗}^{L})} & X ⊗ (Y ⊗ S(Z)) \ar[d]_{1⊗θ} \ar[r]^{a_{⊗}} & (X ⊗ Y) ⊗ S(Z)) \ar[dd]^{θ} \\  & S(Y) &  & X ⊗ S(Y ⊗ Z) \ar[d]_{θ} \\  &  &  & S(X ⊗ (Y ⊗ Z)) \ar[r]_{S(a_{⊗})} & S((X ⊗ Y) ⊗ Z)}

The identity functor is strong (with strength given by the identity), and if S and T are strong, so is their composite, with strength given by θ^{T} T (θ^{S}): X ⊗ T (S(Y)) ⟶ T (X ⊗ S(Y)) ⟶ T (S(X ⊗ Y)).

A natural transformation ψ: S ⟶ T between strong functors is strong if the following commutes.

\xymatrix{X ⊗ S(Y) \ar[d]_{1⊗ψ} \ar[r]^{θ^{S}} & S(X ⊗ Y) \ar[d]^{ψ} \\ X ⊗ T (Y) \ar[r]_{θ^{T}} & T (X ⊗ Y)}

A monad (S, η, μ) is strong if each of S, η, and μ is strong.

Thus we have proved:

2.3.4. Lemma. If 𝕏 has a strongly classified system of linear maps, then S: 𝕏 ⟶ 𝕏 is a strong functor (and thus a morphism of simple fibrations) and determines a fibred right adjoint to the inclusion I: ∂_{L} ⟶ ∂.

The strength θ is given explicitly by

\xymatrix{A × X \ar[d]_{1×φ} \ar[r]^{φ} & S(A × X) \\ A × S(X) \ar@{-->}[ur]_{θ=φ^{♯}}}

and all the natural transformations are appropriately strong. The strength of φ, the unit of the adjunction, is provided by the defining diagram of the strength transformation θ above. Notice that ϵ is not natural as ϵf is not necessarily linear unless f is; however, it does satisfy the strength requirement. However, μ = ϵ_{S( )} is natural and also strong.

This adjunction induces a comonad Š = (S, δ, ϵ) on the linear maps whose data is given by

[figure: A; φ; S(A); ϵ; A; A; φ; φ; S(A); δ=S(φ); S(A); φ; S(S(A))]

Notice that by definition both ϵ and δ are linear (in L[]).

In Cartesian storage categories the classification is also persistent, which means that when you make a function linear in an argument—by classifying it at that argument—you do not destroy the linearity that any of the other arguments might have enjoyed. This has the important consequence that the universal property can be extended to a multiclassification property as mentioned above. Here is the argument for the bi-classification property:

2.3.5. Lemma. In a Cartesian storage category, for each f: A × X × Y ⟶ Z there is a unique f^{♯_{2}}, which is linear in both its second and third arguments (i.e. bilinear), such that

\xymatrix{A × X × Y \ar[d]_{1×φ×φ} \ar[r]^{f} & Z \\ A × S(X) × S(Y) \ar@{.>}[ur]_{f^{♯_{2}}}}

commutes.

Proof. To establish the existence of a map we may extend it in stages:

\xymatrix{A × X × Y \ar[d]_{1×φ×1} \ar[r]^{f} & Z \\ A × S(X) × Y \ar[d]_{1×1×φ} \ar@{.>}[ur]_{f^{♯_{1}}} \\ A × S(X) × S(Y) \ar@{.>}[uur]_{f^{♯_{2}}}}

the map f^{♯_{2}} is then linear in its last two arguments by persistence. Suppose, for uniqueness, that a map g, which is linear in its last two arguments, has (1 × φ × φ)g = f: A × S(X) × S(Y) ⟶ Z. Then f^{♯_{1}} = (1 × 1 × φ)g as the latter is certainly linear in its middle argument. Whence g = f^{♯_{2}}.

This allows the observation that there is a candidate for monoidal structure m_{×}: S(A)× S(B) ⟶ S(A × B) given as the unique bilinear map lifting φ:

\xymatrix{A × B \ar[d]_{φ×φ} \ar[r]^{φ} & S(A × B) \\ S(A) × S(B) \ar@{.>}[ur]_{m_{×}}}

We observe that this implies the following two identities:

2.3.6. Lemma. In any Cartesian storage category:

(i) m_{×} = θS(θ′)μ;

(ii) (ϵ × ϵ)m_{×} = m_{×}S(m_{×})ϵ.

Proof. Both can be verified using the universal property outlined in Lemma 2.3.5. First one notices that all the maps are bilinear, thus it suffices to show that prefixing with φ×φ gives the same maps:

(i) Clearly m_{×} is bilinear. Recall that μ = ϵ_{S( )}. Notice that θS(θ′)μ is linear in its first argument as θ is and S(θ′)μ is linear. However, using persistence it is also linear in its second argument as:

[figure: A × S(B); φ×1; φ; θ′; S(A × B); φ; S(A × B); S(A) × S(B); θ; S(S(A) × B); S(θ′); S^{2}(A × B); ϵ_{S(A×B)}=μ]

This gives:

(φ × φ)m_{×} = φ
(φ × φ)θS(θ′)μ = (φ × 1)(1 × φ)θS(θ′)μ
= (φ × 1)φS(θ′)μ
= (φ × 1)θ′φμ
= φφμ = φ

(ii) In this case both maps are clearly bilinear and thus the equality is given by:

(φ × φ)(ϵ × ϵ)m_{×} = m_{×}
(φ × φ)m_{×}S(m_{×})ϵ = φS(m_{×})ϵ
= m_{×}φϵ = m_{×}

.

Then:

2.3.7. Proposition. In a Cartesian storage category:

(i) S = (S, φ, μ) is a commutative monad, that is S is a monoidal monad with respect to the product with m_{×} = θS(θ′)μ: S(A) × S(B) ⟶ S(A × B);

(ii) for every object X

S(S(X)) ϵ ; \overrightarrow{⟶} ; S(ϵ) S(X) ⟶^{ϵ} X

is an absolute coequalizer;

(iii) f: A × X ⟶ Y is linear in its second argument if and only if

\xymatrix{A × S(X) \ar[d]_{1×ϵ} \ar[r]^{θ} & S(A × X) \ar[r]^{S(f)} & S(Y) \ar[d]^{ϵ} \\ A × X \ar[rr]_{f} &  & Y}

commutes; (iv) and so f: A × B ⟶ Y is bilinear ( i.e. linear in its first two arguments) if and only

if

\xymatrix{S(A) × S(B) \ar[d]_{ϵ×ϵ} \ar[r]^{m_{×}} & S(A × B) \ar[r]^{S(f)} & S(Y) \ar[d]^{ϵ} \\ A × B \ar[rr]_{f} &  & Y}

commutes.

Proof.

(i) To establish this, given that we know the monad is strong, it suffices to show that the strength is commutative. That is that the following diagram commutes:

\xymatrix{S(A) × S(B) \ar[d]_{θ′} \ar[r]^{θ} & S(S(A) × B) \ar[r]^{S(θ′)} & S(S(A × B)) \ar[dd]^{μ} \\ S(A × S(B)) \ar[d]_{S(θ)} \\ S(S(A × B)) \ar[rr]_{μ} &  & S(A × B)}

The defining diagrams for the two routes round this square are:

[figure: A × B; φ; φ×1; S(A) × B; θ′; φ; 1×φ; S(A) × S(B); θ; S(A × B); φ; S(A × S(B)); S(θ′); S(S(A × B)); μ; S(A × B)]

and

[figure: A × B; φ; 1×φ; A × S(B); θ; φ; φ×1; S(A) × S(B); θ′; S(A × B); φ; S(S(A) × B); S(θ); S(S(A × B)); μ; S(A × B)]

Note that, because the classification is persistent, following Lemma 2.3.6 (i), both these constructed maps are bilinear. Thus, using the universal property of φ × φ they are equal. This shows that the two ways round the square making the strength commutative are equal.

(ii) ϵ is split by φ and so this is a split coequalizer: that is ϵφ = φS(ϵ) and both φϵ = 1 and S(φ)ϵ = 1. Thus this is an absolute coequalizer.

(iii) If f is linear in its second argument then (1×ϵ)f is also linear in its second argument (recall ϵ is linear). But this means f^{♯} = (1×ϵ)f. However, also we know f^{♯} = θS(f)ϵ. Thus, the diagram (which shows linearity) commutes.

Conversely, suppose this diagram commutes; then notice it suffices to show that we can factor f^{♯} = (1 × ϵ)g. Then, as 1 × ϵ is linear and also a retraction, g must be linear. Finally g must of course be f as f = (1 × φ)f^{♯} = (1 × φ)(1 × ϵ)g = g. Now to show we can factor f^{♯} in this manner, we can use exactness; it suffices to show that

A × S^{2}(X) 1 × S(ϵ) ; \overrightarrow{⟶} ; 1 × ϵ A × S(X) ⟶^{f^{♯}} Y

commutes. For this we have the following simple calculation which uses the fact that ϵϵ = S(ϵ)ϵ:

(1 × ϵ)f^{♯} = (1 × ϵ)θS(f)ϵ
= (1 × ϵ)(1 × ϵ)f = (1 × ϵϵ)f
= (1 × S(ϵ)ϵ)f = (1 × S(ϵ))(1 × ϵ)f
= (1 × S(ϵ))θS(f)ϵ = (1 × S(ϵ))f^{♯}.

(iv) This is immediate from the preceding.

Notice that this means that in a Cartesian storage category, the system L may equivalently be viewed as being induced by the monad S. The second property says that the induced comonad on the subfibration of linear maps is an exact modality. In the next section, as we study this comonad in more detail, the significance of this property will become clear.

We end this subsection with two observations. The first of these is that the notion of a storage category is simply stable in the sense that each simple slice of a storage category is itself a storage category. This, in principle, will allow us to suppress the fibred context of a statement about storage categories, as such statements will be true in all simple-slice fibres.

2.3.8. Lemma. If 𝕏 is a Cartesian storage category then each simple slice, 𝕏[A], is also a Cartesian storage category.

The second observation concerns the algebras of the monad (S, φ, μ = ϵ_{S}). Recall that an algebra for this monad is an object A with a map ν: S(A) ⟶ A such that

[figure: A; φ; S(A); ν; A; S(φ); A; S^{2}(A); S(ν); ϵ_{S(A)}; S(A); ν; S(A); ν; A]

Consider the algebras whose structure maps are linear. Of course, there could be algebras whose structure map does not lie in L but for now we consider the case ν ∈ L. These algebras, due to the first triangle identity above, must be precisely of the form ν = ϵ_{A}— and then the remaining identities will automatically hold. A homomorphism of such algebras is then precisely a map f: A ⟶ B which is ϵ-natural. Thus, we have:

2.3.9. Lemma. The full subcategory of S-algebras, determined by algebras whose structure maps is linear, is, for any Cartesian storage category 𝕏, isomorphic to the subcategory of linear maps L[].

2.4. Abstract coKleisli categories. Abstract coKleisli categories were introduced (in the dual) by Fuhrmann [F99] to provide a direct description of coKleisli categories. Thus, every coKleisli category is an abstract coKleisli category and, furthermore, from any abstract coKleisli category, 𝕏, one can construct a subcategory, 𝕏̌, with a comonad, Š, whose coKleisli category is exactly the original category 𝕏. Of particular interest is when the constructed category, 𝕐̌_{S}, of a coKleisli category 𝕐_{S} is precisely 𝕐: this, it turns out, happens precisely when S is an exact modality in the sense above.

This section views a Cartesian storage category from the perspective of its being an abstract coKleisli category. A Cartesian storage category is clearly a rather special abstract coKleisli category so that our aim is to determine what extra algebraic conditions are being required.

2.4.1. Definition. An abstract coKleisli category is a category 𝕏 equipped with a functor S, a natural transformation φ: 1_{𝕏} ⟶ S, and a family of maps ϵ_{A}: S(A) ⟶ A (which is not assumed to be natural) such that ϵ_{S( )} is natural. Furthermore:

φϵ = 1, S(φ)ϵ = 1, and ϵϵ = S(ϵ)ϵ

An abstract coKleisli category is said to be Cartesian if its underlying category, 𝕏, is a Cartesian category such that !, π_{0} and π_{1} are all ϵ-natural (in the sense that ϵπ_{0} = S(π_{0})ϵ, etc.).

In an abstract coKleisli category the ϵ-natural maps, that is those f which satisfy S(f)ϵ = ϵf, form a subcategory 𝕏_{ϵ} and on this subcategory Š = (S, S(φ), ϵ) is a comonad.

On 𝕏, the larger category, S = (S, φ, ϵ_{S( )}) is a monad. It is not hard to see that the ϵ-natural maps form a system of linear maps which are classified:

\xymatrix{X \ar[d]_{φ} \ar[r]^{f} & Y \\ S(X) \ar[ur]_{S(f)ϵ}}

where the uniqueness follows since if h: S(X) ⟶ Y has φh = f then S(f)ϵ = S(φh)ϵ = S(φ)ϵh = h.

In an abstract coKleisli category, we shall always use the ϵ-natural maps as the default system L of maps. We now address the question of when this system is a linear system of maps.

2.4.2. Definition. An abstract coKleisli category is said to be strong in case it is Cartesian and S is a strong functor, φ a strong natural transformation, and ϵ is strong, even where it is unnatural, meaning that the following commutes for all objects A and X:

\xymatrix{A × S(X) \ar[r]^{θ} \ar[dr]_{1×ϵ} & S(A × X) \ar[d]^{ϵ} \\  & A × X}

In a strong abstract coKleisli category 𝕏, S = (S, φ, ϵ_{S( )}) is clearly a strong monad. We observe:

2.4.3. Proposition. If (𝕏, S, φ, ϵ) is a strong abstract coKleisli category then the maps f: A × X ⟶ Y of L[A] ⊆ 𝕏[A] such that

\xymatrix{A × S(X) \ar[d]_{1×ϵ} \ar[r]^{θ} & S(A × X) \ar[r]^{S(f)} & S(Y) \ar[d]^{ϵ} \\ A × X \ar[rr]_{f} &  & Y}

form a system, L_{S}[𝕏], of linear maps which are strongly classified by (S, φ).

Proof. We check the conditions for being a system of linear maps:

[LS.1] The identity in 𝕏[A] is ϵ-natural since (by strength) θ; S(π_{1}) = π_{1}:

\xymatrix{A × S(X) \ar[dr]_{π_{1}} \ar[dd]_{1×ϵ} \ar[r]^{θ} & S(A × X) \ar[d]^{S(π_{1})} \\  & S(X) \ar[d]^{ϵ} \\ A × X \ar[r]_{π_{1}} & X}

We check that the projections in 𝕏[A] are ϵ-natural using:

\xymatrix{A × S(X_{1} × X_{2}) \ar[d]_{1×ϵ} \ar[r]^{θ} & S(A × (X_{1} × X_{2})) \ar[r]^{S(π_{1})} & S(X_{1} × X_{2}) \ar[d]^{ϵ} \ar[r]^{S(π_{i})} & S(X_{i}) \ar[d]^{ϵ} \\ A × (X_{1} × X_{2}) \ar[rr]_{π_{1}} &  & X_{1} × X_{2} \ar[r]_{π_{i}} & X_{i}}

Suppose f_{1}: A × X ⟶ Y_{1} and f_{1}: A × X ⟶ Y_{1} are ϵ-natural in 𝕏[A]. Then in the following diagram the left hand square commutes if and only if the two outer squares corresponding to the two post compositions with the projections commute.

\xymatrix{A × S(X) \ar[d]_{1×ϵ} \ar[r]^{θ} & S(A × X) \ar[r]^{S(⟨f_{1},f_{2}⟩)} & S(Y_{1} × Y_{2}) \ar[d]^{ϵ} \ar[r]^{S(π_{i})} & S(Y_{i}) \ar[d]^{ϵ} \\ A × X \ar[rr]_{⟨f_{1},f_{2}⟩} &  & Y_{1} × Y_{2} \ar[r]_{π_{i}} & Y_{i}}

However the outer squares commute by assumption and so ⟨f_{1}, f_{2}⟩ is ϵ-natural in 𝕏[A].

[LS.2] We must show that ϵ-natural maps in 𝕏[A] compose. We shall do it explicitly:

\xymatrix{ & S(A × X) \ar[drrr]^{S(⟨π_{0},f⟩)} \ar[r]^{S(Δ×1)} & S(A × A × X) \ar[drr]^{S(1×f)} \\ A × S(X) \ar[dd]_{1×ϵ} \ar@{-->}[ur]^{θ} \ar[r]^{Δ×1} & A × A × S(X) \ar[r]^{1×θ} \ar[dd]^{1×1×ϵ} & A × S(A × X) \ar[u]^{θ} \ar[r]^{1×S(f)} & A × S(Y) \ar[r]^{θ} \ar[dd]^{1×ϵ} & S(A × Y) \ar[d]^{S(g)} \\  &  &  &  & S(Z) \ar[d]^{ϵ} \\ A × X \ar[rrr]_{⟨π_{0},f⟩} \ar[r]_{Δ×1} & A × A × X \ar[rr]_{1×f} &  & A × Y \ar[r]_{g} & Z}

Next we must show that if gh is ϵ-natural and g is a retraction which is ϵ-natural then h is ϵ-natural. We shall prove it in the basic case leaving it as an exercise for the reader to do the calculation in a general slice.

We have

\xymatrix{S(A) \ar[d]^{ϵ} \ar[r]^{S(g)} & S(B) \ar[d]^{ϵ} \ar[r]^{S(h)} & S(C) \ar[d]^{ϵ} \\ A \ar[r]^{g} & B \ar[r]^{h} & C}

where the left square is known to commute and the outer square commutes. This means S(g)S(h)ϵ = S(g)ϵh but S(g) is a retraction as g is so the right square commutes.

[LS.3] We must show that if f is ϵ-natural in 𝕏[A] then (g × 1)f is ϵ-natural. Here is the diagram:

\xymatrix{A × S(X) \ar[dr]_{g×1} \ar[dd]_{ϵ} \ar[r]^{θ} & S(A × X) \ar[dr]_{S(g×1)} \ar[rr]^{S((g×1)f)} &  & S(Y) \ar[dd]^{ϵ} \\  & B × S(X) \ar[d]_{1×ϵ} \ar[r]_{θ} & S(B × X) \ar[ur]_{S(f)} \\ A × X \ar[r]_{g×1} & B × X \ar[rr]_{f} &  & Y}

This system of linear maps is always strongly classified by (S, φ) by defining f^{♯} = θS(f)ϵ, which is clearly ϵ-natural in 𝕏[A], and certainly has (1 × φ)θS(f)ϵ = f. It is unique, for if g is ϵ-natural in 𝕏[A] and has (1 × φ)g = f, then

θS(f)ϵ = θS((1 × φ)g)ϵ = (1 × S(φ))θS(g)ϵ = (1 × S(φ))(1 × ϵ)g = g.

To complete the story it remains to establish the property to which persistence corresponds:

2.4.4. Lemma. A strong abstract coKleisli category has a persistent strong classification of the ϵ-natural maps if and only if S is a commutative (or monoidal) monad.

Proof. Suppose that f: A × X × Y ⟶ Z is linear in its second argument. That is

\xymatrix{A × S(X) × Y \ar[d]_{1×ϵ×1} \ar[r]^{θ_{2}} & S(A × X × Y) \ar[r]^{S(f)} & S(Z) \ar[d]^{ϵ} \\ A × X × Y \ar[rr]_{f} &  & Z}

commutes. Then we must show that after linearizing the last argument the result is still linear in the second argument. That is the following diagram commutes:

\xymatrix{ & S(A × X × S(Y)) \ar[r]^{S(θ_{3})} & S^{2}(A × X × Y) \ar[dr]^{ϵ} \ar[r]^{S^{2}(f)} & S^{2}(Z) \ar[dr]^{ϵ} \\ A × S(X) × S(Y) \ar@{-->}[ur]^{θ_{2}} \ar[d]_{1×ϵ×1} \ar@{-->}[dr]_{θ_{3}} &  &  & S(A × X × Y) \ar[r]^{S(f)} & S(Z) \ar[d]^{ϵ} \\ A × X × S(Y) \ar@{-->}[dr]_{θ_{3}} & S(A × S(X) × Y) \ar[d]^{S(1×ϵ×1)} \ar[r]^{S(θ_{2})} & S^{2}(A × X × Y) \ar[r]_{S^{2}(f)} \ar[ur]_{ϵ} & S^{2}(Z) \ar@{-->}[ur]_{ϵ} \ar[d]_{S(ϵ)} & Z \\  & S(A × X × Y) \ar[rr]_{S(f)} &  & S(Z) \ar[ur]_{ϵ}}

Conversely we have already established that a persistent strong classification gives rise to a commutative monad.

We shall say that a strong abstract coKleisli category is commutative if its monad is. We have now established:

2.4.5. Theorem. If 𝕏 is a Cartesian category, then 𝕏 is a Cartesian storage category (that is, 𝕏 has a persistently strongly classified system of linear maps) if and only if it is a strong abstract commutative coKleisli category.

2.5. Linear idempotents. A very basic construction on a category is to split the idempotents and we pause our development to briefly consider how this construction applies to storage categories. In a storage category there is a slightly subtle issue as it is quite possible for a linear idempotent to split into two non-linear components. This means that even though an idempotent may split in the “large” category of all maps it need not in the subcategory of linear maps. We shall be interested in splitting the linear idempotents linearly, for in this case we can show that the resulting category is also a storage category which extends the original category without introducing any new linear maps.

We start with a basic observation:

2.5.1. Lemma. In a Cartesian storage category:

(i) When fg is linear and g is monic and linear, then f is linear;

(ii) When fg is linear and f is linear with S(f) epic, then g is linear;

(iii) A linear idempotent e: X ⟶ Y splits linearly, in the sense that there is a splitting (r, s) with rs = e and sr = 1 with both r and s linear iff there is a splitting in which at least one of r and s are linear.

Proof. Consider

[figure: S(X); S(fg); ϵ; S(f); S(Y); ϵ; S(Y); ϵ; S(g); X; fg; f; Y; Y; g]

Under the conditions of (i) the back face commutes since fg is linear (i.e. ϵ-natural), and the “g face” commutes. Then S(f)ϵg = S(f)S(g)ϵ = ϵfg and, thus, as g is monic, S(f)ϵ = ϵf implying f is linear.

Under the conditions of (ii) the back face still commutes and the “f face” commutes. So then S(f)ϵg = ϵfg = S(g)F (g)ϵ and, thus, as S(f) is epic ϵg = S(g)ϵ implying g is linear.

Finally for (iii) if e splits and s is linear then e = rs satisfies (i) while if r is linear it satisfies (ii) as S(r) being a retraction is certainly epic.

In a storage category we shall often wish to split all the linear idempotents, that is split all idempotents e such that e ∈ L. An important observation is that this can be done entirely formally:

2.5.2. Proposition. If 𝕏 is a Cartesian storage category then the category obtained by splitting the linear idempotents, Split_{L}(𝕏), is a Cartesian storage category in which linear idempotents split and the embedding

I: 𝕏 ⟶ Split_{L}(𝕏)

preserves and reflects linear maps and the classification.

Proof. The objects of Split_{L}(𝕏) are the linear idempotents in 𝕏, and the maps f: e ⟶ e′ are, as usual, those such that efe′ = f. As linear idempotents are closed under products (that is whenever e and e′ are linear idempotents then e × e′ is a linear idempotent) it is standard that these form a Cartesian category. We shall say that f: e × e′ ⟶ e′′ is linear in its first argument precisely when it is so as a map in 𝕏. It is then immediate that in Split_{L}(𝕏) linear idempotents will split linearly.

The functor S is now defined on Split_{L}(𝕏) by taking an object e to S(e) and a map f to S(f). The transformations φ and ϵ can also be extended by setting φ_{e}: = eφS(e) = φS(e) = eφ and ϵ_{e}: = S(e)ϵe = ϵe = S(e)ϵ (where here we use the linearity of e).

To show that (S, φ) on Split_{L}(𝕏) classifies linear maps in Split_{L}(𝕏) consider

\xymatrix{a × e \ar[r]^{f} \ar[d]_{a×φ} & e′ \\ a × S(e) \ar@{.>}[ur]_{f^{♯}}}

where a, e, e′ are linear idempotents and f = (a × e)fe′ and f^{♯} is the linear classification for f in 𝕏 then it suffices to show that f^{♯} = (a×S(e))f^{♯}e′ to show this is a classification in Split_{L}(𝕏). To show this first note that (a×S(e))f^{♯}e′ is linear, so if (1×φ)(a×S(e))f^{♯}e′ = f we will have secured the equality. For this we note:

(1 × φ)(a × S(e))f^{♯}e′ = (a × e)(1 × φ))f^{♯}e′ = (a × e)fe′ = f.

Persistence now follows immediately from persistence in 𝕏.

We also need to show that the linear maps in Split_{L}(𝕏) satisfy [LS.1], [LS.2] ,and [LS.3]. The only difficulty concerns [LS.2] and the condition on linear retractions. In a slice Split_{L}(𝕏)[a] we must show that if g is a linear retraction (where the section is not necessarily linear) and gh is linear then h is linear. This gives the following commuting diagram of maps

\xymatrix{a × e′ \ar[d]_{a×e′} \ar[r]^{⟨π_{0},v⟩} & a × e \ar[dl]^{⟨π_{0},g⟩} \ar[d]^{⟨π_{0},g⟩h} \\ a × e′ \ar[r]_{h} & e′′}

in which the downward pointing arrows contain the known linear components and v is the section of g which gives rise to the leftmost arrow being an “identity map” at the idempotent a×e′. We must show that h is linear in this slice, that is that (1×ϵ)h = θS(h)ϵ. Here is the calculation:

θS(h)ϵ = θS((a × e′)h)ϵ  as h: a × e′ ⟶ e′′
= θS(⟨π_{0}, v⟩⟨π_{0}, g⟩h)ϵ as v is a section of g
= ⟨π_{0}, θS(v)⟩θS(⟨π_{0}, g⟩h)ϵ
= ⟨π_{0}, θS(v)⟩(1 × ϵ)⟨π_{0}, g⟩h as gh is linear
= ⟨π_{0}, θS(⟨π_{0}, v⟩g)⟩(1 × ϵ)h as g is linear
= ⟨π_{0}, θS(π_{1}e′)⟩(1 × ϵ)h as v is a section of g
= (1 × ϵ)(1 × e′)h = (1 × ϵ)h.

It is worth remarking that splitting linear idempotents of 𝕏 does not cause linear idempotents in 𝕏[A] to split. One can, of course, split the linear idempotents in 𝕏[A] but this in general will have more objects than Split_{L}(𝕏)[A] as there will be more idempotents which are “linear in one argument” than are just linear. More precisely, a linear idempotent in 𝕏[A] is an e′: A × X ⟶ X linear in X with ⟨π_{0}, e′⟩e′ = e′ and these, in general, will strictly include idempotents π_{1}e where e is a linear idempotent in 𝕏.

2.6. Forceful comonads. At this stage we have a fairly good grasp of what the monad of a Cartesian storage category looks like. However, notably absent has been a discussion of the properties of the comonad Š on the linear maps of a Cartesian storage category. In this section we correct this defect.

Recall that the strength in a Cartesian storage category is not linear, in general, so that the comonad Š will not have a strength. To guarantee that Š be strong, we shall postulate the presence of a map which generates a strength map in the coKleisli category: this we call a force and we develop its properties below.

2.6.1. Definition. A (commutative) force for a comonad Š = (S, ϵ, δ) is a natural transformation

S(A × S(X)) ⟶^{ψ} S(A × X)

which renders the following diagrams commutative:

[Force.1] Associativity of force: (a_{×} is the associativity transformation)

\xymatrix{S(A × (B × S(C)) \ar[d]_{δ} \ar[r]^{a_{×}} & S((A × B) × S(C)) \ar[dddd]^{ψ} \\ S^{2}(A × (B × S(C)) \ar[d]_{S(σ_{×})} \\ S(S(A) × S(B × S(C)) \ar[d]_{S(ϵ×ψ)} \\ S(A × S(B × C)) \ar[d]_{ψ} \\ S(A × (B × C)) \ar[r]_{S(a_{×})} & S((A × B) × C)}

[Force.2] Projection and force:

\xymatrix{S(A × S(B)) \ar[d]_{S(π_{1})} \ar[r]^{ψ} & S(A × B) \ar[d]^{S(π_{1})} \\ S^{2}(B) \ar[r]_{ϵ} & S(B)}

[Force.3] Forceful naturality:

\xymatrix{S(A × S(B)) \ar[r]^{δ} \ar[dd]_{ψ} & S^{2}(A × S(B)) \ar[d]^{S(σ_{×})} \\  & S(S(A) × S^{(}B)) \ar[d]^{S(1×(ϵδ))} \\ S(A × B) \ar[d]_{δ} & S(S(A) × S^{2}(B)) \ar[d]^{ψ} \\ S^{2}(A × B) \ar[r]_{S(σ_{×})} & S(S(A) × S(B))}

[Force.4] The forcefulness of counit:

\xymatrix{S(A × S^{2}(B)) \ar[d]_{ψ} \ar[r]^{S(1×ϵ)} & S(A × S(B)) \ar[d]^{ψ} \\ S(A × S(B)) \ar[r]_{ψ} & S(A × B)}

[Force.5] The forcefulness of comultiplication:

[figure: S(A × B); δ; S^{2}(A × B); S(σ_{×}); S(S(A) × S(B)); ψ; S(A × B); S(S(A) × B); S(ϵ×1)]

[Force.6] Commutativity of force: (c_{×} is the commutativity transformation)

\xymatrix{S(S(A) × S(B)) \ar[d]_{ψ′} \ar[r]^{ψ} & S(S(A) × B) \ar[d]^{ψ′} \\ S(A × S(B)) \ar[r]_{ψ} & S(A × B)}

where ψ′: = S(c_{×})ψS(c_{×}) is the symmetric dual of the force.

We shall say that a comonad is forceful if it comes equipped with a force. First we observe the following.

2.6.2. Proposition. In any Cartesian storage category 𝕏 the comonad, Š on the linear maps has a force.

Proof. If 𝕏 is a Cartesian storage category we may define ψ = S(θ)ϵ: by inspection this is a linear map (i.e. in L[]). We must check it satisfies all the given properties.

[Force.1] The interaction of associativity and strength gives the equation (1×θ)θS(a_{×}) = a_{×}θ. We shall use this and the fact that S(φh)ϵ = h for linear h: S(X) ⟶ Y in the calculation:

δS(σ_{×})S(ϵ × ψ)ψS(a_{×}) = S(φδS(σ_{×})S(ϵ × ψ)ψS(a_{×}))ϵ
= S(φφS(σ_{×})S(ϵ × ψ)ψS(a_{×}))ϵ
= S(φσ_{×}(ϵ × ψ)φψS(a_{×}))ϵ
= S((φ × φ)(ϵ × ψ)φψS(a_{×}))ϵ
= S((1 × θ)θS(a_{×}))ϵ
= S(a_{×}θ)ϵ = S(a_{×})ψ

[Force.2] The projection of force:

ψS(π_{1}) = S(θ)ϵS(π_{1})
= S(θS(π_{1}))ϵ
= S(π_{1})ϵ

[Force.3] Forceful naturality:

We shall use the couniversal properties repeatedly: we need to show ψδS(σ_{×}) = δS(σ_{×}(1 × ϵδ))ψ, but as they are both linear, it suffices to show that they are equal when prefixed with φ:

φψδS(σ_{×}) = θδS(σ_{×})
= (1 × δ)θS(θσ_{×})
φδS(σ_{×}(1 × (ϵδ)))ψ = φφS(σ_{×}(1 × (ϵδ)))ψ
= φ(σ_{×}(1 × (ϵδ)))θ
= (φ × φ)(1 × (ϵδ)))θ
= (φ × δ)θ

The resulting expressions are both linear in the second argument, so they are equal provided precomposing with 1 × φ makes them equal:

(1 × φ)(1 × δ)θS(θσ_{×}) = (1 × (φφ))θS(θσ_{×})
= (1 × φ)φS(θσ_{×})
= (1 × φ)θσ_{×}φ
= φσ_{×}φ = (φ × φ)φ
(1 × φ)(φ × δ)θ = (φ × φ)(1 × φ)θ
= (φ × φ)φ

This establishes the equality!

[Force.4] For the forcefulness of the counit both sides are linear as so equal if they are equal after precomposing with φ. However, φψψ = θψ and φS(1 × ϵ)ψ = (1 × ϵ)φψ = (1 × ϵ)θ. These last are linear in their second argument and, therefore, are equal if and only if precomposing with 1 × φ makes them equal:

(1 × φ)θψ = φψ = θ = (1 × φ)(1 × ϵ)θ

[Force.5] The forcefulness of the comultiplication:

δS(σ_{×})ψS(ϵ × 1) = δS(σ_{×}θ)ϵS(ϵ × 1)
= δS(σ_{×}θS(ϵ × 1))ϵ
= S(φσ_{×}(ϵ × 1)θ)ϵ
= S((φ × φ)(ϵ × 1)θ)ϵ
= S((1 × φ)θ)ϵ
= S(φ)ϵ = 1

[Force.6] Commutativity of the force:

ψψ′ = S(θ)ϵS(θ′)ϵ
= S(θS(θ′)ϵϵ
= S(θ′S(θ))ϵϵ
= S(θ′)ϵS(θ)ϵ
= ψ′ψ

Conversely:

2.6.3. Proposition. Let S be a forceful comonad on 𝕏 a Cartesian category then the coKleisli category 𝕏_{S} is a Cartesian storage category.

Proof. The coKleisli category is immediately an abstract coKleisli category (see [F99]): it remains only to show that all the data (S, φ, and ϵ) are strong, and that the induced monad is commutative.

The following is the interpretation for the data of the Cartesian storage category:

⟦φ⟧ : = 1_{S(A)}
⟦ϵ⟧ : = ϵϵ
⟦S(f)⟧ : = ϵδS(⟦f⟧)
⟦θ⟧ : = ψ
⟦f × g⟧ : = ⟨S(π_{0})⟦f⟧, S(π_{1})⟦g⟧⟩ = σ_{×}(⟦f⟧ × ⟦g⟧)
⟦Δ⟧ : = ϵΔ
⟦π_{i}⟧ : = ϵπ_{i}
⟦a_{×}⟧ : = ϵa_{×}
⟦fg⟧ : = δS(⟦f⟧)⟦g⟧.

First we must show that θ satisfies the requirements of being a strength for S with respect to the product. This may be expressed as following two requirements and naturality:

\xymatrix{A × S(X) \ar[r]^{θ} \ar[dr]_{π_{1}} & S(A × X) \ar[d]^{S(π_{1})} & A × (B × S(X)) \ar[d]_{a_{×}} \ar[r]^{1×θ} & A × S(B × X) \ar[r]^{θ} & S(A × (B × X)) \ar[d]^{S(a_{×})} \\  & S(X) & (A × B) × S(X) \ar[rr]_{θ} &  & S((A × B) × X)}

The two diagrams are verified by the following calculation:

⟦θ • S(π_{1})⟧ = δS(ψ)ϵδS(ϵπ_{1})
= ψS(π_{1}) = S(π_{1})ϵ = ϵπ_{1}
= ⟦π_{1}⟧
⟦(1 × θ) • θ • S(a_{×})⟧ = δS(⟨S(π_{0})ϵ, S(π_{1})ψ⟩)δS(ψ)ϵδS(ϵa_{×})
= δS(⟨S(π_{0})ϵ, S(π_{1})ψ⟩)ψS(a_{×})
= S(a_{×})ψ
= ⟦a_{×} • θ⟧

For naturality we have:

⟦(f × S(g))θ⟧ = δS(σ_{×}(f × (ϵδS(g))))ψ
= δS(σ_{×}(1 × (ϵδ)))S(f × S(g))ψ
= δS(σ_{×}(1 × (ϵδ)))ψS(f × g)
= ψδS(σ_{×})S(f × g)
= δS(ψ)ϵδS(σ_{×}(f × g)) = ⟦θS(f × g)⟧

646  R. BLUTE, J.R.B. COCKETT, AND R.A.G. SEELY

Next we must verify that both φ and ϵ_{S} (i.e. μ) are strong:

\xymatrix{A × X \ar[dr]_{φ} \ar[r]^{1×φ} & A × S(X) \ar[d]^{θ} & A × S^{2}(X) \ar[d]_{1×ϵ_{S}} \ar[r]^{θ} & S(A × S(X)) \ar[r]^{S(θ)} & S^{2}(A × X) \ar[d]^{ϵ_{S}} \\  & S(A × X) & A × S(X) \ar[rr]_{θ} &  & S(A × X)}

⟦(1 × φ)θ⟧ = δS(σ_{×}(ϵ × 1))ψ
= δS(σ_{×})ψS(ϵ × 1)
= 1 = ⟦φ⟧
⟦(1 × ϵ)θ⟧ = δS(σ_{×}(ϵ × ϵϵ))ψ
= δS(σ_{×}(ϵ × ϵ))S(1 × ϵ)ψ
= δS(σ_{×}(ϵ × ϵ))ψψ
= ψψ
= δS(ψδS(ψ)ϵ)ϵ
= δS(ψ)δS(ϵδS(ψ))ϵϵ
= ⟦θS(θ)ϵ⟧

where we used the following equality δS(σ_{×}(ϵ × ϵ)) = 1_{S(A×B)} which holds as δS(σ_{×}(ϵ × ϵ)) = δS(⟨S(π_{0}), S(π_{1})⟩(ϵ × ϵ)) = δS(⟨ϵπ_{0}, ϵπ_{1}⟩)) = δS(ϵ⟨π_{0}, π_{1}⟩) = δS(ϵ) = 1.

Lastly we must show that the induced monad is commutative, that is:

\xymatrix{S(A) × S(B) \ar[d]_{θ′} \ar[r]^{θ} & S(S(A) × B) \ar[r]^{S(θ′)} & S^{2}(A × B) \ar[d]^{μ} \\ S(A × S(B)) \ar[r]_{S(θ)} & S^{2}(A × B) \ar[r]_{μ} & S(A × B)}

⟦θS(θ′)μ⟧ = δS(ψ)(δS(ϵδS(ψ′))ϵϵ
= δS(ψδS(ψ′)ϵ)ϵ
= ψψ′ = ψ′ψ
= δS(ψ′δS(ψ)ϵ)ϵ
= δS(ψ′)(δS(ϵδS(ψ))ϵϵ
= ⟦θ′S(θ)μ⟧

We shall call a Cartesian category with a forceful comonad a Cartesian linear category. We may summarize the above results as follows:

2.6.4. Theorem. A category is a Cartesian storage category if and only if it is the coKleisli category of a Cartesian linear category. A Cartesian linear category is the linear maps of a Cartesian storage category if and only if its comonad is exact.

Recall that a comonad is exact when the commuting diagram:

S(S(X)) S(ϵ) ; \overrightarrow{⟶} ; ϵ S(X) ⟶^{ϵ} X

is a coequalizer. A category with an exact comonad is always the subcategory of ϵ-natural maps of its coKleisli category. This allows the original category to be completely recovered from the coKleisli category.

Starting with a forceful comonad S on a Cartesian category 𝕏 one can directly form the simple fibration of the coKleisli category. The total category 𝕏 can be described by:

Objects: (A, X) where A, X ∈ 𝕐;

Maps: (f, g): (A, X) ⟶ (B, Y) where f: S(A) ⟶ B and g: S(A × X) ⟶ Y;

Identities: (ϵ, S(π_{1})ϵ): (A, X) ⟶ (A, X);

Composition: (f, g)(f′, g′) = (δS(f)f′, δS(⟨S(π_{0})f, g⟩)g′).

That this amounts to the simple fibration ∂: 𝕏_{S}[𝕏_{S}] ⟶ 𝕏_{S}; (f, g) ↦ f is easily checked.

2.6.5. Remark. One might expect for there to be more interactions between the comultiplication and the force. In fact, there are but they are often not so obvious! Here is an example:

\xymatrix{S(A × S(B)) \ar[d]_{ψ} \ar[r]^{S(1×δ)} & S(A × S^{2}(B)) \ar[d]^{ψ} \\ S(A × B) & S(A × S(B)) \ar[l]^{ψ}}

An easy, but perhaps rather unsatisfactory way to check this is by looking in the corresponding Cartesian storage category where we have rather easily:

S(1 × δ)ψψ = S(1 × S(φ))S(θ)ϵS(θ)ϵ
= S((1 × S(φ))θS(θ))ϵϵ
= S(θS((1 × φ)θ)ϵ)ϵ
= S(θφϵ)ϵ = S(θ)ϵ = ψ

However, one might reasonably want a direct proof. We shall use the following equality

δS(σ_{×}(ϵ × ϵ)) = 1_{S(A×B)}

which holds since

δS(σ_{×}(ϵ × ϵ)) = δS(⟨S(π_{0}), S(π_{1})⟩(ϵ × ϵ)) = δS(⟨ϵπ_{0}, ϵπ_{1}⟩)) = δS(ϵ⟨π_{0}, π_{1}⟩) = δS(ϵ) = 1.

Here is the calculation:

ψ = S(1 × δS(ϵ))ψ = (1 × δ)ψS(1 × ϵ)
= (1 × δ)ψδS(σ_{×})ψS(ϵ × 1)S(1 × ϵ)
= (1 × δ)ψδS(σ_{×})ψS(ϵ × ϵ)
= (1 × δ)δS(σ_{×})S(1 × (ϵδ))ψψS(ϵ × ϵ)
= (1 × δ)δS(σ_{×})S(1 × (ϵδ))ψS(ϵ × S(ϵ))ψ
= (1 × δ)δS(σ_{×})S(1 × (ϵδ))S(ϵ × S^{2}(ϵ))ψψ
= (1 × δ)δS(σ_{×})S(ϵ × (ϵδS^{2}(ϵ)))ψψ
= (1 × δ)δS(σ_{×})(ϵ × ϵ)(1 × (S(ϵ)δ))ψψ
= (1 × δ)(1 × (S(ϵ)δ))ψψ
= (1 × δ)ψψ

We now have the following which summarizes the main results of this section

2.6.6. Theorem. For a Cartesian category 𝕏, the following are equivalent:

• 𝕏 is a Cartesian storage category;

• 𝕏 is a strong abstract commutative coKleisli category;

• 𝕏 is the coKleisli category of a Cartesian category with a forceful comonad.

3. Monoidal storage categories

Our objective is now to link our development to the categorical semantics of linear logic through the “storage categories” which were developed from the ideas introduced in [S89]. The original definition of these categories required a comonad S on a ∗-autonomous category and natural isomorphisms s_{×}: S(A × B) ⟶ S(A) ⊗ S(B) and s_{1}: S(1) ⟶ ⊤. Subsequently Gavin Bierman realized that, in order to ensure that equivalent proofs of Multiplicative Exponential Linear Logic (MELL) were sent to the same map, the comonad actually had to be monoidal. Bierman called these categories, in which this new requirement was added, “new Seely” categories.

Bierman’s examination of MELL also revealed that, even in the absence of additives, the (monoidal closure of the) coKleisli category of a symmetric monoidal category with an exponential would have products and, furthermore, when the original category was closed, would be Cartesian closed. Thus, it seemed that the additive structure was not really necessary for the theory. Bierman called the categories which provided models for MELL linear categories. In this manner, the additive structure, basic in Seely’s original definition, was relegated to a secondary and largely optional role.

Andrea Schalk [S04] collected the various axiomatizations of Seely categories originating from this work, and removed the requirement that the category be closed. She showed that this was an orthogonal property whose main purpose was to ensure the coKleisli category was Cartesian closed. She called the modalities linear exponential comonads, and thus replaced linear categories with symmetric monoidal categories with a linear exponential comonad.

Even more recently Paul-André Melliès [M02] while revisiting “categorical models of linear logic” concentrated entirely upon the exponential structure: notably ∗-autonomous categories hardly rated a mention and the additives are reduced to at most products— although closedness is assumed throughout. Of note was the emphasis that was placed on the role of the monoidal adjunction which was induced between the linear and Cartesian categories. Of particular interest was an axiomatization for Seely’s original ideas which showed that rather than demand that the comonad be a monoidal comonad one could obtain the same effect by axiomatizing the Seely isomorphism itself more carefully. Here we shall follow this idea and, adapting it somewhat, obtain a convenient description of the variety of Seely category in which we are interested. These are “new Seely categories”, but following Andrea Schalk’s lead, the requirement of closedness is dropped.

One thing that should be emphasized is that in, this exposition of Seely categories, we are focusing on the product structure: the monoidal structure is regarded as secondary, indeed, even generated by products. This is absolutely the opposite to the general trend in the work cited above where an underlying theme is to decompose the product structure into a more fundamental monoidal structure. Mathematically, of course, there is no tension between these approaches, as in these settings the product and monoidal are linked and it should be no surprise that the linkage can be worked in both directions. However, there is perhaps a philosophical message, as it challenges the precept of what should be taken as primary. Seemingly in spite of this, we shall call the current notion “monoidal storage categories”, as they are very similar to the “storage categories” we considered in [BCS06], in the context of (monoidal) differential categories.

The section starts by providing an exposition of monoidal storage categories: we start from the definition of a storage transformation and explain why this is the same as a coalgebra modality. A monoidal storage category is then defined to be a symmetric monoidal category with products and a storage transformation which is an isomorphism. We then prove that this implies that the modality is a monoidal comonad and, thus, that we do indeed obtain (modulo the relaxing of the closed requirement) what Gavin Bierman called a “new Seely” category.

Next, we return to the main theme of the paper, and formulate the notion of monoidal representation in a Cartesian storage category. We then show that the linear maps of a Cartesian storage category, which has persistent monoidal representation, always form a monoidal storage category. Conversely, the coKleisli category of a monoidal storage category is a Cartesian storage category with monoidal representation. Thus, monoidal storage categories, in which the comonad is exact, correspond precisely to the linear maps of Cartesian storage categories which have persistent monoidal representation.

3.1. Coalgebra modalities. Let 𝕏 be a symmetric monoidal category with tensor (⊗, a_{⊗}, c_{⊗}, u_{⊗}^{L}, u_{⊗}^{R}) which has products and a comonad (S, δ, ϵ). (Note that a_{⊗}, c_{⊗} are associativity and commutativity iso-transformations for the tensor, and u_{⊗}^{L}, u_{⊗}^{R} are the tensor unit iso-transformations.)

3.1.1. Definition. A storage transformation is a symmetric comonoidal transformation s: S ⟶ S from 𝕏, regarded as a symmetric monoidal category with respect to the Cartesian product, to 𝕏, regarded as a symmetric monoidal category with respect to the tensor, for which δ is a comonoidal transformation.

Thus, a storage transformation is a natural transformation s_{2}: S(X × Y) ⟶ S(X) ⊗ S(Y) and a map s_{1}: S(1) ⟶ ⊤ satisfying:

\xymatrix{S((X × Y) × Z) \ar[d]_{S(a_{×})} \ar[r]^{s_{2}} & S(X × Y) ⊗ S(Z) \ar[r]^{s_{2}⊗1} & (S(X) ⊗ S(Y)) ⊗ S(Z) \ar[d]^{a_{⊗}} \\ S(X × (Y × Z)) \ar[r]_{s_{2}} & S(X) ⊗ S(Y × Z) \ar[r]_{1⊗s_{2}} & S(X) ⊗ (S(Y) ⊗ S(Z))}

\xymatrix{S(1 × X) \ar[d]_{S(π_{1})} \ar[r]^{s_{2}} & S(1) ⊗ S(X) \ar[d]^{s_{0}⊗1} & S(X × 1) \ar[d]_{S(π_{0})} \ar[r]^{s_{2}} & S(X) ⊗ S(1) \ar[d]^{1⊗s_{0}} \\ S(X) & ⊤ ⊗ S(X) \ar[l]^{u_{⊗}^{L}} & S(X) & S(X) ⊗ ⊤ \ar[l]^{u_{⊗}^{R}}}

\xymatrix{S(X × Y) \ar[d]_{S(c_{×})} \ar[r]^{s_{2}} & S(X) ⊗ S(Y) \ar[d]^{c_{⊗}} \\ S(Y × X) \ar[r]_{s_{2}} & S(Y) ⊗ S(X)}

In general, a natural transformation is a comonoidal transformation if it respects the comonoidal structure in the sense that the following diagrams commute:

\xymatrix{F (X × Y) \ar[d]_{σ_{2}^{F}} \ar[r]^{α} & G(X × Y) \ar[d]^{σ_{2}^{G}} & F (1) \ar[dr]_{σ_{0}^{F}} \ar[rr]^{α} &  & G(1) \ar[dl]^{σ_{0}^{G}} \\ F (X) ⊗ F (Y) \ar[r]_{α⊗α} & G(X) ⊗ G(Y) &  & ⊤}

A comonad is comonoidal if all its transformations are. However, for the comonad (S, δ, ϵ) it makes no sense to insist that ϵ is comonoidal as the identity functor is not comonoidal (from 𝕏 with products to 𝕏 with tensor). However, it does make sense to require δ is comonoidal. Recall first that, with respect to the product, every functor is canonically comonoidal with:

σ_{2}^{×} = ⟨S(π_{0}), S(π_{1})⟩: S(X × Y) ⟶ S(X) × S(Y) and σ_{0}^{×} = ⟨⟩: S(1) ⟶ 1.

This allows us to express the requirement that δ be comonoidal as follows:

\xymatrix{S(X × Y) \ar[dd]_{s^{2}} \ar[r]^{δ} & S(S(X × Y)) \ar[d]^{σ_{2}^{×}} & S(1) \ar[ddr]_{s_{0}} \ar[r]^{δ} & S(S(1)) \ar[d]^{S(σ_{0}^{×})} \\  & S(S(X) × S(Y)) \ar[d]^{s_{2}} &  & S(1) \ar[d]^{s_{0}} \\ S(X) ⊗ S(Y) \ar[r]_{δ⊗δ} & S(S(X)) ⊗ S(S(Y)) &  & ⊤}

3.1.2. Definition. A symmetric monoidal category 𝕏 with products has a commutative coalgebra modality in case there is a comonad (S, δ, ϵ) such that each S(X) is naturally a cocommutative comonoid (S(X), Δ, e) and δ is a homomorphism of these monoids:

\xymatrix{S(X) \ar[d]_{Δ} \ar[r]^{δ} & S(S(X)) \ar[d]^{Δ} & S(X) \ar[dr]_{e} \ar[rr]^{δ} &  & S(S(X)) \ar[dl]^{e} \\ S(X) ⊗ S(X) \ar[r]_{δ⊗δ} & S(S(X)) ⊗ S(S(X)) &  & ⊤}

We now observe that:

3.1.3. Proposition. For a symmetric monoidal category with products, having a comonad with a symmetric storage transformation is equivalent to having a cocommutative coalgebra modality.

Proof.

(⇒) If one has a storage transformation then one can define natural transformations Δ, e as Δ = S(Δ_{×})s_{2}: S(X) ⟶ S(X) ⊗ S(X) and e = S(⟨⟩)s_{0}: S(X) ⟶ ⊤. As (symmetric) comonoidal functors preserve (commutative) comonoids these do define comonoids. Further, since δ is comonoidal as a transformation it becomes a homomorphism of the induced comonoids. This means that we have a (cocommutative) coalgebra modality.

(⇐) Conversely given a (cocommutative) coalgebra modality on a (symmetric) monoidal category we may define s_{2} = Δ(S(π_{0}) ⊗ S(π_{1})): S(X × Y) ⟶ S(X) ⊗ S(Y) and s_{0} = e: S(1) ⟶ ⊤. s_{2} is clearly a natural transformation and using the fact that Δ is coassociative it is easily seen to satisfy the first comonoidal requirement. For the last we have:

s_{2}(1 ⊗ s_{0})u_{⊗}^{R} = Δ(S(π_{0}) ⊗ S(π_{1}))(1 ⊗ e)u_{⊗}^{R} = Δ(1) ⊗ S(π_{1}))u_{⊗}^{R}S(π_{0}) = S(π_{0}).

Thus these maps do provide comonoidal structure for S. It remains to show that δ is a comonoidal transformation:

δS(σ_{2}^{×})s_{2} = δS(σ_{2}^{×})Δ(S(π_{0}) ⊗ S(π_{1}))
= δΔ(S(σ_{2}^{×}) ⊗ S(σ_{2}^{×}))(S(π_{0}) ⊗ S(π_{1}))
= δΔ(S(σ_{2}^{×}π_{0}) ⊗ S(σ_{2}^{×}π_{1}))
= δΔ(S(S(π_{0})) ⊗ S(S(π_{)}))
= Δ(δ ⊗ δ)(S(S(π_{0})) ⊗ S(S(π_{)}))
= Δ(S(π_{0}) ⊗ S(π_{)})(δ ⊗ δ)
= s_{2}(δ ⊗ δ)

This not only provides an alternative way to describe a commutative coalgebra modality but also leads us into the definition of a monoidal storage category:

3.1.4. Definition. A monoidal storage category is a symmetric monoidal category with a comonad (S, δ, ϵ) which has a storage transformation which is an isomorphism ( i.e. both s_{2} and s_{1} are isomorphisms).

Thinking of monoidal storage categories as “Seely categories”, one notices that this is not the usual definition; in [M02] this definition (essentially) is given as a theorem which relates this description to the more standard definition given by Bierman and adapted by Schalk.

First, we shall compare monoidal storage categories to models of the multiplicative exponential fragment of linear logic (which we shall not assume includes being closed). We shall simply call these linear categories as they are Bierman’s linear categories without the requirement of closure. Thus, a linear category is a symmetric monoidal category 𝕏 with a coalgebra modality on a symmetric monoidal comonad (S, ϵ, δ, m_{⊗}, m_{⊤}) such that Δ and e are both monoidal transformations and coalgebra morphisms.

The requirements of being a linear category are worth expanding. The requirement that e: S(A) ⟶ ⊤ be a monoidal transformation amounts to two coherence diagrams:

[figure: ⊤; m_{⊤}; S(⊤); e; ⊤; S(A) ⊗ S(B); e⊗e; m_{⊗}; S(A ⊗ B); e; ⊤ ⊗ ⊤; u; ⊤]

The requirement the Δ: S(A) ⟶ S(A) ⊗ S(A) is a monoidal transformation amounts to two coherence requirements:

\xymatrix{⊤ \ar[d]_{u} \ar[r]^{m_{⊤}} & S(⊤) \ar[d]^{Δ} & S(A) ⊗ S(B) \ar[d]_{Δ⊗Δ} \ar[r]^{m_{⊗}} & S(A ⊗ B) \ar[dd]^{Δ} \\ ⊤ ⊗ ⊤ \ar[r]_{m_{⊤}⊗m_{⊤}} & S(⊤) ⊗ S(⊤) & S(A) ⊗ S(A) ⊗ S(B) ⊗ S(B) \ar[d]_{_{ex_{⊗}}} \\  &  & S(A) ⊗ S(B) ⊗ S(A) ⊗ S(B) \ar[r]_{m_{⊗}⊗m_{⊗}} & S(A ⊗ B) ⊗ S(A ⊗ B)}

Requiring that e: S(A) ⟶ ⊤ forms a coalgebra morphism amounts to the requirement that

\xymatrix{S(A) \ar[r]^{δ} \ar[d]_{e} & S^{2}(A) \ar[d]^{S(e)} \\ ⊤ \ar[r]_{m_{⊤}} & S(⊤)}

commutes. Finally requiring that Δ is a coalgebra morphism amounts to:

\xymatrix{S(A) \ar[d]_{Δ} \ar[rr]^{δ} &  & S^{2}(A) \ar[d]^{S(Δ)} \\ S(A) ⊗ S(A) \ar[r]_{δ⊗δ} & S^{2}(A) ⊗ S^{2}(A) \ar[r]_{m_{⊗}} & S(S(A) ⊗ S(A))}

In his definition, Bierman had another requirement, namely that whenever f: S(A) ⟶ S(B) is a coalgebra morphism it must also be a comonoid morphism. We have amalgamated this into the definition of a coalgebra modality:

3.1.5. Lemma. In a linear category there is the following implication of commutative diagrams

[figure: S(A); δ; f; S(B); δ; S^{2}(A); S(f); S^{2}(B); S(A); Δ; f; S(B); Δ; S(A) ⊗ S(A); f⊗f; S(B) ⊗ S(B)]

Proof. We use the fact that δ is a morphism of comonoids and is a section (with retraction ϵ). This means the lower diagram commutes if and only if fΔ(δ ⊗ δ) = Δ(f ⊗ f)(δ ⊗ δ) but for this we have:

fΔ(δ ⊗ δ) = fδΔ = δS(f)Δ = δΔ(S(f) ⊗ S(f))
= Δ(δ ⊗ δ)(S(f) ⊗ S(f)) = Δ((δS(f)) ⊗ (δ(S(f)) = Δ((fδ) ⊗ (fδ))
= Δ(f ⊗ f)(δ ⊗ δ).

Note that this immediately means that if f is a coalgebra morphism, it is also then a comonoid morphism, and so Bierman’s original definition of a linear category corresponds to ours (modulo the absence of closedness).

3.1.6. Theorem. A monoidal storage category is a linear category and conversely a linear category with products is a monoidal storage category.

Proof. We rely on a combination of [S04] and [M02] to provide the proof. In particular, the monoidal structure of the monad is given by.

⊤ ⟶^{m_{⊤}} S(⊤) = ⊤ ⟶^{s_{1}^{−1}} S(1) ⟶^{δ} S^{2}(1) ⟶^{S(s_{1})} S(⊤)
S(A) ⊗ S(B) ⟶^{m_{⊗}} S(A ⊗ B) = S(A) ⊗ S(B) ⟶^{s_{2}^{−1}} S(A × B) ⟶^{δ} S^{2}(A × B)

⟶^{S(s_{2})} S(S(A) ⊗ S(B)) ⟶^{ϵ ⊗ ϵ} S(A ⊗ B)

The converse requires checking that a linear category with products provides a storage isomorphism. The fact that there is a coalgebra modality is part of the data above. What remains is to prove that the induced storage transformation is an isomorphism and this is in the literature above.

3.2. Monoidal representation. We now return to the main thread of the paper and consider the notion of monoidal representation for a Cartesian storage category. Our objective is to show that a Cartesian storage category with monoidal representation is precisely the coKleisli category of a monoidal storage category. To achieve this, however, we must first take a detour to develop the notion of tensor representation. Recall that a basic intuition for a tensor product is that it should represent bilinear maps: clearly this intuition can be expressed in any category with a system of linear maps:

3.2.1. Definition.

(i) In any Cartesian category a system of linear maps has monoidal representation in case for each X and Y there is an object X ⊗ Y and a bilinear map φ_{⊗}: X × Y ⟶ X ⊗ Y such that for every bilinear map g: X × Y ⟶ Z in 𝕏 there is a unique linear map in 𝕏 making the following diagram commute:

\xymatrix{X × Y \ar[d]_{φ_{⊗}} \ar[r]^{g} & Z \\ X ⊗ Y \ar@{.>}[ur]_{g_{⊗[A]}}}

(ii) In any Cartesian category a system of linear maps has strong monoidal representation in case for each X and Y there is an object X ⊗ Y and a bilinear map φ_{⊗}: X × Y ⟶ X ⊗ Y such that for every bilinear map g: X × Y ⟶ Z in 𝕏[A] there is a unique linear map in 𝕏[A] making the above diagram commute. Note that this means in 𝕏 we have the diagram:

\xymatrix{A × X × Y \ar[d]_{1×φ_{⊗}} \ar[r]^{g} & Z \\ A × (X ⊗ Y) \ar@{.>}[ur]_{g_{⊗[A]}}}

(iii) A system of linear maps is unit representable in case there is a linear map φ_{⊤}: 1 ⟶ ⊤ such that in 𝕏 for each point p: 1 ⟶ Z there is a unique linear point p_{⊤}: ⊤ ⟶ Z making

\xymatrix{1 \ar[d]_{φ_{⊤}} \ar[r]^{p} & Y \\ ⊤ \ar@{.>}[ur]_{p^{⊤}}}

commute.

(iv) A system of linear maps is strongly unit representable in case it is representable in each simple slice. This means there is a unique p^{⊤[A]} making

\xymatrix{A × 1 \ar[d]_{1×φ_{⊤}} \ar[r]^{p} & Y \\ A × ⊤ \ar@{.>}[ur]_{p^{⊤[A]}}}

commute.

(v) A strong monoidal representation is persistent in case, in (ii) above, whenever A = A_{1} × B × A_{2} and the map g is linear in B, then g^{⊗[A]} is linear in B. Similarly, for a strong monoidal unit representation to be persistent requires, setting A = A_{1}×B×A_{2} in (iv), that whenever p is linear in B then p^{⊤[A]} is also linear in B.

As before, the basic form of monoidal representation assumes only that it holds in the original category: to be a strong monoidal representation requires the property must also hold in every simple slice. Thus, as for classification, there is a progression of notions: monoidal representation, strong monoidal representation, and persistent strong monoidal representation, each of which demands more than the last. This also applies to the unit representation; however, as we shall shortly discover (see Lemma 3.2.4), every storage category already has a persistent strong unit representation. Thus, we shall often talk of monoidal representation when we mean both monoidal and unit representation.

We first observe that persistence produces a simultaneous universal property:

3.2.2. Lemma. If f: A × X × Y × Z ⟶ W is linear in its last two arguments, then there are unique maps linear in their last arguments, f_{1}: A × X ⊗ (Y ⊗ Z) ⟶ W and f_{2}: A × (X ⊗ Y) ⊗ Z ⟶ W such that (1 × ((1 × φ)φ))f_{1} = f = (1 × ((φ × 1)φ))f_{2}.

This is useful in the proof of:

3.2.3. Proposition. If 𝕏 has a system of linear maps for which there is a persistent strong monoidal (and unit) representation, then ⊗ is a symmetric tensor product with unit ⊤ on the subcategory of linear maps, L[].

Proof. When we have a persistent representation we can define the required isomorphisms for a tensor product:

1. The associativity isomorphism:

\xymatrix{A × B × C \ar[d]_{1×φ_{⊗}} \ar[r]^{φ_{⊗}×1} & (A ⊗ B) × C \ar[r]^{φ_{⊗}} & (A ⊗ B) ⊗ C \\ A × (B ⊗ C) \ar[d]_{φ_{⊗}} \ar@{.>}[urr] \\ A ⊗ (B ⊗ C) \ar@{.>}[uurr]_{a_{⊗}}}

where the key is to observe that (1 × φ_{⊗})φ_{⊗}: A × B × C ⟶ (A ⊗ B) ⊗ C is trilinear so that the two extensions indicated are given by the universal property.

2. The symmetry isomorphism:

\xymatrix{A × B \ar[d]_{φ_{⊗}} \ar[r]^{c_{×}} & B × A \ar[r]^{φ_{⊗}} & B ⊗ A \\ A ⊗ B \ar@{.>}[urr]_{c_{⊗}}}

3. The unit isomorphisms:

\xymatrix{A × 1 \ar[d]_{1×φ_{⊤}} \ar[r]^{π_{1}} & A \\ A × ⊤ \ar[d]_{φ_{⊗}} \ar@{.>}[ur]^{(π_{0})_{⊤}^{[A]}}_{= π_{0}} \\ A ⊗ ⊤ \ar@{.>}[uur]_{u_{⊗}^{R}}}

Note that (π_{0})_{⊤}^{[A]} = π_{0} since both fit here and this is bilinear whence one can define u_{⊗}^{R}. It is not obvious that u_{⊗}^{R} is an isomorphism, however, the diagram itself suggests that its inverse is

(u_{⊗}^{R})^{−1} = π_{1}^{−1}(1 × φ_{⊤})φ_{⊗}: A ⊗ ⊤ ⟶ A

and it is easily checked that this works.

We can now obtain the unit elimination on the left using the symmetry map u_{⊗}^{L} = c_{⊗}u_{⊗}^{R}.

The coherences now follow directly from the fact that the product is a symmetric tensor and the multi-universal property of the representation.

When a Cartesian storage category has strong monoidal representation, then this representation is automatically persistent. To establish this we start by observing that a Cartesian storage category already has a fair amount of monoidal representation.

3.2.4. Lemma. In any Cartesian storage category

(i) φ: 1 ⟶ S(1) gives persistent unit monoidal representation;

(ii) m_{×}: S(A) × S(B) ⟶ S(A × B) gives persistent monoidal representation for the objects S(A) and S(B).

Proof. We shall focus on the binary monoidal representation: first note that m_{×} is bilinear as m_{×} = θS(θ′)ϵ = θ′S(θ)ϵ where the last two maps of each expansion are linear while θ is linear in its second argument while θ′ is linear in its first.

The universal property for an arbitrary bilinear h is given by the following diagram, valid in any slice 𝕏[X]:

\xymatrix{A × B \ar[dr]_{φ} \ar[r]^{φ×φ} & S(A) × S(B) \ar[d]^{m_{×}} \ar[r]^{h=m((φ×φ)h)^{♯}} & Z \\  & S(A × B) \ar@{.>}[ur]_{((φ×φ)h)^{♯}}}

where h must be the solution to the simultaneous classification. But this makes the righthand triangle commute by uniqueness of the universal property.

Furthermore this is a persistent representation as the classification is persistent.

Notice that we have shown that the Seely isomorphisms s_{0}: S(1) ⟶ ⊤ and s_{2}: S(A×B) ⟶ S(A) ⊗ S(B) are present. These isomorphisms, which are so central to the structure of linear logic, play an important role in what follows.

The observation above means that a storage category always has (persistent and strong) representation of the tensor unit. Thus, we now focus on understanding monoidal representation. A key observation is:

3.2.5. Lemma. In a Cartesian storage category 𝕏, f: A×B ⟶ C is bilinear if and only if its classifying linear map f^{♯}: S(A × B) ⟶ C coequalizes the linear maps (S(ϵ) ⊗ S(ϵ))s_{2}^{−1} and (ϵ ⊗ ϵ)s_{2}^{−1}.

We shall use tensor notation even though we are not assuming that we have monoidal representation: this is justified by the fact that, for these particular objects, we are always guaranteed representation by Lemma 3.2.4. The translation of these maps, S(ϵ) ⊗ S(ϵ) and ϵ_{S(A)} ⊗ ϵ_{S(A)}, back into tensor-free notation uses the commuting diagrams below:

\xymatrix{S(S(A) × S(B)) \ar[d]_{s_{2}} \ar[r]^{S(ϵ×ϵ)} & S(A × B) \ar[d]^{s_{2}} \\ S^{2}(A) ⊗ S^{2}(B) \ar[r]_{S(ϵ)⊗S(ϵ)} & S(A) ⊗ S(B)}

\xymatrix{S(S(A) × S(B)) \ar[d]_{s_{2}} \ar[r]^{ϵ} & S(A) × S(B) \ar[dr]_{φ_{⊗}} \ar[r]^{m_{×}} & S(A × B) \ar[d]^{s_{2}} \\ S^{2}(A) ⊗ S^{2}(B) \ar[rr]_{ϵ⊗ϵ} &  & S(A) ⊗ S(B)}

Proof. We shall use the characterization of bilinear maps in Proposition 2.3.7 to show that coequalizing these maps is equivalent to bilinearity.

Assume that (S(ϵ) ⊗ S(ϵ))s_{2}^{−1}f^{♯} = (ϵ ⊗ ϵ)s_{2}^{−1}f^{♯} so that

(φ × φ)φ_{⊗}(S(ϵ) ⊗ S(ϵ))s_{2}^{−1}f^{♯} = (φ × φ)φ_{⊗}(ϵ ⊗ ϵ)s_{2}^{−1}f^{♯}

But then we have:

(φ × φ)φ_{⊗}(S(ϵ) ⊗ S(ϵ))s_{2}^{−1}f^{♯}
= (φ × φ)(S(ϵ) × S(ϵ))φ_{⊗}s_{2}^{−1}f^{♯}
= (ϵ × ϵ)(φ × φ)m_{×}f^{♯}
= (ϵ × ϵ)φf^{♯}
= (ϵ × ϵ)f
(φ × φ)φ_{⊗}(ϵ ⊗ ϵ)s_{2}^{−1}f^{♯}
= (φ × φ)(ϵ × ϵ)φ_{⊗}s_{2}^{−1}f^{♯}
= φ_{⊗}s_{2}^{−1}f^{♯}
= m_{×}S(f)ϵ

So this condition implies bilinearity. Conversely, by reversing the argument, assuming bilinearity gives—using classification and monoidal representation—the equality of these maps.

We now have:

3.2.6. Proposition. 𝕏 has (basic) monoidal representation at A and B if and only if

S^{2}(A) ⊗ S^{2}(B) S(ϵ) ⊗ S(ϵ) ; \overrightarrow{⟶} ; ϵ ⊗ ϵ S(A) ⊗ S(B) ⟶^{ϵ ⊗ ϵ} A ⊗ B

is a coequalizer in the subcategory of linear maps.

Proof. Suppose z equalizes S(ϵ) ⊗ S(ϵ) and ϵ ⊗ ϵ then by the previous lemma z′ = (φ × φ)φ_{⊗}z is bilinear and this determines a unique linear map z′_{⊗} with z′ = φ_{⊗}z′_{⊗}.

\xymatrix{S^{2}(A) × S^{2}(B) \ar[d]_{φ_{⊗}} \ar[r]^{S(ϵ)×S(ϵ)} \ar[r]_{ϵ×ϵ} & S(A) × S(B) \ar[d]^{φ_{⊗}} \ar[r]^{ϵ×ϵ} & A × B \ar[d]^{φ_{⊗}} \ar@{.>}[ddr]^{z′} \\ S^{2}(A) ⊗ S^{2}(B) \ar[r]^{S(ϵ)⊗S(ϵ)} \ar[r]_{ϵ⊗ϵ} & S(A) ⊗ S(B) \ar[r]_{ϵ⊗ϵ} \ar[drr]_{z} & A ⊗ B \ar@{.>}[dr]_{z′_{⊗}} \\  &  &  & Z}

We claim z′_{⊗} is the unique comparison map making the fork a coequalizer in the linear map category. To show this we need (ϵ⊗ϵ)z′_{⊗} = z and we must show that any other linear map k with (ϵ ⊗ ϵ)k = z has φ_{⊗}k = z′. For the first of these we note that z is determined by representing (φ × φ)φ_{⊗}z = z′ but

(φ × φ)φ_{⊗}(ϵ ⊗ ϵ)z′_{⊗} = (φ × φ)(ϵ × ϵ)φ_{⊗}z′_{⊗} = φ_{⊗}z′_{o}x = z′

so the two maps are equal. For the second, suppose we have such a k then

φ_{⊗}k = (φ × φ)(ϵ × ϵ)φ_{⊗}k = (φ × φ)φ_{⊗}(ϵ ⊗ ϵ)k = (φ × φ)φ_{⊗}z = z′.

For the converse assume that the linear map category has this fork a coequalizer and suppose f: A × B ⟶ C is bilinear. Returning to the diagram above, by Lemma 3.2.5 we may set z′ = f and z = s_{2}^{−1}f^{♯}. Noting that the top fork is an absolute coequalizer gives the map φ_{⊗}: A × B ⟶ A ⊗ B which will then represent bilinear maps.

Considering what happens in an arbitrary simple slice gives:

3.2.7. Corollary. A storage category has strong monoidal representation if and only if forks of the form:

X × S^{2}(A) ⊗ S^{2}(B) 1 × S(ϵ) ⊗ S(ϵ) ; \overrightarrow{⟶} ; 1 × ϵ ⊗ ϵ X × S(A) ⊗ S(B) ⟶^{1 × ϵ ⊗ ϵ} X × A ⊗ B

are coequalizers for the linear subcategories L[X]

There are a number of different reasons why these forks might be coequalizers. It is often the case that these forks will also be coequalizers in the whole storage category. When this is so, one may decompose the presence of these coequalizers into the presence of the basic coequalizer (of Proposition 3.2.6) and the fact they must be preserved by the functor X × . Because these coequalizers are clearly reflexive, this latter condition is delivered whenever the product functor preserves, more generally, reflexive coequalization. Of course, when the storage category is Cartesian closed, the product functor will preserve all colimits and so in particular these coequalizers. In fact, the case which will be of primary interest to us here, as shall be discussed below, is when these coequalizers are absolute and so are automatically preserved by the product functors and, furthermore, are present under the very mild requirement that linear idempotents split.

We have established that these coequalizers must be present in any storage category with strong monoidal representation. The final ingredient we need is persistence: fortunately this is guaranteed once strong monoidal representation is assumed.

3.2.8. Proposition. In a Cartesian storage category with a strong monoidal representation, the representation is necessarily persistent: that is, given a map h: X_{0}×C×X_{1}×A×B ⟶ Y, which is linear in C, A, and B

\xymatrix{X_{0} × C × X_{1} × A × B \ar[r]^{h} \ar[d]_{1×φ_{⊗}} & Y \\ X_{0} × C × X_{1} × (A ⊗ B) \ar[ur]_{h^{⊗}}}

then its linear lifting h_{⊗}: X_{0} × C × X_{1} × (A ⊗ B) ⟶ Y is linear in C.

Proof. By using Lemma 2.3.8 we may simplify what needs to be proven: namely, given f: A × B × C ⟶ Y which is linear in all its arguments then f^{⊗}: A ⊗ B × C ⟶ Y is linear in C. This latter requires that we show that

\xymatrix{A ⊗ B × S(C) \ar[d]_{1×ϵ} \ar[r]^{φ×1} & S(A ⊗ B) × S(C) \ar[r]^{m_{×}} & S(A ⊗ B × C) \ar[r]^{f^{⊗}} & S(Y) \ar[d]^{ϵ} \\ A ⊗ B × C \ar[rrr]_{f^{⊗}} &  &  & Y}

commutes. Because we have strong monoidal representation we know (ϵ ⊗ ϵ) × 1: S(A) ⊗ S(B) × C ⟶ A ⊗ B × C is epic. Thus, we may preface this square with the map (s^{2} × 1)((ϵ ⊗ ϵ) × 1) to test commutativity. Preliminary to this calculation note that whenever f is bilinear the following diagram

\xymatrix{S(A) × S(B) \ar[dd]^{ϵ×ϵ} \ar[r]_{m_{×}} \ar[dr]_{φ_{⊗}} & S(A × B) \ar[d]^{s_{2}} \ar[r]_{S(f)} & S(Y) \ar[dd]^{ϵ} \\  & S(A) ⊗ S(B) \ar@{.>}[dr] \ar[d]_{ϵ⊗ϵ} \\ A × B \ar[rr]_{f} \ar[r]^{φ_{⊗}} & A ⊗ B \ar[r]^{f^{⊗}} & Y}

commutes as the dotted arrow is the unique linear extension of the bilinear map m_{×}S(f)ϵ = (ϵ×ϵ)f. Putting the right square in the simple slice over C gives the following commuting

CARTESIAN DIFFERENTIAL STORAGE CATEGORIES  661

square:

\xymatrix{S(A × B) × C \ar[d]_{s_{2}×1} \ar[r]^{(1×φ)m_{×}} & S(A × B × C) \ar[r]^{S(f)} & S(Y) \ar[dd]^{ϵ} \\ S(A) ⊗ S(B) × C \ar[d]_{ϵ⊗ϵ×1} \\ A ⊗ B × C \ar[rr]_{f_{⊗}} &  & Y}

We now have the calculation:

(s_{2}(ϵ ⊗ ϵ) × 1)(1 × ϵ)f^{⊗} = (1 × ϵ)(s_{2}(ϵ ⊗ ϵ) × 1)f^{⊗}
= (1 × ϵ)(1 × φ)m_{×}S(f)ϵ
= m_{×}S(f)ϵ
(s_{2}(ϵ ⊗ ϵ) × 1)(φ × 1)m_{×}S(f^{⊗})ϵ = (φ × 1)m_{×}S((s_{2}(ϵ ⊗ ϵ) × 1)f^{⊗})ϵ
= (φ × 1)m_{×}S((1 × φ)m_{×}S(f)ϵ)ϵ
= (φ × 1)m_{×}S((1 × φ)m_{×})ϵS(f)ϵ
= m_{×}S(f)ϵ

where the last step crucially uses the commutativity of the monad.

When one has monoidal representation, if the tensor preserves the coequalizers which witness the exactness of the modality S, that is coequalizers of the form

S^{2}(A) S(ϵ) ; \overrightarrow{⟶} ; ϵ S(A) ⟶^{ϵ} A

then the coequalizer above can be further analyzed via the following parallel coequalizer diagram:

[figure: S^{2}(A) ⊗ S^{2}(B); δ⊗1; ϵ⊗1; S(ϵ)⊗1; 1⊗δ; 1⊗ϵ; 1⊗S(ϵ); ϵ⊗ϵ; S(ϵ)⊗S(ϵ); S(A) ⊗ S^{2}(B); ϵ⊗1; 1⊗ϵ; 1⊗S(ϵ); A ⊗ S^{2}(B); 1⊗ϵ; 1⊗S(ϵ); S^{2}(A) ⊗ S(B); ϵ⊗1; S(ϵ)⊗1; 1⊗ϵ; S(A) ⊗ S(B); 1⊗ϵ; ϵ⊗1; ϵ⊗ϵ; A ⊗ S(B); 1⊗ϵ; S^{2}(A) ⊗ B; ϵ⊗1; S(ϵ)⊗1; S(A) ⊗ B; ϵ⊗1; A ⊗ B]

As proven in [J02, Lemma 1.2.11], for example, given horizontal and vertical reflexive coequalizers as shown above, the diagonal is also a coequalizer. Recall that the basic coequalizers are actually absolute coequalizers in the storage category so they certainly are coequalizers in the linear category (use LS.2]) but they will not necessarily be absolute in the linear category. Thus, assuming that the tensor product preserves them is a far from benign assumption.

3.3. Codereliction and monoidal representation. An important source of monoidal representation in Cartesian storage categories arises from the presence of a codereliction: this is an unnatural transformation η: A ⟶ S(A) which is natural for linear maps such that each η_{A} is linear and splits ϵ in the sense that η_{A}ϵ_{A} = 1_{A}. Notice that φ, in general, will not be a codereliction: is natural for all maps but it is not in general linear—in fact if it were linear then all maps would be linear and S would necessarily be equivalent to the identity functor.

As we shall shortly see, all Cartesian differential storage categories have a codereliction. This is important because of the following observation:

3.3.1. Proposition. Any Cartesian storage category in which linear idempotents split linearly, and which has a codereliction, has persistent monoidal representation.

Recall that a linear idempotent e splits linearly when there is a splitting (r, s) with rs = e and sr = 1 such that both s and r are linear. It follows from Lemma 2.5.1, that both r and s are linear if either is. Furthermore, it follows from Proposition 2.5.2 that we may always formally split linear idempotents.

Proof. Once we have a codereliction we have a split pair

[figure: S^{2}(A) ⊗ S^{2}(B); η⊗η; ϵ⊗ϵ; S(ϵ)⊗S(ϵ); S(A) ⊗ S(B)]

whose absolute coequalizer is the splitting of ϵη ⊗ ϵη. Thus, when linear idempotents split one has basic monoidal representation. As this coequalizer is absolute in the whole storage category it is necessarily preserved by products and so the monoidal representation is strong, hence persistent.

In particular, as we shall discover in Section 4, a Cartesian differential storage category always has a codereliction η = ⟨1, 0⟩D_{×}[φ] which is linear (in the differential sense) and splits ϵ. Thus, in these examples it suffices for linear idempotents (in simple slices) to have linear splittings. This can always be formally arranged by splitting the linear idempotents.

3.4. Monoidal storage categories with an exact modality. We now observe that in a Cartesian storage category, which has monoidal representation, the linear maps form a monoidal storage category:

3.4.1. Proposition. In any Cartesian storage category with monoidal representation, the subcategory of linear maps is a monoidal storage category.

Proof. We have already observed that there is a monoidal comonad present on the linear maps. In addition, when both a persistent classification and representation is present there is are natural isomorphisms s_{⊗}: S(X × Y) ⟶ S(X) ⊗ S(Y) and an isomorphism s_{⊤}: ⊤ ⟶ S(1) constituting an iso-comonoidal structure for the functor S: 𝕏 ⟶ 𝕏 from 𝕏 with product to 𝕏 with tensor: this is the storage isomorphism.

This follows immediately from the fact that

\xymatrix{X × Y \ar[drr]_{φ} \ar[r]^{φ×φ} & S(X) × S(Y) \ar[r]^{φ_{⊗}} & S(X) ⊗ S(Y) \ar@{.>}[d]^{s_{⊗}^{−1}} & and & X × Y \ar[dr]_{(φ×φ)φ_{⊗}} \ar[r]^{φ} & S(X × Y) \ar@{.>}[d]^{s_{⊗}} \\  &  & S(X × Y) &  &  & S(X) ⊗ S(Y)}

have the same universal property. Similarly ⊤ and S(1) have the same universal property. That this constitutes a storage transformation is straightforward to check.

To establish the converse of this observation we need to prove that the coalgebra modality of a monoidal storage category is a comonad with a commutative force:

3.4.2. Proposition. The coKleisli category of a monoidal storage category is a Cartesian storage category with monoidal representation.

Proof. We shall show that the comonad is forceful where the force is defined as:

S(A × S(X)) ⟶^{ψ} S(A × X)

= S(A × S(X)) ⟶^{s_{2}} S(A) ⊗ S^{2}(X) ⟶^{1 ⊗ ϵ} S(A) ⊗ S(X) ⟶^{s_{2}^{−1}} S(A × X).

We now have to check the six coherence diagrams of a force:

[Force.1] For the associativity of force we use the fact that the Seely isomorphism is comonoidal:

δS(σ_{×})S(ϵ × ψ)S(ψ)S(a_{×})
= δS(σ_{×})S(ϵ × 1)S(1 × (s_{2}(1 ⊗ ϵ)s_{2}^{−1}))s_{2}(1 ⊗ ϵ)s_{2}^{−1}S(a_{×})
= δS(σ_{×})s_{2}(ϵ ⊗ S(s_{2}(1 ⊗ ϵ)s_{2}^{−1}))(1 ⊗ ϵ)s_{2}^{−1}S(a_{×})
= δS(σ_{×})s_{2}(ϵ ⊗ (ϵs_{2}(1 ⊗ ϵ)))(1 ⊗ s_{2}^{−1})s_{2}^{−1}S(a_{×})
= δS(σ_{×})s_{2}(ϵ ⊗ (ϵs_{2}(1 ⊗ ϵ)))a_{⊗}(s_{2}^{−1} ⊗ 1)s_{2}^{−1}
= δS(σ_{×})s_{2}(ϵ ⊗ (ϵs_{2})))a_{⊗}(s_{2}^{−1} ⊗ ϵ)s_{2}^{−1}
= s_{2}(δ ⊗ δ)(ϵ ⊗ (ϵs_{2}))a_{⊗}(s_{2}^{−1} ⊗ ϵ)s_{2}^{−1}
= s_{2}(1 ⊗ s_{2})a_{⊗}(s_{2}^{−1} ⊗ ϵ)s_{2}^{−1} = S(a_{×})s_{2}(1 ⊗ ϵ)s_{2}^{−1} = S(a_{×})ψ

[Force.2] For projection of force:

ψS(π_{1}) = s_{2}(1 ⊗ ϵ)s_{2}^{−1}S(π_{1})
= s_{2}(1 ⊗ ϵ)(e ⊗ 1)u_{L}^{⊤}
= s_{2}(e × 1)u_{L}^{⊤}ϵ
= S(π_{1})ϵ

[Force.3] For forceful naturality:

δS(σ_{×})S(1 × (ϵδ)))ψ = δS(σ_{×})S(1 × (ϵδ))s_{2}(1 ⊗ ϵ)s_{2}^{−1}
= δS(σ_{×})s_{2}(1 ⊗ S(ϵδ))(1 ⊗ ϵ)s_{2}^{−1}
= s_{2}(δ ⊗ δ)(1 ⊗ S(ϵδ))(1 ⊗ ϵ)s_{2}^{−1}
= s_{2}(1 ⊗ ϵ)(δ ⊗ δ)s_{2}^{−1}
= s_{2}(1 ⊗ ϵ)s_{2}^{−1}δS(σ_{×})
= ψδS(σ_{×})

[Force.4] For forcefulness of counit:

ψψ = s_{@}(1 ⊗ ϵ)s_{2}^{−1}s_{2}(1 ⊗ ϵ)s_{2}^{−1}
= s_{2}(1 ⊗ ϵϵ)s_{2}^{−1}
= s_{2}(1 ⊗ S(ϵ)ϵ)s_{2}^{−1}
= S(1 × ϵ)s_{2}(1 ⊗ ϵ)s_{2}^{−1}
= S(1 × ϵ)ψ

[Force.5] For forcefulness of comultiplication:

δS(σ_{×})ψS(ϵ × 1) = δS(σ_{×})s_{2}(1 ⊗ ϵ)s_{2}^{−1}S(ϵ × 1)
= s_{2}(δ ⊗ δ)(S(ϵ) ⊗ ϵ)s_{2}^{−1} = 1

[Force.6] Commutativity of force:

ψψ′ = s_{2}(1 ⊗ ϵ)s_{2}^{−1}s^{2}(ϵ ⊗ 1)s_{2}^{−1}
= s_{2}(1 ⊗ ϵ)(ϵ ⊗ 1)s_{2}^{−1}
= s_{2}(ϵ ⊗ 1)(1 ⊗ ϵ)s_{2}^{−1}
= s_{2}(ϵ ⊗ 1)s_{2}^{−1}s^{2}((1 ⊗ ϵ)s_{2}^{−1}
= ψ′ψ

This shows that the coKleisli category is a Cartesian storage category; it remains to show that it has monoidal representation. However, this follows, since in the coKleisli category A × B ⟶^{φ_{⊗}} A ⊗ B is given by the 𝕏-map

S(A × B) ⟶^{s_{2}} S(A) ⊗ S(B) ⟶^{ϵ ⊗ ϵ} A ⊗ B

That this represents the tensor is easily seen, and persistence is automatic in a coKleisli category.

The results above tell us that a monoidal storage category with an exact modality is always the category of linear maps of some Cartesian storage category with monoidal representation. This is because its coKleisli category is a Cartesian storage category with monoidal representation and one can recover, as the linear maps, the original monoidal storage category.

3.5. Closed storage categories. We briefly return to the issue of the closeness of these various categories. Starting with a monoidal storage category (Seely category) it is well-known that if the category is closed in the sense that there is an adjunction

{A ⊗ X ⟶ B \atop X ⟶ A ⊸ B}

then the coKleisli category is Cartesian closed with

A ⇒ B: = S(A) ⊸ B

as we have the following natural equivalences:

{S(A × X) ⟶ B \atop S(A) ⊗ S(X) ⟶ B} ; S(X) ⟶ S(A) ⊸ B

Thus, if the monoidal storage category is closed then the coKleisli category, that is the Cartesian storage category, must be Cartesian closed. We wish to work for a converse, namely, knowing that the Cartesian storage category is Cartesian closed, can we provide some natural conditions for the linear maps to form a monoidal closed category? The conditions that we shall consider, in fact, do not require monoidal representation and, in fact, make the linear maps into a closed category in the original sense of Kelly and Eilenberg [KE65].

Note that if a Cartesian storage category is Cartesian closed, then the functor S is enriched over itself, the enrichment S_{AB}: A ⇒ B ⟶ S(A) ⇒ S(B) being the exponential

adjoint to the composite map S(A) × (A ⇒ B) ⟶^{θ′} S(A × (A ⇒ B)) ⟶^{S(ev)} S(B).

3.5.1. Definition.

(i) A Cartesian storage category has linear hom-objects if the following equalizer A ⊸ B exists for each A and B:

A ⊸ B ⟶^{k_{AB}} A ⇒ B S_{AB} (1 ⇒ ϵ) ; \overrightarrow{⟶} ; ϵ ⇒ 1 S(A) ⇒ B

with k_{AB} linear for each A and B.

(ii) A Cartesian storage category is closed if it is Cartesian closed, the linear maps form a closed system (see Definition 2.2.2), and linear hom-objects exist. We call such a category a Cartesian closed storage category.

Clearly we are intending that the equalizer A ⊸ B should provide the object of linear maps from A to B. That it has this property relies on the following:

666  R. BLUTE, J.R.B. COCKETT, AND R.A.G. SEELY

3.5.2. Proposition. In any Cartesian closed storage category:

(i) If f: A × X ⟶ B is linear in its first argument then there is a unique map f̃: X

⟶ A ⊸ B making

\xymatrix{A × X \ar[rr]^{f} \ar@{.>}[d]^{1×f̃} &  & B \\ A × A ⊸ B \ar[r]_{1×k_{AB}} & A × A ⇒ B \ar[ur]_{ev}}

commute. (ii) Any f which can be expressed as f = (1 × f̃)(1 × k_{AB})ev must be linear in its first

argument. (iii) If f is bilinear then f̃ is linear. Proof.

(i) Clearly f̃k_{AB} must be the unique map to the hom-object A ⇒ B, f̂ = f̃k_{AB}: X ⟶ A ⇒ B, and so, as k_{AB} is monic, f̃, must be unique, if it exists. The difficulty is to show that f̂ factors through this equalizer. Recall that as f is linear in its first argument we have

\xymatrix{S(A) × X \ar[d]_{ϵ×1} \ar[r]^{θ′} & S(A × X) \ar[r]^{S(f)} & S(B) \ar[d]^{ϵ} \\ A × X \ar[rr]_{f} &  & B}

commutes (that is (1 × ϵ)f = θ′S(f)ϵ). But then we have the following two commuting diagrams displaying the curried map for these two maps:

\xymatrix{S(A) × X \ar[d]_{!×f̂} \ar[r]^{ϵ×1} & A × X \ar[d]^{1×f̂} \ar[dr]^{f} \\ S(A) × A ⇒ B \ar[d]_{1×(ϵ⇒1)} \ar[r]_{ϵ×1} & A × A ⇒ B \ar[r]_{ev} & B \\ S(A) × S(A) ⇒ B \ar[urr]_{ev}}

This shows that curry((1 × ϵ)f) = f̂(ϵ ⇒ 1).

\xymatrix{S(A) × X \ar[d]_{1×f̂} \ar[r]^{θ′} & S(A × X) \ar[r]^{S(f)} & S(B) \ar[ddr]^{ϵ} \\ S(A) × A ⇒ B \ar[d]_{1×S_{AB}} \\ S(A) × S(A) ⇒ S(B) \ar[d]_{1×(1⇒ϵ)} \ar[uurr]_{ev} &  &  & B \\ S(A) × S(A) ⇒ B \ar[urrr]_{ev}}

While this shows that curry(θ′S(f)ϵ) = f̂S_{AB}(1 ⇒ ϵ). Thus f̂ factors through the equalizer as desired.

(ii) For the converse we have:

\xymatrix{S(A) × X \ar@{-->}[dr]_{!×f̂} \ar[ddd]^{ϵ×1} \ar[rr]^{θ′} &  & S(A × X) \ar[rr]^{S(f)} &  & S(B) \ar[ddd]^{ϵ} \\  & S(A) × A ⊸ B \ar@{-->}[drr]_{1×(k_{AB}(ϵ⇒1))} \ar[rr]^{1×(k_{AB}S_{AB})} &  & S(A) × S(A) ⇒ S(B) \ar[ur]_{ev} \ar[d]^{1×(1⇒ϵ)} \\  &  &  & S(A) × S(A) ⇒ B \ar[dr]^{ev} \\ A × X \ar[rrrr]_{f} &  &  &  & B}

(iii) It remains to show that f̃ is linear when f is bilinear that is ϵf̃ = S(f̃)ϵ for which

we have:

\xymatrix{A × S(X) \ar[d]_{1×ϵf̃} \ar[r]^{1×ϵ} & A × X \ar[d]^{f} \ar[dl]_{1×f̃} \\ A × A ⊸ B \ar[r]_{_{ev_{⊸}}} & B}

\xymatrix{A × S(X) \ar[r]^{θ} \ar[d]_{1×S(f̃)} & S(A × X) \ar[r]^{S(f)} & S(B) \ar[dd]^{ϵ} \\ A × S(A ⊸ B) \ar[r]_{θ} \ar[d]_{1×ϵ} & S(A × A ⊸ B) \ar@{-->}[ur]_{S(ev_{⊸})} \\ A × A ⊸ B \ar[rr]_{_{ev_{⊸}}} &  & B}

Showing linearity in the second argument implies that f̃ is linear.

In particular, notice that this immediately means that ev_{⊸}: = (1 × k_{AB})ev is linear in its first argument, as ev_{⊸} defined in this manner certainly satisfies Proposition 3.5.2 (ii). However, as k_{AB} is linear and ev is linear in its second argument—as we are assuming a closed linear system—it follows that ev_{⊸} is bilinear. Thus, when one has monoidal representation this means that there is an induced evaluation map ev_{⊗}: A ⊗ (A ⊸ B) ⟶ B with φ_{⊗}ev_{⊗} = ev_{⊸} which is linear. Furthermore, by Proposition 3.5.2 (iii) the curry map for f: A ⊗ X ⟶ B is also linear as it is φ̃_{⊗}f. Thus we have:

3.5.3. Corollary. If 𝕏 is a Cartesian closed storage category which has monoidal representation, then the subcategory of linear maps forms a monoidal closed storage category.

This leaves open the converse: if one starts with a monoidal closed storage category, will its coKleisli category be a Cartesian closed storage category? We shall now show that this is true, giving a complete characterization for the closed case:

3.5.4. Proposition. If 𝕏 is a monoidal storage category which is monoidal closed then its coKleisli category is a Cartesian closed storage category.

Proof. We provide a sketch of the proof. We must show three things:

(1) We need to show that the coKleisli category is a Cartesian closed category and that the functor induced by the modality is suitably enriched. As above, the closed structure is given by A ⇒ B: = S(A) ⊸ B. In a Cartesian closed category a functor is enriched whenever it is strong, so the fact that there is a natural force ψ: S(A×S(B)) ⟶ S(A × B) (described in Proposition 3.4.2) guarantees the functor is strong.

(2) We need to show that the linear maps of the coKleisli category form a closed system. We know already they form a linear system so we need only check that they are a closed linear system. This amounts to checking the following.

(a) The evaluation map is linear in its higher-order argument. This is immediately true by inspection. Here is the definition of the evaluation map in the coKleisli category:

S(A × (S(A) ⊸ B)) ⟶^{s_{2}} S(A) ⊗ S(S(A) ⊸ B) ⟶^{1 ⊗ ϵ} S(A) ⊗ (S(A) ⊸ B) ⟶^{ev_{⊸}} B

The second map in the sequence ensures it is linear in the second argument.

(b) Linearity is “persistent” over currying. To say that a coKleisli map f: S(A × B × C) ⟶ D is linear in its second argument amounts to saying that f = s_{3}(1 ⊗ ϵ ⊗ 1)f′. Currying this map (with respect to the first argument) clearly maintains the linearity in the second argument.

(3) This leaves only the requirement that A ⊸ B occurs as an equalizer:

A ⊸ B ⟶^{k_{AB}} A ⇒ B S_{AB}(1 ⇒ ϵ) ; \overrightarrow{⟶} ; ϵ ⇒ 1 S(A) ⇒ B

Recall that we may assume the modality is exact (if it is not, simply work in the subcategory of linear maps). This equalizer (after considerable unwinding) is exactly the image of

A ⊸ B ⟶^{ϵ ⊸ 1} S(A) ⊸ B S(ϵ) ⊸ 1 ; \overrightarrow{⟶} ; ϵ ⊸ 1 S^{2}(A) ⊸ B

under the inclusion into the coKleisli category. Since

S^{2}(A) S(ϵ) ; \overrightarrow{⟶} ; ϵ S(A) ⟶^{ϵ} A

under this inclusion is a coequalizer, the transpose of this is an equalizer. This shows that A ⊸ B does occur as an equalizer as required.

4. Cartesian differential storage categories

Monoidal differential categories were introduced in [BCS06]: they consist of a symmetric monoidal category with a coalgebra modality and a deriving transformation. In [BCS09] the notion of a Cartesian differential category was introduced. It was proven that an important way in which Cartesian differential categories arise is as the coKleisli categories of monoidal differential categories which satisfied an additional interchange requirement on the deriving transformation. This latter requirement was presented as a sufficient condition: the question of whether it was necessary was left open. Here we partially answer that question for an important class of monoidal differential categories: those whose modality is a storage modality—in other words those which are “Seely categories” in the sense discussed above—and exact: we show that this condition is indeed necessary.

Not surprisingly, the strategy of the proof is to characterize the coKleisli category of a monoidal differential category with a storage modality using the development above. The fact that the coKleisli category of a monoidal differential category (satisfying the interchange condition) is necessarily a Cartesian differential category means we should consider Cartesian storage categories which are simultaneously Cartesian differential categories. Furthermore, we expect the linear maps in the differential sense to be the linear maps in the storage sense. We will then show that, under these assumptions, the linear maps form a monoidal differential category which satisfies the interchange requirement. This then provides a characterization of coKleisli categories of monoidal differential categories (with a storage modality) which form differential categories.

It is worth mentioning—not least as it caused the authors some strife—that there are at least three different sorts of monoidal differential category which have been discussed in the literature:

(A) A differential given by a deriving transformation as introduced in [BCS06].

(B) A differential given by a codereliction as introduced [ER05] and described in [BCS06]

(C) A differential given by a creation operator as introduced in [F07].

Each form of differential is more specialized than its predecessor: the first merely requires a coalgebra modality, the second requires a bialgebra modality, while the last requires a storage modality. A standard way in which a bialgebra modality arises is from the presence of biproducts together with a storage modality: the Seely isomorphism then transfers the bialgebra structure of the biproduct onto the modality. This means that the last two forms of differential are particularly suited to storage settings. As, in the current context, we are considering storage categories one might think that the differential which one extracts from a Cartesian differential storage category should be of type (C) or at least (B). It is, therefore, perhaps somewhat unexpected that the differential that emerges is one of type (A).

Cartesian differential storage categories are important in their own right. Their structure can be approached in two very different ways: from the perspective of being a Cartesian differential category with monoidal representation, or as the coKleisli category of a monoidal differential category. This tension allows one to transfer arguments between the Cartesian and the monoidal worlds. This ability is frequently used in differential geometry where one often wants to view differential forms as maps from tensor products.

4.1. Cartesian differential categories. Cartesian differential categories, were introduced in [BCS09]: here we briefly review their properties.

One way to view the axiomatization of Cartesian differential categories is as an abstraction of the Jacobian of a smooth map f: ℝ^{n} ⟶ ℝ^{m}. One ordinarily thinks of the Jacobian as a smooth map

J(f): ℝ^{n} ⟶ Lin(ℝ^{n}, ℝ^{m}).

Uncurrying, this means the Jacobian can also be seen as a smooth map

J(f): ℝ^{n} × ℝ^{n} ⟶ ℝ^{m}

which is linear in its first variable. A Cartesian differential category asks for an operation of this type, satisfying the axioms described below. However, notice that to express the axioms, one needs the ability to add parallel maps. It turns out this is not an enrichment in commutative monoids as one might expect, but rather a skew enrichment, [Street], which makes it a Cartesian left additive category. In such a category the addition of arrows is only preserved by composition on the left, that is f(g + h) = fg + gh and f0 = 0.

CARTESIAN DIFFERENTIAL STORAGE CATEGORIES  671

4.1.1. Definition. A Cartesian differential category is a Cartesian left additive category with an operation

{X ⟶^{f} Y \atop X × X ⟶_{D[f]} Y} D[ ]

(called “differentiation”) satisfying: [CD.1] D[f + g] = D[f] + D[g] and D[0] = 0 (differentiation preserves addition); [CD.2] ⟨a+b, c⟩D[f] = ⟨a, c⟩D[f]+⟨b, c⟩D[f] and ⟨0, a⟩D[f] = 0 (a derivative is additive

in its first variable); [CD.3] D[1] = π_{0}, D[π_{0}] = π_{0}π_{0}, and D[π_{1}] = π_{0}π_{1} (projections and identity are linear); [CD.4] D[⟨f, g⟩] = ⟨D[f], D[g]⟩ (differentiation is compatible with pairing) ; [CD.5] D[fg] = ⟨D[f], π_{1}f⟩D[g] (the chain rule); [CD.6] ⟨⟨a, 0⟩, ⟨c, d⟩⟩D[D[f]] = ⟨a, d⟩D[f] (the differential is linear); [CD.7] ⟨⟨a, b⟩, ⟨c, d⟩⟩D[D[f]] = ⟨⟨a, c⟩, ⟨b, d⟩⟩D[D[f]] (interchange rule);

We recall a number of examples of Cartesian differential categories: 4.1.2. Example.

(1) If 𝕏 is an additive Cartesian category (i.e. enriched in commutative monoids) then, by defining D[f] = π_{0}f, it can be viewed as a Cartesian differential category in which every map is linear.

(2) Smooth functions on finite dimensional Euclidean vector spaces form a Cartesian differential category.

(3) The coKleisli category of any monoidal differential category (satisfying the interchange law) is a Cartesian differential category, [BCS09]. A basic example of a monoidal differential category is provided by the category of relations, Rel, with respect to the “multi-set” (or “bag”) comonad. The deriving transformation d_{⊗}: A ⊗ M(A) ⟶ M(A), which adds another element to the multi–set M(A), provides the (monoidal) differential structure.

(4) Convenient vector spaces [BET12] form a Cartesian differential category.

(5) There is a comonad Faa on the category of Cartesian left additive categories whose coalgebras are exactly Cartesian differential categories [CS11].

Cartesian differential categories already have a notion of “linear map”: namely those f such that D[f] = π_{0}f. Furthermore, it is a basic result that any simple slice, 𝕏[A], of a Cartesian differential category, 𝕏, is also a Cartesian differential category. The differential in the simple slice 𝕏[A] is given by:

{X × A ⟶^{f} Y \atop (X × X) × A ⟶_{D_{A}[f]} Y} D_{A}[ ]

where

(X × X) × A ⟶^{D_{A}[f]} Y

= (X × X) × A ⟶_{⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩} (X × A) × (X × A) ⟶_{D[f]} Y

This is precisely the familiar notion of a partial derivative.

In particular, this means we may isolate linear maps in this differential sense in each slice as those maps with D_{A}[f] = (π_{0} × 1)f. Our first observation is then:

4.1.3. Proposition. In a Cartesian differential category, 𝕏, the linear maps form a system of linear maps.

Proof. We must check the requirements of being a linear system:

[LS.1] We require, for each A ∈ 𝕏, that the identity maps, projections and pairings of linear maps are linear. As explained above, in 𝕏[A] a map f: X ×A ⟶ Y is linear in case D_{A}[f] = (π_{0} ×1)f: (X ×X)×A ⟶ Y where D_{A}[f] is the partial derivative of f:

D_{A}[f]: = ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[f]

We shall leave all but the last requirement to the reader for which we shall do a concrete calculation in 𝕏. Suppose f and g are linear in this sense in 𝕏[A] (that is they are in L[A]), then we must show that the pairing of f and g in 𝕏[A] is linear: as a map in 𝕏 this pairing is just ⟨f, g⟩ so that:

D_{A}[⟨f, g⟩] = ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[⟨f, g⟩]
= ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩⟨D[f], D[g]⟩
= ⟨⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[f], ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[g]⟩
= ⟨D_{A}[f], D_{A}[g]⟩

(Using linearity of f and g)

= ⟨⟨(π_{0} × 1)f, (π_{0} × 1)g⟩
= (π_{0} × 1)⟨f, g⟩

showing that ⟨f, g⟩ is linear in this sense.

[LS.2] We must show that these linear maps are closed to composition in each slice and that when g is a linear retraction that gh ∈ L[A] implies h ∈ L[A]. Leaving composition to the reader let us focus on the second part. If sg = 1 then using the non-trivial fact that D_{A}[ ] is a differential in 𝕏[A] we have

D_{A}[h] = D_{A}[sgh] = ⟨D_{A}[s], π_{1}s⟩D_{A}[gh] = ⟨D_{A}[s], π_{1}s⟩π_{0}gh
= D_{A}[s]gh = D_{A}[sg]h = D_{A}[1]h = π_{0}h.

[LS.3] For the last part we shall do a concrete calculation in 𝕏: we must show that if h is linear in 𝕏[B] then 𝕏[f](h) is linear in 𝕏[A]; here is the calculation:

D_{A}[𝕏[f](h)] = D_{A}[(1 × f)h] = ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[(1 × f)h]
= ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩⟨D[1 × f], π_{1}(1 × f)⟩D[h]
= ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩⟨⟨π_{0}π_{0}, ⟨π_{0}π_{1}, π_{1}π_{1}⟩D[f]⟩, π_{1}(1 × f)⟩D[h]
= ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩⟨⟨π_{0}π_{0}, ⟨π_{0}π_{1}, π_{1}π_{1}⟩D[f]⟩, π_{1}(1 × f)⟩D[h]
= ⟨⟨π_{0}π_{0}, ⟨0, π_{1}⟩D[f]⟩, ⟨π_{0}π_{1}, π_{1}⟩(1 × f)⟩D[h]
= ⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩(1 × f)⟩D[h]
= (1 × f)⟨⟨π_{0}π_{0}, 0⟩, ⟨π_{0}π_{1}, π_{1}⟩⟩D[h]

(Linearity of h)

= (1 × f)(π_{0} × 1)h
= (π_{0} × 1)(1 × f)h

4.2. Cartesian differential storage categories: the basics. A Cartesian differential storage category is a Cartesian differential category whose linear maps— in the natural differential sense—are (strongly and persistently) classified.

We first observe that every Cartesian differential category has a codereliction map defined by:

η_{A}: = ⟨1, 0⟩D[φ]: A ⟶ S(A).

4.2.1. Lemma. η so defined is a codereliction map: that is it is natural for linear maps and has ηϵ = 1.

Proof. We need to show η_{A}ϵ_{A} = 1_{A}:

η_{A}ϵ_{A} = ⟨1, 0⟩D[φ]ϵ
= ⟨1, 0⟩D[φ]ϵ] (as ϵ is linear)
= ⟨1, 0⟩D[1] = ⟨1, 0⟩π_{0} = 1

and that, if f: A ⟶ B is a linear map, that fη_{B} = η_{A}S(f):

η_{A}S(f) = ⟨1, 0⟩D[φ]S(f)
= ⟨1, 0⟩D[φS(f)] (as S(f) is linear)
= ⟨1, 0⟩D[fφ]
= ⟨1, 0⟩⟨D[f], π_{1}f⟩D[φ]
= ⟨1, 0⟩⟨π_{0}f, π_{1}f⟩D[φ]
= ⟨1, 0⟩⟨π_{0}f, π_{1}f⟩D[φ]
= ⟨f, 0f⟩D[φ] = f⟨1, 0⟩D[φ] = fη_{B}

Because Cartesian differential storage categories always have a codereliction map, up to splitting linear idempotents, they also have monoidal representation. Thus it makes sense to ask whether the subcategory of linear maps forms a monoidal differential category. To prove this is so will be the main aim of the current section. However, before turning to this it is worth making some further basic observations.

4.2.2. Lemma. If 𝕏 is a Cartesian differential storage category with monoidal representation then the tensor product on the linear maps is additive in the sense that (f +g)⊗h = f ⊗ h + g ⊗ h and 0 ⊗ h = 0.

Proof. We illustrate the proof with the first equation: (f + g) ⊗ h = (f ⊗ h) + (g ⊗ h). This follows from the fact that (f +g)⊗h and (f ⊗h)+(g⊗h) are determined respectively byφ_{⊗}((f + g) ⊗ h) and φ_{⊗}((f ⊗ h) + (g ⊗ h)). So:

φ_{⊗}((f + g) ⊗ h) =_{[defn]}  ((f + g) × h)φ_{⊗}
=_{[φ_{⊗} bilinear]} (f × h)φ_{⊗} + (g × h)φ_{⊗}
=_{[defn]}  φ_{⊗}(f ⊗ h) + φ_{⊗}(g ⊗ h)
=_{[left additive]} φ_{⊗}((f ⊗ h) + (g ⊗ h))

The 0-ary case is similar.

Suppose 𝕏 is a Cartesian storage category which is also a Cartesian differential category. In this context, 𝕏, has two notions of “linear” map: viz the notion which all storage categories have, and the notion that all Cartesian differential categories have. An interesting observation is:

4.2.3. Proposition. 𝕏 is a Cartesian differential storage category if and only if it is both a Cartesian differential and storage category and S(f) (for any f) and ϵ are linear in the differential sense and the codereliction map η is linear in the storage sense.

Proof. By assumption, D[S(f)] = π_{0}S(f), for any f, D[ϵ] = π_{0}ϵ, and η is ϵ-natural. We must show that f is ϵ-natural if and only if D_{×}[f] = π_{0}f. So suppose first that f is ϵ-natural:

D[f] = (φ × φ)(ϵ × ϵ)D[f]
= (φ × φ)D[ϵf]
= (φ × φ)D[S(f)ϵ]
= (φ × φ)π_{0}S(f)ϵ
= (φ × φ)π_{0}ϵf
= π_{0}φϵf = π_{0}f

Next, suppose that D[f] = π_{0}f we must show f is ϵ-natural assuming that η is. We observe that, in this case, f = ηS(f)ϵ, from which the result is immediate, as η, S(f), and ϵ are ϵ natural. Here is the calculation:

f = ⟨1, 0⟩π_{0}f
= ⟨1, 0⟩D[f]
= ⟨1, 0⟩D[fφϵ]
= ⟨1, 0⟩D[φS(f)ϵ]
= ⟨1, 0⟩D[φ]S(f)ϵ
= ηS(f)ϵ

Recall that in a monoidal differential category it is possible to re-express the derivative using a deriving transformation d_{⊗}: A ⊗ S(A) ⟶ S(A) into a more compact form. It is natural to wonder whether the same thing cannot be done for Cartesian differential storage categories: that is define the derivative in terms of analogous structure:

4.2.4. Definition. A Cartesian deriving transformation on a Cartesian storage category is a (not-necessarily natural) transformation d_{×}: A × A ⟶ S(A) satisfying:

[cd.1] d_{×}S(0)ϵ = 0, d_{×}S(f + g)ϵ = d_{×}(S(f) + S(g))ϵ

[cd.2] ⟨h + k, v⟩d_{×} = ⟨h, v⟩d_{×} + ⟨k, v⟩d_{×}, ⟨0, v⟩d_{×} = 0

[cd.3] d_{×}ϵ = π_{0}

[cd.4] d_{×}S(⟨f, g⟩)ϵ = d_{×}⟨S(f)ϵ, S(g)ϵ⟩ (Note that d_{×}S(!)ϵ = d_{×}! =! is true since 1 is terminal.)

[cd.5] d_{×}S(fg)ϵ = ⟨d_{×}S(f)ϵ, π_{1}f⟩d_{×}S(g)ϵ

[cd.6] ⟨⟨g, 0⟩, ⟨h, k⟩⟩d_{×}S(d_{×})ϵ = ⟨g, k⟩d_{×} [cd.7] ⟨⟨0, h⟩, ⟨g, k⟩⟩d_{×}S(d_{×})ϵ = ⟨⟨0, g⟩, ⟨h, k⟩⟩d_{×}S(d_{×})ϵ

[cd.8] η =_{def} ⟨1, 0⟩d_{×} is ϵ-natural (or linear).

It is now straightforward to observe:

4.2.5. Proposition. A Cartesian storage category with a Cartesian deriving transformation is precisely a Cartesian differential storage category.

Proof. The translation between the two structures is given by:

D[f]: = d_{×}S(f)ϵ and d_{×}: = D[φ]

Note that these are inverse as

D[f]: = d_{×}S(f)ϵ: = D[φ]S(f)ϵ = D[φS(f)ϵ] = D[fφϵ] = D[f]

and

d_{×}: = D[φ]: = d_{×}S(φ)ϵ = d_{×}.

Most of the axioms are clearly direct translations of each other: [CD.1,2,4-7] and [cd.1,2,4-7] are clearly equivalent through this translation. For [CD.3], note that D[1] = d_{×}ϵ = π_{0} and that D[π_{i}] = d_{×}S(p_{i})ϵ = d_{×}ϵπ_{i} = π_{0}π_{i}, since in a storage category, projections are linear (by [LS.1]).

It remains to show that being linear in the differential sense coincides with being linear in the storage sense. First note if f is epsilon natural, that is ϵf = S(f)ϵ, then D[f] = d_{×}S(f)ϵ = d_{×}ϵf = π_{0}f. Conversely, suppose that D_{×}[f] = π_{0}f, then f = ηS(f)ϵ as

f = ⟨1, 0⟩π_{0}f = ⟨1, 0⟩d_{×}S(f)ϵ = ηS(f)ϵ

which by assumption is linear (in the sense of being ϵ-natural).

4.3. The main theorem. From the results of Section 3, we also note that, in the presence of a codereliction map and when sufficient linear idempotents split, every Cartesian differential storage category has strong persistent monoidal representation. The main result of the paper is:

4.3.1. Theorem. The linear maps of a Cartesian differential storage category, in which linear idempotents split, form a monoidal differential storage category satisfying the interchange rule.

Let us first recall what a monoidal differential category is. A monoidal differential category is a monoidal category with a coalgebra modality (see Definition 3.1.2) equipped with a natural transformation

d_{⊗}: A ⊗ S(A) ⟶ S(A)

called a deriving transformation satisfying:

[d.1] d_{⊗}e = 0 (constants)

[d.2] d_{⊗}ϵ = 1 ⊗ e (linear maps)

[d.3] d_{⊗}Δ = (1 ⊗ Δ)(d_{⊗} ⊗ 1) + (1 ⊗ Δ)(c_{⊗} ⊗ 1)(1 ⊗ d_{⊗}) (the product rule)

[d.4] d_{⊗}δ = (1 ⊗ Δ_{⊗})a_{⊗}(d_{⊗} ⊗ δ)d_{⊗} (the chain rule)

[d.5] (1 ⊗ d_{⊗})d_{⊗} = a_{⊗}(c_{⊗} ⊗ 1)a_{⊗}^{−1}(1 ⊗ d_{⊗})d_{⊗} (the interchange rule)

A monoidalstorage differential category simply means that the storage transformations (see Definition 3.1.1) are isomorphisms. Note also that in [BCS06] a differential category was defined to be one satisfying only the first four of these conditions: the last condition, the interchange rule, was introduced in [BCS09] in order to ensure that the coKleisli category was a Cartesian differential category. Here we shall simply add the interchange law as a condition for being a monoidal differential category, as it will turn out not only to be sufficient but necessary to obtain the characterization of monoidal differential storage categories (with an exact modality) as the linear maps of a Cartesian differential storage category.

The remainder of the section is dedicated to proving Theorem 4.3.1.

Given a Cartesian differential storage category here is the definition of the monoidal deriving transformation:

\xymatrix{A × S(A) \ar[d]_{φ_{⊗}} \ar[r]^{η×1} & S(A) × S(A) \ar[r]^{m_{×}} & S(A × A) \ar[r]^{S(D[φ_{A}])} & S^{2}(A) \ar[d]^{ϵ} \\ A ⊗ S(A) \ar@{.>}[rrr]_{d_{⊗}} &  &  & S(A)}

We start by observing:

4.3.2. Lemma.

(i) d_{⊗} is natural for linear maps;

(ii) The monoidal deriving transformation and the differential are inter-definable with

D[f] = (1 × φ)φ_{⊗}d_{⊗}S(f)ϵ.

Proof.

(i) Note that d_{⊗}S(f) = (f ⊗ S(f))d_{⊗} if and only if φ_{⊗}d_{⊗}S(f) = φ_{⊗}(f ⊗ S(f))d_{⊗} but φd_{⊗} = (η × 1)m_{×}S(D[φ])ϵ which is natural for linear f. This provides the result immediately.

(ii) It suffices to prove the equality:

(1 × φ)φ_{⊗}d_{⊗}S(f)ϵ

= (1 × φ)(η × 1)m_{×}S(D[φ])ϵS(f)ϵ
= (1 × φ)(η × 1)m_{×}S(D[φ])S(S(f)ϵ)ϵ]
= (η × 1)(1 × φ)m_{×}S(D[φS(f)ϵ])ϵ
= (η × 1)θS(D[fφϵ])ϵ (strength)
= (1 × φ)(1 × ϵ)D[f] (linearity of differential in first argument)
= D[f]

We want to show that d_{⊗} as defined satisfies (d.1)–(d.5) above. So we shall simply go through the conditions:

[d.1] Constants (d_{⊗}e = 0)

d_{⊗}e = d_{⊗}S(0)s_{⊤}
= (0 ⊗ S(0))d_{⊗}s_{⊤}
= 0

[d.2] Differentials of linear maps (d_{⊗}ϵ = 1 ⊗ e)

φ_{⊗}d_{⊗}ϵ = (η × 1)m_{×}S(D[φ])ϵϵ
= (η × 1)m_{×}S(D[φ]ϵ)ϵ
= (η × 1)m_{×}S(D[φϵ])ϵ
= (η × 1)m_{×}S(D[1])ϵ
= (η × 1)m_{×}S(π_{0})ϵ
= (η × 1)π_{0}ϵ
= π_{0}ηϵ
= π_{0} = φ_{⊗}(1 ⊗ e)

[d.3] The product rule (d_{⊗}Δ = (1 ⊗ Δ)(d_{⊗} ⊗ 1) + (1 ⊗ Δ)(c_{⊗} ⊗ 1)(1 ⊗ d_{⊗}))

This is more complicated. Start by noting:

d_{⊗}Δ = d_{⊗}S(⟨1, 0⟩ + ⟨0, 1⟩)s_{⊗}
= ((⟨1, 0⟩ + ⟨0, 1⟩) ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{⊗}
= (⟨1, 0⟩ ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{⊗}

+ (⟨0, 1⟩ ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{⊗}

CARTESIAN DIFFERENTIAL STORAGE CATEGORIES  679

It suffices to prove that (⟨1, 0⟩ ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{⊗} = (1 ⊗ Δ)(d_{⊗} ⊗ 1) and

(⟨0, 1⟩ ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{⊗} = (1 ⊗ Δ)(c_{⊗} ⊗ 1)(1 ⊗ d_{⊗})

We shall demonstrate the former leaving the latter to the reader. However, we require some observations first:

4.3.3. Lemma.

(i) If h: A × B ⟶ C is bilinear, then ⟨⟨a, b⟩, ⟨c, e⟩⟩D[h] = ⟨a, e⟩h + ⟨c, b⟩h; (ii) ⟨⟨a, b⟩, ⟨c, e⟩⟩D[m_{×}] = ⟨a, e⟩m_{×} + ⟨c, b⟩m_{×}; (iii) ⟨⟨a, b⟩, ⟨c, e⟩⟩D[φ_{A×B}] = ⟨⟨a, c⟩D[φ_{A}], eφ_{B}⟩m_{×} + ⟨cφ_{A}, ⟨b, e⟩D[φ_{B}]⟩m_{×}; (iv) (⟨1, 0⟩ × 1)D[φ_{A×B}] = a_{×}(D[φ_{A}] × φ_{B})m_{×}.

Proof.

(i) We have the following calculation:

⟨⟨a, b⟩, ⟨c, e⟩⟩D[h] = ⟨⟨a, 0⟩, ⟨c, e⟩⟩D[h] + ⟨⟨0, b⟩, ⟨c, e⟩⟩D[h]
= ⟨a, ⟨c, e⟩⟩D_{B}[h] + ⟨b, ⟨c, e⟩⟩D_{A}[h]
= ⟨a, e⟩h + ⟨c, b⟩h (h is bilinear).

(ii) Use the fact that m_{×} is bilinear (see Lemma 3.2.4). (iii) Using the fact that φ_{A×B} = (φ_{A} × φ_{B})m_{×} (see Proposition 2.3.7) we have:

⟨⟨a, b⟩, ⟨c, e⟩⟩D[φ_{A×B}]

= ⟨⟨a, b⟩, ⟨c, e⟩⟩D[(φ_{A} × φ_{B})m_{×}]
= ⟨⟨a, b⟩, ⟨c, e⟩⟩⟨D[φ_{A} × φ_{B}], π_{1}(φ_{A} × φ_{B})⟩D[m_{×}]
= ⟨⟨a, b⟩, ⟨c, e⟩⟩⟨⟨(π_{0} × π_{0})D[φ_{A}], (π_{1} × π_{1})D[φ_{B}]⟩, ⟨π_{1}π_{0}φ_{A}, π_{1}π_{1}φ_{B}⟩⟩D[m_{×}]
= ⟨⟨⟨a, c⟩D[φ_{A}], ⟨b, e⟩D[φ_{B}]⟩, ⟨cφ_{A}, eφ_{B}⟩⟩D[m_{×}]
= ⟨⟨a, c⟩D[φ_{A}], eφ_{B}⟩m_{×} + ⟨cφ_{A}, ⟨b, e⟩D[φ_{B}]⟩m_{×}.

(iv) We apply (iii):

(⟨1, 0⟩ × 1)D[φ_{A×B}]

= ⟨⟨π_{0}, 0⟩, ⟨π_{1}π_{0}, π_{1}π_{1}⟩⟩D[φ_{A×B}]
= ⟨⟨π_{0}, π_{1}π_{0}⟩D[φ_{A}], π_{1}π_{1}φ_{B}⟩m_{×} + ⟨π_{1}π_{1}φ_{A}, ⟨0, π_{1}π_{1}⟩D[φ_{B}]⟩m_{×}
= ⟨⟨π_{0}, π_{1}π_{0}⟩D[φ_{A}], π_{1}π_{1}φ_{B}⟩m_{×} + ⟨π_{1}π_{1}φ_{A}, 0⟩m_{×}
= ⟨⟨π_{0}, π_{1}π_{0}⟩D[φ_{A}], π_{1}π_{1}φ_{B}⟩m_{×} + 0
= a_{×}(D[φ_{A}] × φ_{B})m_{×}.

We are now ready to calculate. Since both maps are linear we may prefix each side with the universal map which gives monoidal representation; the universal property tells us that the maps are equal if and only if these composites are equal. Here is the calculation:

φ_{⊗}(⟨1, 0⟩ ⊗ S(⟨1, 0⟩ + ⟨0, 1⟩))d_{⊗}s_{2}

= (⟨1, 0⟩ × S(Δ_{×}))φ_{⊗}d_{⊗}s_{2}
= (⟨1, 0⟩ × S(Δ_{×}))(η × 1)m_{×}S(D[φ_{A×A}])ϵs_{2}
= (η × S(Δ_{×}))m_{×}S((⟨1, 0⟩ × 1)D[φ_{A×A}])ϵs_{2}
= (η × Δ_{×})(1 × m_{×})m_{×}S(a_{×}(D[φ_{A}] × φ_{A})m_{×})ϵs_{2} (Lemma 4.3.3 (iv))
= (η × Δ_{×})a_{×}(m_{×} × 1)m_{×}S(D[φ_{A}] × φ_{A})S(m_{×})ϵs_{2}
= (η × Δ_{×})a_{×}(m_{×} × 1)(S(D[φ_{A}]) × S(φ_{A}))m_{×}S(m_{×})ϵs_{2}
= (η × Δ_{×})a_{×}(m_{×} × 1)(S(D[φ_{A}]) × S(φ_{A}))(ϵ × ϵ)m_{×}s_{2} (Lemma 2.3.6 (ii))
= (η × Δ_{×})a_{×}(m_{×} × 1)(S(D[φ_{A}]) × 1)(ϵ × 1)φ_{⊗}
= (1 × Δ_{×})a_{×}(((η × 1)m_{×}S(D[φ_{A}])ϵ) × 1)φ_{⊗}
= (1 × Δ_{×})a_{×}((φ_{⊗}d_{⊗}) × 1)φ_{⊗}
= (1 × Δ_{×})a_{×}(φ_{⊗} × 1)φ_{⊗}(d_{⊗} ⊗ 1)
= (1 × Δ_{⊗})φ_{⊗}(d_{⊗} ⊗ 1)
= φ_{⊗}(1 ⊗ Δ_{⊗})(d_{⊗} ⊗ 1)

[d.4] To prove the chain rule, d_{⊗}δ = (1 ⊗ Δ_{⊗})a_{⊗}(d_{⊗} ⊗ δ)d_{⊗}, we precompose both sides with (1 × φ)φ_{⊗}. As both maps are clearly linear we can then use the universal properties of φ and φ_{⊗} to conclude the original maps are equal if and only if these composites are:

(1 × φ)φ_{⊗}d_{⊗}δ

= (1 × φ)(η × 1)m_{×}S(D[φ])ϵS(φ)
= (1 × φ)(η × 1)m_{×}S(D[φ]S(φ))ϵ
= (η × φ)m_{×}S(D[φS(φ)])ϵ
= (η × 1)θS(D[φφ])ϵ
= (η × 1)(ϵ × 1)D[φφ]
= D[φφ]

(1 × φ)φ_{⊗}(1 ⊗ Δ_{⊗})a_{⊗}(d_{⊗} ⊗ δ)d_{⊗}

= (1 × φ)(1 × Δ_{⊗})φ_{⊗}a_{⊗}(d_{⊗} ⊗ δ)d_{⊗}
= (1 × φΔ_{×})a_{×}(φ_{⊗} × 1)φ_{⊗}(d_{⊗} ⊗ δ)d_{⊗}
= (1 × φΔ_{×})a_{×}((φ_{⊗}d_{⊗}) × S(φ))φ_{⊗}d_{⊗}
= (1 × φΔ_{×})a_{×}(((η × 1)m_{×}S(D[φ])ϵ) × S(φ))(η × 1)m_{×}S(D[φ])ϵ
= (1 × Δ_{×}(φ×φ))a_{×}((η×1)m_{×}S(D[φ])ϵ×S(φ))(η×1)m_{×}S(D[φ])ϵ
= (1 × Δ_{×})a_{×}(((η × φ)m_{×}S(D[φ])ϵ) × φS(φ))(η × 1)m_{×}S(D[φ])ϵ
= (1 × Δ_{×})a_{×}(((η × 1)θS(D[φ])ϵ) × (φφ))(η × 1)m_{×}S(D[φ])ϵ
= (1 × Δ_{×})a_{×}(((η × 1)(ϵ × 1)D[φ]) × (φφ))(η × 1)m_{×}S(D[φ])ϵ
= (1 × Δ_{×})a_{×}(D[φ] × φ)(η × φ)m_{×}S(D[φ])ϵ
= (1 × Δ_{×})a_{×}(D[φ] × φ)(η × 1)(ϵ × 1)D[φ]
= (1 × Δ_{×})a_{×}(D[φ] × φ)D[φ]
= D[φφ]

[d.5] Interchange ((1 ⊗ d_{⊗})d_{⊗} = a_{⊗}(c_{⊗} ⊗ 1)a_{⊗}^{−1}(1 ⊗ d_{⊗})d_{⊗})

We may precompose with (1 × 1 × φ)(1 × φ_{⊗})φ_{⊗}.

⟨a, b, c⟩(1 × 1 × φ)(1 × φ_{⊗})φ_{⊗}(1 ⊗ d_{⊗})d_{⊗}

= ⟨a, b, c⟩(1 × 1 × φ)(1 × φ_{⊗}d_{⊗})φ_{⊗}d_{⊗}
= ⟨a, b, c⟩(1 × 1 × φ)(1 × (η×1)m_{×}S(D[φ])ϵ)(η×1)m_{×}S(D[φ])ϵ
= ⟨aη, bη, c⟩1 × θ(S(D[φ])ϵ)m_{×}S(D[φ])ϵ
= ⟨aη, bη, c⟩(1 × (ϵ × 1)D[φ])m_{×}S(D[φ])ϵ
= ⟨aη, ⟨b, c⟩D[φ]⟩m_{×}S(D[φ])ϵ

The identity requires us to show that a and b can be swapped.

Consider the double differential of φ:

⟨⟨0, a⟩, ⟨b, c⟩⟩D[D[φ]] = ⟨⟨0, a⟩, ⟨b, c⟩⟩D[φS(D[φ])ϵ]
= ⟨0, a⟩, ⟨b, c⟩⟩D[φ]S(D[φ])ϵ
= ⟨0, a⟩, ⟨b, c⟩⟩D[(φ × φ)m_{×}]S(D[φ])ϵ
= ⟨⟨0, a⟩, ⟨b, c⟩⟩D[φ × φ], ⟨bφ, cφ⟩⟩D[m_{×}]S(D[φ])ϵ
= ⟨⟨0, b⟩D[φ], ⟨a, c⟩D[φ]⟩, ⟨bφ, cφ⟩⟩D[m_{×}]S(D[φ])ϵ
= (⟨⟨0, b⟩D[φ], cφ⟩m_{×} + ⟨bφ, ⟨a, c⟩D[φ]⟩m_{×})S(D[φ])ϵ
= (0 + ⟨bφ, ⟨a, c⟩D[φ]⟩m_{×})S(D[φ])ϵ
= ⟨bφ, ⟨a, c⟩D[φ]⟩m_{×}S(D[φ])ϵ

Then we have:

⟨aφ, ⟨b, c⟩D[φ]⟩m_{×}S(D[φ])ϵ
= ⟨0, a⟩, ⟨b, c⟩⟩D[D[φ]]
= ⟨0, b⟩, ⟨a, c⟩⟩D[D[φ]]
= ⟨bφ, ⟨a, c⟩D[φ]⟩m_{×}S(D[φ])ϵ

We are nearly there except we would like to change φ into η, which is allowed by another lemma.

4.3.4. Lemma.

⟨bφ, ⟨a, c⟩D[φ]⟩m_{×}S(D[φ])ϵ = ⟨aη, ⟨b, c⟩D[φ]⟩m_{×}S(D[φ])ϵ

To prove this lemma we partially differentiate both sides of the equation derived above in the form:

⟨π_{0}π_{0}φ, ⟨π_{0}π_{1}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ = ⟨π_{0}π_{1}φ, ⟨π_{0}π_{0}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ

with respect to the first coordinate at position 0. This is best done using the term logic. In the derivation below we flip between the term logic and the categorical term. The derivation may best be read from the middle outward:

⟨π_{0}π_{0}η, ⟨π_{0}π_{1}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ
= ⟦((a, b), c) ↦ ϵ(S(D[φ])(m_{×}(η(a), D[φ](c) · b)))⟧
= ⟦((a, b), c) ↦ ϵ(S(D[φ])(m_{×}(\frac{∂φ(x)}{∂x} (0) · a, D[φ](c) · b)))⟧
= ⟦((a, b), c) ↦ \frac{∂ϵ(S(D[φ])(m_{×}(φ(x), D[φ](c).b)))}{∂x} (0) · a⟧
= ⟨⟨π_{0}π_{0}, 0, ⟩, 0⟩, ⟨⟨0, π_{0}π_{1}⟩, π_{1}⟩⟩D[⟨π_{0}π_{0}φ, ⟨π_{0}π_{1}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ
= ⟨⟨π_{0}π_{0}, 0, ⟩, 0⟩, ⟨⟨0, π_{0}π_{1}⟩, π_{1}⟩⟩D[⟨π_{0}π_{1}φ, ⟨π_{0}π_{0}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ
= ⟦((a, b), c) ↦ \frac{∂ϵ(S(D[φ])(m_{×}(φ(b), D[φ](c).x)))}{∂x} (0) · a⟧
= ⟦((a, b), c) ↦ ϵ(S(D[φ])(m_{×}(φb, \frac{∂D[φ](c) · x}{∂x} (0) · a)))⟧
= ⟦((a, b), c) ↦ ϵ(S(D[φ])(m_{×}(φb, D[φ](c) · a)))⟧
= ⟨π_{0}π_{1}φ, ⟨π_{0}π_{0}, π_{1}⟩D[φ]⟩m_{×}S(D[φ])ϵ

The key step uses the fact that η(a) is the partial derivative of φ(x) at 0 with linear argument a, that is η(a) = \frac{∂φ(x)}{∂x} (0) · a. Otherwise we are using the fact that we are differentiating in linear positions so the term does not change.

4.4. Differential λ-calculus. Cartesian closed differential categories, as defined in [BEM10, Man12], provide a semantics for the differential and the resource λ-calculus. Cartesian closed differential storage categories, by the results of Section 3.5, are precisely those semantic settings which arise as the coKleisli categories of monoidal closed differential storage categories. However, our definition of a Cartesian closed differential storage category is not transparently a Cartesian closed differential category, in the sense of [BEM10, Man12], as in those references it is required that differentiation can be moved inside the λ-abstraction. Recall that here we have only demanded the linearity of evaluation in higher-order arguments. In fact, we shall show these conditions are equivalent and hence the following proposition.

4.4.1. Proposition. To have a closed differential storage category is precisely to have a Cartesian closed differential category whose linear maps are (strongly and persistently) classified and which has linear hom-objects.

Proof. To establish this it suffices to observe that linearity of evaluation in its higherorder argument and being able to move differentials inside λ-abstractions are equivalent requirements. We start be assuming the latter:

Using the term logic, the ability to move differential under the λ-abstraction may be expressed as

\frac{∂λx.t}{∂y} (p) · v = λx. (\frac{∂t}{∂y} (p) · v)

A consequence of this requirement, as proven for example in [Man12, Lemma 3.10], (here translated into the term logic), is that

\frac{∂t s}{∂x} (p) · v = \frac{∂t[p/x] y}{∂y} (s[p/x]) · (\frac{∂s}{∂x} (p) · v) + (\frac{∂t}{∂x} (p) · v) s[p/x]

and so, if s does not contain x (so that \frac{∂s}{∂x} (p) · v = 0 and s[p/x] = s)

\frac{∂t s}{∂x} (p) · v = (\frac{∂t}{∂x} (p) · v) s

which amounts to the observation that evaluation is linear in its higher-order argument.

Conversely, recall (Definition 2.2.2) that a basic assumption on a closed system of maps is that evaluation should be linear in its higher-order argument. So, by the following argument (using η expansion) we see that one can move differentiation inside a λ-abstraction:

\frac{∂λx.t}{∂y} (p) · v = [λx. (\frac{∂λx.t}{∂y} (p) · v)] x = λx. (\frac{∂(λx.t) x}{∂y} (p) · v) = λx. (\frac{∂t}{∂y} (p) · v)

Thus, the axiom that states that one can move differentiation inside λ-abstractions is actually equivalent (under the adjunction for closure) to the requirement that evaluation be linear in its higher-order argument.

This allows us to establish:

4.4.2. Theorem. The coKleisli category of a monoidal differential storage category (satisfying the interchange rule) is a Cartesian closed differential storage category. Furthermore, the linear maps of a Cartesian closed differential storage category, in which linear idempotents split, form a monoidal closed differential storage category.

Proof. For the first statement: Proposition 3.5.4 tells us that the coKleisli category of a monoidal closed storage category is a Cartesian closed storage category. Applying this to the case of a monoidal closed differential storage category produces a Cartesian closed differential storage category, since the linear maps form a closed system and evaluation is linear in its higher-order argument.

For the second statement we note that by Definition 3.5.1, being a Cartesian closed differential storage category not only requires that the setting is Cartesian closed and that the linear maps form a closed system, but also that the equalizer for forming the object of linear maps is present. This then means the linear maps are a monoidal closed differential category by Corollary 3.5.3 and Theorem 4.3.1.

References

[B95] Gavin Bierman What is a categorical model of intutionistic linear logic. LNCS 92 (1995) 73–93.

[BET12] R. Blute, T. Ehrhard and C. Tasson A Convenient Differential Category. Cahiers de Topologie et Géométrie Différentielle Catégorique, 53. (2012) 211-233.

[BCS06] R. Blute, J.R.B. Cockett, R.A.G. Seely Differential categories. Mathematical Structures in Computer Science 16 (2006) 1049–1083.

[BCS09] R. Blute, J.R.B. Cockett, R.A.G. Seely Cartesian differential categories. Theory and Applications of Categories 22 (2009) 622–672.

[BEM10] A. Bucciarelli, T. Ehrhard, and G. Manzonetto Categorical Models for Simply Typed Resource Calculi. Electronic Notes in Theoretical Computer Science, vol. 265 (2010) 213-230.

[CS11] J.R.B. Cockett, R.A.G. Seely The Faà di Bruno Construction. Theory and Applications of Categories 25 (2011) 392-425.

[E04] T. Ehrhard Finiteness spaces. Mathematical Structures in Computer Science 15 (2005) 615–646.

[ER04] T. Ehrhard, L. Regnier The differential λ-calculus. Theoretical Computer Science, 309(1-3) (2003) 1–41.

[ER05] T. Ehrhard, L. Regnier Differential interaction nets. Workshop on Logic, Language, Information and Computation (WoLLIC), invited paper. Electronic Notes in Theoretical Computer Science, vol. 123, March 2005, Elsevier.

[F07] M.P. Fiore Differential structure in models of multiplicative biadditive intuitionistic linear logic. In Typed Lambda Calculi and Applications, Lecture Notes In Computer Science 4583. Springer-Verlag (2007) 163–177.

[F99] C. Fuhrmann Directe models of the computational lambda calculus. ENTCS 20 (1999) 147–172.

[J02] P.T. Johnstone, Sketches of an Elephant: a topos theory compendium 1, Oxford University Press, 2002.

[KE65] G.M. Kelly, S. Eilenberg Closed categories. In Proceedings of the Conference on Categorical Algebra, La Jolla, 1965, Berlin, Springer, 1966.

[Kock12] A. Kock Commutative monoids as a theory of distributions. Theory and Applications of Categories 26 (2012) 97–131.

[G87] J.-Y. Girard Linear logic. Theoretical Computer Science 50 (1987) 1–102.

[Man12] G. Manzonetto What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science 22(3) (2012) 451-520.

[M02] Paul-André Melliés Categorical models of linear logic revisited. Prépublication de l’équipe PPS, September (2003) number 22.

[S04] Andrea Schalk What is a categorical model for linear logic? (2004).

[S89] R.A.G. Seely Linear logic, ∗-autonomous categories and cofree coalgebras. AMS Contemporary Mathematics 92 (1989) 371–382.

[Street] R. Street Skew-closed categories, Journal of Pure and Applied Algebra 217(6) (June 2013) 973-988.

Department of Mathematics, University of Ottawa, 585 King Edward St., Ottawa, ON, K1N 6N5, Canada Department of Computer Science, University of Calgary, 2500 University Drive, Calgary, AL, T2N 1N4, Canada Department of Mathematics and Statistics, McGill University, 805 Sherbrooke St., Montréal, QC, H3A 2K6, Canada

Email: rblute@uottawa.ca
      robin@ucalgary.ca
      rags@math.mcgill.ca
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Radboud University Nijmegen: i.moerdijk@math.ru.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca