Asperti A.Categories,types,and structures.1991

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

(s-conv.) Φ↓sx iff ΦF(x) and 0Φ∩top x 0 . Then top is T0 iff s-convergent filters have a unique limit.

Let N = (ω, 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,η,ε) to (T,H,τ) is not an adjoint equivalence (which one of η and ε 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(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, η , ε) be an adjunction from C to D; then (T = GF, η , = GεF) is a monad on C and (T = FG, δ = GηF, ε) is a comonad.

104

5. Universal Arrows and Adjunctions

Proof Note first that GF, η, and GεF have the correct types, i.e., T = GF: C→C, η: IdC→GF, and = GεF: GFGF→GF. We must prove the unity and associative laws for the monad.

As for the unity laws we have

° Tη = GεF ° GFη = G(εF ° Fη) = G(idF) = idGF

° ηT = GεF ° ηGF = (Gε ° ηG)F = idG(F) = idGF For the associative law, note first that

ε ° εFG = ε ° FGε .
Indeed, for any d ObD , and letting f = εd: FG(d)→d,
εd ° εFG(d)	= f ° εFG(d)
	= εd ° FG(f)	by naturality of ε
	= εd ° FG(εd)
Then one has the following:
° T	= GεF ° GεFGF
	= G(ε ° εFG)(F)
	= G(ε ° FGε)(F)
	= GεF ° GFGεF
	= ° T .

The rest is an exercise in duality. ♦

5.4.2 Definition Let (T, η , ) be a monad over a category C. A resolution for (T, η , ) is a category D and an adjunction (F, G, η , ε) from C to D such that T = GF and = GεF. A morphism between two resolutions (F, G, η , ε): C→D and (F', G', η , ε'): C→D' (for the same monad) is a functor H: D→D' such that F' = H ° F, G = G' ° H , and Hε = ε'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, η , ) 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, η , ) be a monad over a category C , and let CT be the EilenbergMoore category associated with the monad. Then there exists a resolution for (T, η , ) which is an adjunction from CT to C.

Proof Let UT: CT→C be the forgetful functor that takes every algebra (c,α) to c, and every morphism of algebras h to the same h regarded as a morphism in C. Let FT: C→CT be the functor which takes every object c to its free algebra (T(c), c), and every morhism f: c→c' to FT(f) = T(f). Let εΤ: FTUT→idCT be the natural transformation defined by εΤ(c,α) = α (note that α: T(c)=FTUT(c,α)→c). We want to prove that (FT, UT, η , εT) is a resolution for (T, η , ).

105

5. Universal Arrows and Adjunctions

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

(UT εT FT)(c) = UT(εT FT(c))
	= UT(εT(T(c), c))	by def. of FT
	= UT( c)	by def. of εT
	= c	by def. of UT
We still haveto prove that (FT, UT, η , εT) is an adjunction from CT to C, that is,
	(UTεT) ° (ηUT) = idUT
	(εTFT) ° (FTη) = idFT
One has, for every T-algebra (c,α),
(UTεT ° ηUT) (c,α)	= UT(εT(c,α) ) ° ηUT(c,α)	by def. of εT and UT
	= α ° ηc
	= idc	by def. of T-algebra
And for every c ObC :
(εTFT ° FTη) (c)	= εTFT(c) ° FT(ηc)	by def. of εT and FT
	= c ° T(ηc)
	= idT(c)	by the unity law of the monad.♦

We say that the resolution (FT, UT, η , εT) 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, η , ) be a monad over a category C .Then the resolution (FT, UT, η, εT): C→CT, associated with the Eilenberg-Moore Category CT, is a terminal object in the

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

Proof Let (F, G, η , ε): C→D be another resolution for (T, η , ). We must prove that there exists a unique arrow from (F, G, η , ε) to (FT, UT, η , εT). 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 Hε = εTH.

Define, for any object d, and any morphism f of D, H(d) = (G(d), G(ε(d)) )

H(f) = G(f).

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

H(F(c)) = (G(F(c)), G(ε(F(c))) ) = (T(c), c) = 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(ε(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,

εTH(d) = εT(G(d), G(ε(d)) ) = G(ε(d)) = H(ε(d)) that proves the equality Hε = εTH.

We have still to prove that H is the unique morphism from (F, G, η , ε) to (FT, UT, η , εT).

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), εTH'(d))	by def. of UT and εT
= ( G(d), H'(εT(d)) )	as	G = UT ° H'
= ( UT(H(d), H(εT(d)) )	as	H'(f) = H(f)

= ( UT(H'(d), εTH(d))

= H(d).

This completes the proof. ♦

The unique functor to (FT, UT, η , εT) in the category of all resolutions for a given monad (T, η ,) 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, η , ) be a monad over a category C, and let CT be the Kleisli category associated with the monad. Then there exists a resolution for (T, η, ) 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,Τ(c')]) UT(c) = T(c);

UT(h) = c' ° 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) = ηc' ° f ( = T(f) ° ηc ).

Let εΤ: FTUT→id be the natural transformation defined by the following:

for any object c of CT
εΤ(c) = idT(c) (in C).
We want to prove that (FT, UT, η , εT): C→CT	is a resolution for (T, η , ).
Obviously, UT ° FT = T .
Moreover, UT εT FT = , since for any object c one has
(UT εT FT)(c) = UT(εT (c) )	by def. of FT

107

5. Universal Arrows and Adjunctions

=UT(idT(c))

=c.

We have still to prove that (FT, UT, η , εT) is an adjunction from (UTεT) ° (ηUT) = id: UT→UT (εTFT) ° (FTη) = id: FT→FT

One has, for every object c of CT:

(UTεT ° ηUT) (c) = UT(idT(c)) ° ηT(c)

=c ° T(idT(c)) ° ηT(c)

=c ° ηT(c)

=idc.

And, for every c ObC,

(εTFT ° FTη) (c) = εT(c) ° (ηΤ(c) ° ηc)

=idT(c) ° (ηΤ(c) ° ηc)

=C ° T(idT(c)) ° ηΤ(c) ° ηc

=C ° ηΤ(c) ° ηc

=ηc

=idc

by def. of εT by def. of UT C to CT, that is,

by def. of εT and UT

by def. UT on morphisms as T is a functor

by the unity law of the monad

by def. of FT by def. of εT

by def. of composition ° in CT

by the unity law of the monad by def. of the identity in CT. ♦

5.4.6 Proposition Let (T, η, ) be a monad over a category C. The resolution (FT, UT, η , εT): C→CT associated with the Kleisli Category CT is an initial object in the category of resolutions for the monad (T, η , ).

Proof Let (F, G, η , ε): C→D be another resolution for (T, η , ). We must prove that there exists a unique arrow from (FT, UT, η , εΤ) to (F, G, η , ε), that is a unique functor K: CT→D,

such that F = K ° FT, UT = G ° K , and KεΤ = εK.
Define, for any object c of CT, and any morphism f CT[c,c'],
K(c) = F(c);
K(f) = εF(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(ηc' ° h)	by def. of FT
= εF(c') ° F(ηc' ° h)	by def. of K
= εF(c') ° F(ηc') ° F(h)	as F is a functor
= F(h)	as (F, G, η , ε) 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(εF(c') ° F(f))

=G(εF(c')) ° G(F(f))

=c' ° T(f)

=UT(f)

that proves the equality UT = G ° K . Finally, for any d ObD,

K(εΤ(c)) = Κ(idT(c))

=εF(c') ° F(idT(c))

=εF(c')

=εK(c')

that proves the equality KεΤ = εK.

We have still to prove that K is the unique morphism from

Let K': CT→D be another morphism; then, for every object K'(c) = K'(FT(c))

=F(c)

=K(FT(c))

=K(c)

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

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

=K'( c' ° ηT(c') ° f)

=K'( c' ° T(idT(c')) ° ηT(c') ° f)

=K'(idT(c') ° (ηT(c') ° f) )

=K'(idT(c')) ° K'(ηT(c') ° f) )

=K'(εΤ(c')) ° K'(FT(f)) )

=εK'(c') ° F(f)

=εF(c') ° F(f)

=K(f).

This completes the proof. ♦

by def. of K

as G is a functor

as (F, G, η , ε) is a resolution

by def. of UT

by def. of εΤ by def. of K

as F is a functor

by def. of K

(FT, UT, η , εT) to (F, G, η , ε). c of CT,

by def. of FT

as K' ° FT = F

as K ° FT = F by def. of FT

by the unitary law of the monad

by def. of composition ° in CT as K' is a functor

by def. of εΤ and FT

as K'εΤ=εK' and F=(K'°FT) as K'(c) = K(c) = F(c)

by def. of K

For consistency with the terminology adopted for the comparison functor, we shall denote by KT the unique arrow from the initial object (FT, UT, η , εT) in the category of all resolutions for a monad (T, η , ).

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(εΤ(c)) )	by def. of KT
= (T(c), c ° T(idT(c)) )	by def. of UT and εΤ

109

5. Universal Arrows and Adjunctions
= (T(c), c)
= 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
= c' ° T(f)	by def. of UT
= εΤ(T(c'), (c')) ° T(f)	by def. of εΤ
= εΤFT(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.1exponential unary connectives: ! (of course), ? (why not)

5.5.2exponential rules

	Γ |- ∆		Γ |- ∆
(weak-l)	________	(weak-r)	________
	Γ,!Α |- ∆		Γ |- ?A,∆
	Γ,!Α,!Α |- ∆		Γ |- ?A,?A,∆
(contr-l)	___________	(contr-r)	___________
	Γ,!Α |- ∆		Γ |- ?A,∆
	Γ, Α |- ∆		!Γ |- A,?∆
(!,l)	________	(!,r)	________
	Γ,!Α |- ∆		!Γ |- !A,?∆
	!Γ, Α |- ?∆		Γ |- A,∆
(?,l)	_________	(?,r)	_______
	!Γ,?Α |- ?∆		Γ |- ?A,∆

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, Γ |-i A, in intuitionistic Logic, then ! Γ |- 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 δ: !A→!A !A , and ε: !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 δ, and a map ε which dualizes the map η 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, δ: c→c c, ε: c→1), and morphisms f: (c, δ, ε)→(c', δ', ε'), for each arrow f: c→c' in C , such that

δ' ° f = (f f) ° δ : c→c' c', ε' ° f = ε: c→1 .

112

5. Universal Arrows and Adjunctions

Given a commutative comonoid (c, δ: c→c c, ε: c→1) observe that the following equations hold: (ε idc) ° δ = ins-l : c→1 c

exch ° δ = δ : c→c c

assoc ° (idc δ) ° δ = (δ idc) ° δ : 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 δ and ε are canonically given; namely, δ = <id,id> : c→c∩c is the diagonal and ε: 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 δ':!c→!c!c and ε': !c→1, such that (!c, δ', ε') is a comonoid.

Proof. Just set δ'= Ι˚!δ : !c →!(c∩c) →!c!c ε'= Ι˚!ε : !c → !t →1

where δ = <id,id> : c→c∩c and ε: 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: !→!°!, Ε: !→IdC ) 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, δ':!c →!c!c, ε': !c →1) .

This gives the required monoids, while the natural transformations D and E uniformly yield maps Dc : !c →!°!c and Εc : !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