BRICS RS-98-21 Power et al.: A Representation Result for Free Cocompletions BRICS

Basic Research in Computer Science

A Representation Result for Free Cocompletions

John Power Gian Luca Cattani Glynn Winskel BRICS Report Series RS-98-21 ISSN 0909-0878 September 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/21/

A Representation Result for Free Cocompletions

John Power^{1,}^{∗}, Gian Luca Cattani^{2,}^{†}, Glynn Winskel^{3}

1LFCS, University of Edinburgh, Scotland 2Computer Laboratory, University of Cambridge, England

3 BRICS^{‡}, University of Aarhus, Denmark

September 1998

Abstract

Given a class F of weights, one can consider the construction that takes a small category ℂ to the free cocompletion of ℂ under weighted colimits, for which the weight lies in F. Provided these free F - cocompletions are small, this construction generates a 2-monad on Cat, or more generally on V-Cat for monoidal biclosed complete and cocomplete V. We develop the notion of a dense 2-monad on V-Cat and characterise free F -cocompletions by dense KZ-monads on V-Cat. We prove various corollaries about the structure of such 2-monads and their Kleisli 2-categories, as needed for the use of open maps in giving an axiomatic study of bisimulation in concurrency. This requires the introduction of the concept of a pseudo-commutativity for a strong 2-monad on a symmetric monoidal 2-category, and a characterisation of it in terms of structure on the Kleisli 2-category.

∗This work is supported by EPSRC grant GR/J84205: Frameworks for programming language semantics and logic.

†Research carried out while this author was at BRICS.

‡Basic Research in Computer Science, A Centre of the Danish National Research Foundation.

1 Introduction

Given a class of small categories S, one can consider the construction that takes a small category ℂ to the free cocompletion of ℂ under colimits of diagrams with shape in the class S. More subtly, and more naturally from the perspective of enriched category theory, for any monoidal biclosed complete and cocomplete V, given a class F of weights, one can consider the construction that takes a small V-category ℂ to the free cocompletion of ℂ under weighted colimits for which the weight lies in F. Provided that these S- or F -cocompletions are small, this construction generates a 2-monad on Cat, or more generally on V-Cat. We give an axiomatic characterisation of those 2-monads that arise in this way.

Although our characterisation and the results leading up to it hold for monoidal biclosed complete and cocomplete V, we shall only state them for symmetric monoidal closed complete and cocomplete V, because otherwise the swapping between V-categories and V_{t}-categories, where V_{t} = V but has the tensor product switched, becomes notationally tiresome. Some later results only hold for symmetric or even cartesian closed V: where that is so, we state it explicitly.

The notion of KZ-monad was introduced as a property of 2-monads given by cocompletions under classes of colimits [11]. But it is not sufficient to characterise them. For instance, consider the 2-monad T on Cat that sends every category to 1, the category with one object and one arrow only. It is a KZ-monad, but it is not given by a free cocompletion as there are many categories ℂ that do not embed fully into 1. So we need an additional condition. The condition we introduce is that of density of a 2-monad. We say that a 2-monad on V-Cat is dense if both the unit η_{ℂ} : ℂ ⟶ T ℂ and the V-functor induced by the unit η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] are fully faithful, coherently with respect to the action of T on V-functors. It follows that the coherence holds for V-natural transformations too. The central result of this paper is the proof that a 2-monad on V-Cat is a dense KZ-monad if and only if there is a class F of weights such that T is the 2-monad whose algebras are small F -cocomplete V-categories.

En route to that result, we characterise dense KZ-monads as those 2monads for which the V-functors η_{ℂ} and η̃_{ℂ} are always fully faithful and such that, for any V-functor H : ℂ ⟶ T 𝔻, the lifting of H to T ℂ given by the Kleisli construction is the restriction, up to coherent isomorphism, of Lan_{Y_{ℂ}}(η̃_{𝔻}H), where Y_{ℂ} : ℂ^{op} → [ℂ^{op}, V] is the Yoneda embedding.

We further show consequences of the definition, or alternatively of the characterisation, of dense KZ-monads: it follows that T sends finite coproducts to finite products if finite coproducts exist coherently in each T ℂ; in fact, the Kleisli 2-category has finite coproducts and they agree with finite products. Moreover, under a mild extra condition, every dense KZ-monad is pseudo-commutative, or equivalently, the Kleisli category is equivalent to a Gray-monoid, with structure induced by that in V-Cat.

The structures developed here are not purely of abstract interest, but have been used in the study of concurrency. They are at the heart of attempts to model bisimulation by open maps [6, 3]. Given a monad T on Cat, one may define a notion of open map within any category of the form T ℂ, with openness with respect to maps in ℂ. This notion of open map agrees with the notion of functional bisimulation, and can be extended, by considering spans of epimorphic open maps, to account for bisimulation in general as in [12]. One can prove, for a dense KZ-monad T, that all functors in the Kleisli category for T preserve open maps. The above structures allow one to account for the preservation of bisimulation by the various constructors, such as prefixing, nondeterministic sum, and a parallel operator, in a process algebra such as CCS. See [3], which contains an early version of some of the results of this paper, for more detail.

The paper is organised as follows. In Section 2, we recall the definition of weighted colimit in a V-category for monoidal biclosed complete and cocomplete V. In Section 3, we motivate and define the notion of dense KZmonad, and characterise it in terms of a condition on the Kleisli 2-category. In Section 4, we give our characterisation theorem. In Section 5, we develop the notion of a pseudo-commutativity for a strong 2-monad on a symmetric monoidal 2-category, and we characterise it in terms of a Gray-monoid structure on the Kleisli 2-category. Finally, in Section 6, we deduce further properties of dense KZ-monads, requiring some further conditions.

2 Weighted colimits and free cocompletions

In this section, we recall some definitions and results associated with weighted colimits and free cocompletions. The standard reference for these, in the case of enrichment over symmetric monoidal closed V, is Kelly’s book [8]. For the case of monoidal biclosed V, some more delicacy is needed, and the definitions for such V, more generally for enrichment in a biclosed bicategory W, are in [4]. For ease of exposition, we shall write in terms of symmetric V.

2.1 Definition A weight is a small V-category 𝔻 together with a V-functor

f : 𝔻^{op} ⟶ V .

2.2 Definition Given a weight f : 𝔻^{op} ⟶ V and a V-functor g : 𝔻 ⟶ ℂ, an f-weighted colimit of g is an object colim(f, g) of ℂ together with, for each object X of ℂ, an isomorphism between [𝔻^{op}, V](f−, ℂ(g−, X)) and ℂ(colim(f, g), X), V-naturally in X.

This definition can equally be expressed as asking for the existence of a colimiting cylinder [8] (rather than cone), such that composition with that cylinder yields the above natural isomorphism for every X. Here, a cylinder is just an object of [𝔻^{op}, V](f−, ℂ(g−, X)), extending the notion of cone, which is essentially the case where f is the constant at 1: it is not quite that simple, mainly because for arbitrary V, the unit need not be the terminal object, and consequently constant V-functors need not exist. See [8] for more detail on that. Nevertheless, weighted colimits do include all conical colimits. They also include all tensors, which you obtain by considering 𝔻 = 1. For the case of V = Set, i.e., for ordinary categories, tensors are copowers, so the concept of weighted colimit loses much of its force. But that is not true for V-categories in general, for instance for V = Poset or V = Cat. And even in the case of ordinary categories, our characterisation here of free cocompletions under weighted colimits cannot be expressed simply in terms of free cocompletions under conical colimits, as we shall see.

2.3 Definition Given a class F of weights, a locally small V-category with all f-weighted colimits for all f in F is called F -cocomplete. A V-functor between F -cocomplete V-categories that preserves all f-weighted colimits for all f in F is called F -cocontinuous.

2.4 Definition Given a class F of weights, a 2-monad for F -cocompletions is a 2-monad T on V-Cat for which, for every small V-category ℂ, the unit η_{ℂ} : ℂ ⟶ T ℂ exhibits T ℂ as the free F -cocompletion of ℂ, i.e., for any locally small F -cocomplete V-category 𝔻, composition with η_{ℂ} gives an equivalence between the category of F -cocontinuous V-functors from T ℂ to 𝔻 and that of V-functors from ℂ to 𝔻.

Letting F -Coc denote the 2-category of small F -cocomplete V-categories, F -cocontinous V-functors, and all V-natural transformations, an immediate consequence of the definition is

2.5 Corollary If T is a 2-monad for F -cocompletions, then T provides a left biadjoint to the forgetful 2-functor U : F -Coc ⟶ V-Cat.

The corollary does not have a converse. For instance, if V = Set and F consists of all possible weights, then F -Coc is biequivalent to the 2-category of complete lattices, as every small cocomplete category is a preordered set; and a left biadjoint to U is not what we mean by the free cocompletion of a small category. If F is the class of all weights, then there is no 2-monad for free cocompletions, precisely because the free cocompletion of a small category is not small. However, it follows from the corollary that if it exists, a 2-monad for F -cocompletions is unique up to equivalence.

Note that we have been careful to consider F -cocontinuous V-functors, not V-functors that strictly preserve F -weighted colimits. The situation we consider is the natural one, but we remark that our results here do not restrict well, in that the 2-monads we consider do not act as free F -cocompletions with respect to V-functors that strictly preserve F -weighted colimits. For an account of some of the relevant issues, and for our 2-categorical notation, see [2].

The main result of this paper is a characterisation of 2-monads for F - cocompletions. The central background result we use, shown for symmetric V in [8], extending routinely to non-symmetric V by the work of [4], is

2.6 Theorem The free F -cocompletion of a small V-category ℂ is given by the closure of the representables in [ℂ^{op}, V] under F -weighted colimits.

3 Dense KZ-monads

In this section, we motivate and define the notion of dense KZ-monad, and we characterise them in terms of their Kleisli categories. In order to fix notation, we recall

3.1 Definition A 2-monad on a 2-category A consists of a 2-functor

T : A ⟶ A ,

together with 2-natural transformations η : id ⇒ T and μ : T^{2} ⇒ T, satisfying the usual three axioms treated as axioms about 2-natural transformations rather than ordinary natural transformations.

3.2 Definition Given a 2-monad T on A, the Kleisli 2-category has as objects all objects C of A, and arrows those arrows H : T C ⟶ T D that respect μ_{C} and μ_{D}, with composition given by composition in A. An arrow in Kl(T) may equivalently be described as any arrow in A from C to T D. The 2-cells are those 2-cells in A that respect μ.

Considerable detail of 2-monads and the category theoretic constructions associated with them appears in [9].

3.3 Definition A KZ-monad is a 2-monad for which μ : T^{2} ⇒ T is left adjoint to ηT. It is equivalent to ask that μ be right adjoint to T η (see [11]).

The notion of KZ-monad was introduced to study particular features of 2-monads given by free cocompletions under classes of colimits [11]. But they do not characterise such free cocompletions, as the following example shows.

3.4 Example Consider the 2-monad on Cat that sends every category to the one object one arrow category 1. It is a KZ-monad trivially, but it does not give free cocompletions under a class of colimits because ℂ typically is not a full subcategory of 1.

So we need to consider a condition that is stronger than that of being a KZ-monad.

3.5 Notation

• Given a 2-monad T on V-Cat, let η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] denote the Vfunctor that sends an object X to the V-functor

T ℂ(η_{ℂ}−, X) : ℂ^{op} ⟶ V .

• Given V-functors H : C ⟶ D and J : C ⟶ C′, the left Kan extension of H along J is given by a V-functor Lan_{J}H : C′ ⟶ D and a V-natural transformation α : H ⇒ (Lan_{J}H)J that is universal among such V-natural transformations, i.e., given any V-functor K : C′ ⟶ D and any V-natural transformation β : H ⇒ KJ, there exists a unique V-natural transformation γ : Lan_{J}H ⇒ K making the evident triangle commute.

If it exists, a left Kan extension is unique up to coherent isomorphism. If J is fully faithful and a left Kan extension exists, then α is necessarily an isomorphism. The left Kan extension always exists if C is a small V-category and D is cocomplete (see [8] for more detail on left Kan extensions).

3.6 Definition A 2-monad T on V-Cat is dense if for every small Vcategory ℂ, the V-functors η_{ℂ} : ℂ ⟶ T ℂ and η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] are fully faithful, and for any H : ℂ ⟶ 𝔻, the V-functor

Lan_{Y_{ℂ}}(Y_{𝔻}H) : [ℂ^{op}, V] ⟶ [𝔻^{op}, V]

restricts to T H : T ℂ ⟶ T 𝔻 up to coherent isomorphism, where Y_{ℂ} : ℂ ⟶ [ℂ^{op}, V] is the Yoneda embedding.

It follows from our conditions that the behaviour of T on 2-cells is given by the restriction of that determined by left Kan extension on [ℂ^{op}, V], cf the proof of Corollary 3.8.

For 2-monads given by free cocompletions, η_{ℂ} : ℂ ⟶ T ℂ and η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] are fully faithful by Theorem 2.6, and for every V-functor H : ℂ ⟶ 𝔻, the V-functor Lan_{Y_{ℂ}}(Y_{𝔻}H) : [ℂ^{op}, V] ⟶ [𝔻^{op}, V] restricts to T H : T ℂ ⟶ T 𝔻 up to coherent isomorphism (see [8]).

3.7 Theorem Let T be a 2-monad on V-Cat for which η_{ℂ} : ℂ ⟶ T ℂ and η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] are fully faithful for every ℂ. Then T is a dense KZ-monad if and only if every V-functor H : T ℂ ⟶ T 𝔻 in Kl(T) is the restriction of Lan_{Y_{ℂ}}(η̃_{𝔻}Hη_{ℂ}) : [ℂ^{op}, V] ⟶ [𝔻^{op}, V] up to coherent isomorphism.

Proof Suppose T is dense and KZ, and let H : T ℂ ⟶ T 𝔻 be a V-functor in Kl(T). Then H = μ_{𝔻}K where K = Hη_{ℂ} : ℂ ⟶ T 𝔻. Using the density condition applied to K and the definition of KZ-monad, and the fact that left Kan extensions into cocomplete V-categories (such as [𝔻^{op}, V]) are colimits, so are preserved by V-functors with right V-adjoints, gives the result.

For the converse, given L : ℂ ⟶ 𝔻, let H = T L. By V-naturality of η and since η̃_{𝔻}η_{𝔻} is isomorphic to Y_{𝔻} : 𝔻 ⟶ [𝔻^{op}, V] by fully faithfulness of η_{𝔻}, it follows that η̃_{𝔻}Hη_{ℂ} = Y_{𝔻}L, so T is dense.

To see that T is KZ, first observe that μ_{ℂ} : T^{2}ℂ ⟶ T ℂ is a V-functor in Kl(T). So, up to isomorphism, μ_{ℂ} is the restriction of

Lan_{Y_{T ℂ}}(η̃_{ℂ}μ_{ℂ}η_{T ℂ}) = Lan_{Y_{T ℂ}} η̃_{ℂ} .

But, by fully faithfulness of η̃_{ℂ}, the V-functor η_{T ℂ} : T ℂ ⟶ T^{2}ℂ is the restriction of the V-functor sending Kϵ[ℂ^{op}, V] to [ℂ^{op}, V](η̃_{ℂ}−, K), but this latter V-functor is the right V-adjoint of Lan_{Y_{T ℂ}} η̃_{ℂ}. Since η̃_{ℂ} and η̃_{T ℂ} are both fully faithful, it follows that μ_{ℂ} is left V-adjoint to η_{T ℂ}.

3.8 Corollary For any dense KZ-monad on V-Cat, every H in Kl(T) is a left Kan extension of Hη_{ℂ} : ℂ ⟶ T 𝔻 along η_{ℂ} : ℂ ⟶ T ℂ.

Proof Given any K : T ℂ ⟶ T 𝔻, it follows by fully faithfulness of η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, V] that η̃_{𝔻}K is isomorphic to Lanη̃_{ℂ}(η̃_{𝔻}K)η̃_{ℂ}. Moreover, since η_{ℂ} is fully faithful, the Yoneda embedding Y_{ℂ} : ℂ ⟶ [ℂ^{op}, V] is isomorphic to η̃_{ℂ}η_{ℂ}. So any V-natural transformation α : Hη_{ℂ} ⇒ Kη_{ℂ}, induces a V-natural transformation from η̃_{𝔻}Hη_{ℂ} : ℂ ⟶ [𝔻^{op}, V] to Lanη̃_{ℂ}(η̃_{𝔻}K)Y_{ℂ}, hence by definition of left Kan extension, a V-natural transformation

ᾱ : Lan_{Y_{ℂ}}(η̃_{𝔻}Hη_{ℂ}) ⇒ Lanη̃_{ℂ}(η̃_{𝔻}K) .

The result follows immediately from Theorem 3.7, the commutativity up to coherent isomorphism for K, and fully faithfulness of η̃_{𝔻}.

3.9 Corollary Given a dense KZ-monad T on V-Cat, for every ℂ, μ_{ℂ} is the left Kan extension of id : ℂ ⟶ ℂ along η_{T ℂ} : T ℂ ⟶ T^{2}ℂ. Moreover, it is the restriction of [η−, V] : [T ℂ^{op}, V] ⟶ [ℂ^{op}, V].

4 The representation theorem

For a dense KZ-monad T, it is not true that there exists a class S of small V-categories such that T is the 2-monad for S-cocompletions. This is the case even for V = Set, i.e., even for ordinary categories.

4.1 Example Let T be the 2-monad on Cat such that T 0 = 0, where 0 is the empty category and T ℂ is given by freely adding an initial object to ℂ. It is routine to check the 2-monad axioms and to verify that T is dense and KZ. However, it is not a free cocompletion. Suppose otherwise. Let S be a class of small categories such that T ℂ is the free S-cocompletion of ℂ. Since T 0 is empty, every category in S must be nonempty. Now consider the transfinite construction of the free S-cocompletion. Since each category in S is nonempty, every colimit that is introduced has a map into it from an already existing object, so ultimately from an object in ℂ. So at no point in the transfinite induction do we introduce an initial object, a contradiction.

We now state our representation theorem. The above counterexample means we need to consider weighted colimits rather than restricting ourselves to conical ones. Moreover, we need a little caution about the precise statement here, because the class F is typically not small. So the assumption that T is a 2-monad is important to ensure that the free F -cocompletion of a small V-category is small.

4.2 Theorem A 2-monad T on V-Cat is a dense KZ-monad if and only if there is a class F of weights for which T is the 2-monad for F -cocompletions.

Proof The forward direction of this largely follows immediately from Theorem 2.6. It is routine to verify from the universal property and construction in [8] that the 2-monad is a KZ-monad.

For the converse, given T, define F to be the disjoint union over all small V-categories D of {f : 𝔻^{op} ⟶ V|fϵT 𝔻}. We must show for every small V-category ℂ, that T ℂ is the closure in [ℂ^{op}, V] of the representables under colimits of diagrams with weight in F. Trivially, T ℂ is contained in the latter V-category, as every object of T ℂ lies in F, and is the colimit of representables determined by itself as a weight. So it remains to show for any small V-category 𝔻, any X in T 𝔻, and any g : 𝔻 ⟶ T ℂ, that the weighted colimit colim(η̃_{𝔻}X, η̃_{ℂ}g) in [ℂ^{op}, V] lies in T ℂ. But this colimit is (Lan_{Y_{𝔻}}(η̃_{ℂ}g))η̃_{𝔻}X, and Lan_{Y_{𝔻}}(η̃_{ℂ}g) restricts to the lifting of g. So the colimit does lie in T ℂ and is given by the lifting of g.

We can gain a little more out of this with care. Given a small class F of weights, such as the class of weights for all finite colimits, one can consider the 2-monad T_{F} for F -cocompletions. One can then use the construction of the Theorem to obtain another class of weights F′ such that T is the 2monad for F′-cocompletions. But by construction, F′ will be large. But we can characterise F′ directly in terms of F. Albert and Kelly [1] defined a notion of closed class of weights.

4.3 Definition A class F of weights is closed if for any weight f : 𝔻^{op} → V, if every F -cocomplete V-category has f-weighted colimits, and if every F - cocontinuous V-functor preserves f-weighted colimits, then f lies in F.

Any class of weights F has a closure F̄. For instance, if F includes weights for finite products and equalisers, then F̄ includes weights for all finite limits. Albert and Kelly showed

4.4 Proposition A weight f : 𝔻^{op} ⟶ V is in F̄ if and only if it is in the closure of the representables in [𝔻^{op}, V] under F -weighted colimits.

So, it follows from the construction of the Theorem that we have

4.5 Corollary The class of weights given by the construction of the Theorem is always closed. And for any class F of weights for which F -cocompletions of small V-categories are small, the class of weights given by the construction of the Theorem is the closure F̄ of F.

5 Pseudo-commutativity

In order to study the properties of dense KZ-monads, we need a notion of pseudo-commutativity of a strong 2-monad on a symmetric monoidal 2category, and we need a result characterising pseudo-commutative 2-monads in terms of the Kleisli construction. So we develop such definitions and results in this section. A notion of pseudo-commutativity appeared in Kelly’s [7], but was not developed in general. We have the same notion but more compact axioms.

5.1 Definition Let V be a symmetric monoidal 2-category. A pseudocommutativity for a strong 2-monad T on V consists of, for every pair of objects (C, D), an isomorphic 2-cell χ_{C,D} between the two maps from T ℂ ⊗ T 𝔻 to T (C ⊗ D) induced by the strength, such that χ is natural in ℂ and D and satisfies three coherence conditions: T (c_{C,D})χ_{C,D} = (χ_{D,C})^{−1}c_{T C,T D}, coherence with respect to μ_{C}, and χ_{C,D}(η_{C} ⊗ id_{T D}) = id (coherence for D being a consequence). A pseudo-commutative monad is a strong 2-monad together with a pseudo-commutativity.

In general, a strong monad T on a symmetric monoidal category is commutative if and only if Kl(T) is symmetric monoidal, with tensor product given by T (C ⊗ D). We generalise that result. Modulo a straightforward generalisation of the usual coherence relating monoidal and strict monoidal categories, the notion we need here is that of Gray-monoid.

The category 2-Cat has a symmetric monoidal closed structure for which the closed structure is given by the 2-category P s(ℂ, 𝔻) of 2-functors from ℂ to 𝔻 and pseudo-natural transformations between them. The category 2-Cat together with this symmetric monoidal closed structure is called Gray [5].

5.2 Definition A Gray-monoid is a monoid in the symmetric monoidal closed category Gray, i.e., a 2-category A together with a 2-functor

· : A ⊗ A ⟶ A ,

subject to the monoid laws.

Spelling this out, we have

5.3 Proposition A Gray-monoid consists of

• a 2-category A,

• for each object X of A, 2-functors h_{X} : A ⟶ A and k_{X} : A ⟶ A, such that for every pair of objects (X, Y), h_{X}Y = k_{Y} X, which we denote by X ⊗ Y,

• for each pair of maps f : X ⟶ X′ and g : Y ⟶ Y′, a natural isomorphism between the two induced maps from X ⊗ Y to X′ ⊗ Y′

such that the isomorphisms respect the 2-functorial structure of h_{X} and k_{X}, and all the data respects associativity and units for ⊗.

5.4 Definition A symmetry for a Gray-monoid consists of, for each X and Y, an isomorphism c : X ⊗ Y ⟶ Y ⊗ X, such that c^{2} = id and (id_{Y} ⊗ c_{X,Z})(c_{X,Y} ⊗ id_{Z}) = c_{X,Y ⊗Z}, and such that ℂ respects all the Gray-structure. A symmetric Gray-monoid is a Gray-monoid together with a symmetry on it.

We want to characterise a pseudo-commutativity of a strong monad T by the structure of a Gray-monoid on Kl(T). That involves some delicate coherence. So we first recall a characterisation of a strength for a monad on a symmetric monoidal category in terms of structure on the Kleisli category [13]. A strict premonoidal category is exactly a Gray-monoid but with no two-dimensional data. In the following result, the notion of strict symmetric premonoidal functor is not entirely obvious, as it includes the axiom that the functor preserves central maps, as we shall define in our setting shortly.

5.5 Theorem Let V be a symmetric monoidal category, and let T be a monad on it. Then, to give a strength for T is to give a symmetric premonoidal structure on Kl(T) such that the canonical functor J : V ⟶ Kl(T) is a strict symmetric premonoidal functor.

We generalise the constructions of this result.

5.6 Definition A 1-cell f : X ⟶ X′ in a Gray-monoid is central if for every 1-cell g : Y ⟶ Y′, the isomorphic 2-cell between (X′ ⊗ g)(f ⊗ Y) and (f ⊗ Y′)(X ⊗ g) is the identity, and the dual.

5.7 Theorem Given a strong 2-monad T on a strict symmetric monoidal 2-category V, to give a pseudo-commutativity for T is to give Kl(T) the structure of a symmetric Gray-monoid such that the canonical 2-functor J : V ⟶ Kl(T) strictly preserves the strict symmetric monoidal structure, with each 1-cell in V sent to a central 1-cell in Kl(T).

Proof Given a pseudo-commutativity for T, and given f : T X ⟶ T X′ and g : T Y ⟶ T Y′ in Kl(T), a study of the construction of the two composites from T (X⊗Y) to T (X′⊗Y′) in Kl(T) yields the desired isomorphism, and the coherence laws follow directly from the coherence for pseudo-commutativity.

Conversely, to obtain a pseudo-commutativity from a symmetric Graymonoid structure on Kl(T), consider the components ϵ_{X} : T^{2}X ⟶ T X and ϵ_{Y} : T^{2}Y ⟶ T Y of the counit ϵ of the adjunction between V and Kl(T), and use the isomorphism determined by them. The coherence follows directly.

It is routine to verify that these constructions are mutually inverse.

We have glossed over a coherence issue here by assuming that V is strict symmetric monoidal. If V is symmetric monoidal, we cannot obtain a Graymonoid structure on Kl(T) because the monoidal structure is not strict on the objects of Kl(T). The most natural structure to consider in this regard is that of a monoidal bicategory, or a one object tricategory [5]. There is a coherence theorem that says every monoidal bicategory is equivalent to a Gray-monoid. But although the structure on Kl(T) is more general than that of a Gray-monoid, it is not as complicated as the structure of a monoidal bicategory, as the monoidal structure of Kl(T) involves coherent isomorphisms rather than coherent equivalences, and several commutativities hold here but do not hold in an arbitrary monoidal bicategory. The structure does not seem important enough to merit its own name, but we can at least say what structure Kl(T) has.

5.8 Theorem To give a pseudo-commutativity for a strong 2-monad T on a symmetric monoidal 2-category V is equivalent to the assertion that the Kleisli 2-category Kl(T) has the following structure:

• for each object X, 2-functors h_{X} : Kl(T) ⟶ Kl(T) and k_{X} : Kl(T) ⟶ Kl(T) such that h_{X}Y = k_{Y} X, extending ⊗ on V,

• for each pair of maps f : T X ⟶ T X′ and g : T Y ⟶ T Y′ in Kl(T), a natural isomorphism between the two induced maps from T (X ⊗ Y) to T (X′ ⊗ Y′), extending the commutativity on V,

such that

• the isomorphisms respect the 2-functorial structure of h_{X} and k_{X},

• all 1-cells in V are sent to central 1-cells in Kl(T),

• all the data respects the associativity and units for ⊗, meaning that h_{X}h_{X′} is isomorphic to h_{X⊗X′}, the dual for k, that h_{X}k_{Y} is isomorphic to k_{Y} h_{X}, and that h_{I} is isomorphic to the identity and dually for k_{I}, all with the isomorphisms on objects determined by those of V, and

• the symmetry ℂ of V extends to being 2-natural on Kl(T).

6 Properties of dense KZ-monads

Now we have the notion of pseudo-commutativity, we can investigate further properties of dense KZ-monads. For our first result, we need care with the precise statement for two reasons. In general, to give a strength to a monad on a symmetric monoidal closed V is equivalent to giving a V-enrichment of the monad. So every 2-monad on Cat has a unique strength associated with it. If V is symmetric monoidal closed, complete and cocomplete, V-Cat acquires a symmetric monoidal closed structure as a 2-category [8], but a 2-monad on V-Cat is not a V-Cat-enriched monad on V-Cat, so there is no reason in general to expect it to have a strength. In particular cases, it does have a strength, for instance if V is the arrow category, and so V-Cat is Poset. We resolve this by restricting attention to V-Cat-enriched monads on V-Cat. If V = Cat, this reduces to 2-monads on Cat.

6.1 Example Let F be any class of weights such that the F -cocompletion of any small V-category is small. Then the induced 2-monad acquires an enrichment in V-Cat. This follows by close inspection of left Kan extensions in enriched category theory [8].

Second, there is delicacy with coherence. In principle, we should like to prove that dense KZ-monads are always commutative. But we cannot prove precisely that, but can only prove the result up to canonical isomorphism. Here, we need the definition of pseudo-commutativity we developed in Section 5. By the usual constructions involving change of universe, the definitions and results extend from small to large categories. So assuming that, we have

6.2 Theorem Every V-Cat-monad T on V-Cat whose underlying 2-monad is dense KZ has a pseudo-commutativity.

Proof This is most easily proved by use of Theorem 4.2. The two Vfunctors from T ℂ ⊗ T 𝔻 to T (ℂ ⊗ 𝔻) send (f, g) to colim(f, colim(g, Y)) and colim(g, colim(f, Y)). Since colimits commute with colimits, and because comparison maps are unique, we have a pseudo-commutativity.

6.3 Corollary If T is a V-Cat-monad on V-Cat whose underlying 2-monad is dense KZ, then Kl(T) is equivalent to a symmetric Gray-monoid with monoidal operation given by T (C ⊗ D).

A detailed description of the structure of Kl(T) rather than that of a 2category equivalent to Kl(T) is given by Theorem 5.8.

We now consider constructions of the form T ℂ × T 𝔻. Here, we can make a slightly stronger statement by an axiomatic proof than we can by using an explicit construction of an equivalent version of T. The latter would yield an equivalence of V-categories, whereas axiomatically we can obtain an isomorphism, avoiding unpleasant coherence issues. We need to assume V cartesian closed here, as we use constant V-functors.

6.4 Theorem Let V be cartesian closed and let T be a dense KZ-monad on V−Cat. Suppose every T ℂ has and every T H and μ_{ℂ} strictly preserve finite coproducts. Then T ℂ × T 𝔻 is isomorphic to T (ℂ + 𝔻) 2-naturally in ℂ and 𝔻 and coherently with respect to the associative, commutative, and unit structures of binary product and coproduct.

Proof First observe that every V-functor in Kl(T) strictly preserves finite coproducts. Using the universal property of the Kleisli construction, and using the universal properties of products and coproducts, and in order to define a V-functor H : T (ℂ + 𝔻) ⟶ T ℂ × T 𝔻, we give V-functors from ℂ to each of T ℂ and T 𝔻 and from 𝔻 to each of T ℂ and T 𝔻. We define them by η_{ℂ} and the constant at the initial object of T 𝔻, and by duality.

We define K : T ℂ × T 𝔻 ⟶ T (ℂ + 𝔻) by sending (X, Y) to (T i_{0})X + (T i_{1})Y, where i_{0} : ℂ ⟶ ℂ + 𝔻 and i_{1} : ℂ ⟶ ℂ + 𝔻 are the left and right coprojections respectively.

We must show that H and K are mutually inverse. They are obviously 2-natural in ℂ and 𝔻. To see that KH = id_{T (ℂ+𝔻)}, first see that KHη_{ℂ+𝔻} = η_{ℂ+𝔻}, which may be checked on each component. That follows routinely since T i_{0} strictly preserves the initial object, and dually. Now, using the explicit coherence assumption of the theorem and some routine manipulation of diagrams, the commutativity extends to T (ℂ + 𝔻).

To see that HK = id_{T ℂ×T 𝔻}, we must verify that π_{0}HK = π_{0} and π_{1}HK = π_{1}, where π_{0} and π_{1} are the first and second projections from T ℂ × T 𝔻 respectively. By definition, π_{0}H and π_{1}H both lie in Kl(T), so preserve finite coproducts strictly. Restricting our attention to π_{0}, the other case being dual, it suffices to show that (π_{0}H × π_{0}H)(T i_{0} × T i_{1}) sends (X, Y) to (X, 0), where 0 is the initial object of T ℂ. Again, this amounts to two commutativities.

For the first, observe that π_{0}H = μ_{ℂ}T (η_{ℂ}, 0), so precomposing with T i_{0} yields the identity since (η_{ℂ}, 0)i_{o} = η_{ℂ} and by one of the monadic unit laws, giving the desired commutativity.

For the second, by a similar calculation, it suffices to show that the lifting of the constant V-functor 0 : 𝔻 ⟶ T ℂ to T 𝔻 is the constant V-functor at the initial object 0 of T ℂ. But by Theorem 3.7, the lifting is given by the left Kan extension of 0 : 𝔻 ⟶ T ℂ along η_{ℂ} : ℂ ⟶ T ℂ; and one can check by calculation that that is necessarily the constant at 0. .

6.5 Corollary Under the hypotheses of the Theorem, Kl(T) has finite products and finite coproducts, both given by T ℂ × T 𝔻.

Proof Observe by construction that the projections from T (ℂ × 𝔻) to each of T ℂ and T 𝔻 are in Kl(T) and the compositions used in the proof of the Theorem agree with those in Kl(T).

References

[1] M.H. Albert and G.M. Kelly, The closure of a class of colimits, J. Pure Appl. Algebra 51 (1988) 1–17.

[2] R. Blackwell, G.M. Kelly, and A.J. Power, Two-dimensional monad theory, J. Pure Appl. Algebra 59 (1989) 1–41.

[3] G. L. Cattani, A.J. Power, and G. Winskel, A categorical axiomatics for bisimulation, In Proceedings of CONCUR ’98, Lecture Notes in Computer Science 1466 (1998) 581–596.

[4] R. Gordon and A.J. Power, Gabriel Ulmer duality for categories enriched in bicategories, J. Pure Appl. Algebra (to appear).

[5] R. Gordon, A.J. Power, and Ross Street, Coherence for tricategories, Memoirs Amer. Math. Soc. 558 (1995).

[6] A. Joyal, M. Nielsen, and G. Winskel, Bisimulation from open maps, Information and Computation 127 (1996) 164–185.

[7] G.M. Kelly, Coherence conditions for lax algebras and for distributive laws, Proc. Sydney Category Theory Seminar 1972/73, Lecture Notes in Math. 420, Springer (1974) 281–375.

[8] G.M. Kelly, Basic concepts of enriched category theory, Notes London Math. Soc Lecture Series 64, Cambridge University Press (1982).

[9] G.M. Kelly and R. Street, Review of the elements of 2-categories, Proc. Sydney Category Theory Seminar 1972/73, Lecture Notes in Math. 420, Springer (1974) 75–103.

[10] A. Kock, Closed categories generated by commutative monads, J. Austral. Math. Soc. 12 (1971) 405–424.

[11] A. Kock, Monads for which structures are adjoints to units, J. Pure Appl. Algebra 104 (1995) 41–59.

[12] R. Milner, Communication and concurrency, Prentice Hall (1989).

[13] A.J. Power and E.P. Robinson, Premonoidal categories and notions of computation, Math. Structures in Computer Science 7 (1997) 453–468.

Recent BRICS Report Series Publications

RS-98-21 John Power, Gian Luca Cattani, and Glynn Winskel. A Representation Result for Free Cocompletions. September 1998. 16 pp.

RS-98-20 Søren Riis and Meera Sitharam. Uniformly Generated Submodules of Permutation Modules. September 1998. 35 pp.

RS-98-19 Søren Riis and Meera Sitharam. Generating Hard Tautologies Using Predicate Logic and the Symmetric Group. September 1998. 13 pp.

RS-98-18 Ulrich Kohlenbach. Things that can and things that can’t be done in PRA. September 1998. 24 pp.

RS-98-17 Roberto Bruni, José Meseguer, Ugo Montanari, and Vladimiro Sassone. A Comparison of Petri Net Semantics under the Collective Token Philosophy. September 1998. 20 pp. To appear in 4th Asian Computing Science Conference, ASIAN ’98 Proceedings, LNCS, 1998.

RS-98-16 Stephen Alstrup, Thore Husfeldt, and Theis Rauhe. Marked Ancestor Problems. September 1998.

RS-98-15 Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the Overhead of ML Exceptions by Selective CPS Transformation. September 1998. 31 pp. To appear in the proceedings of the 1998 ACM SIGPLAN Workshop on ML, Baltimore, Maryland, September 26, 1998.

RS-98-14 Sandeep Sen. The Hardness of Speeding-up Knapsack. August 1998. 6 pp.

RS-98-13 Olivier Danvy and Morten Rhiger. Compiling Actions by Partial Evaluation, Revisited. June 1998. 25 pp.

RS-98-12 Olivier Danvy. Functional Unparsing. May 1998. 7 pp. This report supersedes the earlier report BRICS RS-98-5. Extended version of an article to appear in Journal of Functional Programming.

RS-98-11 Gudmund Skovbjerg Frandsen, Johan P. Hansen, and Peter Bro Miltersen. Lower Bounds for Dynamic Algebraic Problems. May 1998. 30 pp.