Oosten Basic Category Theory (1995) [sharethefiles com]

background image

BRICS

LS-95-1

J.
van

Oosten:

Basic

Category

Theory

BRICS

Basic Research in Computer Science

Basic Category Theory

Jaap van Oosten

BRICS Lecture Series

LS-95-1

ISSN 1395-2048

January 1995

background image

Copyright c

1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

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

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

Telephone: +45 8942 3360
Telefax:

+45 8942 3255

Internet:

BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and
anonymous FTP:

http://www. bri cs .aa u. dk/ BRI CS /

ftp

ftp.brics. aa u.d k

(cd

pub/BRICS )

background image

Basic Category Theory

Jaap van Oosten

background image

Jaap van Oosten

BRICS

1

Department of Computer Science

University of Aarhus

Ny Munkegade

DK-8000 Aarhus C, Denmark

1

B

asic

R

esearch

I

n

C

omputer

S

cience,

Centre of the Danish National Research Foundation.

background image

Preface

These notes contain the material of a short course on categories I gave in Arhus

in the autumn of 1994, as part of Glynn Winskel's semantics course. Later on,

while writing, I added some material, but not much.

The style in which they are written reects my view on category theory: it

is, especially at this low level, practice rather than theory which counts. I have

therefore given many proofs as exercises. If you really want to get a grip on the

subject, I strongly suggest you do as many of them as you can.

The same goes for the examples. They are the esh and bones of the theory,

and many of them have been chosen so they are a recurring theme functors

C

//

D

oo

may be given as examples in chapter 1, be shown to constitute an

adjunction in chapter 5, while this may turn out to be a monadic situation in

chapter 6.

For the same reason, references are omitted. Even a sketchy proof, or a hint

of the crucial argument, is better than an intimidating reference to R].

Of course, the examples will be best understood by students who are familiar

with the mathematicalnotions involved, but in general these notes do not require

a lot of mathematical background, except for some basic knowledge of groups,

rings and topological spaces (although examples on the latter may be skipped,

since I have not pursued them through the whole text).

What I

did

presuppose is some familiarity with logic and the -calculus.

Although denitions are given, standard facts about substitution and the like

are suppressed (a teacher can easily supply them when he gives the course).

This familiarity does not include a good understanding of set theory or even

an inkling of the size problems one can run into. I've used the terms \set" and

\small" wherever necessary, although I don't suppose they mean much to many

students. For that reason I've also omitted a proof of Freyd's Adjoint Functor

Theorem and an explanation of the role of the solution set condition.

Apart from chapters 4 and 7, where in spite of the fact that the results are

well-known I haven't been able to nd references where they are treated in a

concise enough form, and so had to develop the material myself, everything is

pretty standard. I have consulted the following sources:

S. MacLane, Categories for the Working Mathematician, Springer (Berlin)

1971.

Still the best text. For non-mathematicians it may be a little tough going,

but it is worth the trouble.

F. Borceux, Handbook of Categorical Algebra, (Encyclopaedia of Math-

ematics and its Applications) Cambridge University Press (Cambridge)

1994.

Next best. Gives a lot of material in a very readable style also on spe-

cialized topics. Three volumes.

i

background image

A strange error in the denition of Grothendieck universes in the rst

chapter, making the denition inconsistent, supports the point about set

theory, I made before.

Many concrete examples. The reader will nd many answers to my exer-

cises in this book.

M. Barr & C. Wells, Category Theory for Computing Science, Prentice

Hall (New York) 1990.

At this moment out of print. The emphasis on sketches is debatable, for

a rst course in the theory. Otherwise a very valuable source.

P.T. Johnstone, Stone Spaces, Cambridge University Press (Cambridge)

1982. Not a book on category theory proper, but a systematic study on

various dualities of the Stone type. A lot of material on posetal structures

like frames, Boolean algebras etc.

A. Asperti, Categorical Topics in Computer Science, Ph.D. Thesis, Pisa

1990. Later reworked into:

A. Asperti & G. Longo, Categories, Types, and Structures: An Introduc-

tion to Category Theory for the Working Computer Scientist (Foundations

of Computing), MIT Press (Cambridge Massachusetts) 1991.

M. Makkai & G. Reyes, First Order Categorical Logic (Lecture Notes in

Mathematics 611), Springer (Berlin) 1977.

\The" book on categorical logic. It is my feeling that a sequel is badly

needed. The main ideas are developed here.

S. MacLane & I. Moerdijk, Sheaves in Geometry and Logic (Universitext),

Springer 1992.

Treats topos theory, with important applications to logic. Can almost be

read from scratch.

J. Lambek & P. Scott, Introduction to higher order categorical logic, Cam-

bridge University Press (Cambridge) 1986.

This may very well be a book of the future, but for a rst acquaintance

with category theory the approach is too formal for my taste. Gives a

very elaborate account of the correspondences between type theories and

certain types of categories.

Of course this list doesn't make any pretense whatsoever at being complete or

even a guide into the literature. It mainly reects my personal attitude.

Acknowledgements

. I am grateful to the group of students who patiently

and critically sat through my lectures, and in particular to Thomas Hildebrandt

ii

background image

and Sren Bgh Lassen who pointed out mistakes in my original hand-written

notes.

The help of my oce mate Vladi Sassone, has been invaluable. A critical

reading by him of the whole rst version revealed a couple of embarassing mis-

takes (\the functor (

;

)

X also has a left adjoint", ha ha|there is no limit to

what a confused brain can come up with) then he put a lot of eort in the visual

layout of the text, teaching me

emacs

and L

a

TEX in the process, and designed

the rococo painting which is the title page.

It goes without saying that the remaining errors are mine, and that the poor

visual quality of the text is a testimony of my ignorance of L

a

TEX, which I am

not proud of.

References

R] J. Razdajev, Some facts about functors, Novosibirsk Journal of Diving

Research XLVII (1947), pp. 634-98 (Russian)

iii

background image

iv

background image

Contents

1 Categories and Functors

1

1.1 Denitions and examples : : : : : : : : : : : : : : : : : : : : : : : 1

1.2 Some special objects and arrows : : : : : : : : : : : : : : : : : : 6

2 Natural transformations

9

2.1 The Yoneda lemma : : : : : : : : : : : : : : : : : : : : : : : : : : 9

2.2 Examples of natural transformations : : : : : : : : : : : : : : : : 12

2.3 Equivalence of categories an example : : : : : : : : : : : : : : : 14

3 (Co)cones and (co)limits

17

3.1 Limits : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 17

3.2 Limits by products and equalizers : : : : : : : : : : : : : : : : : 24

3.3 Colimits : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 25

4 A little piece of categorical logic

29

4.1 Regular categories and subobjects : : : : : : : : : : : : : : : : : 29

4.2 Coherent logic in regular categories : : : : : : : : : : : : : : : : : 33

4.3 The language

L

(

C

) and theory T(

C

) associated to a regular cat-

egory

C

: : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 38

4.4 Example of a regular category : : : : : : : : : : : : : : : : : : : : 39

5 Adjunctions

43

5.1 Adjoint functors : : : : : : : : : : : : : : : : : : : : : : : : : : : 43

5.2 Expressing (co)completeness by existence of adjoints preserva-

tion of (co)limits by adjoint functors : : : : : : : : : : : : : : : : 48

6 Monads and Algebras

53

6.1 Algebras for a monad : : : : : : : : : : : : : : : : : : : : : : : : 54

6.2 T-Algebras at least as complete as

D

: : : : : : : : : : : : : : : : 59

6.3 The Kleisli category of a monad : : : : : : : : : : : : : : : : : : : 59

7 Cartesian closed categories and the

-calculus

63

7.1 Cartesian closed categories (ccc's) examples and basic facts : : : 63

7.2 Typed -calculus and cartesian closed categories : : : : : : : : : 67

7.3 Representation of primitive recursive functions in ccc's with nat-

ural numbers object : : : : : : : : : : : : : : : : : : : : : : : : : 70

Index

73

v

background image

vi

background image

Categories

1 Categories and Functors

1.1 Denitions and examples

A

category

C

is given by a class

C

0

of

objects

and a class

C

1

of

arrows

which

have the following structure.

Each arrow has a

domain

and a

codomain

which are objects one writes

f : X

!

Y or X

f

!

Y if X is the domain of the arrow f, and Y its

codomain. One also writes X = dom(f) and Y = cod(f)

Given two arrows f and g such that cod(f) = dom(g), the

composition

of f and g, written gf, is dened and has domain dom(f) and codomain

cod(g):

X

f

!

Y

g

!

Z

Composition is

associative

, that is: given f : X

!

Y , g : Y

!

Z and

h : Z

!

W, h(gf) = (hg)f

For every object X there is an

identity

arrow id

X

, satisfying id

X

g = g for

every g : Y

!

X and fid

X

= f for every f : X

!

Y .

Exercise 1

. Show that id

X

is the

unique

arrow with domain X and codomain

X with this property.
Instead of \arrow" we also use the terms \morphism" or \map".

Examples

a)

1

is the category with one object

and one arrow, id

b)

0

is the empty category

c) A

preorder

is a set X together with a binary relation

which is reexive

(i.e. x

x for all x

2

X) and transitive (i.e. x

y and y

z imply x

z

for all xyz

2

X). This can be viewed as a category, with set of objects

X and exactly one arrow: x

!

y i x

y.

Exercise 2

. Prove this. Prove also the converse: if

C

is a category such that

C

0

is a set, and such that for any two objects XY of

C

there is at most one

arrow: X

!

Y , then

C

0

is a preordered set.

d) A

monoid

is a set X together with a binary operation, written like mul-

tiplication: xy for xy

2

X, which is associative and has a unit element

e

2

X, satisfying ex = xe = x for all x

2

X. Such a monoid is a category

with one object, and an arrow x for every x

2

X.

1

background image

Categories

e) Set is the category which has the class of all sets as objects, and functions

between sets as arrows.

Most basic categories have as objects certain mathematical structures, and the

structure-preserving functions as morphisms. Examples:

f) Top is the category of topological spaces and continuous functions.

g) Grp is the category of groups and group homomorphisms.
h) Rng is the category of rings and ring homomorphisms.

i) Grph is the category of graphs and graph homomorphisms.
j) Pos is the category of partially ordered sets and monotone functions.

Given two categories

C

and

D

, a

functor

F :

C

!

D

consists of operations

F

0

:

C

0

!

D

0

and F

1

:

C

1

!

D

1

, such that for each f : X

!

Y , F

1

(f) :

F

0

(X)

!

F

0

(Y ) and:

for X

f

!

Y

g

!

Z, F

1

(gf) = F

1

(g)F

1

(f)

F

1

(id

X

) = id

F

0

(X)

for each X

2

C

0

.

But usually we write just F instead of F

0

F

1

.

Examples

.

a) There is a functor U : Top

!

Set which assigns to any topological space

X its underlying set. We call this functor \forgetful": it \forgets" the

mathematicalstructure. Similarly,there are forgetful functors Grp

!

Set,

Grph

!

Set, Rng

!

Set, Pos

!

Set etcetera

b) For every category

C

there is a unique functor

C

!

1

and a unique one

0

!

C

c) Given two categories

C

and

D

we can dene the

product category

C

D

which has as objects pairs (CD)

2

C

0

D

0

, and as arrows:(CD)

!

(C

0

D

0

) pairs (fg) with f : C

!

C

0

in

C

, and g : D

!

D

0

in

D

. There

are functors

0

:

C

D

!

C

and

1

:

C

D

!

D

d) Given two functors F :

C

!

D

and G :

D

!

E

one can dene the

composition GF :

C

!

E

. This composition is of course associative and

since we have, for any category

C

, the

identity functor

C

!

C

, we have a

category Cat which has categories as objects and functors as morphisms.

2

background image

1. Categories and Functors

e) Given a set A, consider the set ~A of strings a

1

:::a

n

on the alphabet

A

A

;

1

(A

;

1

consists of elements a

;

1

for each element a of A the sets

A and A

;

1

are disjoint and in 1-1 correspondence with each other), such

that for no x

2

A, xx

;

1

or x

;

1

x is a substring of a

1

:::a

n

. Given two

such strings ~a = a

1

:::a

n

~b = b

1

:::b

m

, let ~a ?~b the string formed by rst

taking a

1

:::a

n

b

1

:::b

m

and then removing from this string, successively,

substrings of form xx

;

1

or x

;

1

x, until one has an element of ~A.

This denes a group structure on ~A. ~A is called the

free group

on the set

A.

Exercise 3

. Prove this, and prove that the assignment A

7!

~A is part of a

functor: Set

!

Grp. This functor is called the

free functor

.

f) Every directed graph can be made into a category as follows: the objects

are the vertices of the graph and the arrows are paths in the graph. This

denes a functor from the category Dgrph of directed graphs to Cat. The

image of a directed graph D under this functor is called the category

generated

by the graph D.

g)

Quotient categories

. Given a category

C

, a

congruence relation

on

C

species, for each pair of objects XY , an equivalence relation

XY

on

the class of arrows

C

(XY ) which have domain X and codomain Y , such

that

for fg : X

!

Y and h : Y

!

Z, if f

XY

g then hf

XZ

hg

for f : X

!

Y and gh : Y

!

Z, if g

YZ

h then gf

XZ

hf.

Given such a congruence relation

on

C

, one can form the quotient cat-

egory

C

=

which has the same objects as

C

, and arrows X

!

Y are

XY

-equivalence classes of arrows X

!

Y in

C

.

Exercise 4

. Show this and show that there is a functor

C

!

C

=

, which takes

each arrow of

C

to its equivalence class.

h) An example of this is the following (\homotopy"). Given a topological

space X and points xy

2

X, a

path

from x to y is a continuous mapping

f from some closed interval 0a] to X with f(0) = x and f(a) = y. If

f : 0a]

!

X is a path from x to y and g : 0b]

!

X is a path from y to z

there is a path gf : 0a+b]

!

X (dened by gf(t) =

f(t)

t

a

g(t

;

a) else )

from x to z. This makes X into a category, the

path category

of X,

and of course this also denes a functor Top

!

Cat. Now given paths

f : 0a]

!

X, g : 0b]

!

X, both from x to y, one can dene f

xy

g if

3

background image

Categories

there is a continuous map F : A

!

X where A is the area:

(01)

(b1)

F

F

F

F

F

F

F

F

(00)

(a0)

in IR

2

, such that

F(t0) = f(t)

F(t1) = g(t)

F(0s) = x

s

2

01]

F(st) = y

(st) on the segment (b1)

;

(a0)

One can easily show that this is a congruence relation. The quotient of the

path category by this congruence relation is a category called the category

of

homotopy classes

of paths in X.

i) let

C

be a category such that for every pair (XY ) of objects the class

C

(XY ) of arrows from X to Y is a set (such

C

is called

locally small

).

For any object C of

C

then, there is a functor h

C

:

C

!

Set which assigns

to any object C

0

the set

C

(CC

0

). Any arrow f : C

0

!

C

00

gives by

composition a function

C

(CC

0

)

!

C

(CC

00

), so we have a functor. A

functor of this form is called a

representable functor

.

j) Let

C

be a category and C an object of

C

. The

slice category

C

=C has as

objects all arrows g which have codomain C. An arrow from g : D

!

C

to h : E

!

C in

C

=C is an arrow k : D

!

E in

C

such that hk = g. Draw

like:

D

//

k

g

@

@

@

@

@

@

@

E

h

~

~

~

~

~

~

~

C

We say that

this diagram commutes

if we mean that hk = g.

Exercise 5

. Convince yourself that the assignment C

7!

C

=C gives rise to a

functor

C

!

Cat.

k) Remember that for every group (G

) we can form a group (G?) by

putting f ? g = g

f.

For categories the same construction is available: given

C

we can form

a category

C

op

which has the same objects and arrows as

C

, but with

reversed direction so if f : X

!

Y in

C

then f : Y

!

X in

C

op

. To

4

background image

1. Categories and Functors

make it notationally clear, write "f for the arrow Y

!

X corresponding to

f : X

!

Y in

C

. Composition in

C

op

is dened by:

"f"g = gf

Often one reads the term \contravariant functor" in the literature. What I

call functor, is then called \covariant functor". A contravariant functor F

from

C

to

D

inverts the direction of the arrows, so F

1

(f) : F

0

(cod(f))

!

F

0

(dom(f)) for arrows f in

C

. In other words, a contravariant functor

from

C

to

D

is a functor from

C

op

!

D

(equivalently, from

C

to

D

op

).

Exercise 6

. Let

C

be locally small. Show that there is a functor (the \Hom

functor")

C

(

;

;

) :

C

op

C

!

Set, assigning to the pair (AB) of objects of

C

,

the set

C

(AB).

l) Given a partially ordered set (X

) we make a topological space by den-

ing U

X to be open i for all xy

2

X, x

y and x

2

U imply y

2

U

(U is \upwards closed", or an \upper set"). This is a topology, called the

Alexandro topology

w.r.t. the order

.

If (X

) and (Y

) are two partially ordered sets, a function f : X

!

Y is monotone for the orderings if and only if f is continuous for the

Alexandro topologies. This gives an important functor: Pos

!

Top.

Exercise 7

. Show that the construction of the quotient category in example

g) generalizes that of a quotient group by a normal subgroup. That is, re-

gard a group G as a category with one object show that there is a bijection

between congruence relations on G and normal subgroups of G, and that for

a normal subgroup N of G, the quotient category by the congruence relation

corresponding to N, is to the quotient group G=N.

m) \Abelianization". Let Abgp be the category of abelian groups and ho-

momorphisms. For every group G the subgroup GG] generated by all

elements of form aba

;

1

b

;

1

is a normal subgroup. G=GG] is abelian, and

for every group homomorphism : G

!

H with H abelian, there is a

unique homomorphism " : G=GG]

!

H such that the diagram

G

{{

p

v

v

v

v

v

v

v

v

v

?

?

?

?

?

?

?

?

G=GG]

//

H

commutes. Show that this gives a functor: Grp

!

Abgp.

5

background image

Categories

n) \Specialization ordering". Given a topological space X, you can dene an

ordering

s

on X as follows: say x

s

y if for all open sets U, if x

2

U

then y

2

U.

For many spaces,

s

is trivial (in particular when X is T

1

) but in case X

is for example the Alexandro topology on a poset (X

) as in l), then

x

s

y i x

y.

Exercise 8

. If f : X

!

Y is a continuous map of topological spaces then

f is monotone w.r.t. the specialization orderings

s

. This denes a functor

Top

!

Pos.

1.2 Some special objects and arrows

We call an arrow f : A

!

B

mono

(or a monomorphism, or monomorphic) in a

category

C

, if for any other object C and for any pair of arrows gh : C

!

A,

fg = fh implies g = h.

In Set, f is mono i f is an injective function. The same is true for Grp,

Grph, Rng, Preord, Pos,:::

We call an arrow f : A

!

B

epi

(epimorphism, epimorphic) if for any pair

gh : B

!

C, gf = hf implies g = h.

The denition of epi is \dual" to the denition of mono. That is, f is epi in

the category

C

if and only if f is mono in

C

op

, and vice versa. In general, given

a property P of an object, arrow, diagram,:::we can associate with P the dual

property P

op

: the object or arrow has property P

op

in

C

i it has P in

C

op

.

The

duality principle

, a very important, albeit trivial, principle in category

theory, says that any valid statement about categories, involving the proper-

ties P

1

:::P

n

implies the \dualized" statement (where direction of arrows is

reversed) with the P

i

replaced by P

op

i

.

Example

. If gf is mono, then f is mono. From this, \by duality", if fg is epi,

then f is epi.

Exercise 9

. Prove these statements.

In Set, f is epi i f is a surjective function. This holds (less trivially!) also

for Grp, but not for Mon, the category of monoids and monoid homomorphisms:
In Mon, the embedding

N

!

Z

is an epimorphism.

For suppose

Z

//

f

//

g

(Me?) two monoid homomorphisms which agree on the

nonnegative integers. Then

f(

;

1) = f(

;

1) ? g(1) ? g(

;

1) = f(

;

1) ? f(1) ? g(

;

1) = g(

;

1)

6

background image

1. Categories and Functors

so f and g agree on the whole of

Z

.

We say a functor F

preserves

a property P if whenever an object or arrow

(or:::) has P, its F-image does so.

Now a functor does not in general preserve monos or epis: the example of

Mon shows that the forgetful functor Mon

!

Set does not preserve epis.

An epi f : A

!

B is called

split

if there is g : B

!

A such that fg = id

B

(other names: in this case g is called a

section

of f, and f a

retraction

of g).

Exercise 10

. By duality, dene what a split mono is. Prove that every functor

preserves split epis and monos.
f : A

!

B is an

isomorphism

if there is g : B

!

A such that fg = id

B

and gf = id

A

We call g the

inverse

of f (and vice versa, of course) it is unique

if it exists. We also write g = f

;

1

.

Every functor preserves isomorphisms.

Exercise 11

. In Set, every arrow which is both epi and mono is an isomor-

phism. Not so in Mon, as we have seen. Here's another one: let CRng1 be the

category of commutative rings with 1, and ring homomorphisms (preserving 1)

as arrows. Show that the embedding

Z

!

Q

is epi in CRng1.

Exercise 12

.

i) If two of f, g and fg are iso, then so is the third

ii) if f is epi and split mono, it is iso

iii) if f is split epi and mono, f is iso.

A functor F

reects

a property P if whenever the F-image of something (object,

arrow,:::) has P, then that something has.

A functor F :

C

!

D

is called

full

if for every two objects AB of

C

,

F :

C

(AB)

!

D

(FAFB) is a surjection. F is

faithful

if this map is always

injective.

Exercise 13

. A faithful functor reects epis and monos.

An object X is called

terminal

if for any other object Y there is exactly one

morphism Y

!

X in the category. Dually, X is

initial

if for all Y there is

exactly one X

!

Y .

Exercise 14

. A full and faithful functor reects the property of being a termi-

nal (or initial) object.

7

background image

Categories

Exercise 15

. If X and X

0

are two terminal objects, they are

isomorphic

,

that is there exists an isomorphism between them. Same for initial objects.

8

background image

2. Natural transformations

2 Natural transformations

2.1 The Yoneda lemma

A

natural transformation

between two functors FG :

C

!

D

consists of a family

of morphisms (

C

: FC

!

GC)

C

2C

0

indexed by the collection of objects of

C

,

satisfying the following requirement: for every morphism f : C

!

C

0

in

C

, the

diagram

FC

Ff

//

C

GC

Gf

FC

0

//

C

0

GC

0

commutes in

D

(the diagram above is called the naturality square). We say

= (

C

)

C

2C

0

: F

)

G and we call

C

the

component at

C of the natural

transformation .

Given natural transformations : F

)

G and : G

)

H we have a natural

transformation = (

C

C

)

C

: F

)

H, and with this composition there is a

category

D

C

with functors F :

C

!

D

as objects, and natural transformations

as arrows.

One of the points of the naturality square condition in the denition of a

natural transformation is given by the following proposition. Compare with the

situation in Set: denoting the set of all functions from X to Y by Y

X

, for any

set Z there is a bijection between functions Z

!

Y

X

and functions Z

X

!

Y

(Set is

cartesian closed

: see chapter 7).

Proposition 2.1

For categories

C

,

D

and

E

there is a bijection:

Cat(

E

C

D

)

!

Cat(

E

D

C

)

Proof

. Given F :

E

C

!

D

dene for every object E of

E

the functor

F

E

:

C

!

D

by F

E

(C) = F(EC) for f : C

!

C

0

let F

E

(f) = F(id

E

f) :

F

E

(C) = F(EC)

!

F(EC

0

) = F

E

(C

0

)

Given g : E

!

E

0

in

E

, the family (F(gid

C

) : F

E

(C)

!

F

E

0

(C))

C

2C

0

is a

natural transformation: F

E

)

F

E

0

. So we have a functor F

7!

F

(

;

)

:

E

!

D

C

.

Conversely, given a functor G :

E

!

D

C

we dene a functor ~G :

E

C

!

D

on

objects by ~G(EC) = G(E)(C), and on arrows by ~G(gf) = G(g)

C

0

G(E)(f) =

9

background image

Categories

G(E

0

)(f)G(g)

C

:

G(E)(C) = ~G(EC)

G

(

E

)(

f

)

//

G

(

g

)

C

~G(E

0

C) = G(E

0

)(C)

G

(

E

0

)(

f

)

~G(EC

0

)

//

G

(

g

)

C

0

~G(E

0

C

0

) = G(E

0

)(C

0

)

Exercise 16

. Write out the details. Check that ~G as just dened, is a functor,

and that the two operations

Cat(

E

C

D

)

//

Cat(

E

D

C

)

oo

are inverse to each other.
An important example of natural transformations arises from the functors h

C

:

C

op

!

Set (see example i) in the preceding chapter) dened on objects by

h

C

(C

0

) =

C

(C

0

C) and on arrows f : C

00

!

C

0

so that h

C

(f) is composition

with f:

C

(C

0

C)

!

C

(C

00

C).

Given g : C

1

!

C

2

there is a natural transformation

h

g

: h

C

1

)

h

C

2

whose components are composition with g.

Exercise 17

. Spell this out.

We have, in other words, a functor

h

(

;

)

:

C

!

Set

C

op

This functor is also often denoted by Y and listens to the name

Yoneda embed-

ding

.

An embedding is a functor which is full and faithful and injective on objects.

That Y is injective on objects is easy to see, because id

C

2

h

C

(C) for each object

C, and id

C

is in no other set h

D

(E) that Y is full and faithful follows from the

famous

Proposition 2.2 (Yoneda lemma)

For every object

F

of Set

C

op

and every

object

C

of

C

, there is a bijection

f

CF

: Set

C

op

(h

C

F)

!

F(C)

. Moreover, this

bijection is

natural

in

C

and

F

in the following sense: given

g : C

0

!

C

in

C

10

background image

2. Natural transformations

and

: F

)

F

0

in

Set

C

op

, the diagram

Set

C

op

(h

C

F)

Set

C

op

(

g

)

//

f

CF

F(C)

C

0

F

(

g

)=

F

0

(

g

)

C

Set

C

op

(h

C

0

F

0

)

//

f

C

0

F

0

F

0

(C

0

)

commutes in

Set

.

Proof

. For every object C

0

of

C

, every element f of h

C

(C

0

) =

C

(C

0

C) is equal

to id

C

f which is h

C

(f)(id

C

).

If = (

C

0

j

C

0

2

C

0

) is a natural transformation: h

C

)

F then,

C

0

(f)

must be equal to F(f)(

C

(id

C

)). So is completely determined by

C

(id

C

)

2

F(C) and conversely, any element of F(C) determines a natural transformation

h

C

)

F.

Given g : C

0

!

C in

C

and : F

)

F

0

in Set

C

op

, the map Set

C

op

(g) sends

the natural transformation = (

C

00

j

C

00

2

C

0

) : h

C

)

F to = (

C

00

j

C

00

2

C

0

)

where

C

00

: h

C

0

(C

00

)

!

F

0

(C

00

) is dened by

C

00

(h : C

00

!

C

0

) =

C

00

(

C

00

(gh))

Now

f

C

0

F

0

() =

C

0

(id

C

0

)

=

C

0

(

C

0

(g))

=

C

0

(F(g)(

C

(id

C

)))

= (

C

0

F(g))(f

CF

())

which proves the naturality statement.

Corollary 2.3

The functor

Y :

C

!

Set

C

op

is full and faithful.

Proof

. Immediate by the Yoneda lemma, since

C

(CC

0

)

= h

C

0

(C)

= Set

C

op

(h

C

h

C

0

)

and this bijection is induced by Y .
The use of the Yoneda lemma is often the following. One wants to prove that

objects A and B of

C

are isomorphic. Suppose one can show that for every

object X of

C

there is a bijection f

X

:

C

(XA)

!

C

(XB) which is natural in

11

background image

Categories

X i.e. given g : X

0

!

X in

C

one has that

C

(XA)

C

(

g

id

A

)

//

f

X

C

(XB)

C

(

g

id

B

)

C

(X

0

A)

//

f

X

0

C

(X

0

B)

commutes.

Then one can conclude that A and B are isomorphic in

C

for, from what

one has just shown it follows that h

A

and h

B

are isomorphic objects in Set

C

op

that is, Y (A) and Y (B) are isomorphic. Since Y is full and faithful, A and B

are isomorphic by the following exercise:

Exercise 18

. Check: if F :

C

!

D

is full and faithful, and F(A) is iso-

morphic to F(B) in

D

, then A is isomorphic to B in

C

.

Exercise 19

. Suppose objects A and B are such that for every object X

in

C

there is a bijection f

X

:

C

(AX)

!

C

(BX), naturally in a sense you dene

yourself. Conclude that A and B are isomorphic (hint: duality + the previous).
This argument can be carried further. Suppose one wants to show that two

functors FG :

C

!

D

are isomorphic as objects of

D

C

. Let's rst spell out

what this means:

Exercise 20

. Show that F and G are isomorphic in

D

C

if and only if there is

a natural transformation : F

)

G such that all components

C

are isomor-

phisms (in particular, if is such, the family ((

C

)

;

1

j

C

2

C

0

) is also a natural

transformation G

)

F).

Now suppose one has for each C

2

C

0

and D

2

D

0

a bijection

D

(DFC)

=

D

(DGC)

natural in D and C. This means that the objects h

FC

and h

GC

of Set

D

op

are

isomorphic, by isomorphisms which are natural in C. By full and faithfulness

of Y , FC and GC are isomorphic in

D

by isomorphisms natural in C which

says exactly that F and G are isomorphic as objects of

D

C

.

2.2 Examples of natural transformations

a) Let M and N be two monoids, regarded as categories with one object as in

chapter 1. A functor F : M

!

N is then just the same as a homomorphism

12

background image

2. Natural transformations

of monoids. Given two such, say FG : M

!

N, a natural transformation

F

)

G is (given by) an element n of N such that nF(x) = G(x)n for all

x

2

M

b) Let P and Q two preorders, regarded as categories. A functor P

!

Q

is a monotone function, and there exists a unique natural transformation

between two such, F

)

G, exactly if F(x)

G(x) for all x

2

P.

Exercise 21

. In fact, show that if

D

is a preorder and the category

C

is

small

,

i.e. the classes

C

0

and

C

1

are sets, then the functor category

D

C

is a preorder.

c) Let U : Grp

!

Set denote the forgetful functor, and F : Set

!

Grp the

free functor (see chapter 1). There are natural transformations " : FU

)

id

Grp

and : id

Set

)

UF.

Given a group G, "

G

takes the string = g

1

:::g

n

to the product g

1

g

n

(here, the \formal inverses" g

;

1

i

are interpreted as the real inverses in G!).

Given a set A,

A

(a) is the singleton string a.

d) Let i : Abgp

!

Grp be the inclusion functor and r : Grp

!

Abgp the

abelianization functor dened in example m) in chapter 1. There is " :

ri

)

id

Abgp

and : id

Grp

)

ir.

The components

G

of are the quotient maps G

!

G=GG] the com-

ponents of " are isomorphisms.

e) There are at least two ways to associate a category to a set X: let F(X)

be the category with as objects the elements of X, and as only arrows

identities (a category of the form F(X) is called

discrete

and G(X) the

category with the same objects but with exactly one arrow f

xy

: x

!

y

for each pair (xy) of elements of X (We might call G(X) an

indiscrete

category

).

Exercise 22

. Check that F and G can be extended to functors: Set

!

Cat and

describe the natural transformation : F

)

G which has, at each component,

the identity function on objects.

f) Every class of arrows of a category

C

can be viewed as a natural transfor-

mation. Suppose S

C

1

. Let F(S) be the discrete category on S as in

the preceding example. There are the two functors domcod : F(S)

!

C

,

giving the domain and the codomain, respectively. For every f

2

S we

have f : dom(f)

!

cod(f), and the family (f

j

f

2

S) denes a natural

transformation: dom

)

cod.

g) Let A and B be sets. There are functors (

;

)

A : Set

!

Set and (

;

)

B :

Set

!

Set. Any function f : A

!

B gives a natural transformation

(

;

)

A

)

(

;

)

B.

13

background image

Categories

h) A category

C

is called a

groupoid

if every arrow of

C

is an isomorphism.

Let

C

be a groupoid, and suppose we are given, for each object X of

C

, an

arrow

X

in

C

with domain X.

Exercise 23

. Show that there is a functor F :

C

!

C

in this case, which

acts on objects by F(X) = cod(

X

), and that = (

X

j

X

2

C

0

) is a natural

transformation: id

C

)

F.

i) Given categories

C

,

D

and an object D of

D

, there is the constant functor

$

D

:

C

!

D

which assigns D to every object of

C

and id

D

to every arrow

of

C

.

Every arrow f : D

!

D

0

gives a natural transformation $

f

: $

D

)

$

D

0

dened by ($

f

)

C

= f for each C

2

C

0

.

j) Let

P

(X) denote the power set of a set X: the set of subsets of X. The

powerset operation can be extended to a functor

P

: Set

!

Set. Given a

function f : X

!

Y dene

P

(f) by

P

(f)(A) = fA], the image of A

X

under f.

There is a natural transformation : id

Set

)

P

such that

X

(x) =

f

x

g

2

P

(X) for each set X.

There is also a natural transformation :

P

P

)

P

. Given A

2

P

P

(X),

so A is a set of subsets of X, we take its union

S

(A) which is a subset of

X. Put

X

(A) =

S

(A).

2.3 Equivalence of categories an example

As will become clear in the following chapters, equality between objects plays

only a minor role in category theory. The most important categorical notions

are only dened \up to isomorphism". This is in accordance with mathematical

practice and with common sense: just renaming all elements of a group does

not give you really another group.

We have already seen one example of this: the property of being a terminal

object denes an object up to isomorphism. That is, any two terminal objects

are isomorphic. There is, in the language of categories, no way of distinguishing

between two isomorphic objects, so this is as far as we can get.

However, once we also consider functor categories, it turns out that there is

another relation of \sameness" between categories, weaker than isomorphism of

categories, and yet preserving all \good" categorical properties. Isomorphism of

categories

C

and

D

requires the existence of functors F :

C

!

D

and G :

D

!

C

such that FG = id

D

and GF = id

C

but bearing in mind that we can't really say

meaningfulthings about equality between objects, we may relax the requirement

by just asking that FG is

isomorphic

to id

D

in the functor category

D

D

(and

14

background image

2. Natural transformations

the same for GF) doing this we arrive at the notion of

equivalence of categories

,

which is generally regarded as the proper notion of sameness.

So two categories

C

and

D

are

equivalent

if there are functors F :

C

!

D

,

G :

D

!

C

and natural transformations : id

C

)

GF and : id

D

)

FG whose

components are all isomorphisms. F and G are called

pseudo inverses

of each

other. A functor which has a pseudo inverse is also called an

equivalence of

categories

.

Exercise 24

. Show that a category is equivalent to a discrete category if and

only if it is a groupoid and a preorder.
In this section I want to give an important example of an equivalence of cat-

egories: the so-called \Lindenbaum-Tarski duality between Set and Complete

Atomic Boolean Algebras". A duality between categories

C

and

D

is an equiv-

alence between

C

op

and

D

(equivalently, between

C

and

D

op

).

We need some denitions. A

lattice

is a partially ordered set in which every

two elements xy have a least upper bound (or join) x

_

y and a greatest lower

bound (or meet) x

^

y moreover, there exist a least element 0 and a greatest

element 1.

Such a lattice is called a

Boolean algebra

if every element x has a

complement

:

x, that is, satisfying x

_

:

x = 1 and x

^

:

x = 0 and the lattice is

distributive

,

which means that x

^

(y

_

z) = (x

^

y)

_

(x

^

z) for all xyz.

In a Boolean algebra, complements are unique, for if both y and z are com-

plements of x, then

y = y

^

1 = y

^

(x

_

z) = (y

^

x)

_

(y

^

z) = 0

_

(y

^

z) = y

^

z

so y

z similarly, z

y so y = z. This is a non-example:

1

?

?

?

?

?

?

?

x

/

/

/

/

/

/

/

/

/

/

/

/

/

/

z

y

;

;

;

;

;

;

;

0

It is a lattice, and every element has a complement, but it is not distributive

(check!).

A Boolean algebra B is

complete

if every subset A of B has a least upper

bound

W

A and a greatest lower bound

V

A.

15

background image

Categories

An

atom

in a Boolean algebra is an element x such that 0 < x but for no

y we have 0 < y < x. A Boolean algebra is atomic if every x is the join of the

atoms below it:

x =

_

f

a

j

a

x and a is an atom

g

The category CABool is dened as follows: the objects are complete atomic

Boolean algebras, and the arrows are complete homomorphisms, that is: f :

B

!

C is a complete homomorphism if for every A

B,

f(

_

A) =

_

f

f(a)

j

a

2

A

g

and f(

^

A) =

^

f

f(a)

j

a

2

A

g

Exercise 25

. Show that 1 =

V

and 0 =

W

. Conclude that a complete

homomorphism preserves 1, 0 and complements.

Exercise 26

. Show that

V

A =

:

W

f:

a

j

a

2

A

g

and conclude that if a function

preserves all

W

's, 1 and complements, it is a complete homomorphism.

Theorem 2.4

The category

CABool

is equivalent to

Set

op

.

Proof

. For every set X,

P

(X) is a complete atomic Boolean algebra and if

f : Y

!

X is a function, then f

;

1

:

P

(X)

!

P

(Y ) which takes, for each subset

of X, its inverse image under f, is a complete homomorphism. So this denes

a functor F : Set

op

!

CABool.

Conversely, given a complete atomic Boolean algebra B, let G(B) be the set

of atoms of B. Given a complete homomorphism g : B

!

C we have a function

G(g) : G(C)

!

G(B) dened by: G(g)(c) is the unique b

2

G(B) such that

c

g(b). This is well-dened: rst, there is an atom b with c

g(b) because

1

B

=

W

G(B) (B is atomic), so 1

C

= g(1

B

) =

W

f

g(b)

j

b is an atom

g

and:

Exercise 27

. Prove: if c is an atom and c

W

A, then there is a

2

A with

c

a (hint: prove for all ab that a

^

b = 0

,

a

:

b, and prove for ac with c

atom: c

6

a

,

a

:

c).

Secondly, the atom b is unique since c

g(b) and c

g(b

0

) means c

g(b)

^

g(b

0

) = g(b

^

b

0

) = g(0) = 0.

So we have a functor G : CABool

!

Set

op

.

Now the atoms of the Boolean algebra

P

(X) are exactly the singleton sub-

sets of X, so GF(X) =

ff

x

gj

x

2

X

g

which is clearly isomorphic to X. On the

other hand, FG(B) =

P

(

f

b

2

B

j

b is an atom

g

). There is a map from FG(B)

to B which sends each set of atoms to its least upper bound in B, and this map

is an isomorphism in CABool.

Exercise 28

. Prove the last statement: that the map from FG(B) to B,

dened in the last paragraph of the proof, is an isomorphism.

16

background image

3. (Co)cones and (co)limits

3 (Co)cones and (co)limits

3.1 Limits

Given a functor F :

C

!

D

, a

cone

for F consists of an object D of

D

together

with a natural transformation : $

D

)

F ($

D

is the constant functor with

value D). In other words, we have a family (

C

: D

!

F(C)

j

C

2

C

0

), and the

naturality requirement in this case means that for every arrow f : C

!

C

0

in

C

,

D

||

C

z

z

z

z

z

z

z

z

""

C

0

E

E

E

E

E

E

E

E

F(C)

//

F

(

f

)

F(C

0

)

commutes in

D

(this diagram explains, I hope, the name \cone"). Let us denote

the cone by (D). D is called the

vertex

of the cone.

A

map of cones

(D)

!

(D

0

0

) is a map g : D

!

D

0

such that

0

C

g =

C

for all C

2

C

0

.

Clearly, there is a category Cone(F) which has as objects the cones for F

and as morphisms maps of cones.

A

limiting cone

for F is a terminal object in Cone(F). Since terminal objects

are unique up to isomorphism, as we have seen, any two limiting cones are

isomorphic in Cone(F) and in particular, their vertices are isomorphic in

D

.

A functor F :

C

!

D

is also called a

diagram

in

D

of type

C

, and

C

is the

index category

of the diagram.

Let us see what it means to be a limiting cone, in some simple, important

cases.

i) A limiting cone for the unique functor ! :

0

!

D

(

0

is the empty category)

\is" a terminal object in

D

. For every object D of

D

determines, together

with the empty family, a cone for !, and a map of cones is just an arrow

in

D

. So Cone(!) is isomorphic to

D

.

ii) Let

2

be the discrete category with two objects xy. A functor

2

!

D

is

just a pair

h

AB

i

of objects of

D

, and a cone for this functor consists of

an object C of

D

and two maps

C

//

A

B

@

@

@

@

@

@

@

A

B

since there are no nontrivial

arrows in

2

.

(C(

A

B

)) is a limiting cone for

h

AB

i

i the following holds: for any

object D and arrows f : D

!

A, g : D

!

B, there is a unique arrow

17

background image

Categories

h : D

!

C such that

C

A

B

0

0

0

0

0

0

0

0

0

0

0

0

0

0

D

>>

h

~

~

~

~

//

f

''

g

P

P

P

P

P

P

P

P

P

P

P

P

P

P

A

B

commutes. In other words, there is, for any D, a 1-1 correspondence

between maps D

!

C and pairs of maps

D

~

~

~

~

~

~

~

@

@

@

@

@

@

@

A

B

This is

the property of a

product

a limiting cone for

h

AB

i

is therefore called a

product cone, and usually denoted:

A

B

||

A

x

x

x

x

x

x

x

x

x

##

B

F

F

F

F

F

F

F

F

F

A

B

The arrows

A

and

B

are called

projections

.

iii) Let

^2

denote the category x

//

a

//

b

y . A functor

^2

!

D

is the same thing

as a parallel pair of arrows A

//

f

//

g

B in

D

I write

h

fg

i

for this functor.

A cone for

h

fg

i

is:

D

A

~

~

~

~

~

~

~

B

@

@

@

@

@

@

@

A

//

f

//

g

B

But

B

= f

A

= g

A

is already dened from

A

, so giving a cone is the

same as giving a map

A

: D

!

A such that f

A

= g

A

. Such a cone is

limiting i for any other map h : C

!

A with fh = gh, there is a unique

k : C

!

D such that h =

A

k.

We call

A

, if it is limiting, an

equalizer

of the pair fg, and the diagram

D

//

A

A

//

f

//

g

B an equalizer diagram.

In Sets, an equalizer of fg is isomorphic (as a cone) to the inclusion

of

f

a

2

A

j

f(a) = g(a)

g

into A. In categorical interpretations of logical

18

background image

3. (Co)cones and (co)limits

systems (see chapters 4 and 7), equalizers are used to interpret

equality

between terms

.

Exercise 29

. Show that every equalizer is a monomorphism.

Exercise 30

. If E

//

e

X

//

f

//

g

Y is an equalizer diagram, show that e

is an isomorphism if and only if f = g.

Exercise 31

. Show that in Set, every monomorphism ts into an equalizer

diagram.

iv) Let J denote the category

y

b

x

//

a

z

A functor F : J

!

D

is specied

by giving two arrows in

D

with the same codomain, say f : X

!

Z,

g : Y

!

Z. A limit for such a functor is given by an object W together

with projections

W

//

p

Y

p

X

Y

X

satisfying fp

X

= gp

Y

, and such that,

given any other pair of arrows:

V

//

r

s

Y

X

with gr = fs, there is a

unique arrow V

!

W such that

V

s

0

0

0

0

0

0

0

0

0

0

0

0

0

0

A

A

A

A

A

A

A

A

((

r

P

P

P

P

P

P

P

P

P

P

P

P

P

P

P

W

p

X

//

p

Y

Y

g

X

//

f

Z

commutes.

The diagram

W

p

X

//

p

Y

Y

g

X

//

f

Z

19

background image

Categories

is called a

pullback diagram

. In Set, the pullback cone for fg is isomorphic

to

f

(xy)

2

X

Y

j

f(x) = g(y)

g

with the obvious projections.

We say that a category

D

has binary products

(equalizers, pullbacks) i every

functor

2

!

D

(

^2

!

D

, J

!

D

, respectively) has a limiting cone. Some

dependencies hold in this context:

Proposition 3.1

If a category

D

has a terminal object and pullbacks, it has

binary products and equalizers.

If

D

has binary products and equalizers, it has pullbacks.

Proof

. Let 1 be the terminalobject in

D

given objects X and Y , if

C

p

Y

//

p

X

X

Y

//

1

is a pullback diagram, then

C

//

p

X

p

Y

X

Y

is a product cone.

Given a product cone

A

B

//

A

B

A

B

and maps

X

//

f

g

A

B

we write

X

h

fg

i

!

A

B for the unique factorization through the product. Write also

: Y

!

Y

Y for

h

id

Y

id

Y

i

.

Now given fg : X

!

Y , if

E

//

e

X

h

fg

i

Y

//

Y

Y

is a pullback diagram, then E

//

e

X

//

f

//

g

Y is an equalizer diagram. This

proves the rst statement.

As for the second: given

X

f

Y

//

g

Z

let E

//

e

X

Y

//

f

X

//

g

Y

Z be an

20

background image

3. (Co)cones and (co)limits

equalizer then

E

Y

e

//

X

e

X

f

Y

//

g

Z

is a pullback diagram.

Exercise 32

. Let

A

a

//

b

B

f

X

//

g

Y

a pullback diagram with f mono. Show that a is also mono. Also, if f is iso

(an isomorphism), so is a.

Exercise 33

. Given:

A

a

//

b

B

f

//

c

C

d

X

//

g

Y

//

h

Z

a) if both squares are pullback squares, then so is the composite square

A

a

//

cb

C

d

X

//

hg

Z

b) If the right hand square and the composite square are pullbacks, then so

is the left hand square.

Exercise 34

. f : A

!

B is a monomorphism if and only if

A

id

A

//

id

A

A

f

A

//

f

B

is a pullback diagram.

21

background image

Categories

A monomorphism f : A

!

B which ts into an equalizer diagram

A

//

f

B

//

g

//

h

C

is called a

regular mono

.

Exercise 35

. If

A

b

//

a

X

g

B

//

f

Y

is a pullback and g is regular mono, so is b.

Exercise 36

. If f is regular mono and epi, f is iso. Every split mono is regular.

Exercise 37

. Give an example of a category in which not every mono is regular.

Exercise 38

. In Grp, every mono is regular This is not so easy].

Exercise 39

. In Pos, every mono is regular.

Exercise 40

. If a category

D

has binary products and a terminal object,

it has

all nite products

, i.e. limiting cones for every functor into

D

from a nite

discrete category.

Exercise 41

. Suppose

C

has binary products and suppose for every ordered

pair (AB) of objects of

C

a product cone

A

B

B

//

A

A

B

has been chosen.

a) Show that there is a functor:

C

C

;;

!

C

(the product functor) which

sends each pair (AB) of objects to A

B and each pair of arrows (f :

A

!

A

0

g : B

!

B

0

) to f

g =

h

f

A

g

B

i

.

b) From a), there are functors:

C

C

C

//

(

;;

)

;

//

;

(

;;

)

C

22

background image

3. (Co)cones and (co)limits

sending (ABC) to (A

B)

C

A

(B

C) Show that there is a natural trans-

formation a = (a

ABC

j

ABC

2

C

0

) from (

;

;

)

;

to

;

(

;

;

)

such that for any four objects ABCD of

C

:

((A

B)

C)

D

a

AB C

id

D

//

a

AB CD

(A

B)

(C

D)

a

AB C D

(A

(B

C))

D

))

a

AB CD

T

T

T

T

T

T

T

T

T

T

T

T

T

T

T

A

(B

(C

D))

A

((B

C)

D)

55

id

A

a

BCD

j

j

j

j

j

j

j

j

j

j

j

j

j

j

j

commutes (This diagram is called \MacLane's pentagon").

A functor F :

C

!

D

is said to

preserve limits of type

E

if for all functors M :

E

!

C

, if (D) is a limiting cone for M in

C

, then (FDF = (F(

E

)

j

E

2

E

0

))

is a limiting cone for FM in

D

.

So, a functor F :

C

!

D

preserves binary products if for every product dia-

gram

A

B

A

//

B

B

A

its F-image

F(A

B)

F

(

A

)

//

F

(

B

)

F(B)

F(A)

is again a product

diagram. Similarly for equalizers and pullbacks.

Some more terminology: F is said to

preserve all nite limits

if it preserves

limits of type

E

for every nite

E

. A category which has all nite limits is called

lex

(

left exact

),

cartesian

or

nitely complete

.

A category is called

complete

if it has limits of type

E

for all small

E

.

In general, limits over large (i.e. not small) diagrams do not exist. For ex-

ample in Set, there is a limiting cone for the identity functor Set

!

Set (its

vertex is the empty set), but not for the inclusion functor of the subcategory of

all nonempty sets into Set.

Exercise 42

. If a category

C

has equalizers, it has

all nite equalizers

: for

every category

E

of the form

X

//

f

1

//

f

n

...

Y

every functor

E

!

C

has a limiting cone.

23

background image

Categories

Exercise 43

. Suppose F :

C

!

D

preserves equalizers (and

C

has equaliz-

ers) and reects isomorphisms. Then F is faithful.

Exercise 44

. Let

C

be a category with nite limits. Show that for every

object C of

C

, the slice category

C

=C (example j) of 1.1) has binary products:

the vertex of a product diagram for two objects D

!

C, D

0

!

C is D

00

!

C

where

D

00

//

D

D

0

//

C

is a pullback square in

C

.

3.2 Limits by products and equalizers

In Set, every small diagram has a limit given a functor F :

E

!

Set with

E

small, there is a limiting cone for F in Set with vertex

f

(x

E

)

E

2E

0

2

Y

E

2E

0

F(E)

j8

E

f

!

E

0

2

E

1

(F(f)(x

E

) = x

E

0

)

g

So in Set, limits are equationally dened subsets of suitable products. This

holds in any category:

Proposition 3.2

Suppose

C

has all small products (including the empty prod-

uct, i.e. a terminal object 1) and equalizers then

C

has all small limits.

Proof

. Given a set I and an I-indexed family of objects (A

i

j

i

2

I) of

C

, we

denote the product by

Q

i

2

I

A

i

and projections by

i

:

Q

i

2

I

A

i

!

A

i

an arrow

f : X

!

Q

i

2

I

A

i

which is determined by the compositions f

i

=

i

f : X

!

A

i

,

is also denoted (f

i

j

i

2

I).

Now given

E

!

C

with

E

0

and

E

1

sets, we construct

E

//

e

Q

i

2E

0

F(i)

//

(

cod

(u)

j

u

2E

1

)

//

(

F

(

u

)

dom

(u)

j

u

2E

1

)

Q

u

2E

1

F(cod(u))

in

C

as an equalizer diagram. The family (

i

=

i

e : E

!

F(i)

j

i

2

E

0

) is a

natural transformation $

E

)

F because, given an arrow u

2

E

1

, say u : i

!

j,

we have that

E

}}

i

e

{

{

{

{

{

{

{

{

!!

j

e

C

C

C

C

C

C

C

C

F(i)

//

F

(

u

)

F(j)

24

background image

3. (Co)cones and (co)limits

commutes since F(u)

i

e = F(u)

dom(

u

)

e =

cod(

u

)

e =

j

e.

So (E) is a cone for F, but every other cone (D) for F gives a map

d : D

!

Q

i

2E

0

F(i) equalizing the two horizontal arrows so factors uniquely

through E.

Exercise 45

. Check that \small" in the statement of the proposition, can

be replaced by \nite": if

C

has all nite products and equalizers,

C

is nitely

complete.

3.3 Colimits

The dual notion of limit is colimit. Given a functor F :

E

!

C

there is clearly a

functor F

op

:

E

op

!

C

op

which does \the same" as F. We say that a

colimiting

cocone

for F is a limiting cone for F

op

.

So: a cocone for F :

E

!

C

is a pair (D) where : F

)

$

D

and a

colimiting cocone is an initial object in the category Cocone(F).

Examples

i) a colimiting cocone for ! :

0

!

C

\is" an initial object of

C

ii) a colimiting cocone for

h

AB

i

:

2

!

C

is a

coproduct

of A and B in

C

:

usually denoted A + B or A

t

B there are

coprojections

or

coproduct

inclusions

A

##

A

F

F

F

F

F

F

F

F

F

B

//

B

A

t

B

with the property that, given any pair of arrows A

f

!

C, B

g

!

C there is a

unique map

f

g

: A

t

B

!

C such that f =

f

g

A

and g =

f

g

B

iii) a colimiting cocone for A

//

f

//

g

B (as functor

^2

!

C

) is given by a map

B

c

!

C satisfying cf = cg, and such that for any B

h

!

D with hf = hg

there is a unique C

h

0

!

D with h = h

0

c. c is called a

coequalizer

for f and

g the diagram A

//

//

B

//

C a coequalizer diagram.

Exercise 46

. Is the terminology \coproduct inclusions" correct? That is, it

suggests they are monos. Is this always the case?
In Set, the coproduct of X and Y is the disjoint union (

f

0

g

X)

(

f

1

g

Y )

25

background image

Categories

of X and Y . The coequalizer of X

//

f

//

g

Y is the quotient map Y

!

Y=

where

is the equivalence relation generated by

y

y

0

i there is x

2

X with f(x) = y and g(x) = y

0

The dual notion of pullback is

pushout

. A pushout diagram is a colimiting

cocone for a functor ;

!

C

where ; is the category

x

//

y

z

. Such a diagram

is a square

X

g

//

f

Y

a

Z

//

b

P

which commutes and such that, given

Y

?

?

?

?

?

?

?

Z

//

Q

with f = g, there is a

unique P

p

!

Q with = pa and = pb. In Set, the pushout of X

f

!

Y and

X

g

!

Z is the coproduct Y

t

Z where the two images of X are identied:

X

Z

X

X

Y

X

H

H

H

j

*

*

H

H

H

j

Exercise 47

. Give yourself, in terms of X

f

!

Y and X

g

!

Z, a formal denition

of a relation R on Y

t

Z such that the pushout of f and g is Y

t

Z=

,

being

the equivalence relation generated by R.
One can now dualize every result and exercise from the section on limits:

26

background image

3. (Co)cones and (co)limits

Exercise 48

. f is epi if and only if

f

//

f

id

//

id

is a pushout diagram.

Exercise 49

. Every coequalizer is an epimorphism if e is a coequalizer of

f and g, then e is iso i f = g

Exercise 50

. If

C

has an initial object and pushouts,

C

has binary coproducts

and coequalizers if

C

has binary coproducts and coequalizers,

C

has pushouts.

Exercise 51

. If

a

//

f

//

is a pushout diagram, then a epi implies f epi,

and a regular epi (i.e. a coequalizer) implies f regular epi.

Exercise 52

. The composition of two puhout squares is a pushout if both

the rst square and the composition are pushouts, the second square is.

Exercise 53

. If

C

has all small (nite) coproducts and coequalizers,

C

has

all small (nite) colimits.

Exercise 54

. In Pos, X

f

!

Y is a regular epi if and only if for all yy

0

in

Y :

y

y

0

,

9

x

2

f

;

1

(y)

9

x

0

2

f

;

1

(y

0

):x

x

0

Show by an example that not every epi is regular in Pos.

Exercise 55

. In Grp, every epi is regular.

27

background image

Categories

28

background image

4. A little piece of categorical logic

4 A little piece of categorical logic

One of the major achievements of category theory in mathematical logic and

in computer science, has been a unied treatment of semantics for all kinds of

logical systems and term calculi which are the basis for programming languages.

One can say that mathematical logic, seen as the study of classical rst

order logic, rst started to be a real subject with the discovery, by G'odel,

of the

completeness theorem

for set-theoretic interpretations: a sentence ' is

provable if and only if ' is true in all possible interpretations. This unites the

two approaches to logic: proof theory and model theory, makes logic accessible

for mathematical methods and enables one to give nice and elegant proofs of

proof theoretical properties by model theory (for example, the Beth and Craig

denability and interpolation theorems).

However the completeness theorem needs generalization once one considers

logics, such as intuitionistic logic (which does not admit the principle of excluded

middle), minimal logic (which has no negation) or modal logic (where the logic

has an extra operator, expressing \necessarily true"), for which the set-theoretic

interpretation is not complete. One therefore comes with a general denition of

\interpretation" in a category

C

of a logical system, which generalizes Tarski's

truth denition: this will then be the special case of classical logic and the

category Set.

In this chapter I treat, for reasons of space, only a fragment of rst order

logic: coherent logic. On this fragment the valid statements of classical and

intuitionistic logic coincide.

For an interpretation of a term calculus like the -calculus, which is of

paramount importance in theoretical computer science, the reader is referred

to chapter 7.

4.1 Regular categories and subobjects

Denition 4.1

A category

C

is called

regular

if the following conditions hold:

a)

C

has all nite limits

b) For every arrow

f

, if

Z

p

1

//

p

0

X

f

X

//

f

Y

is a pullback (then

Z

//

p

0

//

p

1

X

is called the

kernel pair

of

f

), the coequal-

izer of

p

0

p

1

exists

29

background image

Categories

c) Regular epimorphisms (coequalizers) are

stable under pullback

, that is: in

a pullback square

a

//

f

//

if

f

is regular epi, so is

a

.

Exercise 56

. Set is regular. Prove that Pos is regular. Show that Top is not

regular the case of Top may cause you some trouble don't worry].

Proposition 4.2

In a regular category, every arrow

f : X

!

Y

can be factored

as

f = me : X

e

!

E

m

!

Y

where

e

is regular epi and

m

is mono and this

factorization is unique in the sense that if

f

is also

m

0

e

0

: X

e

0

!

E

0

m

0

!

Y

with

m

0

mono and

e

0

regular epi, there is an isomorphism

: E

!

E

0

such that

e = e

0

and

m

0

= m

.

Proof

. Given f : X

!

Y we let X

e

!

E be the coequalizer of the kernel pair

Z

//

p

0

//

p

1

X of f. Since fp

0

= fp

1

there is a unique m : E

!

Y such that

f = me. By construction e is regular epi we must show that m is mono, and

the uniqueness of the factorization.

Suppose mg = mh for gh : W

!

E we prove that g = h. Let

V

h

q

0

q

1

i

//

a

W

h

gh

i

X

X

//

e

e

E

E

be a pullback square. Then

fq

0

= meq

0

= mga = mha = meq

1

= fq

1

so there is a unique arrow V

b

!

Z such that

h

q

0

q

1

i

=

h

p

0

p

1

i

b : V

!

X

X

(because of the kernel pair property). It follows that

ga = eq

0

= ep

0

b = ep

1

b = eq

1

= ha

I claim that a is epi, so it follows that g = h. It is here that we use the

requirement that regular epis are stable under pullback. Now e

e : X

X

!

E

E is the composite

X

X

e

id

X

!

E

X

id

E

e

!

E

E

30

background image

4. A little piece of categorical logic

and both maps are regular epis since both squares

X

X

0

//

e

id

X

E

X

0

X

//

e

E

and

E

X

1

//

id

E

e

E

E

1

X

//

e

E

are pullbacks. The map a, being the pullback of a composite of regular epis, is

then itself the composite of regular epis (check this!), so in particular epi.

This proves that m is mono, and we have our factorization.

As to uniqueness, suppose we had another factorization f = m

0

e

0

with m

0

mono and e

0

regular epi. Then m

0

e

0

p

0

= fp

0

= fp

1

= m

0

e

0

p

1

so since m

0

mono,

e

0

p

0

= e

0

p

1

. Because e is the coequalizer of p

0

and p

1

, there is a unique :

//

e

e

0

?

?

?

?

?

?

?

Then m

0

e = m

0

e

0

= f = me so since e epi, m = m

0

.

Now e

0

: X

!

E

0

is a coequalizer say U

//

k

//

l

X

//

e

0

E

0

is a coequalizer

diagram. Then it follows that ek = el (since mek = m

0

e

0

k = m

0

e

0

l = mel and

m mono) so there is a unique :

//

e

e

0

?

?

?

?

?

?

?

OO

Then me = me

0

= me since m

mono and e epi, = id

E

. Similarly, = id

E

0

. So is the required isomor-

phism.

Exercise 57

. Check this detail: in a regular category

C

, if

//

a

//

b

is a

pullback diagram and b = c

1

c

2

with c

1

and c

2

regular epis, then a = a

1

a

2

for

some regular epis a

1

a

2

.

Subobjects

. In any category

C

we dene a

subobject

of an object X to be

an equivalence class of monomorphisms Y

m

!

X, where Y

m

!

X is equivalent to

Y

0

m

0

!

X if there is an isomorphism : Y

!

Y

0

with m

0

= m (then m

;

1

= m

0

follws). We say that Y

m

!

X represents a

smaller

subobject than Y

0

m

0

!

X if

there is : Y

!

Y

0

with m

0

= m ( not necessarily iso but check that is

always mono).

The notion of subobject is the categorical version of the notion of subset in

set theory. In Set, two injective functions represent the same subobject i their

images are the same one can therefore identify subobjects with subsets. Note

31

background image

Categories

however, that in Set we have a \canonical"

choice

of representative for each

subobject: the inclusion of the subset to which the subobject corresponds. This

choice is not always available in general categories.

We have a partial order Sub(X) of subobjects of X, ordered by the smaller-

than relation.

Proposition 4.3

In a category

C

with nite limits, each pair of elements of

Sub

(X)

has a greatest lower bound. Moreover, Sub

(X)

has a largest element.

Proof

. If Y

m

!

X and Y

0

m

0

!

X represent two subobjects of X and

Z

//

Y

m

Y

0

//

m

0

X

is a pullback, then Z

!

X is mono, and represents the greatest lower bound

(check!).

Of course, the identity X

id

X

!

X represents the top element of Sub(X).

Because the factorization of X

f

!

Y as X

e

!

E

m

!

Y with e regular epi and

m mono, in a regular category

C

, is only dened up to isomorphism, it denes

rather a subobject of Y than a mono into Y this dened subobject is called the

image

of f and denoted Im(f) (compare with the situation in Set).

Exercise 58

. Im(f) is the smallest subobject of Y through which f factors:

for a subobject represented by n : A

!

Y we have that there is X

a

!

A with

f = na, if and only if Im(f) is smaller than the subobject represented by n.
Since monos and isos are stable under pullback, in any category

C

with pull-

backs, any arrow f : X

!

Y determines an order preserving map f

: Sub(Y )

!

Sub(X)

by pullback along

f: if E

m

!

Y represents the subobject M of Y and

F

n

//

E

m

X

//

f

Y

is a pullback, F

n

!

X represents f

(M).

Exercise 59

. Check that f

is well dened and order preserving.

Proposition 4.4

In a regular category, each

f

preserves greatest lower bounds

and images, that is: for

f : X

!

Y

,

i) for subobjects

MN

of

Y

,

f

(M

^

N) = f

(M)

^

f

(N)

ii) if

g

0

//

g

//

f

is a pullback, then

f

(Im(g)) = Im(g

0

)

.

32

background image

4. A little piece of categorical logic

Exercise 60

. Prove proposition 4.4.

4.2 Coherent logic in regular categories

The fragment of rst order logic we are going to interpret in regular categories

is the so-called coherent fragment.

The logical symbols are = (equality),

^

(conjunction) and

9

(existential

quantication). A

language

consists of a set of

sorts

ST::: a denumerable

collection of

variables

x

S

1

x

S

2

::: of sort S, for each sort and a collection of

function symbols

(f : S

1

:::S

n

!

S). The case n = 0 is not excluded (one

thinks of

constants

of a sort), but not separately treated. We now dene,

inductively, terms of sort S and formulas.

Denition 4.5

Terms of sort

S

are dened by:

i)

x

S

is a term of sort

S

if

x

S

is a variable of sort

S

ii) if

t

1

:::t

n

are terms of sorts

S

1

:::S

n

respectively, and

(f : S

1

:::S

n

!

S)

is a function symbol of the language, then

f(t

1

:::t

n

)

is a term of sort

S

.

Formulas are dened by:

i)

>

is a formula (the formula \true")

ii) if

t

and

s

are terms of the same sort, then

t = s

is a formula

iii) if

'

and

are formulas then

('

^

)

is a formula

iv) if

'

is a formula and

x

a variable of some sort, then

9

x'

is a formula.

An

interpretation

of such a language in a regular category

C

starts by choos-

ing for each sort S an object S ]] of

C

, and for each function symbol (f :

S

1

:::S

n

!

S) of the language, an arrow f ]] : S

1

]]

S

n

]]

!

S ]] in

C

.

Given this, we dene interpretations t]] for terms t and ']] for formulas

', as follows.

Write FV (t) for the set of variables which occur in t, and FV (') for the set

of

free

variables in '.

We put FV (t)]] = S

1

]]

S

n

]] if FV (t) =

f

x

S

1

1

:::x

S

n

n

g

the same

for FV (')]]. Note: in the products FV (t)]] and FV (')]] we take a copy

of S ]] for every variable of sort S! Let me further emphasize that the empty

product is 1, so if FV (t) (or FV (')) is

, FV (t)]] (or FV (')]]) is the terminal

object of the category.

33

background image

Categories

Denition 4.6

The interpretation of a term

t

of sort

S

is a morphism

t]] :

FV (t)]]

!

S ]]

and is dened by the clauses:

i)

x

S

]]

is the identity on

S ]]

, if

x

S

is a variable of sort

S

ii) Given

t

i

]] : FV (t

i

)]]

!

S

i

]]

for

i = 1:::n

and a function symbol

(f : S

1

:::S

n

!

S)

of the language,

f(t

1

:::t

n

)]]

is the map

FV (f(t

1

:::t

n

))]]

//

(~

t

i

j

i

=1

:::n

)

Q

n

i

=1

S

i

]]

//

f

]]

S ]]

where

~t

i

is the composite

FV (f(t

1

:::t

n

))]]

//

i

FV (t

i

)]]

//

t

i

]]

S

i

]]

in which

i

is the appropriate projection, corresponding to the inclusion

FV (t

i

)

FV (f(t

1

:::t

n

))

.

Finally, we interpret formulas ' as

subobjects

']] of FV (')]]. You should try

to keep in mind the intuition that '(x

1

:::x

n

)]] is the \subset"

f

(a

1

:::a

n

)

2

A

1

A

n

j

'a

1

:::a

n

]

g

Denition 4.7

The interpretation

']]

as subobject of

FV (')]]

is dened as

follows:

i)

>

]]

is the maximal subobject of

FV (

>

)]] = 1

ii)

t = s]]

!

FV (t = s)]]

is the equalizer of

FV(t = s)]]

//

//

FV (t)]]

FV (s)]]

//

t

]]

//

s

]]

T ]]

if

t

and

s

are of sort

T

again, the left hand side maps are projections,

corresponding to the inclusions of

FV (t)

and

FV (s)

into

FV (t = s)

iii) if

']]

!

FV (')]]

and

]]

!

FV ()]]

are given and

FV ('

^

)]]

//

1

''

2

O

O

O

O

O

O

O

O

O

O

O

FV (')]]

FV ()]]

are again the suitable projections, then

('

^

)]]

!

FV ('

^

)]]

is the

greatest lower bound in

Sub(FV ('

^

)]])

of

1

(']])

and

2

( ]])

34

background image

4. A little piece of categorical logic

iv) if

']]

!

FV (')]]

is given and

: FV (')]]

!

FV (

9

x')]]

the projec-

tion, let

FV

0

(')]]

be the product of the interpretations of the sorts of the

variables in

FV (')

f

x

g

(so

FV

0

(')]] = FV (')]]

if

x

occurs freely in

'

and

FV

0

(')]] = FV (')]]

S ]]

if

x = x

S

does not occur free in

'

).

Write

0

: FV

0

(')]]

!

FV (')]]

.

Now take

9

x']]

!

FV (

9

x')]]

to be the image of the composition:

(

0

)

(']])

!

FV

0

(')]]

0

!

FV (

9

x')]]

We have now given an interpretation of formulas. Basically, a formula ' is

true

under this interpretation if ']]

!

FV (')]] is the maximal subobject

but since we formulate the logic in terms of sequents we rather dene when a

sequent is true under the interpretation.

Denition 4.8

A

labelled sequent

is an expression of the form

`

'

or

`

'

where

and

'

are the formulas of the sequent (but

may be absent), and

is a nite set of variables which includes all the variables which occur free in a

formula of the sequent.

Let

]] = S

1

]]

S

n

]]

if

=

f

x

S

1

1

:::x

S

n

n

g

there are projections

]]

'

!

FV (')]]

and (in case

is there)

]]

!

FV ()]]

we say that the

sequent

`

'

is true for the interpretation if

(

)

( ]])

(

'

)

(']])

as

subobjects of

]]

, and

`

'

is true if

(

'

)

(']])

is the maximal subobject of

]]

.

Exercise 61

. Show that the sequent

`

9

x

S

(x

S

= x

S

) is true if and only if the

unique map S ]]

!

1 is a regular epimorphism.

We now turn to the logic. Instead of giving deduction rules and axioms, I

formulate a list of closure conditions which determine what sets of labelled se-

quents will be called a

theory

. I write

`

x

for

`

f

x

g

and

`

for

`

.

Denition 4.9

Given a language, a set

T

of labelled sequents of that language

is called a

theory

i the following conditions hold (the use of brackets around

caters in a, I hope, self-explanatory way for the case distiction as to whether

is or is not present):

i)

`

>

is in

T

`

x

x = x

is in

T

for every variable

x

x = y

^

y = z

`

f

xyz

g

x = z

is in

T

for variables

xyz

of the same sort

ii) if

()

`

'

is in

T

then

()

`

'

is in

T

whenever

iii) if

()

`

'

is in

T

and

FV ()

then

(

^

)

`

'

and

(

^

)

`

'

are

in

T

35

background image

Categories

iv) if

()

`

'

and

()

`

are in

T

then

()

`

'

^

and

()

`

^

'

are in

T

v) if

`

'

is in

T

and

x

is a variable not occurring in

'

then

9

x

`

nf

x

g

'

is in

T

vi) if

x

occurs in

'

and

()

`

't=x]

is in

T

then

()

`

9

x'

is in

T

if

x

does not occur in

'

and

()

`

'

and

()

`

9

x(x = x)

are in

T

,

then

()

`

9

x'

is in

T

vii) if

()

`

'

is in

T

then

(t=x])

`

nf

x

g

FV

(

t

)

't=x]

is in

T

viii) if

()

`

't=x]

and

()

`

t = s

are in

T

then

()

`

's=x]

is in

T

ix) if

()

`

'

and

'

`

are in

T

then

()

`

is in

T

Exercise 62

. Show that the sequent '

`

FV

(

'

)

' is in every theory, for every

formula ' of the language.
As said, the denition of a theory is a list of closure conditions: every item

can be seen as a rule, and a theory is a set of sequents closed under every rule.

Therefore, the intersection of any collection of theories is again a theory, and it

makes sense to speak, given a set of sequents S, of the theory Cn(S)

generated

by

S:

Cn(S) =

\

f

T

j

T is a theory and S

T

g

We have the following theorem:

Theorem 4.10 (Soundness theorem)

Suppose

T = Cn(S)

and all sequents

of

S

are true under the interpretation in the category

C

. Then all sequents of

T

are true under that interpretation.

Before embarking on the proof, rst a lemma:

Lemma 4.11

Suppose

t

is substitutable for

x

in

'

. There is an obvious map

t] : FV (')

n

f

x

g

FV (t)]] = FV ('t=x])]]

!

FV (')]]

induced by

t]]

the components of

t]

are projections except for the factor of

']]

corresponding to

x

, where it is

FV ('t=x])]]

!

FV (t)]]

t

]]

!

f

x

g

]]

There is a pullback diagram:

't=x]]]

//

FV ('t=x])]]

t

]

']]

//

FV (')]]

36

background image

4. A little piece of categorical logic

Exercise 63

. Prove this lemma not trivial. Use induction on ' and proposi-

tion 4.4].

Proof

. (of theorem 4.10) The proof checks that for every rule in the list of

denition 4.9, if the premiss is true then the conclusion is true in other words,

that the set of true sequents is a theory.

i)

`

>

is true by the denition

>

]] = 1

x

S

= x

S

]] is the equalizer of two maps which are both the identity on S ]],

so isomorphic to S ]]. For x = y

^

y = z

`

f

xyz

g

x = z, just observe

that E

12

^

E

23

E

13

if E

ij

is the equalizer of the two projections

i

j

:

S ]]

S ]]

S ]]

!

S ]].

ii) This is because if

and : ]]

!

]] is the projection,

is monotone.

iii)-iv) By the interpretation of

^

as the greatest lower bound of two subobjects,

and proposition 4.4.

v) Let

]]

//

n

f

x

g

]]

//

FV (')]]

FV()]]

FV (

9

x)]]

the projections. Since by assumption

( ]])

()

(']]) there is a commu-

tative diagram

( ]])

//

]]

(']])

//

n

f

x

g

]]

By proposition 4.4,

(

9

x]]) is the image of the map

( ]])

!

n

f

x

g

]],

so

( ]])

(']]) in Sub(

n

f

x

g

]]).

vi) Suppose x occurs free in '. Consider the commutative diagram

]]

ww

o

o

o

o

o

o

o

o

o

o

o

o

0

++

00

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

W

FV ()]]

FV ('t=x])]]

//

t

]

FV (')]]

//

FV (')

n

f

x

g

]]

with t] as in lemma4.11 and the other maps projections. Now ']]

(

9

x']])

because ']]

!

FV (')]]

!

FV (')

n

f

x

g

]] factors through

9

x']] by deni-

tion so if

( ]])

0

('t=x]]]) then with lemma 4.11,

( ]])

0

('t=x]]]) =

0

t]

(']])

0

t]

(

9

x']]) =

00

(

9

x']])

in Sub(]]) and we are done.

37

background image

Categories

The case of x not occurring in ' is left to you.

vii) Direct application of lemma 4.11

viii-ix) Left to you.

Exercise 64

. Fill in the \left to you" gaps in the proof.

4.3 The language

L(C

)

and theory

T

(C

)

associated to a

regular category

C

Given a regular category

C

(which, to be precise, must be assumed to be small),

we associate to

C

the language which has a sort C for every object of

C

, and a

function symbol (f : C

!

D) for every arrow f : C

!

D of

C

.

This language is called

L

(

C

) and it has trivially an interpretation in

C

.

The theory T(

C

) is the set of sequents of

L

(

C

) which are true for this inter-

pretation.

One of the points of categorical logic is now, that categorical statements

about objects and arrows in

C

can be reformulated as statements about the

truth of certain sequents in

L

(

C

). You should read the relevant sequents as

expressing that we can \do as if the category were Set".

Examples

a) C is a terminal object of

C

if and only if the sequents

`

xy

x = y and

`

9

x(x = x) are valid, where xy variables of sort C

b) the arrow f : A

!

B is mono in

C

if and only if the sequent f(x) =

f(y)

`

xy

x = y is true

c) The square

A

g

//

f

B

h

C

//

d

D

is a pullback square in

C

if and only if the sequents

h(x

B

) = d(y

C

)

`

xy

9

z

A

(f(z) = x

^

g(z) = y)

and

f(z

A

) = f(z

0

A

)

^

g(z

A

) = g(z

0

A

)

`

zz

0

z = z

0

are true

38

background image

4. A little piece of categorical logic

d) the fact that f : A

!

B is epi can not similarly be expressed! But: f is

regular epi if and only if

`

x

B

9

y

A

(f(y) = x)

is true

e) A

//

f

B

//

g

//

h

C is an equalizer diagram i f is mono (see b) and the

sequent

g(x

B

) = h(x

B

)

`

x

B

9

y

A

(f(y) = x)

is true.

Exercise 65

. Check (a number of) these statements. Give the sequent(s) cor-

responding to the statement that

A

g

//

f

B

C

is a product diagram.

Exercise 66

. Check that the formulas

9

x' and

9

x(x = x

^

') are

equiva-

lent

, that is, every theory contains the sequents

9

x'

`

9

x(x = x

^

')

and

9

x(x = x

^

')

`

9

x'

for any containing the free variables of

9

x'.

Exercise 67

. Can you express: A

f

!

B is regular mono?

4.4 Example of a regular category

In this section, I treat an example of a type of regular categories which are

important in categorical logic. They are categories of (-valued sets for some

frame (. Let's dene some things.

Denition 4.12

A

frame (

is a partially ordered set which has suprema (least

upper bounds)

W

B

of all subsets

B

, and inma (meets)

V

A

for

nite

subsets

A

(so, there is a top element

>

and every pair of elements

xy

has a meet

x

^

y

),

and moreover,

^

distributes over

W

, that is,

x

^

_

B =

_

f

x

^

b

j

b

2

B

g

for

x

2

(

,

B

(

.

39

background image

Categories

Given a frame ( we dene the category

C

as follows:

Objects are functions X

E

X

!

(, X a set

Maps from (XE

X

) to (YE

Y

) are functions X

f

!

Y satisfying the requirement

that E

X

(x)

E

Y

(f(x)) for all x

2

X.

It is easily seen that the identity function satises this requirement, and if two

composable functions satisfy it, their composition does so we have a category.

Proposition 4.13

C

is a regular category.

Proof

. Let

fg

be any one-element set, together with the function which sends

to the top element of (. Then

fg

!

( is a terminal object of

C

.

Given (XE

X

) and (YE

Y

), a product of the two is the object (X

YE

X

Y

)

where E

X

Y

(xy) is dened as E

X

(x)

^

E

Y

(y).

Given two arrows fg : (XE

X

)

!

(YE

Y

) their equalizer is (X

0

E

X

0

) where

X

0

X is

f

x

2

X

j

f(x) = g(x)

g

and E

X

0

is the restriction of E

X

to X

0

.

This is easily checked, and

C

is a nitely complete category.

An arrow f : (XE

X

)

!

(YE

Y

) is regular epi if and only if the function f

is surjective and for all y

2

Y , E

Y

(y) =

W

f

;

1

(y).

For suppose f is such, and g : (XE

X

)

!

(ZE

Z

) coequalizes the kernel

pair of f. Then g(x) = g(x

0

) whenever f(x) = f(x

0

), and so for all y

2

Y , since

f(x) = y implies E

X

(x)

E

Z

(g(x)), we have

E

Y

(y) =

_

f

E

X

(x)

j

f(x) = y

g

E

Z

(g(x))

so there is a unique map h : (YE

Y

)

!

(ZE

Z

) such that g = hf that is f is

the coequalizer of its kernel pair.

The proof of the converse is left to you.

Finally we must show that regular epis are stable under pullback. This is

an exercise.

Exercise 68

. Show that the pullback of

X

f

Y

//

g

Z

(I suppress reference

to the E

X

etc.) is (up to isomorphism) the set

f

(xy)

j

f(x) = g(y)

g

, with

E(xy) = E

X

(x)

^

E

Y

(y) and then, use the distributivity of ( to show that

regular epis are stable under pullback.

Exercise 69

. Fill in the other gap in the proof: if f : (XE

X

)

!

(YE

Y

)

is a regular epi, then f satises the condition given in the proof.

Exercise 70

. Given (XE

X

)

f

!

(YE

Y

), give the interpretation of the for-

mula

9

x(f(x) = y), as subobject of (YE

Y

).

40

background image

4. A little piece of categorical logic

Exercise 71

. Characterize those objects (XE

X

) for which the unique map

to the terminal object is a regular epimorphism.

Exercise 72

. Give a categorical proof of the statement: if f is the coequalizer

of something, it is the coequalizer of its kernel pair.

Exercise 73

. Characterize the regular monos in

C

.

41

background image

Categories

42

background image

5. Adjunctions

5 Adjunctions

The following kind of problem occurs quite regularly: suppose we have a functor

C

G

!

D

and for a given object D of

D

, we look for an object G(C) which \best

approximates" D, in the sense that there is a map D

!

G(C) with the property

that any other map D

g

!

G(C

0

) factors uniquely as G(f) for f : C

!

C

0

in

C

.

We have seen, that if G is the inclusion of Abgp into Grp, the abelianization

of a group is an example. Another example is the )Cech-Stone compactication

in topology: for an arbitrary topological space X one constructs a compact

space X out of it, and a map X

!

X, such that any continuous map from

X to a compact space factors uniquely through this map.

Of course, what we described here is a sort of \right-sided" approximation

the reader can dene for himself what the notion for a left-sided approxiamtion

would be.

The categorical description of this kind of phenomena goes via the concept

of

adjunction

, which this chapter is about.

5.1 Adjoint functors

Let

C

//

G

D

oo

F

be a pair of functors between categories

C

and

D

.

We say that F is

left adjoint

to G, or G is

right adjoint

to F, notation:

F

a

G, if there is a natural bijection:

C

(FDC)

//

m

D C

D

(DGC)

for each pair of objects C

2

C

0

D

2

D

0

. Two maps f : FD

!

C in

C

and

g : D

!

GC in

D

which correspond to each other under this correspondence

are called

transposes

of each other.

The naturality means that, given f : D

!

D

0

, g : C

0

!

C in

D

and

C

respectively, the diagram

C

(FDC)

//

m

D C

D

(DGC)

C

(FD

0

C

0

)

OO

C

(

Ffg

)

//

m

D

0

C

0

D

(D

0

GC

0

)

OO

D

(

fGg

)

commutes in Set. Remind yourself that given : FD

0

!

C

0

,

C

(Ffg)() :

FD

!

C is the composite

FD

//

Ff

FD

0

//

C

0

//

g

C

43

background image

Categories

Such a family m = (m

DC

j

D

2

D

0

C

2

C

0

) is then completely determined by

the values it takes on identities i.e. the values

m

DFD

(id

FD

) : D

!

GFD

For, given : FD

!

C, since =

C

(id

FD

)(id

FD

),

m

DC

() = m

DC

(

C

(id

FD

)(id

FD

))

=

D

(id

D

G())(m

D

FD

(id

FD

))

which is the composite

D

//

m

D F

D

(id

FD

)

GFD

//

G

(

)

G(C)

The standard notation for m

DFD

(id

FD

) is

D

: D

!

GF(D).

Exercise 74

. Show that (

D

: D

2

D

0

) is a natural transformation:

id

D

)

GF

By the same reasoning, the natural family(m

;

1

DC

j

D

2

D

0

C

2

C

0

) is completely

determined by its actions on identities

m

;

1

GCC

(id

GC

) : FGC

!

C

Again, the family (m

;

1

GCC

(id

GC

)

j

C

2

C

0

) is a natural transformation: FG

)

id

C

. We denote its components by "

C

and this is also standard notation.

We have that m

;

1

DC

( : D

!

GC) is the composite

FD

//

F

FGC

//

"

C

C

Now making use of the fact that m

DC

and m

;

1

DC

are each others inverse we get

that for all : FD

!

C and : D

!

GC the diagrams

D

D

//

GC

GFD

//

GF

(

)

GFG(C)

OO

G

(

"

C

)

and

FD

//

F

(

D

)

C

FGFD

//

FG

(

)

FGC

OO

"

C

commute applying this to the identities on FD and GC we nd that we have

commuting diagrams of natural transformations:

44

background image

5. Adjunctions

G

+3

?G

&

id

G

E

E

E

E

E

E

E

E

E

E

E

E

E

E

E

E

GFG

G

"

G

F

+3

F

&

id

F

E

E

E

E

E

E

E

E

E

E

E

E

E

E

E

E

FGF

"?F

F

Here ? G denotes (

GC

j

C

2

C

0

) and G

" denotes (G("

C

)

j

C

2

C

0

).

Conversely, given

C

//

G

D

oo

F

with natural transformations : id

D

)

GF

and " : FG

)

id

C

which satisfy the above

triangle equalities

, we have that

F

a

G.

The tuple (FG") is called an

adjunction

. is the

unit

of the adjunction,

" the

counit

.

Exercise 75

. Prove the last statement, i.e. given

C

//

G

D

oo

F

, : id

D

)

GF

and " : FG

)

id

C

satisfying (G

")

( ? G) = id

G

and (" ? F)

(F

) = id

F

,

we have F

a

G.

Exercise 76

. Given

C

//

G

1

D

oo

F

1

//

G

2

E

oo

F

2

, if F

1

a

G

1

and F

2

a

G

2

then

F

1

F

2

a

G

2

G

1

.

Examples

. The world is full of examples of adjoint functors. We have met

several:

a) Consider the forgetful functor U : Grp

!

Set and the free functor F :

Set

!

Grp. Given a function from a set A to a group G (which is an arrow

A

!

U(G) in Set) we can uniquely extend it to a group homomorphism

from ( ~A?) to G (see example e) of 1.1), i.e. an arrow F(A)

!

G in Grp,

and conversely. This is natural in A and G, so F

a

U

b) The functor Dgrph

!

Cat given in example f) of 1.1 is left adjoint to the

forgetful functor Cat

!

Dgrph

c) Given functors P

//

G

Q

oo

F

between two preorders P and Q, F

a

G if and

only if we have the equivalence

y

G(x)

,

F(y)

x

for x

2

Py

2

Q if and only if we have FG(x)

x and y

GF(y) for all

xy

45

background image

Categories

d) In example m) of 1.1 we did \abelianization" of a group G. We made

use of the fact that any homomorphism G

!

H with H abelian, factors

uniquely through G=GG], giving a natural 1-1 correspondence

Grp(GI(H))

!

Abgp(G=GG]H)

where I : Abgp

!

Grp is the inclusion. So abelianization is left adjoint

to the inclusion functor of abelian groups into groups

e) The

free monoid

F(A) on a set A is just the set of strings on the alphabet

A. F : Set

!

Mon is a functor left adjoint to the forgetful functor from

Mon to Set

f) Given a set X we have seen (example g) of 2.2) the product functor (

;

)

X : Set

!

Set, assigning the product Y

X to a set Y .

Since there is a natural bijection between functions Y

X

!

Z and

functions Y

!

Z

X

, the functor (

;

)

X

: Set

!

Set is right adjoint to

(

;

)

X

g) Example e) of 2.2 gives two functors FG : Set

!

Cat. F and G are

respectively left and right adjoint to the functor Cat

Ob

!

Set which assigns

to a (small) category its set of objects (to be precise, for this example to

work we have to take for Cat the category of

small

categories), and to a

functor its action on objects.

h) Given a regular category

C

we saw in 4.1 that every arrow f : X

!

Y

can be factored as a regular epi followed by a monomorphism. This gives

rise to a monotone function: Sub(X)

Im

f

!

Sub(Y ) dened as follows: if

M

2

Sub(X) is represented by m, Im

f

(M) is the image of fm (see 4.1).

We have seen that Im

f

(M)

N

,

M

f

(N) for any subobject N of

Y , so Im

f

is left adjoint to f

.

We can also express this logically: in the logic developed in chapter 4, for

any formulas M(x) and N(y), the sequents

9

x(f(x) = y

^

M(x))

`

y

N(y)

and

M(x)

`

x

N(f(x))

are equivalent.

One of the slogans of categorical logic is therefore, that \existential quan-

tication is left adjoint to substitution".

46

background image

5. Adjunctions

i) Let

C

be a category with nite products for C

2

C

0

consider the slice

category

C

=C. There is a functor C

:

C

!

C

=C which assigns to D the

object C

D

C

!

C of

C

=C, and to maps D

f

!

D

0

the map id

C

f.

C

has a left adjoint *

C

which takes the domain: *

C

(D

!

C) = D.

j) Let P : Set

op

!

Set be the functor which takes the powerset on objects,

and for X

f

!

Y , P(f) : P(Y )

!

P(X) gives for each subset B of Y its

inverse image under f.

Now P might as well be regarded as a functor Set

!

Set

op

let's write "P

for that functor. Since there is a natural bijection:

Set(XP(Y ))

!

Set(YP(X)) = Set

op

( "P(X)Y )

we have an adjunction "P

a

P.

Exercise 77

. Suppose that

C

F

D

is a functor and that for each object C of

C

there is an object GC of

D

and an arrow "

C

: FGC

!

C with the property that

for every object D of

D

and any map FD

f

!

C, there is a unique ~f: D

!

GC

such that

FD

##

F

~

f

G

G

G

G

G

G

G

G

G

//

f

C

FGC

<<

"

C

y

y

y

y

y

y

y

y

commutes.

Prove that G :

C

0

!

D

0

extends to a functor G :

C

!

D

which is right

adjoint to F, and that ("

C

: FGC

!

C

j

C

2

C

0

) is the counit of the adjunction.

Construct also the unit of the adjunction.

Exercise 78

. Given

C

G

!

D

, for each object D of

D

we let (D

#

G) denote

the category which has as objects pairs (Cg) where C is an object in

C

and

g : D

!

GC is an arrow in

D

. An arrow (Cg)

!

(C

0

g

0

) in (D

#

G) is an arrow

f : C

!

C

0

in

C

which makes

D

}}

g

{

{

{

{

{

{

{

{

!!

g

0

D

D

D

D

D

D

D

D

GC

//

Gf

GC

0

commute.

Show that G has a left adjoint if and only if for each D, the category (D

#

G)

has an initial object.

47

background image

Categories

5.2 Expressing (co)completeness by existence of adjoints

preservation of (co)limits by adjoint functors

Given categories

C

and

D

, we dened for every functor F :

C

!

D

its

limit

(or limiting cone), if it existed, as a pair (D) with : $

D

)

F, and (D)

terminal in the category of cones for F.

Any other natural transformation

0

: $

D

0

)

F factors uniquely through

(D) via an arrow D

0

!

D in

D

and conversely, every arrow D

0

!

D gives

rise to a natural transformation

0

: $

D

0

)

F.

So there is a 1-1 correspondence between

D

(D

0

D) and

D

C

($

D

0

F)

which is natural in D

0

.

Since every arrow D

0

!

D

00

in

D

gives a natural transformation $

D

0

)

$

D

00

(example i) of 2.2), there is a functor $

(

;

)

:

D

!

D

C

.

The above equation now means that:

Proposition 5.1

D

has all limits of type

C

(i.e. every functor

C

F

!

D

has a

limiting cone in

D

) if and only if

$

(

;

)

has a right adjoint.

Exercise 79

. Give an exact proof of this proposition.

Exercise 80

. Use duality to deduce the dual of the proposition:

D

has all

colimits of type

C

if and only if $

(

;

)

:

D

!

D

C

has a left adjoint.

Exercise 81

. (Uniqueness of adjoints) Any two left (or right) adjoints of a

given functor are isomorphic as objects of the appropriate functor category.

Exercise 82

.

D

!

1

has a right adjoint i

D

has a terminal object, and a

left adjoint i

D

has an initial object.

Exercise 83

. Suppose

D

has both an initial and a terminal object denote

by L the functor

D

!

D

which sends everything to the initial, and by R the

one which sends everything to the terminal object. L

a

R.

Exercise 84

. Let F

a

G with counit " : FG

)

id. Show that " is a nat-

ural isomorphism if and only if G is faithful.
A very important aspect of adjoint functors is their behaviour with respect

to limits and colimits.

Theorem 5.2

Let

C

//

G

D

oo

F

such that

F

a

G

. Then:

48

background image

5. Adjunctions

a)

G

preserves all limits which exist in

C

b)

F

preserves all colimits which exist in

D

.

Proof

. Suppose M :

E

!

C

has a limiting cone (C) in

C

. Now a cone (D)

for GM is a natural family D

E

!

GM(E), i.e. such that

D

//

E

##

E

0

G

G

G

G

G

G

G

G

G

GM(E)

GM

(

e

)

GM(E

0

)

commutes for every E

e

!

E

0

in

E

.

This transposes under the adjunction to a family (FD

~

E

!

ME

j

E

2

E

0

) and

the naturality requirement implies that

FD

//

~

E

##

~

E

0

G

G

G

G

G

G

G

G

ME

M

(

e

)

ME

0

commutes in

C

, in other words, that (FD) is a cone for M in

C

. There is,

therefore, a unique map of cones from (FD ~) to (C).

Transposing back again, we get a unique map of cones (D)

!

(GCG

).

That is to say that (GCG

) is terminal in Cone(GM), so a limiting cone for

GM, which was to be proved.

The argument for the other statement is dual.

Exercise 85

. Given

C

//

G

D

oo

F

, F

a

G and M :

E

!

C

. Show that the

functor Cone(M)

!

Cone(GM) induced by G has a left adjoint.

From the theorem on preservation of (co)limits by adjoint functors one can

often conclude that certain functors cannot have a right or a left adjoint.

Examples

a) The forgetful functor Mon

!

Set does not preserve epis, as we have seen

in 1.2. In chapter 3 we've seen that f is epi i

id

//

id

f

//

f

is a pushout

since left adjoints preserve identities and pushouts, they preserve epis

therefore the forgetful functor Mon

!

Set does not have a right adjoint

49

background image

Categories

b) The functor (

;

)

X : Set

!

Set does not preserve the terminal object

unless X is itself terminal in Set therefore, it does not have a left adjoint

for non-terminal X.

c) The forgetful functor Pos

!

Set has a left adjoint, but it cannot have a

right adjoint: it preserves all coproducts, including the initial object, but

not all coequalizers.

Exercise 86

. Prove the last example. Hint: think of the coequalizer of the fol-

lowing two maps

Q

!

R

: one is the inclusion, the other is the constant zero map.

Another use of the theorem has to do with the computation of limits. Many

categories, as we have seen, have a forgetful functor to Set which has a left

adjoint. So the forgetful functor preserves limits, and since these can easily be

computed in Set, one already knows the \underlying set" of the vertex of the

limiting cone one wants to compute.
Does a converse to the theorem hold? I.e. given G :

C

!

D

which preserves

all limits does G have a left adjoint? In general

no

, unless

C

is suciently

complete, and a rather technical condition, the \solution set condition" holds.

The

adjoint functor theorem

(Freyd) tells that in that case there is a converse:

Denition 5.3 (Solution set condition)

G :

C

!

D

satises the solution

set condition (ssc) for an object

D

of

D

, if there is a

set X

D

of objects of

C

,

such that every arrow

D

!

GC

factors as

D

//

!!

D

D

D

D

D

D

D

D

GC

GC

0

OO

G

(

f

)

for some

C

0

2

X

D

and

f : C

0

!

C

in

C

.

Theorem 5.4 (Adjoint Functor Theorem)

Let

C

be a complete category

and

G :

C

!

D

a functor.

G

has a left adjoint if and only if

G

preserves

all small limits and satises the ssc for every object

D

of

D

.

I won't prove the theorem, but you may like to try yourself. It is a, not too

trivial, exercise.

For small categories

C

, the ssc is of course irrelevant. But categories which

are small

and

complete are rather special:::they are complete preorders.

For preorders

C

,

D

we have: if

C

is complete, then G :

C

!

D

has a left

adjoint if and only if G preserves all limits, that is: greatest lower bounds

V

B

for all B

C

. For, put

F(d) =

^

f

c

j

d

G(c)

g

50

background image

5. Adjunctions

Then F(d)

c

0

implies (since G preserves

V

)

V

f

G(c)

j

d

G(c)

g

G(c

0

) which

implies d

G(c

0

) since d

V

f

G(c)

j

d

G(c)

g

conversely, d

G(c

0

) implies

c

0

2

f

c

j

d

G(c)

g

so F(d) =

V

f

c

j

d

G(c)

g

c

0

.

51

background image

Categories

52

background image

6. Monads and Algebras

6 Monads and Algebras

Given an adjunction (FG") :

C

//

D

oo

let us look at the functor T =

GF :

D

!

D

.

We have a natural transformation : id

D

)

T and a natural transformation

: T

2

)

T. The components

D

are

T

2

(D) = GFGFD

G

(

"

F

D

)

!

GFD = T(D)

Furthermore the equalities

T

3

T

//

T

T

2

T

2

//

T

and

T

//

T

=

A

A

A

A

A

A

A

A

T

2

T

oo

T

~~

=

}

}

}

}

}

}

}

}

T

hold. Here (T)

D

= T(

D

) : T

3

D

!

TD and (T)

D

=

TD

: T

3

D

!

TD

(Similar for T and T).

Exercise 87

. Prove these equalities.

A triple (T) satisfying these identities is called a

monad

. Try to see the

formal analogy between the dening equalities for a monad and the axioms for

a monoid: writing m(ef) for ef in a monoid, and for the unit element, we

have

m(em(gh)) = m(m(eg)h) (associativity)

m(e) = m(e) = e

(unit)

Following this one calls the

multiplication

of the monad, and its

unit

.

Example

. The powerset functor

P

: Set

!

Set (example j) of 2.2, with

and indicated there) is a monad (check).
Dually, there is the notion of a

comonad

(L") on a category

C

, with equalities

L

//

L

2

L

L

2

//

L

L

3

L

~~

=

~

~

~

~

~

~

~

~

=

@

@

@

@

@

@

@

@

L

L

2

oo

"L

//

L"

L

Given an adjunction (FG"), (FG = FG") is a comonad on

C

. We call

the

comultiplication

and " the

counit

(this is in harmony with the unit-counit

terminology for adjunctions).

53

background image

Categories

Although, in many contexts, comonads and the notions derived from them

are at least as important as monads, the treatment is dual so I concentrate on

monads.

Every adjunction gives rise to a monad conversely, every monad arises from

an adjunction, but in more than one way. Essentially, there are a maximal and

a minimal solution to the problem of nding an adjunction from which a given

monad arises.

Example

. A monad on a poset P is a monotone function T : P

!

P with

the properties x

T(x) and T

2

(x)

T(x) for all x

2

P such an operation

is also often called a

closure operation

on P. Note that T

2

= T because T is

monotone.

In this situation, let Q

P be the image of T, with the ordering inherited

from P. We have maps r : P

!

Q and i : Q

!

P such that ri is the identity

on Q and ir = T : P

!

P.

For x

2

P, y

2

Q we have x

i(y)

,

r(x)

y (check) so r

a

i and the

operation T arises from this adjunction.

6.1 Algebras for a monad

Given a monad (T) on a category

C

, we dene the category T-Alg of T

-

algebras

as follows:

Objects

are pairs (Xh) where X is an object of

C

and h : T(X)

!

X is

an arrow in

C

such that

T

2

(X)

X

//

T

(

h

)

T(X)

h

T(X)

//

h

X

and

X

//

X

""

=

E

E

E

E

E

E

E

E

E

T(X)

h

X

commute

Morphisms

: (Xh)

!

(Yk) are morphisms X

f

!

Y in

C

for which

T(X)

h

//

T

(

f

)

T(Y )

k

X

//

f

Y

commutes.

54

background image

6. Monads and Algebras

Theorem 6.1

There is an adjunction between

T

-Alg and

C

which brings about

the given monad

T

.

Proof

. There is an obvious forgetful functor U

T

: T-Alg

!

C

which takes (Xh)

to X. I claim that U

T

has a left adjoint F

T

:

F

T

assigns to an object X the T-algebra T

2

(X)

X

!

T(X) to X

f

!

Y

the map T(f) this is an algebra map because of the naturality of . That

T

2

(X)

X

!

T(X) is an algebra follows from the dening axioms for a monad T.

Now given any arrow g : X

!

U

T

(Yh) we let ~g : (T(X)

X

)

!

(Yh) be

the arrow T(X)

T

(

g

)

!

T(Y )

h

!

Y . This is a map of algebras since

T

2

(X)

X

//

T

2

(

g

)

T

2

(Y )

Y

//

T

(

h

)

Y

h

T(X)

//

T

(

g

)

T(Y )

//

h

Y

commutes the left hand square is the naturality of the right hand square is

because (Yh) is a T-algebra.

Conversely, given f : (TX

X

)

!

(Yh) we have an arrow "f : X

!

Y by

taking the composite X

X

!

TX

f

!

Y .

Now ~"f: TX

!

Y is the composite

TX

T

(

X

)

!

T

2

X

T

(

f

)

!

TY

h

!

Y

By naturality of this is

TX

f

!

Y

Y

!

TY

h

!

Y

which is f since (Yh) is a T-algebra.

Conversely, "~g : X

!

Y is the composite

X

X

!

TX

T

(

g

)

!

TY

h

!

Y

Again by naturality of and the fact that (Yh) is a T-algebra, we conclude

that "~g = g. So we have a natural 1-1 correspondence

C

(XU

T

(Yh))

'

T-Alg(F

T

(X)(Yh))

and our adjunction.

Note that the composite U

T

F

T

is the functor T, and that the unit of the

adjunction is the unit of T the proof that for the counit " of F

T

a

U

T

we have

that

T

2

= U

T

F

T

U

T

F

T U

T

"F

T

!

U

T

F

T

= T

55

background image

Categories

is the original multiplication , is left to you.

Exercise 88

. Complete the proof.

Example

. The

group monad

. Combining the forgetful functor U : Grp

!

Set

with the left adjoint, the free functor Set

!

Grp, we get the following monad

on Set:

T(A) is the set of sequences on the alphabet A

t

A

;

1

(A

;

1

is the set

f

a

;

1

j

a

2

A

g

of formal inverses of elements of A, as in example e) of 1.1) in which no

aa

;

1

or a

;

1

a occur. The unit A

A

!

TA sends a

2

A to the string

h

a

i

. The

multiplication : T

2

(A)

!

T(A) works as follows. Dene (

;

)

;

: A

t

A

;

1

!

A

t

A

;

1

by a

;

= a

;

1

and (a

;

1

)

;

= a. Dene also (

;

)

;

on strings by (a

1

:::a

n

)

;

=

a

;

n

:::a

;

1

. Now for an element of TT(A), which is a string on the alphabet

T(A)

t

T(A)

;

1

, say

1

:::

n

, we let

A

(

1

:::

n

) be the concatenation of the

strings ~

1

::: ~

n

on the alphabet A

t

A

;

1

, where ~

i

=

i

if

i

2

T(A), and

~

i

= (

i

)

;

if

i

2

T(A)

;

1

. Of course we still have to remove possible substrings

of the form aa

;

1

etc.

Now let us look at algebras for the group monad: maps T(A)

h

!

A such that

for a string of strings

=

1

:::

n

=

hh

s

11

:::s

k

1

1

i

:::

h

s

1

n

:::s

k

n

n

ii

we have that

h(

h

h

1

:::h

n

i

) = h(

h

s

11

:::s

k

1

1

:::s

1

n

:::s

k

n

n

i

)

and

h(

h

a

i

) = a for a

2

A

I claim that this is the same thing as a group structure on A, with multiplication

a

b = h(

h

ab

i

).

The unit element is given by h(

hi

) the inverse of a

2

A is h(

h

a

;

1

i

) since

h(

h

ah(

h

a

;

1

i

)

i

) = h(

h

h(

h

a

i

)h(

h

a

;

1

i

)

i

) =

h(

h

aa

;

1

i

) = h(

hi

), the unit element

Try to see for yourself how the associativity of the monad and its algebras trans-

forms into associativity of the group law.

Exercise 89

. Finish the proof of the theorem: for the group monad T, there

is an equivalence of categories between T-Alg and Grp.
This situation is very important and has its own name:

56

background image

6. Monads and Algebras

Denition 6.2

Given an adjunction

C

//

G

D

oo

F

,

F

a

G

there is always a

com-

parison functor K :

C

!

T

-Alg for

T = GF

, the monad induced by the adjunc-

tion.

K

sends an object

C

of

C

to the

T

-algebra

GFG(C)

G

(

"

C

)

!

G(C)

.

We say that

C

is

monadic

over

D

if

K

is an equivalence.

Exercise 90

. Check that K(C) is a T-algebra. Complete the denition of

K as a functor. Check that in the example of the group monad, the functor

T-Alg

!

Grp dened there is a pseudo inverse to the comparison functor K.

In many cases however, the situation is not monadic. Take the forgetful functor

U : Pos

!

Set. It has a left adjoint F which sends a set X to the discrete

ordering on X (x

y i x = y). Of course, UF is the identity on Set and the

UF-algebras are just sets. The comparison functor K is the functor U, and this

is not an equivalence.

Exercise 91

. Why not? Hint: think of coproducts in both categories. Every

equivalence reects coproducts]
Another example of a monadic situation is of importance in domain theory.

Let Pos

?

be the category of partially ordered sets with a least element, and

order preserving maps which also preserve the least element.

There is an obvious inclusion functor U : Pos

?

!

Pos, and U has a left

adjoint F. Given a poset X, F(X) is X \with a bottom element added":

r

X

?

Given f : X

!

Y in Pos, F(f) sends the new bottom element of X to the new

bottom element of Y , and is just f on the rest. If f : X

!

Y in Pos is a map

and Y has a least element, we have F(X)

!

Y in Pos

?

by sending

?

to the

least element of Y . So the adjunction is clear.

The monad UF : Pos

!

Pos, just adding a least element, is called the

lifting

monad

. Unit and multiplication are:

57

background image

Categories

-

:

-

-

r

r

r

r

X

: X

!

T(X)

X

: T

2

(X)

!

T(X)

A T-algebra h : TX

!

X is rst of all a monotone map, but since h

X

= id

X

,

h is epi in Pos so surjective. It follows that X must have a least element h(

?

).

From the axioms for an algebra one deduces that h must be the identity when

restricted to X, and h(

?

) the least element of X.

Exercise 92

. Given

C

//

G

D

oo

F

, F

a

G, T = GF. Prove that the com-

parison functor K :

C

!

T-Alg satises U

T

K = G and KF = F

T

where

T-Alg

//

U

T

D

oo

F

T

as in theorem 6.1.

Another poset example: algebras for the power set monad

P

on Set (exam-

ple j)2.2). Such an algebra h :

P

(X)

!

X must satisfy h(

f

x

g

) = x and for

P

(X):

h(

f

h(A)

j

A

2

g

) = h(

f

x

j9

A

2

(x

2

A)

g

) = h(

)

Now we can, given an algebra structure on X, dene a partial order on X by

putting x

y i h(

f

xy

g

) = y.

Indeed, this is clearly reexive and antisymmetric. As to transitivity, if x

y

and y

z then

h(

f

xz

g

)=h(

f

xh(

f

yz

g

)

g

)

=

h(

f

h(

f

x

g

)h(

f

yz

g

)

g

)=h(

f

x

g

f

yz

g

)

=

h(

f

xy

g

f

z

g

)=h(

f

h(

f

xy

g

)h(

f

z

g

)

g

)=

h(

f

yz

g

)=z

so x

z.

Furthermore this partial order is

complete

: least upper bounds for arbitrary

subsets exist. For

W

B = h(B) for B

X: for x

2

B we have h(

f

xh(B)

g

) =

h(

f

x

g

B) = h(B) so x

W

B and if x

y for all x

2

B then

h(

f

h(B)y

g

)=h(B

f

y

g

)

=

h(

S

x

2

B

f

xy

g

)=h(

f

h(

f

xy

g

)

j

x

2

B

g

)=

h(

f

y

g

)=y

58

background image

6. Monads and Algebras

so

W

B

y.

We can also check that a map of algebras is a

W

-preserving monotone

function. Conversely, every

W

-preserving monotone function between complete

posets determines a

P

-algebra homomorphism.

We have an equivalence between the category of complete posets and

W

-

preserving functions, and

P

-algebras.

Exercise 93

. Let P : Set

op

!

Set be the contravariant powerset functor,

and "P its left adjoint, as in j) of 5.1. Let T : Set

!

Set the induced monad.

a) Describe unit and multiplication of this monad explicitly.
b) Show that Set

op

is equivalent to T-Alg Hint: if this proves hard, have a

look at VI.4.3 of Johnstone's \Stone Spaces"].

c) Conclude that there is an adjunction

CABool

//

Set

oo

which presents CABool as monadic over Set.

6.2

T

-Algebras at least as complete as

D

Let T be a monad on

D

. The following exercise is meant to show that if

D

has

all limits of a certain type, so does T-Alg. In particular, if

D

is complete, so is

T-Alg this is often an important application of a monadic situation.

Exercise 94

. Let

E

be a category such that every functor M :

E

!

D

has

a limiting cone. Now suppose M :

E

!

T-Alg. For objects E of

E

, let M(E) be

the T-algebra T(m

E

)

h

E

!

m

E

.

a) Let (D(

E

j

E

2

E

0

)) be a limiting cone for U

T

M :

E

!

D

. Using the

T-algebra structure on M(E) and the fact that U

T

M(E) = m

E

, show

that there is also a cone (TD(

E

j

E

2

E

0

)) for U

T

M

b) Show that the unique map of cones: (TD)

!

(D) induces a T-algebra

structure TD

h

!

D on D

c) Show that TD

h

!

D is the vertex of a limiting cone for M in T-Alg.

6.3 The Kleisli category of a monad

I said before that for a monad T on a category

D

, there are a \maximal and

a minimal solution" to the problem of nding an adjunction which induces the

given monad.

59

background image

Categories

We've seen the category T-Alg, which we now write as

D

T

we also write

G

T

: T-Alg

!

D

for the forgetful functor. In case T arises from an adjunction

C

//

G

D

oo

F

, there was a comparison functor

C

K

!

D

T

. In the diagram

C

//

K

G

>

>

>

>

>

>

>

>

D

T

~~

G

T

}

}

}

}

}

}

}

}

D

__

F

>

>

>

>

>

>

>

>

>>

F

T

}

}

}

}

}

}

}

}

we have that KF = F

T

and G

T

K = G.

Moreover, the functor K is unique with this property.

This leads us to dene a category T-Adj of adjunctions

C

//

G

D

oo

F

such

that GF = T. A

map

of such T-adjunctions from

C

//

G

D

oo

F

to

C

0

//

G

0

D

oo

F

0

is

a functor K :

C

!

C

0

satisfying KF = F

0

and G

0

K = G.

What we have proved about T-Alg can be summarized by saying that the

adjunction

D

T

//

G

T

D

oo

F

T

is a

terminal object

in T-Adj. This was the \maximal"

solution.

T-Adj has also an initial object: the

Kleisli category

of T, called

D

T

.

D

T

has the same objects as

D

, but a map in

D

T

from X to Y is an arrow X

f

!

T(Y )

in

D

. Composition is dened as follows: given X

f

!

T(Y ) and Y

g

!

T(Z) in

D

, considered as a composable pair of morphisms in

D

T

, the composition gf in

D

T

is the composite

X

f

!

T(Y )

T

(

g

)

!

T

2

(Z)

Z

!

T(Z)

in

D

.

Exercise 95

. Prove that composition is associative. What are the identi-

ties of

D

T

?

The adjunction

D

T

//

G

T

D

oo

F

T

is dened as follows: the functor G

T

sends the

object X to T(X) and f : X

!

Y (f : X

!

T(Y ) in

D

) to

T(X)

T

(

f

)

!

T

2

(Y )

Y

!

T(Y )

The functor F

T

is the identity on objects and sends X

f

!

Y to X

f

!

Y

Y

!

T(Y ),

considered as X

!

Y in

D

T

.

60

background image

6. Monads and Algebras

Exercise 96

. Dene unit and counit check F

T

a

G

T

.

Now for every adjunction

C

//

G

D

oo

F

with GF = T, there is a unique com-

parison functor L :

D

T

!

C

such that GL = G

T

and LF

T

= F.

L sends the object X to F(X) and f : X

!

Y (so f : X

!

T(Y ) = GF(Y )

in

D

) to its transpose ~f: F(X)

!

F(Y ).

Exercise 97

. Check the commutations. Prove the uniqueness of L w.r.t. these

properties.

61

background image

Categories

62

background image

7. Cartesian closed categories and the

-calculus

7 Cartesian closed categories and the

-calculus

Many set-theoretical constructions are completely determined (up to isomor-

phism, as always) by their categorical properties in Set. We are therefore

tempted to generalize them to arbitrary categories, by taking the character-

istic categorical property as a denition. Of course, this procedure is not really

well-dened and it requires sometimes a real insight to pick the `right' categori-

cal generalization. For example, the category of sets has very special properties:

f : X

!

Y is mono if and only if fg = fh implies g = h for any two maps

gh : 1

!

X, where 1 is a terminal object (we say 1 is

a generator

)

objects X and Y are isomorphic if there exist monos f : X

!

Y and

g : Y

!

X (the Cantor-Bernstein theorem)

every mono X

f

!

Y is part of a coproduct diagram

X

f

@

@

@

@

@

@

@

Z

//

g

Y

And if you believe the axiom of choice, there is its categorical version:

Every epi is split

None of these properties is generally valid, and categorical generalizations based

on them are usually of limited value

2

.

In this chapter we focus on a categorical generalization of a set-theoretical

concept which has proved to have numerous applications: Cartesian closed cat-

egories as the generalization of \function space".

In example f) of 5.1 we saw that the set of functions Z

X

appears as the value

at Z of the right adjoint to the product functor (

;

)

X. A category is called

cartesian closed

if such right adjoints always exist. In such categories we may

really think of this right adjoint as giving the \object of functions (or arrows)",

as the treatment of the -calculus will make clear.

7.1 Cartesian closed categories (ccc's) examples and ba-

sic facts

Denition 7.1

A category

C

is called

cartesian closed

or

a ccc

if it has nite

products, and for every object

X

of

C

the product functor

(

;

)

X

has a right

adjoint.

2

Asperti, for example, restricts his interpretation of the

-calculus to ccc's where 1 is a

generator. You might as well immediately restrict to Set, then.

63

background image

Categories

Of course, \the" product functor only exists once we have chosen a product

diagram for every pair of objects of

C

. In this chapter we assume that we

have such a choice, as well as a distinguished terminal object 1 and we assume

also that for each object X we have a

specied

right adjoint to the functor

(

;

)

X, which we write as (

;

)

X

(Many authors write X

)

(

;

), but I think

that overloads the arrows notation too much). Objects of the form Z

X

are

called

exponents

.

We have the

unit

Y

Y X

!

(Y

X)

X

and

counit

Y

X

X

"

Y X

!

Y

of the adjunction (

;

)

X

a

(

;

)

X

. Anticipating the view of Y

X

as the object

of arrows X

!

Y , we call "

evaluation

.

Examples

a) A preorder (or partial order) is cartesian closed if it has a top element 1,

binary meets x

^

y and for any two elements xy an element x

!

y satisfying

for each z:

z

x

!

y i z

^

x

y

b) Set is cartesian closed Cat is cartesian closed (2.1)

c) Top is not cartesian closed, however the category of locally compact spaces

and continuous maps is

d) Pos is cartesian closed. The exponent Y

X

is the set of all monotone maps

X

!

Y , ordered pointwise (f

g i for all x

2

X, fx

gx in Y )

e) Grp and Abgp are not cartesian closed. In both categories, the initial

object is the one-element group. Since for non-initial groups G, (

;

)

G

does not preserve the initial object, it cannot have a right adjoint

f)

1

is cartesian closed

0

isn't (why?)

g) Set

C

op

is cartesian closed. Products and 1 are given \pointwise" (in fact

all limits are), that is F

G(C) = F(C)

G(C) and 1(C) is the terminal

1 in Set, for all C

2

C

0

.

The construction of the exponent G

F

is a nice application of the Yoneda

lemma. Indeed, for G

F

to be the right adjoint (at G) of (

;

)

F, we need

for every object C of

C

:

Set

C

op

(h

C

FG)

'

Set

C

op

(h

C

G

F

)

'

G

F

(C)

64

background image

7. Cartesian closed categories and the

-calculus

where the last isomorphism is by the Yoneda lemma.
Now the assignment C

7!

Set

C

op

(h

C

FG) denes a functor

C

op

!

Set,

which we denote by G

F

. At the same time, this construction denes a

functor (

;

)

F

: Set

C

op

!

Set

C

op

, which is right adjoint to (

;

)

F. It is

a nice exercise to prove this.

h) A monoid is never cartesian closed unless it's trivial.

Exercise 98

. Show that every Boolean algebra is cartesian closed.

Exercise 99

. Show that CABool is not cartesian closed use 2.3].

Exercise 100

. Show that a complete partial order is cartesian closed if and

only if it's a frame see 4.4].

Exercise 101

. Let ( be a frame. By the preceding exercise, it is cartesian

closed denote by x

!

y the exponent in (. This exercise is meant to let you

show that

C

is cartesian closed.

a) Show that ( also has greatest lower bounds

V

B for all subsets B.

b) Given objects (XE

X

) and (YE

Y

), dene their exponent (YE

Y

)

(

XE

X

)

as (Y

X

E) where Y

X

is the set of all functions X

!

Y in Set, and

E(f) =

^

E

X

(x)

!

E

Y

(f(x))

j

x

2

X

Show that this denes a right adjoint (at (YE

Y

)) of (

;

)

(XE

X

).

Some useful facts:

C

is cartesian closed if and only if it has nite products, and for each pair

of objects XY there is an object Y

X

and an arrow " : Y

X

X

!

Y such

that for every Z and map Z

X

f

!

Y there is a unique Z

~

f

!

Y

X

such

that

Z

X

//

f

%%

~

f

id

X

K

K

K

K

K

K

K

K

K

K

Y

Y

X

X

"

v

v

v

v

v

v

v

v

v

commutes.

In a ccc, there are natural isomorphisms 1

X

'

1 (Y

Z)

X

'

Y

X

Z

X

(Y

Z

)

X

'

Y

Z

X

.

65

background image

Categories

If a ccc has coproducts, we have X

(Y + Z)

'

(X

Y ) + (X

Z) and

Y

Z

+

X

'

Y

Z

Y

X

.

Exercise 102

. Prove these facts.

Recall that two maps Z

X

!

Y and Z

!

Y

X

which correspond to each

other under the adjunction are calles each other's

transposes

.

Exercise 103

. In a ccc, prove that the transpose of a composite Z

g

!

W

f

!

Y

X

is

Z

X

g

id

X

;

!

W

X

~

f

!

Y

if ~f is the transpose of f.

Lemma 7.2

In a ccc, given

f : X

0

!

X

let

Y

f

: Y

X

!

Y

X

0

be the transpose

of

Y

X

X

0

id

f

!

Y

X

X

"

!

Y

Then for each

f : X

0

!

X

and

g : Y

!

Y

0

the diagram

Y

X

Y

f

//

g

X

Y

0

X

Y

0f

Y

X

0

//

g

X

0

Y

0

X

0

commutes.

Proof

. By the exercise, the transposes of both composites are the top and

bottom composites of the following diagram:

Y

0

X

X

0

//

id

f

Y

0

X

X

$$

"

I

I

I

I

I

I

I

I

I

I

Y

X

X

0

88

g

X

id

q

q

q

q

q

q

q

q

q

q

//

id

f

&&

Y

f

id

M

M

M

M

M

M

M

M

M

M

Y

X

X

88

g

X

id

p

p

p

p

p

p

p

p

p

p

p

//

"

Y

//

g

Y

0

Y

X

0

X

0

88

"

p

p

p

p

p

p

p

p

p

p

p

p

//

g

X

0

id

Y

0

X

0

X

0

::

"

u

u

u

u

u

u

u

u

u

u

This diagram commutes because the right hand \squares" are naturality squares

for ", the lower left hand square commutes because both composites are the

transpose of Y

f

, and the upper left hand square commutes because both com-

posites are g

X

f.

66

background image

7. Cartesian closed categories and the

-calculus

Proposition 7.3

For every ccc

C

there is a functor

C

op

C

!

C

, assigning

Y

X

to

(XY )

, and given

g : Y

!

Y

0

and

f : X

0

!

X

,

g

f

: Y

X

!

Y

0

X

0

is either of

the composites in the lemma.

Exercise 104

. Prove the proposition.

7.2 Typed

-calculus and cartesian closed categories

The -calculus is an extremely primitive formalism about functions. Basically,

we can form functions (by -abstraction) and apply them to arguments that's

all. Here I treat briey the

typed

-calculus.

We start with a set

S

of

type symbols

S

1

S

2

:::

Out of

S

we make the set of types as follows: every type symbol is a type,

and if T

1

and T

2

are types then so is (T

1

)

T

2

).

We have also

terms

of each type (we label the terms like t:T to indicate that

t is a term of type T):

we may have constants c:T of type T

for every type T we have a denumerable set of variables x

1

:Tx

2

:T:::

given a term t:(T

1

)

T

2

) and a term s:T

1

, there is a term (ts):T

2

given t:T

2

and a variable x:T

1

there is a term x:t:T

1

)

T

2

.

Terms x:t are said to be formed by -

abstraction

. This procedure binds the

variable x in t. Furthermore we have the usual notion of substitution for free

variables in a term t (types have to match, of course). Terms of form (ts) are

said to be formed by

application

.

In the -calculus, the only statements we can make are equality statements

about terms. Again, I formulate the rules in terms of theories. First, let us say

that a

language

consists of a set of type symbols and a set of constants, each of

a type generated by the set of type symbols.

An

equality judgement

is an expression of the form ;

j

t = s:T (to be read:

\; thinks that s and t are equal terms of type T "), where ; is a nite set of

variables which includes all the variables free in either t or s, and t and s are

terms of type T.

A

theory

is then a set

T

of equality judgements which is closed under the

following rules:

i) ;

j

t = s:T in

T

implies $

j

t = s:T in

T

for every superset $ of ;

ii) FV (t)

j

t = t:T is in

T

for every term t:T of the language (again, FV (t) is

the set of free variables of t)

if ;

j

t = s:T and ;

j

s = u:T are in

T

then so is ;

j

t = u:T

67

background image

Categories

iii) if t(x

1

:::x

n

):T is a term of the language, with free variables x

1

:S

1

,:::,x

n

:S

n

,

and ;

j

s

1

= t

1

:S

1

:::;

j

s

n

= t

n

:S

n

are in

T

then

;

j

ts

1

=x

1

:::s

n

=x

n

] = tt

1

=x

1

:::t

n

=x

n

]:T

is in

T

iv) if t and s are terms of type (T

1

)

T

2

), x a variable of type T

1

which does

not occur in t or s, and ;

f

x

gj

(tx) = (sx):T

2

is in

T

, then ;

n

f

x

gj

t =

s:(T

1

)

T

2

) is in

T

v) if s:T

1

and t:T

2

are terms and x a variable of type T

2

, then

FV (s)

n

f

x

g

FV (t)

j

((x:s)t) = st=x]:T

1

is in

T

.

Given a language, an interpretation of it into a ccc

C

starts by choosing objects

S ]] of

C

for every type symbol S. This then generates objects T ]] for every

type T by the clause

T

1

)

T

2

]] = T

2

]]

T

1

]]

The interpretation is completed by choosing interpretations

1

c

]]

!

T ]]

for every constant c:T of the language.

Such an interpretation then generates, in much the same way as in chapter 4,

interpretations of all terms. For a nite set ; =

f

x

1

:T

1

:::x

n

:T

n

g

let's again

write ;]] for the product T

1

]]

T

n

]] (this is only dened modulo a

permutation of the factors of the product, but that will cause us no trouble).

The interpretation of t:T will now be an arrow

FV (t)]]

t

]]

!

T ]]

dened as follows:

x]] is the identity on T ]] for every variable x:T

given t]] : FV (t)]]

!

T

2

]]

T

1

]]

and s]] : FV (s)]]

!

T

1

]] we let

(ts)]] : FV ((ts))]]

!

T

2

]] be the composite

FV ((ts))]]

h

t

]]

t

s

]]

s

i

;

!

T

2

]]

T

1

]]

T

1

]]

"

!

T

2

]]

where

t

and

s

are the projections from FV ((ts))]] to FV (t)]] and

FV (s)]], respectively

68

background image

7. Cartesian closed categories and the

-calculus

given t]] : FV (t)]]

!

T

2

]] and the variable x:T

1

we let x:t]] : FV (t)

n

f

x

g

]]

!

T

2

]]

T

1

]]

be the transpose of

FV (t)

n

f

x

g

]]

T

1

]]

~

t

!

T

2

]]

where, if x occurs free in t so FV (t)

n

f

x

g

]]

T

1

]]

'

FV (t)]], ~t is

just t]] and if x doesn't occur in t, ~t is t]] composed with the obvious

projection.

We now say that an equality judgement ;

j

t = s:T is

true

in this interpretation,

if the diagram

FV (t)]]

$$

t

]]

I

I

I

I

I

I

I

I

I

;]]

::

t

u

u

u

u

u

u

u

u

u

$$

s

I

I

I

I

I

I

I

I

I

T ]]

FV (s)]]

::

s

]]

u

u

u

u

u

u

u

u

u

commutes (again,

s

and

t

projections).

Lemma 7.4

Let

t(x

1

:::x

n

):T

have free variables

x

i

:T

i

and let

t

i

:T

i

be terms.

Let

~t

i

: FV (tt

1

=x

1

:::t

n

=x

n

])]]

!

T

i

]]

be the obvious composite of projection and

t

i

]]

.

Then the composition

FV (tt

1

=x

1

:::t

n

=x

n

])]]

h

~

t

i

j

i

=1

:::n

i

;

!

n

Y

i

=1

T

i

]] = FV (t)]]

t

]]

!

T ]]

is the interpretation

tt

1

=x

1

:::t

n

=x

n

]]]

.

Exercise 105

. Prove the lemma take your time. This is not immediate].

Theorem 7.5

Let

S

be a set of equality judgements and

T

= Cn(S)

be the

least theory containing

S

. If every judgement of

S

is true in the interpretation,

so is every judgement in

T

.

Proof

. Again, we show that the set of true judgements is a theory, i.e. closed

under the rules in the denition of a theory.

i) and ii) are trivial

iii) follows at once by lemma 7.4

69

background image

Categories

iv) Since ;

(;

n

f

x

g

)

f

x

g

and because of the inductive hypothesis, we have

that

FV (s)]]

T

1

]]

//

s

]]

id

T

1

)

T

2

]]

T

1

]]

''

"

O

O

O

O

O

O

O

O

O

O

O

;

n

f

x

g

]]

66

s

id

n

n

n

n

n

n

n

n

n

n

n

n

((

t

id

P

P

P

P

P

P

P

P

P

P

P

P

T

2

]]

FV (t)]]

T

1

]]

//

t

]]

id

T

1

)

T

2

]]

T

1

]]

77

"

o

o

o

o

o

o

o

o

o

o

o

commutes. Taking the transposes of both maps, we get the equality we want.

v) According to lemma 7.4, FV (st=x])]]

s

t=x

]]]

;

!

T

1

]] is

FV (st=x])]]

~

t

!

FV (s)]]

s

]]

!

T

1

]]

This is the same as
FV (st=x])]]

h

t

]]

i

!

FV (s)

n

f

x

g

]]

T

2

]]

x:s

]]

id

;

!

T

2

)

T

1

]]

T

2

]]

"

!

T

1

]]

which is

FV ((x:s)t)]]

((

x:s

)

t

)]]

;

!

T

1

]]

There is also a

completeness theorem

: if a judgement ;

j

t = s:T is true in all

possible interpretations, then every theory (in a language this judgement is in)

contains it.

The relevant construction is that of a syntactic cartesian closed category

out of a theory, and an interpretation into it which makes exactly true the

judgements in the theory. The curious reader can nd the, somewhat laborious,

treatment in Lambek & Scott's \Higher Order Categorical Logic".

7.3 Representation of primitiverecursive functions in ccc's

with natural numbers object

Dedekind observed, that in Set, the set ! is characterized by the following

property: given any set X, any element x

2

X and any function X

f

!

X, there

is a unique function F : !

!

X such that F(0) = x and F(x + 1) = f(F(x)).

Lawvere took this up, and proposed this

categorical

property as a denition

(in a more general context) of a \natural numbers object" in a category.

70

background image

7. Cartesian closed categories and the

-calculus

Denition 7.6

In a category

C

with terminal object 1, a

natural numbers ob-

ject

is a triple

(0NS)

where

N

is an object of

C

and

1

0

!

N

,

N

S

!

N

arrows

in

C

, such that for any other such diagram

1

//

x

X

//

f

X

there is a

unique

map

: N

!

X

making

1

//

0

x

?

?

?

?

?

?

?

?

N

//

S

N

X

//

f

X

commute.

Of course we think of 0 as the zero element, and of S as the successor map. The

dening property of a natural numbers object enables one to \do recursion",

a weak version of which we show here: we show that every primitive recursive

function can be represented in a ccc with natural numbers object.

Denition 7.7

Let

C

be a ccc with natural numbers object

(0NS)

. We say

that a number-theoretic function

F :

N

k

!

N

is

represented

by an arrow

f :

N

k

!

N

if for any

k

-tuple of natural numbers

n

1

:::n

k

, the diagram

1

//

0

&&

0

M

M

M

M

M

M

M

M

M

M

M

M

M

N

//

h

S

n

1

:::S

n

k

i

N

k

f

N

//

S

F

(n

1

:::

n

k

)

N

commutes.

Recall that the class of

primitive recursive

functions is given by the following

clauses:

The constant zero function ~x:0 :

N

k

!

N

, the function x:x+ 1 :

N

!

N

and the projections ~x:x

i

:

N

!

N

are primitive recursive

The primitive recursive functions are closed under composition: if F

1

:::F

k

:

N

l

!

N

and G :

N

k

!

N

are primitiverecursive, then so is G(

h

F

1

:::F

k

i

) :

N

l

!

N

The primitive recursive functions are closed under

denition by primitive

recursion

: if G :

N

k

!

N

and H :

N

k

+2

!

N

are primitive recursive,

and F :

N

k

+1

!

N

is dened by F(0~x) = G(~x) and F(n + 1~x) =

H(nF(n~x)~x) then F is primitive recursive.

71

background image

Categories

Proposition 7.8

In a ccc

C

with natural numbers object, every primitive re-

cursive function is representable.

Proof

. I do only the case for denition by primitive recursion. So by inductive

hypothesis we have arrows G and H representing the homonymous functions.

By interpretation of the -calculus, I use -terms: so there is an arrow

~x:G(~x) : 1

!

N

(

N

k

)

and an arrow

~x:H(n(~x)~x) : N

(

N

k

)

N

!

N

(

N

k

)

which is the interpretation of a term with free variables :N

(

N

k

)

and n:N this

map is the exponential transpose of the map which intuitively sends (n~x) to

(n(~x)~x). Now look at

1

//

h

~x:G

(

~x

)

0

i

N

(

N

k

)

N

//

(

~x:H

(

n

(

~x

)

~x

))

S

N

(

N

k

)

N

By the natural numbers object property, there is now a unique map

"F =

h

~F

i

: N

!

N

(

N

k

)

N

which makes the following diagram commute:

1

//

0

))

h

~x:G

(

~x

)

0

i

R

R

R

R

R

R

R

R

R

R

R

R

R

R

R

R

N

F

//

S

N

F

N

(

N

k

)

N

//

(

~x:H

(

n

(

~x

)

~x

))

S

N

(

N

k

)

N

One veries that is the identity, and that the composite

N

k

+1

//

~

F

id

N

(

N

k

)

N

k

//

"

N

represents F.

Exercise 106

. Make these verications.

That's it!!

72

background image

Index

abelianization, 5

adjoint functor theorem, 50

adjunction, 45

Alexandro topology, 5

algebras for monad, 54

arrows, 1

associative, 1

atom in Boolean algebra, 16
Boolean algebra, 15

atomic, 16

complete, 15

category, 1

cartesian, 23

cartesian closed, 63

complete, 23

discrete, 13

nitely complete, 23

has binary products, 20

has equalizers, 20

has pullbacks, 20

indiscrete, 13

left exact, 23

lex, 23

locally small, 4

path, 3

quotient, 3

regular, 29

slice, 4

small, 13

ccc, 63

closure operation on poset, 54

cocone for a functor, 25

codomain, 1

coequalizer, 25

coequalizer diagram, 25

coherent logic, 33

colimiting cocone, 25

comonad, 53

comparison functor, 57

complement in a lattice, 15

composition, 1

comultiplication of comonad, 53

cone for a functor, 17

congruence relation, 3

coproduct, 25

coproduct inclusions, 25

coprojections, 25

counit of adjunction, 45

counit of comonad, 53
diagram commutes, 4

diagram of type

C

, 17

domain, 1

duality principle, 6
embedding, 10

epi, 6

epimorphism, 6

equality judgement in -calculus, 67

equalizer, 18

equalizer diagram, 18

equivalence of categories, 15

equivalent categories, 15

equivalent formulas, 39

evaluation in ccc, 64

exponents in ccc, 64
frame, 39

free group, 3

free monoid, 46

functor, 2

contravariant, 5

covariant, 5

faithful, 7

forgetful, 2

free, 3

full, 7

Hom, 5

73

background image

INDEX

preserving a property, 7

preserving limits, 23

reecting a property, 7

representable, 4

generator, 63

group monad, 56

groupoid, 14

Grp, 2

Grph, 2
homotopy, 3
identity arrow, 1

image of a map, 32

index category of diagram, 17

initial object, 7

inverse of an arrow, 7

isomorphic objects, 8

isomorphism, 7
kernel pair of a map, 29

Kleisli category of monad, 60
labelled sequent, 35

-abstraction, 67

-calculus, 67

lattice, 15

distributive, 15

left adjoint functor, 43

lifting monad, 57

limiting cone, 17
MacLane's pentagon, 23

map, 1

monad, 53

monadic, 57

mono, 6

monoid, 1

monomorphism, 6

morphism, 1

multiplication of monad, 53
natural

bijection, 10

natural numbers object, 71

natural transformation, 9
objects, 1
Pos, 2

preorder, 1

primitive recursive function, 71

product category, 2

product cone, 18

product in category, 18

projections, 18

pseudo inverse of a functor, 15

pullback along a map, 32

pullback diagram, 20

pushout, 26
regular epi, 27

regular mono, 22

retraction, 7

right adjoint functor, 43

Rng, 2
section, 7

solution set condition (ssc), 50

specialization ordering, 6

split epi, 7

split mono, 7

stable under pullback, 30

subobject, 31
terminal object, 7

theory in -calculus, 67

theory in coherent logic, 35

Top, 2

transpose of map, 43

triangle equalities, 45
unit of adjunction, 45

unit of monad, 53
vertex of a cone, 17

74

background image

INDEX

Yoneda embedding, 10

Yoneda lemma, 10

75


Wyszukiwarka

Podobne podstrony:
Heckerman Tutorial On Learning Bayesian Networks (1995) [sharethefiles com]
Passman Group Rings, Crossed Products & Galois Theory (1986) [sharethefiles com]
Jay An Introduction to Categories in Computing [sharethefiles com]
Chen Elementary & Analytic Number Theory (1981) [sharethefiles com]
Lasenby et al Multivector Derivative Approach 2 Lagrangian Field Theory (1993) [sharethefiles com]
Halpern A logical approach to reasoning about uncertainty a tutorial (1995) [sharethefiles com]
Fokkinga A Gentle Introduction to Category Theory the calculational approach (1994) [sharethefiles
Elkies Combinatorial game Theory in Chess Endgames (1996) [sharethefiles com]
Turbiner Lie Algebraic Approach 2 the Theory of Polynomial Solutions (1992) [sharethefiles com]
Czichowski Lie Theory of Differential Equations & Computer algebra [sharethefiles com]
[Martial arts] Physics of Karate Strikes [sharethefiles com]
Meinrenken Clifford Algebras & the Duflo Isomorphism (2002) [sharethefiles com]
Guided Tour on Wind Energy [sharethefiles com]
Brin Introduction to Differential Topology (1994) [sharethefiles com]
Olver Lie Groups & Differential Equations (2001) [sharethefiles com]
Major A Spin Network Primer (1999) [sharethefiles com]
Parashar Differential Calculus on a Novel Cross product Quantum Algebra (2003) [sharethefiles com]
Kollar The Topology of Real & Complex Algebraic Varietes [sharethefiles com]
Doran Geometric Algebra & Computer Vision [sharethefiles com]

więcej podobnych podstron