ñòð. 20 |

@ Â¡ (G wr H ) wr K

G wr(H wr K)

@ Â¡

@

R Â¡

Âª

Cat

Note that the standard wreath product is not associative.

4.4 Wreath products 55

4.4.9 Applications of the wreath product It is natural to wish to simulate

complicated state transition systems using systems built up in some way from a

small stock of simpler ones. This requires a precise notion of simulation. This is

deÂ¯ned in various ways in the literature. In some cases one says a functor F :

Â¡! is a simulation of (the word `cover' is often used) if it has certain special

properties. Other authors have the functor going the other way.

The Krohn{Rhodes Theorem for monoids says that every Â¯nite monoid action

is simulated by an iterated wreath product of Â¯nite simple groups and certain

very small monoids. The original Krohn{Rhodes Theorem was stated for semi-

groups. Discussions are in [Wells, 1976] and [Eilenberg, 1976]; the latter uses a

diÂ®erent deÂ¯nition of cover. Wells [1980] proved a generalization of a weak form of

the Krohn{Rhodes Theorem for Â¯nite categories and set-valued functors (which

generalize the concept of action by a monoid, as discussed in Section 3.2). Wells

[1988a, 1988b] describes how to use some of these decomposition techniques for

category-valued functors.

Rhodes and Tilson use the idea of `division' of categories, which is related

to the notion of cover, as the basic idea of an extensive study of varieties of

semigroups and complexity. See See [Rhodes and Tilson, 1989, Rhodes and Weil,

1989].

Nico [1983] deÂ¯nes a category induced by any functor called the `kernel cate-

gory' of the functor and proves a theorem which embeds the domain of the functor

into the standard wreath product of the codomain and the kernel. This gener-

alizes an old theorem of Kaloujnine and Krasner. It follows that every functor

factors as a full and faithful functor which is injective on objects, followed by a

Â¯bration. Street and Walters [1973] have a related theorem.

In the case of groups, the kernel category of a homomorphism is a category

equivalent, but not isomorphic, to the actual kernel of the homomorphism. In the

case that and are monoids, the kernel category (which is not a monoid in

general) is called the derived category of F . Rhodes and Tilson [1989] have a

tighter deÂ¯nition obtained by imposing a congruence on the kernel. A theorem

analogous to Nico's theorem is true for the tighter deÂ¯nition, as well. It is stated

for semigroups and relations, not merely monoids and homomorphisms, so it is

neither more nor less general than Nico's theorem. In the semigroup case, the

`category' is replaced by a `semigroupoid', which is like a category but does not

have to have identity arrows.

4.4.10 Exercises

1. Show that the discrete wreath product of two monoids is a monoid.

2. Show that the wreath product of two groups (monoids in which every element

is invertible) regarded as categories is a category in which every arrow is an

isomorphism.

5

Toposes

A topos is a cartesian closed category with some extra structure which produces

an object of subobjects for each object. This structure makes toposes more like

the category of sets than cartesian closed categories generally are.

Toposes, and certain subcategories of toposes, have proved attractive for the

purpose of modeling computation. A particular reason for this is that in a topos, a

subobject of an object need not have a complement. One of the fundamental facts

of computation is that it may be possible to list the elements of a subset eÂ®ectively,

but not the elements of its complement (see [Lewis and Papadimitriou, 1981],

Theorems 6.1.3 and 6.1.4.). Sets which cannot be listed eÂ®ectively do not exist for

computational purposes, and toposes provide a universe of objects and functions

which has many nice set-like properties but which does not force complements to

exist. We discuss one speciÂ¯c subcategory of a topos, the category of modest sets,

which has been of particular interest in the semantics of programming languages.

Toposes have interested mathematicians for other reasons. They are an ab-

straction of the concept of sheaf, which is important in pure mathematics. They

allow the interpretation of second-order statements in the category in an exten-

sion of the language associated to cartesian closed categories in Chapter 6. This

fact has resulted in toposes being proposed as an alternative to the category

of sets for the foundations of mathematics. Toposes can also be interpreted as

categories of sets with an internal system of truth values more general than the

familiar two-valued system of classical logic; this allows an object in a topos to be

thought of as a variable or time-dependent set, or as a set with various degrees of

membership. In particular, most ways of deÂ¯ning the category of fuzzy sets lead

to a category which can be embedded in a topos.

Sections ES 5.1 and ES 5.2 describe the basic properties of toposes, for the

most part without proof. Section ES 5.3 takes a closer look at an aspect of toposes

which make many of them a better model of computation than, for example, Set.

Sections ES 5.4 and ES 5.5 describe a special case of categories of sheaves

which makes the connection with sets with degrees of membership clear. The

category of graphs is discussed as an example there. Section ES 5.6 describes the

connection with fuzzy sets.

In Section ES 5.7 we describe category objects in a category, a notion that is

needed in Section ES 5.8, which is a brief description of the realizability topos

and modest sets.

56

5.1 DeÂ¯nition of topos 57

This chapter depends on Chapters 1 through 6, Chapter 8, and Chapter 9. In

addition, Section ES 5.7 needs ES 2.1.5, 11.1 and 11.2.

Sections 15.1 and 15.2 are needed in all the remaining sections. After that,

the chapter consists of four independent units: Section 15.3, Sections 15.4 and 5,

Section 15.6 and Sections 15.7 and 8.

Basic toposes are [Johnstone, 1977], [Barr and Wells, 1985], [Lambek and

Scott, 1986], [Bell, 1988], [McLarty, 1992], [Mac Lane and Moerdijk, 1992]. None

of these are aimed at applications to computer science. We do not discuss the

language and logic corresponding to a topos in this book. The most accessible

introduction to this is perhaps that of [McLarty, 1992], Chapter 11. Other discus-

sions of the language and the relation with logic are in [Makkai and Reyes, 1977],

[Fourman, 1977], [Fourman and Vickers, 1986], [Boileau and Joyal, 1981]. The

texts [Makkai and Reyes, 1977] and [Freyd and Scedrov, 1990] discuss toposes

and also more general classes of categories that have a rich logical structure. The

use of toposes speciÂ¯cally for semantics is discussed in [Hyland, 1982], [Hyland

and Pitts, 1989], [Vickers, 1992].

5.1 DeÂ¯nition of topos

5.1.1 The subobject functor Recall from 2.8.11 that if C is an object of a

!

category, a subobject of C is an equivalence class of monomorphisms C0 )Â¡ C

! !

where f0 : C0 )Â¡ C is equivalent to f1 : C1 )Â¡ C if and only if there are arrows

(necessarily isomorphisms) g : C0 Â¡ C1 and h : C1 Â¡ C0 such that f1 Â± g = f0

! !

and f0 Â± h = f1 .

Assuming the ambient category has pullbacks, the `set of subobjects' func-

tion is the object function of a functor Sub : op Â¡ Set: precisely, for an object

!

C, Sub(C) is the set of subobjects of C. We must deÂ¯ne Sub on arrows.

If k : C 0 Â¡ C is an arrow and if f0 : C0 )Â¡ C represents a subobject of C,

! !

then in a pullback

k0 -

0

C0 C0

? ?

0 (5.1)

f0 f0

? ?

-C

C0 k

0

the arrow f0 is also a monomorphism (see 8.3.4).

It is left as an exercise to prove, using the universal mapping property of

! !

pullbacks, that if the monomorphism f0 : C0 )Â¡ C is equivalent to f1 : C1 )Â¡ C,

0 0 0 0 0 0

! !

then the pullbacks f0 : C0 )Â¡ C and f1 : C1 )Â¡ C are also equivalent. Thus not

only is a pullback of a monomorphism a monomorphism, but also a pullback of

a subobject is a subobject.

58 Toposes

Thus we can deÂ¯ne, for an arrow k as above,

Sub(k) : Sub(C) Â¡ Sub(C 0)

!

to be the function that sends the equivalence class containing f0 to the equivalence

0

class containing the pullback f0 .

ñòð. 20 |