From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7817 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Sat, 27 Jul 2013 10:33:02 +0200 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1374970375 12014 80.91.229.3 (28 Jul 2013 00:12:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 28 Jul 2013 00:12:55 +0000 (UTC) Cc: Marta Bunge , categories@mta.ca To: "Eduardo J. Dubuc" Original-X-From: majordomo@mlist.mta.ca Sun Jul 28 02:12:58 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1V3EbY-0006HB-W5 for gsmc-categories@m.gmane.org; Sun, 28 Jul 2013 02:12:57 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54781) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3EaD-0000by-Ig; Sat, 27 Jul 2013 21:11:33 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3EaE-00048L-J5 for categories-list@mlist.mta.ca; Sat, 27 Jul 2013 21:11:34 -0300 Content-Disposition: inline In-Reply-To: <51F2EDAC.3010403@dm.uba.ar> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7817 Archived-At: Dear Eduardo, let's carefully look how internal to SS your statement is. You start from a bounded geometric morphism F -| U : EE -> SS and an object X of EE. What ensures your claim is that there is a diagram (in EE) e X <<--- u^*G -----> G | | | p.b. | V V FJ ----> FI Fu where G --> FI is a generic family for P_F (the fibered topos associated with F : SS -> EE). Here you have an EXTERNAL existential quantification over J, u and e. But using local smallness of P_F you can concretely witness J as \coprod_{i \in I} hom_EE(G_i,X) and u as first projection on I. From this you also get e. But that means that one proves the statement on the metalevel which allows one to speak about SS, EE and functors between them. In particular, you have to argue how you can express within SS that e (a morphism of EE) is epic. How can you do this in the internal language of SS? You have to quantify over arbitrary maps in EE with source X. Moreover, you do not want to have your claim valid for just a single particular external X in EE but you want to have it "for all X in EE". Kripke-Joyaling this amounts to considering all external families a : A --> FK (as on p.51 of Marta and Jonathon's book though they use different letters). There is some possibility of giving a coherent account of this. If you have your base topos SS then split fibrations over SS are the same as categories internal to Psh(SS) (where Psh(SS) = Set^{SS^op} for Set big enough to contain SS as an internal category). Now you can reason in the internal language of Psh(SS) but not in the internal language of SS. That I have learnt from B'enabou some years ago but it's unpublished (as usual). Now the problem is that Psh(SS) is too weak a logic and one might want to work rather in sheaves over SS w.r.t. regular cover topology. In the work of Awodey, Forssell and Warren on their variant of algebraic set theory (http://www.phil.cmu.edu/projects/ast/Papers/afw_06.pdf) this is preformed to some extent. They consider Idl(SS), the "ideal completion of SS" within which SS appears as a small category. Best regards, Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]