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

*To*: categories <categories@mta.ca>*Subject*: categories: Re: effective topos*From*: F W Lawvere <wlawvere@acsu.buffalo.edu>*Date*: Thu, 10 Jan 2002 13:13:51 -0500 (EST)*In-reply-to*: <Pine.GSO.3.96.1020109153019.7372L-100000@lisa>*Reply-to*: wlawvere@acsu.buffalo.edu*Sender*: cat-dist@mta.ca

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 complements. 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 infinity. 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? Bill ************************************************************ 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 > > > > > >

**References**:**categories: effective topos***From:*Jiri Adamek <adamek@iti.cs.tu-bs.de>

- Prev by Date:
**categories: Re: lluf subcategory** - Next by Date:
**categories: effective topos** - Previous by thread:
**categories: Re: effective topos** - Next by thread:
**categories: effective topos** - Index(es):