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 10-Jan-2002 22:33:44 -0400,1768;000000000000-00000000
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
A locally finitely presentable category has all colimits the effective topos has not! Nor has the effective topos filtered colimits as otherwise it were cocomplete. Moreover, the global sections functor Gamma from Eff to Set doesn't have a left adjoint Delta but instead a right adjoint Nabla. Of course, one might ask nevertheless which objects are finitely presentable taking only account of existing filtered colimits. Alas, there the answer isn't easy at all (for me at least) and I don't even see why it should be interesting. Thomas Streicher
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
11-Jan-2002 08:50:59 -0400,3619;000000000000-00000000
Dear all, As Thomas and Bill pointed out, the effective topos is quite far from being cocomplete; indeed, a countable coproduct of copies of 1 does not exist. So the locally finitely presentable machinery seems not to work here, at least, externally. Bill points to Mulry's recursive topos as an approximation. Here is a question, related to a possible other approximation. Does the effective topos have a dense set of generators? In this case one could embed it into a Grothendieck topos by an embedding which preserves a lot of structure. It is easy to see that the full subcategory of Eff on the countable projective objects is essentially small and generates Eff. But is it dense? This is related to the following question: does the functor Nabla: Sets --> Eff preserve \omega _1-filtered colimits? (it is easy to see that it doesn't preserve filtered colimits; it does preserve \omega _1-filtered colimits as functor from Sets to the separated objects of Eff) I have been trying for some time to solve this; but I couldn't. It appears that set-theoretic combinatorics plays an important role here, and is more important than recursiveness. Jaap van Oosten 11-Jan-2002 08:51:05 -0400,2228;000000000000-00000000
participants (4)
-
F W Lawvere -
Jiri Adamek -
jvoosten@math.uu.nl -
Thomas Streicher