We next give two alternative characterizations of the notion of universal arrow: the first one, in

theorem 5.1.6, is of an equational nature; the second one, in theorem 5.1.7, makes use only of the

notion of a natural isomorphism. In a sense, the definition of universal arrow given in definition

5.1.1 is in the middle way: it is based on one equation and on the existence of an isomorphism (does

the reader see any analogy with the various characterizations of products and exponents we have

given?).

5.1.6 Theorem Let G: C® D be a functor, dÎ O b D and cd Î O b C . Then there exists

uÎD[d,G(c d )] such that <u,cd > is universal from d to G iff, for every cÎOb C there is an

operation tc: D[d,G(c)]®C[cd,c] such that, for every fÎD[d,G(c)] and every hÎC[cd,c] ,

1. G(tc(f)) ° u = f

2. tc(G(h) ° u) = h

91

5. Universal Arrows and Adjunctions

Proof

(Ü) let <u,cd> be universal from d to G. For every fÎD[d,G(c)] define tc(f) as the unique

arrow f' such that G(f') ° u = f. (1) is then immediate by definition, and (2) follows by unicity.

(Þ) let tc: D[d,G(c)]®C[cd,c] be an operation which satisfies (1) and (2) above. We must

only prove that it is an isomorphism. Define then, for every hÎC[cd,c] tc-1(h) = G(h) ° u ; thus,

we have:

tc-1(tc(f)) = G(tc(f)) ° u = f by (1)

tc(tc-1(h)) = tc(G(h) ° u) = h by (2). ¨

5.1.7 Theorem. Let C, D be locally small categories, G: C®D, dÎOb D and cdÎOb C . Then

there exists uÎD[d,G(cd)] such that <u,cd> is universal from d to G iff C[cd,_] @ D[d,G_] .

Proof

(Ü) For c'ÎObC and f'ÎC[cd,c'], set tc'(f') = G(f') ° u Î D[d,Fc'] .

Then t: C[cd,_]®D[d,G_] is a natural transformation, since tc'(g ° h) = G(g ° h) ° u = G(g) ° tc(h).

That is, for gÎC[c,c'], the following diagram commutes:

Moreover, "fÎD[d,Fc'] $!f'ÎC[cd,c'] f = tc'(f') , by definition. Thus, by proposition 3.2.3, t

is a natural isomorphism.

(Þ) Let t : C[cd,_] @ D[d,G_] and set u = tcd(id). Then uÎD[d,G(cd)] . By the naturality of

t, for all c,c'ÎObC , G(g) ° tc(_) = tc'(g°_) and, hence, "fÎD[d,G(c')]

G(tc'-1(f)) ° u = G(tc'-1(f))°tcd(id)

= tc'(tc'-1(f))

=f.

That is, "fÎD[d,G(c')] $!f'(= tc'-1(f))ÎC[cd,c'] such that f = G(f')°u . ¨

Exercise: Give the dual version of theorems 5.1.6 and 5.1.7.

Recall now that a functor F : C®Set is representable if there exists a cÎC such that F @ C[c,_]

naturally.

92

5. Universal Arrows and Adjunctions

5.1.8 Corollary Let C, D be small categories, G: C®D, dÎOb D and cd ÎOb C . Then there

exists uÎD[d,G(c d )] such that <u,cd > is universal from d to G iff the functor D[d,G_]:

C®Set is representable.

5.2 From Universal Arrows toward Adjunctions

The construction of a universal arrow ud: G(cd)®d from G: C®D to d usually depends on d.

If this construction can always be performed, the function d |_ cd can be extended to a functor F:

D®C. We shall see in the next section that such G and F relate in an important way called

adjunction; for the moment we concentrate on the construction of the functor F.

In this and in the following section, we assume that we are dealing with locally small categories.

5.2.1 Theorem. Let G: C®D be a functor such that "dÎObD $<ud,cd> universal from d to

G Then there exists a functor F: D®C such that

i. F(d) = cd

ii. C[F_,_] @ D[_,G_].

(Note that C[F_,_], D [_,G_] : D op ´C® Set). Moreover, the functor F is unique, up to

isomorphism.

Proof: By assumption we know that, for all fÎD[d,d'] ,

Set then F(f) = g, that is, ud'°f = G(Ff))°ud . By the uniqueness property, G(id) = id.

Moreover, by twice the definition of F,

93

5. Universal Arrows and Adjunctions

And again by unicity of F(h ° f), one then has F(f°h) = F(f) ° F(h).

We need now to define a natural isomorphism j: D[_,G_] @ C[F_,_]. Thus we first need to check,

for a suitable j, that for all gÎD[d',d] and hÎC[c,c'] the following diagram commutes:

Equivalently,

1. "fÎD[d,Fc] j(G(h)°f°g) = h°j(f)°Fg .

Now write u (u') for ud (ud', respectively). We know then that "fÎD[d,G(c)] $!f'ÎC[F(d),c]

f = G(f') ° u . Define j(f) = f', that is, f = G(j(f))°u (compare with the definition of F ). j is

clearly a set-theoretic isomorphism; thus, we have only to prove the naturality (1).

By the definition of the functors G and F, the following diagram commutes:

94

5. Universal Arrows and Adjunctions

That is, G(j(f°g))°u' = G(j(f)°F(g) )°u' , since G is a functor. By unicity,

2. j(f ° g) = j(f) ° F(g) .

Moreover, for all fÎD[d,G(c)],

by the definition of G .

Therefore,

(G(h) ° f ° g) = h ° j(f ° g) by the diagram and unicity

= h ° j(f) ° F(g) by (2).

This proves (1), i.e. the naturality of j , and by proposition 3.2.3 the proof is completed. ¨

Dually, we have the following:

5.2.2 Theorem. Let F: D®C be a functor such that "cÎObC $<uc,dc> universal from F to

c. Then there exists a (unique) functor G: C®D such that

i. G(c) = dc

ii. C[F_,_] @ D[_,G_] .

95

5. Universal Arrows and Adjunctions

Proof The result follows by duality; anyway we explicitly reprove it, but by using a different

technique from the one used above. As the reader will see, the difference is essentially notational, but

she or he is invited to study both proofs since they are good examples of two common proof styles in

Category Theory.

Let GOb: ObC®ObD be the function defined by GOb(c) = dc, where uc: F(dc)®c is the

universal arrow. We have

"fÎC[F(d),c] $!gÎD[d,GOb(c)] f = uc ° F(g)

Now define, "gÎD[d,GOb(c)] td,c(g) = uc ° F(g) .

For every dÎOb D and cÎOb C , t d,c :D[d,G Ob (c)]® C[F(d),c] is clearly a set-theoretic

isomorphism. Note that, "hÎD[d',d],

1. td',c(g ° h) = uc ° F( g ° h ) = uc ° F(g) ° F(h) = td,c(g) ° F(h)

By taking td,c-1(f) for g in (1), we have td',c( td,c-1(f) ° h ) = f ° F(h), or equivalently,

2. td,c-1(f) ° h = td,c-1( f ° F(h) )

For simplicity, we now omit the indexes of t and t-1 .

Let GMor: MorC ® MorD be the function defined by

"kÎC[c,c'] GMor(k) = t-1(k ° uc) ÎD[GOb(c), GOb(c')]

We want to prove that G = (GOb, GMor) is a functor:

G(idc) = t-1(uc)

= t-1(uc ° idF(G(c)) )

= t-1(uc ° F(idG(c)) )

= t-1( t(idG(c) ) )

= idG(c)

and, for every f: c'®c", k: c®c',

G(f ° k) = t-1( f ° k ° uc)

= t-1(f ° uc' ° F( t-1(k ° uc) ) )

= t-1(f ° uc') ° t-1(k ° uc) by (2)

= G(f) ° G(k)

(1) proves the naturality of td,c in the component d . We have still to prove the naturality in c, that

is, "gÎD[d,GOb(c)], "kÎC[c,c']

3. td,c'(G(k) ° g ) = k ° td,c(g)

We have:

t(G(k) ° g ) = t( t-1(k ° uc) ° g )

= t( t-1(k ° uc ° F(g) ) ) by (2)

= k ° uc ° F(g)

= k ° t(g)

By taking td,c-1(f) for g in (3) we obtain td,c'(G(k) ° td,c-1(f) ) = k ° f , or equivalently:

4. G(k) ° td,c-1(f) = td,c'-1(k ° f).

96

5. Universal Arrows and Adjunctions

(2) and (4) state the naturality of t-1.

Note that since G must satisfies (4) , then

G(k) = G(k) ° id = G(k) ° t-1(uc) = t-1(k ° uc)

which shows that the adopted definition for G was actually forced. This proves the unicity of the

functor G. ¨

5.2.3 Example An interesting example of application of theorem 5.2.2 refers to Cartesian closed

categories. By the previous section, we know that if C is a CCC, then for all a,b in ObC , (p:

a´b®a, p2: a´b®b) is universal from D to (a,b), and evala,b: ba´a®b is universal from _´a

to b. Then the functions _´_: ObC´ C®ObC and _a : ObC®ObC which respectively take (a,b)

´

to a´b and b to ba, can be extended to two functors _´_: C´ C®C and _a : C®C. The explicit

´

definition is the following: for every f: a®c , g: b®d

(_´_)(f,g) = f´g = < f ° p1, g ° p2 > : a´b®c´d

(_a)(g) = L(evala,b ° g) : ba®da

For every object c in C, even the unique arrow !c: c®t may be seen as universal arrow from the

unique functor !C: C®1 to t. In this case, the extension of the function that takes 1ÎOb1 to t

to a functor T: 1®C is trivial, but it is interesting that the existence of the terminal object t in C

may be expressed by the natural isomorphism 1[!C(c)=1 ,1] @ C[c,T(1)=t].

5.2.4 Example Consider C, C t and Inc as in example 5.1.4, and assume that for each object

aÎObC there exists the lifting a°. By example 5.1.4 we know that exa: a°®a is an universal

arrow from the embedding functor Inc: Ct®Cp to a. By theorem 5.2.2 the function _°: ObC®ObC

which takes every object a to its lifting a°, may be extended to a functor _°: Cp®Ct. The explicit

definition of the functor _° on a partial arrow f: b®c is the following

(_°)(f) = f° = t(f ° exb)ÎCt[b°,c°]

where t(f°exa) is the only arrow such that exc ° t(f°exb) = f°exb.

Note that nearly all the facts about partiality and extendability we proved depend directly on

properties of natural transformations and adjunctions. That is, it was not possible to derive the

properties of the lifting of b by assuming just a set-theoretic isomorphism between Cp[a,b] and

C t[a,b°] for all a, as one may be tempted at first thought. The expressive categorical notion of

natural transformation turns out to be essential for these purposes.

5.3 Adjunctions

In this section we derive a general notion from the previous constructions and say that the functors F

and G in theorems 5.2.1 and 5.2.2 are ’adjoint“ to one another. The idea is that an adjunction

establishes a relation between two categories C and D through two functors F: D®C and G:

97

5. Universal Arrows and Adjunctions

C®D; this relation creates a bijective correspondence j of arrows in the two categories of the kind

described by the following picture:

5.3.1 Definition Let F: D®C and G: C®D be functors. Then an adjunction from D to C is

a triple <F,G,j> such that j: C[F_,_] @ D[_,G_] is a natural isomorphism. F is called left

adjoint of G, and G is called right adjoint of F.

The naturality of the isomorphism j deserves to be spelled out. For any fÎC[F(d),c], kÎC[c,c']

and hÎD[d',d], we have

1. jd,c'(k ° f) = G(k) ° jd,c(f)

2. jd',c(f °F(h) ) = jd,c(f) ° h

98

5. Universal Arrows and Adjunctions

It is equivalent to require that j -1 is natural, that is, for any gÎC[d,G(c)], kÎC[c,c'] and

hÎD[d',d],

3. j-1d,c'(G(k) ° g) = k ° j-1d,c(g)

4. j-1d',c(g ° h) = j-1d,c(g) ° F(h) .

Examples

1. Let D, C be partial order categories, and (ObD ,£D ), (ObC ,£C ) the associated p.o.sets. An

adjunction from D to C is a pair of monotone functions f: ObD®ObC, g: ObC®ObD such that,

for every dÎObD , cÎObC,

f(d) £C c Û d £D g(d) .

Consider for example the partial order Z of relative numbers, and the partial order R of real

numbers. Let I: Z®R be the obvious inclusion, and «_»: R®Z be the function that takes a real

number r to its lower integer part «r». Then I and «_» define an adjunction from Z to R , since

1. I(z) £R r Û z £Z «r»

Conversely let ©_ù: R®Z be the function that takes a real number r to its upper integer part ©rù.

Then ©_ù and I define an adjunction from R to Z, since

2. ©rù £Z z Û r £R I(z)

Note that «_» and ©_ù are respectively the right and left adjoint to the same functor I. Note,

moreover, that «_» and ©_ù are the unique functions that respectively satisfy conditions (1) and (2)

for all r and z.

Another interesting example of adjunctions between partial orders as categories is the following:

consider the p.o.set of positive integers N. For every natural number n , let _ .n : N®N be the

function that takes a natural numbers m to the product m.n . The right adjoint to _ .n is the the

function div(_,n): N®N that takes q to (the lower integer part of) q divides n .

Indeed, for every m, q, m.n £ q Û m £ div(q,n)

Analogously the ’minus“ operation is right adjoint to ’plus.“

2. This further example uses familiar notions and applies the categorical understanding of a

fundamental technique in (universal) algebra. Given a category C of structures and a category D of

slightly more general ones, the right adjoint of the forgetful functor from C to D defines the ’free

structures“ over the objects in the category D. This technique is widely explained in several places

(see references), so that we just hint at it here.

The category Graph was defined in the example 4.1.5. Recall now that a graph G is given by:

- a set V of objects (nodes)

- a set T of arrows (edges)

- a function ¶1: T®O which assigns to each arrow f its range ¶1(f)

- a function ¶2: T®O which assigns to each arrow f its target ¶2(f) .

99

5. Universal Arrows and Adjunctions

Morphisms of graphs G, G' are pairs <f,g>, where f: T®T' and g: V®V' have the properties in

the example 4.1.5. We already mentioned (see the exercise following that example) that each small

category C may be regarded as a graph G = U(C), just forgetting identities and composition. Of

course, U takes objects to nodes and arrows to edges. Moreover, every functor F: C®D gives a

morphisms H = U(F): U(C)®U(D) between the associated graphs; the reader should have checked

that U: Cat ®Graph is actually a (forgetful) functor. Conversely every graph G generates a

category C = C(G) with the same objects of G, and, for arrows, the finite strings (f1,...,fn) of

composable arrows of G, i.e., of arrows in the due types (the empty strings are the identities in

C(G)). Composition in C(G) is just string concatenation, that is,

(f1 , . . . ,fn ) ° (g 1 , . . . ,gm ) = (f1 , . . . ,fn ,g1 , . . . ,gm ) .

Note that (f1,...,fn) = f1 ° . . . ° fn. The category C(G) is called the free category generated by

G.

This construction may be extended to morphisms of graphs: if H: G ® G' then C(H):

C(G)®C(G') is the functor that coincides with H on objects, and that is defined on morphisms by:

C(H)(f 1 ,...,fn ) = (H(f1 ),... H(fn )).

It is easy to prove that C is a functor from Grph to Cat. Actually, we have an adjoint situation, since

there is an isomorphism Q : Cat[C(G), C] @ Grph[G, U(C)] which is natural in G and C. The

isomorphism Q takes every functor F: C(G)®C to the morphism Q(F): G®C, which is the

’restriction“ of F on G. For the nature of C(G), every functor F: C(G)®C is uniquely determined

by its behavior on the arrows of G, indeed if (f1,. . . ,fn) is an arrow in C(G), by definition of a

functor, F((f1,. . . ,fn)) = F( f1 ° . . . ° fn) = F(f1) ° . . . ° F(fn). This proves that Q is injective. But

Q is also surjective, since if H: G®U(C) , we can define a functor F: C(G)®C by F((f1,. . . fn))

= H(f1) ° ... ° H(fn), and clearly Q(F) = H. We leave it to the reader to prove the naturality of the

isomorphism.

Exercise In section 4.3 we turned each Petri net N into a monoidal category C„(N) . Describe

C„(N) as a freely generated category.

Exercise Let C and D be discrete categories (i.e., the only morphisms of the categories are

identities). Prove that <G,F,t>: C ® D is an adjunction if and only if G and F define an

isomorphism between C and D.

In the previous section, we have actually shown how to construct an adjunction when one can

uniformly obtain a universal arrow <ud,cd> from each object d . Now we show how to obtain

universal arrows out of an adjunction, and put together the two results.

5.3.2 Theorem. If < F: D®C , G: C®D ,j > is an adjunction from D to C, then

1. < u =j(idF(d)) : d®G(F(d)) , F(d)> is universal from d to G

100

5. Universal Arrows and Adjunctions

u is called unit of the adjunction

2. <u'=j-1(idG(c)): F(G(c))®c ,G(c) > is universal from F to c

u' is called counit of the adjunction.

Conversely, if G: C®D is a functor and (1) holds (or F: D®C is a functor and (2) holds), then

<F,G,j > is an adjunction from D to C.

Proof. (1) is given by theorem 5.1.6 (Ü) and the definition of G. Note that (2) follows dually. The

converse is stated in theorems 5.2.1 and 5.2.2. ¨

Thus, if < F, G ,j > is an adjunction, then the functor F of theorem 5.2.1 is the left adjoint of G

and, conversely, G in theorem 5.2.2 is the right adjoint of F. In view of the expressive power of the

notion of adjunction, we can now state in one line some of the concepts we introduced in the

previous chapters.

5.3.3 Corollary Let C be a category. Then

i. C has a terminal object iff the unique functor !C: C ® 1 has a right adjoint;

ii. C has finite products iff the diagonal functor has a right adjoint;

iii. C is a CCC iff it is cartesian (i.e., !C: C®1 and D : C®C´C have right adjoints) and, for

each aÎObC, the functor _´a : C®C has a right adjoint.

Proof. Immediate by theorem 5.2.2 and the considerations in example 5.2.3. ¨

5.3.4 Corollary Let C be a category of partial morphisms. The lifting functor _° : C®Ct is the

right adjoint of the embedding functor Inc: Ct®C.

Proof Immediate by 5.2.2 and the considerations in example 5.2.4. ¨

As the reader probably expects, it is also possible to give a fully equational characterization of

adjunctions.

5.3.5 Theorem An adjunction <F, G,t> : C®D is fully determined by the following data:

- the functor G: D®C

- a function f: ObC®ObD such that, for every object c of C, f(c) = F(c)

- for every object c of C, an arrow unitcÎC[c, G(f(c))]

- for every object c of C and d of D, a function tc,d-1: C[c,G(d)]®D[f(c),d]

such that, for every hÎC[c,G(d)] and kÎD[f(c),d],

1. G(tc,d-1(h)) ° unitc = h ;

2. tc,d-1(G(k) ° unitc ) = k .

101

5. Universal Arrows and Adjunctions

Proof The theorem is an immediate consequence of theorems 5.3.2 and 5.1.6. A direct proof is not

difficult, and its study is a good exercise for the reader since it summarizes many of the previous

results. Here it is:

The function f may be extended to a functor F by setting, for kÎC[c,c'], F(k) = tc',d-1(unitc' ° k).

Note that

F(idc) = tc,f(c)-1(unitc)

= tc,f(c)-1(idG(f(c)) ° unitc)

= tc,f(c)-1(G(idf(c)) ° unitc)

= idf(c) . by (2)

and moreover, omitting the indexes for notational convenience,

F(h ° k) = t-1(unit ° h ° k )

= t-1( G(t-1(unit ° h)) ° unit ° k ) by (1)

= t-1( G(t-1(unit ° h)) ° G(t-1(unit ° k)) ° unit ) by (1)

= t-1( G( t-1(unit ° h) ° t-1(unit ° k) ) ° unit )

= t-1(unit ° h) ° t-1(unit ° k) by (2)

= F(h) ° F(k) .

Let now, for every object c of C and d of D, tc,d: D[f(c),d]®C[c,G(d)] be the function defined by

tc,d(k) = G(k) ° unitc . Equations (1) and (2) express exactly the fact that tc,d and tc,d-1 define an

isomorphism. We have still to prove their naturality. Let kÎD[d,d'], hÎC[c,G(d)], h'ÎC[c',c],

and k'ÎD[f(c),d] ; then

nat-1. t-1(G(k) ° h ) = t-1(G(k) ° G(t-1(h)) ° unitc )

= t-1(G(k ° t-1(h)) ° unitc )

= k ° t-1(h) ;

t-1(h ° k ) = t-1(G(t-1(h) ) ° unit ° k )

nat-2. by (1)

= t-1(h) ° t-1(unit ° k ) by (nat-1)

= t-1(h) ° F(k) ;

t(k' ° F(h') ) = t (t-1(t(k')) ° F(k) )

nat-3.

= t (t-1(t(k') ° h') by (nat-2)

= t(k') ° h' ;

nat-4. t(k ° k' ) = G( k ° k') ° unit

= G( k ) ° G(k') ° unit

= G( k ) ° t(k'). ¨

5.3.6 Proposition Let <F,G,t>: C ® D be an adjunction. Then there exist two natural

transformations h : IdC®GF and e: FG®IdD such that, for every c in C and d in D, h(c) and

e(d) are respectively the unit and counit of the adjunction.

Proof: exercise. ¨

102

5. Universal Arrows and Adjunctions

In other words, one may construct the unit and counit ’uniformely“ and naturally. Observe also

that, if h : IdC®GF and e: FG®IdD are the natural transformations in proposition 5.3.6, then the

following diagram commutes:

The previous diagrams fully characterize an adjunction: as a matter of fact many authors prefer to

define an adjunction between two categories C and D as a quadruple (F, G, h , e) where F:

C®D and G: D®C are functors, and h : IdC®GF , e: FG®IdD are natural transformations

such that

(Ge) ° (hG) = idG ;

(eF) ° (Fh) = idF .

We leave it as an exercise for the reader to prove the equivalence of this notion with the one we have

adopted. We shall use the definition of adjunction as a quadruple in the next section, since it

simplifies the investigation of the relation between adjunctions and monads.

Exercises

1. An adjointness (F, G, h , e) from C to D is an adjoint equivalence if and only if h and e

are natural isomorphisms. Prove that given two equivalent categories C and D (see section 3.2) it

is always possible to define an adjoint equivalence between them.

2. Given an adjointness (F, G, h, e) from C to D, prove the equivalence of the following

statements:

i. hGF = GFh;

ii. hG is an isomorphism;

iii. eFG = FGe;

iv. eF is an isomorphism.

5.3.7 Example In section 3.4 we defined the CCCs of limit and filter spaces, L-spaces and FIL

respectively, which generalize topological spaces, Top. The functorial ’embeddings“ mentioned in

that example are actually adjunctions. Recall that H : Top ® FIL is given by

H((X,top)) = (X,F) where F(x) = {F | F is a filter and "0Îtop (xÎ0 Þ 0ÎF)}.

H(f) = f by the definition of continuity. H has a left adjoint T : FIL ® Top defined by

T((X, F)) = (X,top) where 0Îtop iff "xÎ0 "FÎF(x) 0ÎF .

Also in this case, filter continuity corresponds to topological continuity, i.e., T(f) = f . The reader

may easily define the natural isomorphism t .

103

5. Universal Arrows and Adjunctions

In general, limits are not unique in filter spaces. A stronger notion of convergence, to be used for

computability (see the final remark in section 8.4), may be given as follows. For (X,F) in FIL

consider (X,top) = T((X, F)) and define

F¯sx iff FÎF(x) and "0ÎFÇtop xÎ0 .

(s-conv.)

Then top is T0 iff s-convergent filters have a unique limit.

Let N = (w, F) be the natural numbers with the filter structure induced by the discrete topology

and M = NN. With some work (see references) one can show that MM is not topological, i.e. for

no (X,top) one has MM = H((X,top)). The idea is that each topological filter space has a least filter

for each F(x), the neighborhood filter at x; deduce from this that the associated adjointness

(T,H,h,e) to (T,H,t) is not an adjoint equivalence (which one of h and e is not a natural

isomorphism?).

Exercises (based on the previous example and exercises)

1. Consider the full subcategory of FIL given by the filter spaces (X,F) such that, for each x, there

is a least FÎF(x). Give an adjoint equivalence between Top and this category.

2. Check that the functors between L-spaces and FIL defined in the exercise in section 3.4.2 yield

an adjunction, which is not an adjoint equivalence.

3. Give directly an adjunction between Top and FIL, and compare the definition with the adjunction

obtained by composition of functors. (Hint for the direct construction: given an L-space (X,¯),

define (X,top) by 0Îtop iff "xÎ0, "{xi}¯x, {xi}Í 0 eventually. Conversely, for (X, top)

topological space, define (X,¯) by {xi}¯x iff "0Îtop (xÎ0 Þ {xi}Í 0 eventually).

5.4 Adjunctions and Monads

In this section we study the relation between two seemingly distant concepts as adjunction and

monad. As a matter of fact, every adjunction immediately defines a monad, and conversely every

monad can be thought of as generated by an adjunction, called a resolution for the monad (see

5.4.2 below). Resolutions for a given monad can be build up in a category by introducing a natural

notion of morphism between them; it then happens that the Eilenberg-Moore and the Kleisli

Categories associated with the monad (see definitions 4.2.3 and 4.2.4) are respectively the terminal

and initial object of the category.

The presentation is rather technical; at first reading, the reader may just look at the first theorem,

which will be applied in the next section.

5.4.1 Proposition Let (F, G, h , e) be an adjunction from C to D; then (T = GF, h , m = GeF)

is a monad on C and (T = FG, d = GhF, e) is a comonad.

104

5. Universal Arrows and Adjunctions

Proof Note first that GF, h, and GeF have the correct types, i.e., T = GF: C®C, h: IdC ®GF,

and m = GeF: GFGF®GF. We must prove the unity and associative laws for the monad.

As for the unity laws we have

m ° Th = GeF ° GFh = G(eF ° Fh) = G(idF) = idGF

m ° hT = GeF ° hGF = (Ge ° hG)F = idG(F) = idGF

For the associative law, note first that

e ° eFG = e ° FGe .

Indeed, for any dÎObD , and letting f = ed: FG(d)®d,

ed ° eFG(d) = f ° eFG(d)

= ed ° FG(f) by naturality of e

= ed ° FG(ed)

Then one has the following:

m ° mT = GeF ° GeFGF

= G(e ° eFG)(F)

= G(e ° FGe)(F)

= GeF ° GFGeF

= m ° Tm .

The rest is an exercise in duality. ¨

5.4.2 Definition Let (T, h , m) be a monad over a category C. A resolution for (T, h , m) is a

category D and an adjunction (F, G, h , e) from C to D such that T = GF and m = GeF. A

morphism between two resolutions (F, G, h , e): C®D and (F', G', h , e'): C®D' (for the

same monad) is a functor H: D®D' such that F' = H ° F, G = G' ° H , and He = e'H.

It is easily proved that resolutions with the associated morphisms form a category. Now we are going

to prove that the Eilenberg-Moore and Kleisli categories associated with a monad (T, h , m) both give

rise to resolutions. In particular, they are respectively the terminal and initial objects in the category of

all resolutions for that monad.

5.4.3 Proposition Let (T, h , m) be a monad over a category C , and let CT be the Eilenberg-

Moore category associated with the monad. Then there exists a resolution for (T, h , m) which is an

adjunction from CT to C.

Proof Let UT: C T®C be the forgetful functor that takes every algebra (c,a) to c, and every

morphism of algebras h to the same h regarded as a morphism in C. Let FT : C®C T be the

functor which takes every object c to its free algebra (T(c),mc), and every morhism f: c®c' to

FT(f) = T(f). Let eT: FTUT®idCT be the natural transformation defined by eT(c,a) = a (note

that a: T(c)=FTUT(c,a)®c). We want to prove that (FT, UT, h , eT) is a resolution for (T, h , m).

105

5. Universal Arrows and Adjunctions

Obviously UT ° FT = T . UT eT FT = m, since for any object c one has

(UT eT FT)(c) = UT(eT FT(c))

= UT(eT(T(c), mc)) by def. of FT

= UT(mc) by def. of eT

by def. of UT

= mc

We still haveto prove that (FT, UT, h , eT) is an adjunction from CT to C, that is,

(UTeT) ° (hUT) = idUT

(eTFT) ° (FTh) = idFT

One has, for every T-algebra (c,a),

(UTeT ° hUT) (c,a) = UT(eT(c,a) ) ° hUT(c,a)

by def. of eT and UT

= a ° hc

= idc by def. of T-algebra

And for every cÎObC :

(eTFT ° FTh) (c) = eTFT(c) ° FT(hc)

by def. of eT and FT

= mc ° T(hc)

= idT(c) by the unity law of the monad.¨

We say that the resolution (FT, UT, h , eT) from C to the Eilenberg-Moore category CT, and given

by proposition 5.4.3, is associated with CT .

5.4.4 Proposition Let (T, h , m) be a monad over a category C .Then the resolution (FT, UT,

h, eT ): C®C T , associated with the Eilenberg-Moore Category C T , is a terminal object in the

category of all the resolution for the monad (T, h , m).

Proof Let (F, G, h , e): C®D be another resolution for (T, h , m). We must prove that there

exists a unique arrow from (F, G, h , e) to (FT, UT, h , eT). Remember (cf. definition 5.4.2) that

such an arrow is a functor H: D®CT , such that FT = H ° F, G = UT ° H , and He = eTH.

Define, for any object d, and any morphism f of D,

H(d) = (G(d), G(e(d)) )

H(f) = G(f).

Then one has, for any cÎObC, any hÎMorC,

H(F(c)) = (G(F(c)), G(e(F(c))) ) = (T(c), mc) = FT(c)

H(F(h)) = G(F(h)) = T(h) = FT(h)

that proves the equality H ° F = FT.

Moreover, for any dÎObD, and any fÎMorD,

UT(H(d)) = UT(G(d), G(e(d)) ) = G(d)

UT(H(f)) = UT(G(f)) = G(f), as UT is the identity on morphisms.

That proves the equality G = UT ° H .

106

5. Universal Arrows and Adjunctions

Finally, for any dÎObD,

eTH(d) = eT(G(d), G(e(d)) ) = G(e(d)) = H(e(d))

that proves the equality He = eTH.

We have still to prove that H is the unique morphism from (F, G, h , e) to (FT, UT, h , eT).

Let H' be another morphism; then, for any fÎMorD,

H'(f) = UT(H'(f) = G(f) = UT(H(f) = H(f)

and, for any dÎMorD,

H'(d) = ( UT(H'(d), eTH'(d)) by def. of UT and eT

= ( G(d), H'(eT(d)) ) as G = UT ° H'

= ( UT(H(d), H(eT(d)) ) as H'(f) = H(f)

= ( UT(H'(d), eTH(d))

= H(d).

This completes the proof. ¨

The unique functor to (FT, UT, h , eT) in the category of all resolutions for a given monad (T, h ,

m) is called comparison functor and it is usually denoted by KT.

The category of resolutions of a monad has also an initial object, which is based on the Kleisli

category associated with the monad.

5.4.5 Proposition Let (T, h , m) be a monad over a category C, and let C T be the Kleisli

category associated with the monad. Then there exists a resolution for (T, h, m) that is an adjunction

from CT to C.

Proof: Let UT: CT®C be the functor defined by the following:

for any object c of CT (i.e., of C ), and any morphism hÎCT[c,c'] (and thus hÎC[c,T(c')])

UT(c) = T(c);

UT(h) = mc' ° T(h).

Let FT: C®CT be functor defined by the following:

for any object c of C, and any morphism fÎC[c,c']

FT(c) = c;

FT(f) = hc' ° f ( = T(f) ° hc ).

Let eT: FTUT®id be the natural transformation defined by the following:

for any object c of CT

eT(c) = idT(c) (in C).

We want to prove that (FT, UT, h , eT): C®CT is a resolution for (T, h , m).

Obviously, UT ° FT = T .

Moreover, UT eT FT = m, since for any object c one has

(UT eT FT)(c) = UT(eT (c) ) by def. of FT

107

5. Universal Arrows and Adjunctions

= UT(idT(c)) by def. of eT

= mc. by def. of UT

We have still to prove that (FT, UT, h , eT) is an adjunction from C to CT, that is,

(UTeT) ° (hUT) = id: UT®UT

(eTFT) ° (FTh) = id: FT®FT

One has, for every object c of CT:

(UTeT ° hUT) (c) = UT(idT(c)) ° hT(c) by def. of eT and UT

= mc ° T(idT(c)) ° hT(c) by def. UT on morphisms

= mc ° hT(c) as T is a functor

= idc. by the unity law of the monad

And, for every cÎObC,

(eTFT ° FTh) (c) = eT(c) ° (hT(c) ° hc) by def. of FT

= idT(c) ° (hT(c) ° hc) by def. of eT

= mC ° T(idT(c)) ° hT(c) ° hc by def. of composition ° in CT

= mC ° hT(c) ° hc

= hc by the unity law of the monad

= idc by def. of the identity in CT. ¨

5.4.6 Proposition Let (T, h, m) be a monad over a category C. The resolution (FT, UT, h , eT):

C®CT associated with the Kleisli Category CT is an initial object in the category of resolutions for

the monad (T, h , m).

Proof Let (F, G, h , e): C®D be another resolution for (T, h , m). We must prove that there

exists a unique arrow from (FT, UT, h , eT) to (F, G, h , e), that is a unique functor K: CT®D,

such that F = K ° FT, UT = G ° K , and KeT = eK.

Define, for any object c of CT, and any morphism fÎCT[c,c'],

K(c) = F(c);

K(f) = eF(c') ° F(f).

where c and f are regarded as object and morphism of C.

Then one has, for any cÎObC, any hÎC[c,c'],

K(FT(c)) = K(c) = F(c)

K(FT(h)) = K(hc' ° h) by def. of FT

= eF(c') ° F(hc' ° h) by def. of K

= eF(c') ° F(hc') ° F(h) as F is a functor

= F(h) as (F, G, h , e) is an adjunction

This proves the equality K ° FT = F .

Moreover, for any object c of CT, and any morphism fÎCT[c,c'],

G(K(c)) = G(F(c)) = T(c) = UT(c)

108

5. Universal Arrows and Adjunctions

G(K(f)) = G(eF(c') ° F(f)) by def. of K

= G(eF(c')) ° G(F(f)) as G is a functor

= mc' ° T(f) as (F, G, h , e) is a resolution

= UT(f) by def. of UT

that proves the equality UT = G ° K .

Finally, for any dÎObD,

K(eT(c)) = K(idT(c)) by def. of eT

= eF(c') ° F(idT(c)) by def. of K

as F is a functor

= eF(c')

by def. of K

= eK(c')

that proves the equality KeT = eK.

We have still to prove that K is the unique morphism from (FT, UT, h , eT) to (F, G, h , e).

Let K': CT®D be another morphism; then, for every object c of CT,

K'(c) = K'(FT(c)) by def. of FT

= F(c) as K' ° FT = F

= K(FT(c)) as K ° FT = F

= K(c) by def. of FT

and, for any fÎCT[c,c'],

K'(f) = K'(idc' ° f )

= K'(mc' ° hT(c') ° f) by the unitary law of the monad

= K'(mc' ° T(idT(c')) ° hT(c') ° f)

= K'(idT(c') ° (hT(c') ° f) ) by def. of composition ° in CT

= K'(idT(c')) ° K'(hT(c') ° f) ) as K' is a functor

= K'(eT(c')) ° K'(FT(f)) ) by def. of eT and FT

= eK'(c') ° F(f) as K'eT=eK' and F=(K'°FT)

= eF(c') ° F(f) as K'(c) = K(c) = F(c)

= K(f). by def. of K

This completes the proof. ¨

For consistency with the terminology adopted for the comparison functor, we shall denote by KT

the unique arrow from the initial object (FT, UT, h , eT) in the category of all resolutions for a

monad (T, h , m).

Consider now the comparison functor from the initial to the terminal object. Of course, it must be

KT = KT; let us check this explicitly.

For any object c in CT,

KT(c) = (UT(c), UT(eT(c)) ) by def. of KT

= (T(c), mc ° T(idT(c)) ) by def. of UT and eT

109

5. Universal Arrows and Adjunctions

= (T(c), mc)

= FT(c) by def. of FT

= KT(c). by def. of KT

And for any morphism fÎCT[c,c'],

KT(f) = UT(f) by def. of KT

= mc' ° T(f) by def. of UT

= eT(T(c'), m(c')) ° T(f) by def. of eT

= eTFT(c') ° FT(f) by def. of FT

= KT(f) . by def. of KT

Exercises

1. Prove that the comparison functor KT = KT : CT®CT is full and faithful.

2. Prove that the Kleisli Category is isomorphic to the full subcategory of CT consisting of all free

algebras.

5.5 More on Linear Logic

In this section, we complete an introductory presentation of linear logic and its categorical meaning,

initiated in section 4.4. As already mentioned, the leading idea of this system refers to the ’linear“ use

of ’resources“ or logical assumptions. From assuming A, one derives less than from assuming A, A,

i.e., twice A . The logic-oriented reader, mostly used to classical or intuitionistic reasoning, may find

this a little strange. Probably, though, this habit hides a nonconstructive view which may result in a

limitation of our understanding of effective processes. Indeed, the alternative approach proposed by

linear logic, which enriches and complements the traditional ones, seems to suggest formalizations

and understanding of processes, such as parallel ones, which have so far escaped to a description by

usual tools (see the examples on monoids and Petri nets in section 4.3 and the references, for recent

developments of this idea).

As the reader may recall, the changes in the structural rules motivate a duplication of the

connectives (see section 4.4). However, there is a way to recover the usual possibility, in classical as

well as in intuitionistic logic, of an iterated use of assumptions. The idea is to introduce a connective

’!“ (read ’of course“), which allows to assume as (finitely) many times one wishes a given

assumption. This connective has a categorical meaning, which may be given in the terms of

adjunctions and monads, following the previous section. The interesting categorical significance of

this relation to classical and intuitionistic logic, as well as the categorical understanding we described

in section 4.4, via structures such as the categories Stab and Lin, is probably what makes the

difference between linear logic and previous formal experiments with the structural rules in other

areas of logic.

110

5. Universal Arrows and Adjunctions

The rules below are meant to extend the system in section 4.4. Observe that the structural rules of

weakening and contractions apply with respect to the connective !. This is exactly what it is

introduced for: it is meant to allow copies of assumptions and observe that they lead to the same

consequences. This is expressed also by the rules (!,r) and (!,l) . Following Girard•s work, we

explicitly introduce the dual ’?“ (read ’why not“), of the connective ! . Its operational behaviour is

described by the rules, which mimic those for ! on the other side of the entailment (cf. the duality of

(-)^ in 4.4.3), and by the equivalence of !A and (?(A^))^, proved below.

The exponential fragment of Linear Logic is as follows:

5.5.1 exponential unary connectives: ! (of course), ? (why not)

5.5.2 exponential rules

G |- D G |- D

________ ________

(weak-l) (weak-r)

G,!A |- D G |- ?A,D

G,!A,!A |- D G |- ?A,?A,D

___________ ___________

(contr-l) (contr-r)

G,!A |- D G |- ?A,D

G, A |- D !G |- A,?D

________ ________

(!,l) (!,r)

G,!A |- D !G |- !A,?D

!G, A |- ?D G |- A,D

_________ _______

(?,l) (?,r)

!G,?A |- ?D G |- ?A,D

The duality between ! and ? is easily obtained by the following deductions:

A |- A A |- A

_______ _______

(!,l) (^,r)

|- A^, A

!A |- A

_______ _______

(^,l) (?,r)

!A, A^ |- |- ?A^, A

_________ ________

(?,l ) (!,r)

!A, ?A^ |- |- !A,?A^

__________ __________

(^,r) (^,l)

!A |- (?A^)^ (?A^)^ |- !A

111

5. Universal Arrows and Adjunctions

Exercise Prove that !(AÇB) |- !A „!B and !A „!B |-!(AÇB).

5.5.3 Remark The connective ’!“ is exactly what is needed to recover the intuitionistic calculus: it

is possible to prove that there is an embedding of intuitionistic (and classical) logic into linear logic.

The embedding maps every intuitionistic formula A to a linear formula A in the following way:

A=A if A is an atomic formula

A™B = A Ç B

A•ÚB = !A … !B

A•ÞB = ! A __o B

( ! is supposed to bind tighter than __o and È ).

The absurdum F of intuitionistic is translated into 0, the identity for … . Thus ˜A = !A__o0.

In other words, the iterated use of the premises, in a linear implication, gives exactly the intuitionistic

implication. Then, if, G |-i A, in intuitionistic Logic, then ! G |- A in Linear Logic.

Our aim now is to give categorical meaning to the connective !, of course. By duality, in linear

categories (see definition 4.4.4), we also obtain an interpretation for ?, why not.

We have already remarked that a resource such as !A can be duplicated and erased, and in a

sense these properties characterize the meaning of the connective ! . Thus, at the sematic level, we

expect to have two morphisms d: !A®!A „!A , and e: !A®1 where 1 is the identity of the

monoidal category. (Commutative) comonoids in 4.3.4 seem the right structure for this, as they are

characterized by a sort of diagonal map, such as d, and a map e which dualizes the map h in

definitions 4.2.1 and 4.3.3.

We start then with a monoidal category C. By definition, C must satisfy certain natural

isomorphisms, given in 4.3.1, which we rebaptize in this section, for convenience, with more

suggestive names

1. assoc: X „ ( Y „ Z ) @ ( X „ Y ) „ Z

2. ins-l: X @ 1 „ X

3. exch: X „ Y @ Y „ X

Let also:

4. ins-r = exch ° ins-l : X @ X „ 1

As mentioned in section 4.4, the connective of linear implication __o is interpreted by the right

adjoint to the tensor product „ , when C is a monoidal closed category, as defined in section 4.3.

Recall that the category CoMonC of commutative comonoids over a monoidal category C, has

as objects, for c in C, (c, d: c®c„c, e: c®1), and morphisms f: (c, d, e)®(c', d', e'), for each

arrow f: c®c' in C , such that

d' ° f = (f„f) ° d : c®c'„c',

e' ° f = e: c®1 .

112

5. Universal Arrows and Adjunctions

Given a commutative comonoid (c, d: c®c„c, e: c®1) observe that the following equations hold:

(e„idc) ° d = ins-l : c®1„c

exch ° d = d : c®c„c

assoc ° (idc„d) ° d = (d„idc) ° d : c®(c„c)„c .

Exercise As pointed out after definition 4.3.6, if C is Cartesian, in the sense that „ is actually a

cartesian product Ç and the isomorphisms are the canonical ones, then all the maps and

isomorphisms above can be constructed for each object in C (in particular, recall that d and e are

canonically given; namely, d = <id,id> : c®cÇc is the diagonal and e: c®t is the unique map to

the terminal object). Prove that, if C is Cartesian, then C is actually isomorphic to CoMonC. Does

the converse hold?

5.5.4 Definition A ! - model is a linear category C and a comonad (!,D,E) such that there

exist natural isomorphisms

I : !(AÇ B) @ !(A)„!(B)

J : !t @ 1

where t and 1 are the identities for Ç and „ , the Cartesian and tensor products in C.

Indeed, by definition, in a linear category one has both a monoidal and a Cartesian structure. The

relation established by the natural isomorphisms gives the monoids we need.

5.5.5 Lemma Let <C,(!,D,E)> be an !-model. Then, for each object c in C, there exist maps

d':!c®!c„!c and e': !c®1, such that (!c, d', e') is a comonoid.

Proof. Just set d'= I»!d : !c ®!(cÇc) ®!c„!c

e'= I»!e : !c ® !t ®1

where d = <id,id> : c®cÇc and e: c®t are the monoidal maps in the remark above, w.r.t. the

Cartesian product Ç. The rest is easy.¨

Thus, the comonad (!: C®C, D: !®!° !, E: !®Id C ) associated with a !-model gives all the

ingredients for the interpretation of the connective !, of course. In view of the above lemma, we can

define the functor !: C ® CoMonC by

!(c) = (!c, d':!c ®!c„!c, e': !c ®1) .

This gives the required monoids, while the natural transformations D and E uniformly yield maps

Dc : !c ®!°!c and Ec : !c ®c, which are needed to interpret the rules in (!,r) and (!,l).

We already mentioned in section 4.4 that the idea of the interpretation relies on viewing

entailments as morphisms. In short, observe that, with an informal blend of syntax and semantics,

113

5. Universal Arrows and Adjunctions

the rules are interpreted by the fact that

(weakenings) each morphism f: 1®D

gives a morphism f»ea: !a®D

(contractions) each morphism f: !a„!a®D

gives a morphism f»da: !a®D

(!,l) each morphism f: a®D

gives a morphism f»Ea: !a®D

(!,r) each morphism f: !c®a

gives a morphism !f»Dc: !c®!a .

As for the rules which contain ?, their meaning is easily derivable by duality. The idea is to define a

functor ? : C®C by

?=*»!»*

that is ?A = (!A*)*. Then the following theorem gives the categorical meaning of the modality ?,

why not.

5.5.6 Theorem Let <C,(!,D,E)> be an !-model. Then there exist a monad (?, D': ?» ?®?, E':

Id®?) and natural isomorphisms

I': ?(A…B) @ ?(A)È?(B)

J': ?0 @ ^ ,

where 0 and ^ are the identities for … and È, the duals of the Cartesian and tensor products in

C.

Proof. Set ? = * » ! » * : C ® C and, for each object A, D'A = (DA*)* and E'A = (EA*)*. As

D: !®!°!, one has

DA*: !A*®!°!A*

(DA*)*: (!°!A*)*®(!A*)* by def.of (-)*

(DA*)*: (!°*°*°!A*)*®(!A*)* by Id @ (-)**

D'A: ?°?A®?A

Each of these steps is an isomorphism, uniform in A, and gives a natural transformation D': ?»?®?.

Similarly, from E: !®Id C one has EA* : !A*®A* and, thus, E'A = (EA* )*: A®?A. The

properties required for a monad follow by duality.

As for the natural isomorphisms, compute

?(A…B) = * » ! » *(A…B)

= * » !(A*ÇB*) by theorem 4.4.6

114

5. Universal Arrows and Adjunctions

@ (!(A*)„!(B*))* by def. of !-model

= ?AÈ?B by theorem 4.4.6.

Finally, ?0 = * » ! » *0 @ * » ! t @ 1* @ ^ , by definition and theorem 4.4.6. ¨

Exercise Endow a structure of monoid over each object in a monoidal category whose tensor

product is actually a Cartesian coproduct. Then give the details of the interpretation of the rules for ?.

Next we find, within any categorical model of linear logic, an interpretation for the intuitionistic

connectives Ç and Þ, by using the comonad construction in the !-model. Namely, given an !-

model C, one may interpret intuitionistic ’and“ and ’implication“ by Cartesian product and

exponential in a suitable category derived from C. As the purpose of the iterator ! was to take us

back to intuitionistic logic, we use its categorical meaning to construct this new category.

As a matter of fact, in the remark 5.5.3, we hinted how to derive intuitionistic connectives from

linear ones, once the connective ! is available. The following result gives the categorical counterpart

of that construction.

Observe that in general, given a comonad (T, d, e) over C, the co-Kleisli category K is the

category whose objects are those of C, and the set K[A,B] of morphisms from A to B in K is

C[T(A),B]. The identity in K[A,A] is eA: T(A)®A. The composition of fÎK[A,B] and gÎK[B,C]

in K is

gof = g ° T(f) ° dA : T(A)®T2(A)®T(B)®C

o

(see definition 4.2.4 where Kleisli categories over monads were defined).

5.5.7 Theorem If C be an !-model. Then the co-Kleisli category K associated with the comonad

(!,D,E) is Cartesian closed.

Proof (hint) The exponent of two objects B and C is (!B__oC). We then have the following

chain of isomorphisms:

K[AÇB, C] @ C[!(AÇB), C] by definition of K

@ C[!(A)„!(B), C] as !(AÇB) @ !(A)„!(B)

@ C[!(A), !B__oC ] as C is monoidal closed

@ K[A, !B__oC ] by definition of K. ¨

Example In section 2.4.2 we defined the category Stab of coherent domains and stable functions.

In that section (see exercise 4) the subcategory Lin, with linear maps, was also introduced and, later

(see section 4.4), it was given as an example of linear category. We also defined a function ! on

coherent domains as follows: if X is a coherent domain, then !X is the coherent domain defined by:

i. |!X| = {a / aÎX, a finite};

ii. a-b [mod !X] iff aÈbÎX.

115

5. Universal Arrows and Adjunctions

We need now to extend it to a functor ! : Stab®Lin. Recall that a linear map g: Z®Z' is uniquely

determined by its behavior on the points of the coherent domain Z, i.e., on the elements of |Z|.

Moreover, any stable map may be equivalently described in terms of its trace. Set then, for each

stable map f : X®Y,

Tr(!f) = {({a}, b) | bÎY, b finite, aÎX, a finite and least such b Í f(a) }.

Next, we define an adjunction between ! and the obvious inclusion functor Inc from Lin into

Stab. This is given by a natural isomorphism

(iso) j : Lin[!A,B] @ Stab[A,B]

where the inclusion functor is omitted.

Once more we use traces, that is, for each gÎLin[!A,B] set

Tr(j(g)) = {(a, y) | ({a}, y)ÎTr(g) } .

The reader may prove for exercise the naturality of j. In particular, the unit and counit of the

adjunction are given, as usual, by

hA = j(id!A) : A®!A where Tr(hA) = {(a, a) | aÎA finite }

eA = j-1(idA) : !A®A where Tr(eA) = {({x}, x) | xÎ|A| }.

Exercise Check, by actual computations in the structure, that !f = j-1(hA»f) and f = j(eA»!f).

Following theorem 5.4.1, (!, Inc, h, e) yields a comonad

(! = !»Inc: Lin®Lin, D = !hInc: !®!°!, E = e: !®IdC )

as required to turn Lin into an !-model. Moreover, it is a matter of a simple observation on the

’hardware“ of coherent domains to show that the isomorphisms needed to complete the definition

hold in Lin, namely, that !(AÇB) @ !(A)„!(B) and !t @ 1 are uniformly valid in this model (see

the example in section 4.4).

Interestingly enough, by (iso) above, Stab is the co-Kleisli category associated with the

comonad (!, D, E) on Lin.

We conclude this section by identifying a class of categories which yield an interesting interpretation

of the modality ! . The idea is to interpret !A as the commutative comonoid freely cogenerated by A,

not just as a comonoid in the intended linear category.

5.5.8 Definition Let C be a linear category and U: CoMonC®C be the forgetful functor which

takes (c, d, e) to c. Then C is a free !-model if there exists a right adjoint to U, that is a functor

! : C®CoMonC and a natural isomorphism W: C[c,a] @ CoMonC[(c,d,e), !(a)] .

We need to show that free !-models are indeed !-models. This follows from the simple, but

powerful, adjointness property stated in 5.5.8. As already recalled, by proposition 5.4.1, each

116

5. Universal Arrows and Adjunctions

adjunction yields a comonad. We explicitly reconstruct the units and counits as they bear some

information.

5.5.9 Lemma Let C be a free !-model and <U,!,W > be the given adjunction. Then, for ! =

W

U°!, there exist natural transformations D: !®!°! and E: !®IdC such that

(!: C®C, D: !®!°!, E: !®IdC )

is the comonad associated with C, in the sense of proposition 5.4.1.

Proof By the definition of morphism in CoMon C , for every hÎC[c,a], the morphism W(h)Î

CoMonC[(c,d,e),!(a)] satisfies the following equations:

hom-1. da ° W(h) = ( W(h)„W(h) ) ° d : c®!a„!a ;

hom-2. ea ° W(h) = e : c®1 .

Moreover, the naturality of W is expressed by the following equations:

for every hÎC[c,a] , fÎC[a,b] , gÎCoMon C [(c',d',e'), (c,d,e)] :

nat-1. W(f ° h) = !(f) ° W(h) ;

nat-2. W(h ° U(g)) = W(h) ° g .

The counits of the adjunction (W, U, !): CoMon C ®C, are arrows E c=W -1(id!(c)): !c®c. By

equation (nat-1) above, for h = Ec, we obtain !(f) = W(f ° Ec), and by equation (nat-2), Ec ° U(W(h))

= h . The family of arrows {Ec}cÎC defines a natural transformation E: (U ° !)®I. Dually the

units of the adjunction define a natural transformation H : I®(! ° U), where: H(c,d,e) = W(idc) :

(c,d,e)® !c. The adjunction between CoMon C and C is thus equivalently expressed by the

parameters (U, ! , H: I®(! ° U), E: (U ° !)® I ).

Remember now that a comonad over a category C is a comonoid in the category of endofunctors

from C to C (with composition as product, see 4.2.2).

By proposition 5.4.1, every adjunction (F, G, h: IdC ®G °F, e: F °G®IdC' ) from C to C'

determines a comonad (T = F°G, d = FhG: T® T°T, e : T®IdC') over C'.

In particular the adjunction (U, ! , H: I®(! ° U), E: (U ° !)® I ): CoMon C ®C, defines a

comonad (! = U ° ! , D = UH! : ! ® ! ° ! , E : ! ®IdC ) over the !-model C. ¨

Finally we derive the natural isomorphisms in definition 5.5.4.

5.5.10 Theorem Let C be a free !-model and (!: C®C, D: !®!°!, E: !®IdC) be the comonad

associated with it by the lemma. Then there exist natural isomorphisms

I: !(AÇB) @ !(A)„!(B)

J: !t @ 1

where t and 1 are the identities for Ç and „ , the Cartesian and tensor products in C.

Proof Consider the comonoid (!(A)„!(B),d,e) where

d = mix ° (dA„dB) : !(A)„!(B) ® (!(A)„!(B))„(!(A)„!(B))

117

5. Universal Arrows and Adjunctions

e = ins-r-1 ° (eA„eB) : !(A)„!(B) ® 1

and

mix : (!(A)„!(A))„(!(B)„!(B)) ® (!(A)„!(B))„(!(A)„!(B))

is the obvious isomorphism.

Then, by hypothesis, we have an isomorphism

W: C[!(A)„!(B),AÇB] @ CoMonC[ (!(A)„!(B),d,e), !(AÇB) ]

The isomorphism IA,B from !(AÇB) to !(A)„!(B), which we write I for short, is given by

I = (!fst „!snd) ° dAÇB : !(AÇB) ® !(A)„!(B)

Note that I is a morphism of comonoids, that is, as it is easily verified,

d ° I = (I„I) ° dAÇB

e ° I = eAÇB

The inverse image of I is defined in the following way.

Let

k1 = EA ° ins-r-1 ° (id!A „ eB): !(A)„!(B)®A

k2 = EB ° ins-l-1 ° (eA „ idB): !(A)„!(B)®B

and

k = <k1, k2> : !(A)„!(B)®AÇB

Then the inverse image of I is U(W(k)) = W(k) : !(A)„!(B)®!(AÇB), indeed:

W(k) ° I =

= W(k ° I) by (nat-2)

= W( <k1, k2> ° I ) by def. of k

= W( <k1 ° I, k2 ° I >)

= W( <EA°ins-r-1°(id!A„eB)°(!fst„!snd)°dAÇB, EB°ins-l-1°(eA„idB)°(!fst„!snd) ° dAÇB >)

by def. of k1, k2 and I

= W( <EA°ins-r-1°(id!A„eA)°(!fst„!fst)°dAÇB, EB°ins-l-1°(eB„idB)°(!snd„!snd) ° dAÇB >)

as eB°!snd = eAÇB = eA°!fst

= W( < EA ° ins-r-1 ° (id!A„eA) ° dA ° !fst, EB ° ins-l-1 ° (eB„idB) ° dB ° !snd >)

as !fst and !snd are comonoid morphisms

= W( < EA ° !fst, EB ° !snd >) by properties of comonoids

= W( < fst ° EAÇB, snd ° EAÇB >) by naturality of E

= W( EAÇB)

= id!(AÇB) . by def. of E

I ° W(k) =

= (!fst „!snd) ° dAÇB ° W(k)

= (!fst „!snd) ° ( W(k)„W(k) ) ° d by (hom-1)

= (!fst ° W(k) )„(!snd ° W(k) ) ° d

118

5. Universal Arrows and Adjunctions

= ( W( fst ° k) )„( W( fst ° k) ) ° d by (nat-1)

= ( W(k1) )„( W(k2) ) ° d by def. of k

= ( W( EA ° ins-r-1 ° (id!A „ eB) )„( W(EB ° ins-l-1 ° (eA „ idB) ) ° d

by def. of k1 and k2

= ( ins-r-1 ° (id!A „ eB) )„( ins-l-1 ° (eA „ idB) ) ° d

by (nat-2) and def. of E

= ( ins-r-1 ° (id!A „ eB) )„( ins-l-1 ° (eA „ idB) ) ° mix ° (dA„dB)

by def. of d

= ( ins-r-1 ° (id!A „ eA) )„( ins-l-1 ° (eB „ idB) ) ° (dA„dB)

by application of mix

= ( ins-r-1 ° (id!A „ eA) ° dA )„( ins-l-1 ° (eB „ idB) ° dB)

by properties of comonoids

= id!(A)„id!(B)

= id!(A)„!(B) .

The construction is clearly uniform in A and B.

As for the natural isomorphism J, note that !A @ !(AÇt) @ !A„!t , !A @ !(tÇA) @ !t„!A and

that the right and left identity, in a monoidal category, are unique. ¨

References Universal arrows and adjunctions are fundamental notions in Category Theory.

Their treatment, in various forms, and references to their origin may be found in all textbooks we

mentioned in the previous chapters. References for Linear Logic have been given in chapter 4.

119

6. Cones and Limits

Chapter 6

CONES AND LIMITS

In chapter 2, we learned how common constructions can be defined in the language of Category

Theory by means of equations between arrows of given objects. In chapter 4, we saw that those

definitions were based on the existence of an universal arrow to a given functor. The category-

theoretic notion of limit is merely a generalization of those particular constructions, as it stresses their

common universal character. From another point of view, the limit is a particular and important case

of universal arrow, where the involved functor is a ’diagonal,“ or ’constant“ functor, as we shall

see. To help the reader become confident with this new notion, we begin this chapter by looking back

at the constructions of chapter 2 and we regard them as particular instances of limits. Then we study

some relevant properties concerning existence, creation, and preservation of limits. As for computer

science, limits have been brought to the limelight mainly by the semantic investigation of recursive

definition of data types: this particular application of the material in this chapter will be discussed in

chapter 10.

6.1 Limits and Colimits

The concept of limit embodies the general idea of universal construction, that is, of an entity which

has a privileged behavior amongt a class of objects that satisfy a certain property. The only way to

define a property in the categorical language is by specifying the existence and equality of certain

arrows, that is, essentially by imposing the existence of a particular commutative diagram amongt

objects inside the category.

6.1.1 Definition A diagram D in a category C is a directed graph whose vertices iÎI are

labeled by objects di and whose edges eÎE are labeled by morphisms fe.

A diagram D in C is similar to a subcategory of C; however, it does not need to contain identities,

nor must it be closed under composition of morphisms.

More formally, a diagram in a category C should be defined as a graph homomorphism D

from an index graph I to the (graph underlyng the) category C . Such a diagram is called ’of type

I“. For the adjunction between graphs and categories, this is exactly the same as a functor from the

category I freely generated by the graph I (the index category) to C. A graph is called small when

the index category is small.

120

6. Cones and Limits

6.1.2 Definition. Let C be a category and D a diagram with objects di, iÎI . Then a cone to

D is an object c and a family of morphisms {fiÎC[c,di] | iÎI } such that

"i,jÎI "eÎE feÎC[di,dj] ’Þ fe ° fi = fj .

A cone may be visualized by

Cocones are defined dually.

Example In a partial order P, cones correspond to lower bounds, cocones to upper bounds.

Note now that, given a diagram D, the cones to D form a category, call it ConesC,D . Just take

as morphisms from (c,{fiÎC[c,di] | iÎI}) to (c',{hiÎC[c',di] | iÎI}) any gÎC[c,c'] such that

"iÎI hi ° g = fi. That is,

Clearly, ConesC,D is a category. Dually one defines the category CoconesC,D .

6.1.3 Definition. Let C be a category and D a diagram. Then a limit for D is a terminal object

in Cones C,D . Colimits are defined dually.

(c,{fiÎC[di,c] | iÎI}) is the initial object in CoconesC,D, it may be visualized by the following

commutative diagram:

121

6. Cones and Limits

Limits are also called universal cones, as any other cone uniquely factorizes via them. Dually,

colimits are called universal cocones.

Examples

1. Let P be a partial order. Then limits correspond to greater lower bounds, while colimits

correspond to least upper bounds.

2. Let D = ({di}iÎw, {fiÎSet[di, di+1]}iÎw ) be a diagram in Set such that di Í di+1, and fi =

incl (the set-theoretic inclusion). Then the colimit of d0 ®.......di ® di+1 ®..... is È{d i}

(exercise: what is the limit of the same diagram?) .

Exercise Prove that the colimits in C are the limits in Cop of the dual diagram.

Consider now a diagram as a functor from an index category I to C. Note first that any object c

of the category C is the image of a constant functor Kc: I®C, and so Kc can be regarded as a

degenerate diagram of type I in C. Once diagrams are defined as functors, it makes sense to

consider natural transformations between diagrams. If D and D' are two diagrams of type I, a

natural transformation from D to D' is a family of arrows fi indexed on objects in I such that for

each arrow e in I (each edge of the graph of type I)

A cone for a diagram D of type I from an object c is then a natural transformation from the

constant diagram Kc to D

122

6. Cones and Limits

Dually, a cocone for a diagram D of type I to an object c is a natural transformation from D to

the constant diagram Kc .

6.2 Some Constructions Revisited

Let D be an empty diagram, that is a diagram with no objects and no arrows. By definition, a cone

in C to D is then just an object c of C, with no other structure (and every object of C can be seen

as a cone). A limit for the empty diagram is then an object t such that for any other object c there is

exactly one arrow from c to t, i.e., it is a terminal object. Dually, the initial object is the colimit

of the empty diagram.

A graph is called discrete if it has no arrows. For example the set {1,2} can be regarded as a

discrete graph. A diagram of type {1,2} in a category C is an ordered pair of objects, (c1,c2). A

limit for such a diagram is an object d, together with two arrows f1: d®c1 and f2: d®c2, such

that for any other cone (d',{giÎC[d',ci] | iÎ{1,2} }) there exists exactly one arrow h: d'®d, with

fi ° h = gi for iÎ{1,2}.

But this is just the definition of product d of c1 and c2 with f1 : d®c 1 and f2 : d®c 2 as

projections.

Dually, the coproduct ci#cj, if it exists, is just the the colimit of the diagram {ci,cj}.

The product of any indexed collection of objects in a category is defined analogously as the limit

of the diagram D: I®C where I is the index set considered as a discrete graph. This product is

usually denoted by PiÎIDi, although explicit mention of the index set is often omitted.

Consider the graph I with two vertices and two edges

A diagram of type I in a category C is a pair of objects, a and b, and a pair of parallel arrows

f,gÎC[a,b]. A cone for this diagram consists of an object d, and two arrows hÎC[d,a] and

kÎC[d,b] such that g ° h = k and f ° h = k. A limit is a cone (d,{h,k}) that is universal, that is,

for any other cone (d',{h',k'}) there exists exactly one arrow l: d'®d such that h ° l = h', and k °

l = k'.

123

6. Cones and Limits

Note now that the existence of two arrows, h and k, such that g ° h = k and f ° h = k, is

equivalent to the existence of an arrow h such that g ° h = f ° h. Moreover, h ° l = h' implies k ° l =

k', since k ° l = f ° h ° l = f ° h' = k', thus the above limit is just the equalizer of f and g .

Dually, coequalizers are the colimits for the same diagram.

Consider now the following graph: