[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

categories: Re: effective topos

Dear Jirka,

My partial understanding of the effective topos suggests that it is not
LFP and indeed does not even have small colimits. It is not a Grothendieck
topos (i.e. does not have a geometric morphism to sets with a discrete
left adjoint, although it does misleadingly have a "codiscrete"-like
functor from sets). Replying to your two specific questions:

a) The effective topos does not have many finite hom sets, as can be seen
by comparing it with the approximation below.

b) In the absence of colimits, it is not clear how to even formulate
the idea that finite generation implies finite presentability.

There is a first approximation, due to Phil Mulry, which is a
categorical version of the concepts of Banach, Mazur, and Ersov. It is not
only a topos, but a Grothedieck topos and indeed a coherent one and hence
locally finitely presentable. Consider the category of recursive sets and
recursive maps (or equivalently just the monoid of recursive endomaps of
N). Its canonical Grothendieck topology turns out to be finitary. The
Mulry topos consists of sheaves on this site. In a sense, all maps and
objects have some aspect of recursiveness or "effectiveness" in the spirit
of Banach, Mazur, and Ersov, and the distinction between
"recursive" and "recursively enumerable" does not apply to objects,
but rather to inclusion maps, which may or may not have Boolean

Perhaps though, as you suggest, a category generated by a category with
finite hom sets would better express the needs of iteration theory
than anything (like the effective topos) based on an already-achieved bad

There is an issue involving recursivity that categorists should settle:
How general is Higman's theorem? In group theory the word problem (whether
a given finitely generated group is recursively related) is equivalent to
the purely algebraic one of whether the given group can be embedded as a
subgroup of a finitely presentable one. 
For which other algebraic categories is the same statement true? or
is it possibly true for the category of single-sorted algebraic theories?
The latter problem was posed by Bill Boone, but as far as I know, is 
not yet resolved.

For the category of first-order theories, a theorem analogous to Higman's
was proved by Craig and Vaught; for that case, they gave a kind of
intuitive argument: using a few additional predicates one can express
enough of number theory to encode a fragmentary satisfaction relation and
any given recursive set of axioms, so that one can then add the one
additional axiom that says "all those axioms are true".
Of course, it is non-trivial that this argument actually works.

Do you or anybody on the catnet know of any progress on this question?


F. William Lawvere			
Mathematics Department, State University of New York
244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA
Tel. 716-645-6284		   
HOMEPAGE:  http://www.acsu.buffalo.edu/~wlawvere

On Wed, 9 Jan 2002, Jiri Adamek wrote:

> In the study of iterative theories we use the concept of a strongly
> locally presentable category. This is an extensive, locally finitely
> presentable category such that
> a. hom-sets of finitely presentable objects are finite
> and 
> b. a strong quitent of a finitely presentable object is finitely pres.
> I would appreaciate knowing whether the effective topos has all these
> properties.
> Thanks,
> Jiri Adamek
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> alternative e-mail address (in case reply key does not work):
> J.Adamek@tu-bs.de
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx