From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7820 Path: news.gmane.org!not-for-mail From: "Eduardo J. Dubuc" Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Sat, 27 Jul 2013 17:00:53 -0300 Message-ID: References: <20130726200858.GB32154@mathematik.tu-darmstadt.de> <51F2EDAC.3010403@dm.uba.ar> <20130727083302.GA6955@mathematik.tu-darmstadt.de> Reply-To: "Eduardo J. Dubuc" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1374970774 15736 80.91.229.3 (28 Jul 2013 00:19:34 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 28 Jul 2013 00:19:34 +0000 (UTC) Cc: Thomas Streicher , "categories@mta.ca" To: Marta Bunge Original-X-From: majordomo@mlist.mta.ca Sun Jul 28 02:19:37 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 1V3Ehi-0002LC-Dw for gsmc-categories@m.gmane.org; Sun, 28 Jul 2013 02:19:18 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54802) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3EgH-0001Is-1j; Sat, 27 Jul 2013 21:17:49 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3EgI-0004Gt-20 for categories-list@mlist.mta.ca; Sat, 27 Jul 2013 21:17:50 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7820 Archived-At: Well, I intent to work as Joyal-Tierney do in their memoir, justified by the internal logic of the topos (e.g. Joyal-Boileau). In this way, internal sites have objects, internal lattices have elements, presheaves H can be evaluated in an object C of the site CC yielding an object HC in SS, etc etc. Sheaves are presheaves satisfying the usual requirements, they form a Grothendieck (or bounded) topos sh(CC) = EE ---> SS over SS, etc etc. In this context I asked: > Consider F: CC ---> SS to be > the inverse image of a point. Then the family Ff: FC ---> FX is > epimorphic in SS. > > My question is: > > Can I do the following ? (meaning, is it correct the following arguing, > certainly valid if SS is the topos of sets): > I clarify now, given a fix (but arbitrary) object X in EE, and > Given a in FX, take f:C ---> X and c in FC such that a = Ff(c). The answers of David Roberts and Andreas Blass on MathOverflow (that I quoted in a previous posting) say the arguing (in the internal language) was correct, and this seems quite satisfactory to me. But there was no explicit or detailed justification. Thomas Streicher (and Marta Bunge making Thomas answer her own) answer bringing into play the theory of fibrations/indexed. I appreciate this answer because made me think different aspects of the question, and for the references given. But fibrations/indexed are not necessary when working as in Joyal-Tierney Memoir (as they are not used in that memoir, which by the way, is extremely carefully written) In this last posting, I realized they are answering a different question, it seems quite extraordinary! that we were taking of different things without realizing it !! (I reading their answers, and they reading my question and my expanded clarification) I say F: CC ---> SS the inverse image of a point. Abusing notation as usual, we also write F: EE ---> SS. Now, as it follows from this last posting, they (for some reason that I ignore) interpret that F is the inverse image SS ---> EE of the g.m. EE ---> SS defining EE over SS (g.m. that I did not even denoted by any letter since it does not play a role in the formulation of the question). The g.m whose inverse image I denoted F is that of a point SS ---> EE, as I explicitely say it, and as I thought it was clear in my question. I should have realized in the original Thomas answer that he was thinking in a different question, but did not !. All this is mathematics, so I hope it should be completely clarified. The question and its derivations may be of interest to members of the list that do not post about it, but if the moderator thinks this is not so, I will pursue my search for understanding these matters privately. best e.d. On 27/07/13 05:56, Marta Bunge wrote: > Dear Thomas, > > What you wrote in the first part of your letter ( before the last > paragraph) is precisely what I wanted to write but decided to wait > until Montreal also to answer Eduardo's other questions, for which I > needed to have the references at hand. Also a better computer than my > laptop here in Greece. But I shall be home next week. > > In short, I fully agree with you. Thanks for answering Eduardo's > question to me with such precision. I could not have done it better > myself. > > Best regards, Marta > > Sent from my iPad > > On 2013-07-27, at 4:33 AM, "Thomas > Streicher" wrote: > >> 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/ ]