From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4641 Path: news.gmane.org!not-for-mail From: "Prof. Peter Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Subtoposes of Eff Date: Mon, 29 Sep 2008 13:40:15 +0100 (BST) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1241020075 14167 80.91.229.2 (29 Apr 2009 15:47:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:47:55 +0000 (UTC) To: Categories mailing list Original-X-From: rrosebru@mta.ca Mon Sep 29 09:49:54 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 29 Sep 2008 09:49:54 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1KkI6x-0007Rx-MO for categories-list@mta.ca; Mon, 29 Sep 2008 09:44:23 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 137 Original-Lines: 44 Xref: news.gmane.org gmane.science.mathematics.categories:4641 Archived-At: Readers of Jaap van Oosten's new book on realizability will have come across the statement on p. 235 that the question "Is Set the only Grothendieck topos which occurs as a subtopos of the effective topos?", which Ieke Moerdijk asked him at his Ph.D. viva in 1991, is still unanswered. In fact I've known the answer to this question for at least five years: I referred to it in my talks at the European category theory meeting in Haute-Bodeux (September 2003) and the meeting on Ramifications of Category Theory in Firenze (November 2003). However, the proof hasn't been published anywhere (it will of course be in volume 3 of the Elephant when that is published -- and please don't ask me to predict when that will be!), so I thought I should let people know about it. We work in the realizability topos over an arbitrary pca A (all unexplained notation can be found in Jaap's book). Andy Pitts showed in his thesis that local operators on this topos correspond to maps j: PA --> PA whch "are nuclei in the logic of A-realizability", and that the corresponding subtopos of sheaves is equivalent to Set (or degenerate) iff the intersection \bigcap_{a \in A} j({a}) is inhabited. Suppose this condition fails; we shall show that the subtopos of j-sheaves is not complete. Let A_1 denote the assembly with underlying set A and [[a \in A_1]] = {a} for all a, and A_2 the assembly with the same underlying set and [[a \in A_2]] = j({a}). Note that A_2 is the j-closure of A_1 in \nabla A, and hence its associated j-sheaf. Also, by the assumption we've made, it is not the whole of \nabla A. We claim that the product of A copies of A_2 cannot exist in the topos of sheaves: if it did, it would obviously be a subobject of \nabla(A^A) (the latter being the product of A copies of \nabla A) and hence an assembly; moreover, its underlying set would be the whole of A^A since the forgetful functor from assemblies to Set (is representable, and hence) preserves all products which exist. Writing P for the product, for each a \in A the a^th projection A^A --> A must be trackable as a morphism P --> A_2; let e_a be an element of A which tracks it. Since A_2 is not the whole of \nabla A, we can find f(a) such that e_aa \not \in [[f(a) \in A_2]] (if e_aa is undefined, choose f(a) to be any element of A). Then f: A --> A has no realizers as a member of P. Peter Johnstone