Asperti A.Categories,types,and structures.1991

4. Categories Derived from Functors and Natural Transformations

Exercise Show the logical equivalence of (A B)__oC and A__o(B__oC). Derive also that A |- (A ) and (A ) |- A, i.e. ( ) is “dualizing”.

This may be enough to suggest that the categorical meaning of linear logic may be found in particular symmetric monoidal closed categories, where and __o are interpreted by the tensorial product and the bifunctor given in definition 4.3.5, respectively. Observe that the cartesian product is needed too, so to provide an interpretation for ∩ and its identity T (see later). Negation and all dual constructions are taken care of by a “dualizing” endofunctor (-)*, which is closed in the sense of 4.3.7. Indeed, theorem 4.4.6 below shows that this functor, given and ∩ , immediately yields their duals.

4.4.4 Definition A -autonomous category							K is a symmetric monoidal closed category and a
contravariant closed functor (-)*: K → Κ such that:
-	there exists a natural isomorphism d : Id						(-)**
-	the following diagram commutes (where						(-)* is the action of the functor on exponents)
			A B				(-)*	B* A*
	d	˚	_	˚	d-1
									(-)*

A** B**

A -autonomous category is linear if it is also cartesian.

In other words, a linear category has both a monoidal and a Cartesian structure, and ∩ , plus a dualizing functor (-)*.

4.4.5 Proposition Both the vertical and the horizontal arrows in the diagram in definition 4.4.4 are isomorphisms. Moreover,

i.A* B* iff A B;

ii.A* A 1*.

Proof By definition, the following diagram commutes and d ˚ _ ˚ d-1 is an isomorphism,

f**

A** B**

d-1		d

A B f

84

4. Categories Derived from Functors and Natural Transformations

Then the horizontal (-)*, in the diagram in definition 4.4.4, is a split mono (see section 1.4) and the vertical one is a split epi. Since the latter is an instance of the former, they are both split monos and split epis as well and, thus, isomorphisms. In conclusion, ΑB Β* A*. Finally, A* B* implies A A** B** B and, by exercise 4.3.6.3, A* 1A*. Thus, A* B* iff A B and, moreover, A* Α 1*. ♦

4.4.6 Theorem Let K be a linear category. Define
	A B = (A* B*)*
	A B = (A*∩B*)*.
Then is a dual to the tensor product and is the coproduct in K. Their identies are		= 1* and
0 = T*,	respectively.
Proof	is a well-defined dual to : just compare with definition 4.3.1 (and	the remark
afterwards) and note that

-A = (A* 1)* A** A (similarly for the identity to the left),

-(A* B*) C* A*(B* C*) implies (A B)* C* A*(B C)* implies

((A B)* C*)* (A*(B C)*)* implies (A B) C A(B C) .

As for the Cartesian coproduct, note that, if pA* and pB* are the projections for A*∩B*, then their images (pA*)* and (pB*)* via the (-)* functor are the injections for A B. Finally, A = (A* 1)* A and A 0 = (A*∩T)* A. ♦

The results in proposition 4.4.5 and theorem 4.4.6 prove the “dualizing” role of the (-)* functor and of = 1*. In particular, theorem 4.4.6 is a version of De Morgan rules in the semantic structures for linear logic, when described in categorical terms. Note also that

A* B (A B*)*

(A B*)

A(B*)

A(1Β)

A B

which gives the “classic” flavor of this fragment of Linear Logic.

The meaning of linear logic as a deductive system is then given by interpreting each entailment A |- B as a morphism between the interpretation of the formulas. Linear categories yield such an interpretation, which we sketch here, by induction on rules. Here are some of the basic cases. Some crucial ones are simply the properties corresponding to ( AB), (evalAB), (αABC) and (α−1ABC), given before definition 4.4.4, in monoidal closed categories. As for the others,

the rules

are interpreted by

the fact that

85

4. Categories Derived from Functors and Natural Transformations
for 1 and	1 and are (the unique) identies for and , which
	are expressed by commas, on the left or right, respectively,
	of |-.
( ,r) and ( ,l)	and are bifunctors
(∩,r) and ( ,l)	∩ and have pairing and sum of morphisms
(∩,l,1) and (∩,l,2)	there exist projections for ∩
( ,r,1) and ( ,r,2)	there exist injections for
(contrap)	(-)* is so defined in linear categories
( , )	= 1* and, thus, * 1 .

(By the argument before 4.4.4, (contrap) and ( , ) are equivalent to ( ,r) and ( ,l) .)

Example The category Lin of coherent domains and linear maps, in 2.4.2, not only provides an example of linear category, but it has even been the source of inspiration for linear logic, since linear functions depend on inputs “additively” as deductions from assumptions in this logic. (There is more than that analogy, though, as this example and section 5.5 should clarify.)

We noticed that Lin is Cartesian in 2.3.7(II). Lin is also co-Cartesian. Indeed, let (|X|,↑) and (|Y|,↑) be coherent structures. Define then the coproduct X Y as the coherent domain associated with the coherent structure ({(0,z) | z |X|} {(1,z) | z |Y|},↑ ), where (a,x)↑ (a',y) iff a = a' and x↑y . (Note the difference with the product: the support is the same, but the coherence relation

changes. Give the embedding linear maps for exercise.)

The singleton coherent domain T = 0 = { } , associated with the empty coherent structure, is both terminal and initial in the category. Indeed, it is the identity for both the product and the coproduct.

In the previous section we turned Lin into a symmetric monoidal closed category (see exercise 4.3.6). Recall, in particular, that the tensor product A B is the coherent domain associated with the coherent structure (|A|×|B|, ↑ ), where (x,y)↑ (x',y') iff x↑x' and y↑y'.

The dual of the tensor product, is given by the tensor sum A B, that is, the coherent domain associated with the coherent structure (|A|×|B|, ↑ ), where (x,y)↑ (x',y') iff ( (x,y) = (x',y') or x↑↑x' or y↑↑y'). Also in this case, the tensor product and sum have the same support, but the coherence relation changes.

Notice that the identity for both the tensor product and its dual is the coherent domain 1 = = { ,{1}}, associated with ({1}, =).

86

4. Categories Derived from Functors and Natural Transformations

As for the contravariant functor (-)* , given a coherent structure (|A|, ↑), define A* as the coherent domain associated with (|A|, ↑*), where x↑*y iff ~(x↑y) in A . On a linear function f: A→B, f*: B*→A* is defined in the following way: (y,x) Tr(f*) iff (x,y) Tr(f) .

As one could expect (and easily compute), in coherent domains one has T* = 0 = T and 1* = = 1 . Moreover, the equations in theorem 4.4.6 are realized in Lin.

Memo For the reader's convenience, we summarize the identities in linear logic (and linear categories):

1 for ; for ; T for ∩ ; 0 for

which are interpreted in Lin as 1 = = { ,{1}} and T = 0 = { }, with the obvious coherent structure.

References Textbooks, which stress the applications of Category Theory to computer science with an algebraic perspective, are Arbib and Manes (1975) and Rydeheard and Burstall (1988). Goguen and Burstall (1984) contains a survey and references to part of this area, broadly construed, which ranges from the work in Elgot (1971), to the contributions of the ADJ group (see, at the end of this volume, the many references which include the names of Goguen, Thatcher, Wagner, or Wright).

Besides the references to general Category Theory, the reader may consult Barr (1979) and Barr and Wells (1985) for monoidal categories, monads and their mathematical applications. Further references, which also discuss Linear Logic, are Barr (1990) and Marti-Oliet and Meseguer (1990). The recent applications of “monoidal notions” we described are borrowed from Moggi (1989), as for the understanding of programs as “functions from values to computations”, and from Meseguer and Montanari (1988) or Degano and al. (1989), as for the examples on Petri nets (see also Marti-Oliet and Meseguer (1989)).

The main reference for linear logic is Girard (1987). Further work may be found, among others, in Girard and Lafont (1987), Lafont (1988), DePavia (1987), and Seely (1987), where -autonomous categories are proposed for its semantics. Lambek (1968) contains early work on the categorical significance of logical systems and discusses weakenings of the structural rules.

87

5. Universal Arrows and Adjunctions

Chapter 5

UNIVERSAL ARROWS AND ADJUNCTIONS

In chapter 3, we introduced the notion of functor as a uniform way to describe “acceptable” constructions in Category Theory. The reader may have noticed that in some cases, for a given construction F: C→D, there exists a particular object c in C and an arrow u: F(c)→d , which has a “universal behaviour” with respect to d, in the sense that every other arrow f: F(c')→d uniquely factorizes through u , i.e., there exists a unique f': c→c' such that f = u ° F(f') or the following diagram commutes:

Consider for example the product functor _×a: C→C where C is a CCC and a ObC. The arrow eval: ba×a→b is universal with respect to b, in the previous sense, since for every arrow f: c×a→b there exists a unique arrow Λ(f): c→ba such that f = eval ° Λ(f), i.e.,

Also the product of two objects may be described in terms of universal arrows. Just take the diagonal functor ∆: C→CxC , with ∆(c) = (c,c) and ∆(f) = (f,f) and observe that the following diagram commutes:

88

5. Universal Arrows and Adjunctions

The aim of this chapter is to study the concept of universal arrow outlined above, and some of its implications. In particular we prove that given a functor F: C→D, if for every d D there exists an universal arrow ud: F(cd)→d, then the function g: ObD→ObC that takes d to cd may be extended to a functor G: D→C. Such a functor G is called (right) adjoint to F. Remarkably, if G is a (right) adjoint to F, then F is a (left) adjoint to G, in a dual sense, and each one describes the other up to isomorphism. From another point of view, F and G can be seen as a pair of “mutually representable” functors.

The notion of adjointness is probably the most profound and original contribution of Category Theory to mathematics. The reader must not expect to understand its relevance upon first reading the definition, or the few examples and applications in this chapter: only by a systematic use of adjunctions will she or he become competent on the subject.

5.1 Universal arrows

In addition to the previous remarks, the careful reader has surely noticed that most of the definitions of the constructions defined in chapter 2 (products, coproducts, terminal object, exponents . . .) have the following common pattern:

for all . . . there exist a unique . . . such that . . . .

As a matter of fact, all those definitions can be seen as particular cases of a same notion (or its dual): the universal arrow. For historical reasons, universal arrows are defined dually with respect to the examples just mentioned (exponents, products . . . ). Couniversal maps, to be defined next, will fit the examples.

5.1.1 Definition. Let F: C→D be a functor and d ObD. Then <u,cd> is universal from d to F iff u D[d,F(cd)], cd ObC, and c' ObC, f D[d,F(c')], ! f' C[cd,c'] f = F(f')° u .

As usual, this may be equivalently visualized by

89

5. Universal Arrows and Adjunctions

Example <(q1,q2),(a#b,a#b)> is universal from (a,b) to ∆, where ∆: C→C×C is the diagonal functor.

5.1.2 Definition. Let F: C→D be a functor and d ObD. <u,cd> is (co)universal from F to d iff u D[F(cd),d], cd ObC, and c' ObC, f D[F(c'),d] ! f' C[c',cd] f = u ° F(f').

The diagrams and examples in the introduction to this chapter refer this “dual” notion. Here are other interesting examples:

5.1.3 Example Let !C be the unique functor from the category C to the category 1; if id1 = u 1[!C(c),1] is universal, then c is terminal in C:

5.1.4 Example Let C be a category of partial morphisms, Ct be the associated category of total morphisms, and Inc: Ct→C be the embedding functor (see section 2.6). Recall that, by definition, the lifting of a ObC is an object a° ObC together with a morphism exa Ct[a°,a] such that for every f C[c,a] , there exists one and only one f' Ct[c,a°] satisfying the equation exa ° f' = f . This says exactly that exa: a°→a is an universal arrow from Inc to a :

90

5. Universal Arrows and Adjunctions

Exercise Define an initial object as a universal arrow from 1				to	!C.
5.1.5 Proposition. Let		F: C→D be a functor and d ObD . Assume that <u,c> is universal
from d to F . Then
1.	<u',c'> is universal from d to		F c c' ;
2.	c c' via (h,h-1)	<F(h)	u,c'> is universal from	d	to F.
		°

Proof

1.!h C[c,c'] !h' C[c',c] u'= F(h)°u = F(h)°F(h')°u'= F(h°h')°u'. But u' = F(id) °u'. By unicity, h°h' = id . Similarly, h'°h = id .

2.Exercise. ♦

By the proof of proposition 5.1.5, one even has that the isomorphism is unique. This is a strong property of universal constructions as a very common tool in mathematics (see the examples below). It is hard to think of a more suitable language than the categorical one for expressing properties like this.

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 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, for every c ObC there is an operation τc: D[d,G(c)]→C[cd,c] such that, for every f D[d,G(c)] and every h C[cd,c] ,

1.G(τc(f)) ° u = f

2.τc(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 τc(f) as the unique arrow f' such that G(f') ° u = f. (1) is then immediate by definition, and (2) follows by unicity.

( ) let τc: 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] τc-1(h) = G(h) ° u ; thus, we have:

	τc-1(τc(f)) = G(τc(f)) ° u = f		by (1)
	τc(τc-1(h)) = τc(G(h) ° u) = h		by (2). ♦
5.1.7 Theorem. Let C, D be locally small categories, G: C→D,			d ObD and cd ObC. 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	τc'(f') = G(f') ° u D[d,Fc'] .
Then τ: C[cd,_]→D[d,G_]	is a natural transformation, since τc'(g ° h) = G(g ° h) ° u = G(g) ° τc(h).

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

Moreover, f D[d,Fc'] !f' C[cd,c'] f = τc'(f') , by definition. Thus, by proposition 3.2.3, τ is a natural isomorphism.

( )	Let τ : C[cd,_] D[d,G_] and set u = τcd(id). Then u D[d,G(cd)] . By the naturality of
τ, for all	c,c' ObC , G(g) ° τc(_) = τc'(g°_) and, hence, f D[d,G(c')]
	G(τc'-1(f)) ° u = G(τc'-1(f))°τcd(id)
	= τc'(τc'-1(f))
	= f .

That is, f D[d,G(c')] !f'(= τc'-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.8Corollary Let C, D be small categories, G: C→D, d ObD and cd ObC. Then there exists u D[d,G(cd)] 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

GThen there exists a functor F: D→C such that

i.F(d) = cd

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

(Note that C[F_,_], D[_,G_] : Dop×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