From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7821 Path: news.gmane.org!not-for-mail From: Marta Bunge Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Sun, 28 Jul 2013 01:08:06 -0400 Message-ID: References: <20130726200858.GB32154@mathematik.tu-darmstadt.de> <51F2EDAC.3010403@dm.uba.ar> <20130727083302.GA6955@mathematik.tu-darmstadt.de> <22264_1374970724_51F46364_22264_166_1_E1V3EgI-0004Gt-20@mlist.mta.ca> Reply-To: Marta Bunge NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1375100605 2640 80.91.229.3 (29 Jul 2013 12:23:25 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 29 Jul 2013 12:23:25 +0000 (UTC) To: "Eduardo J. Dubuc" , Original-X-From: majordomo@mlist.mta.ca Mon Jul 29 14:23:27 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 1V3mU1-00064Y-Og for gsmc-categories@m.gmane.org; Mon, 29 Jul 2013 14:23:26 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:55328) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3mRq-0005mD-Ah; Mon, 29 Jul 2013 09:21:10 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3mRp-00023c-4k for categories-list@mlist.mta.ca; Mon, 29 Jul 2013 09:21:09 -0300 In-Reply-To: <22264_1374970724_51F46364_22264_166_1_E1V3EgI-0004Gt-20@mlist.mta.ca> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7821 Archived-At: Eduardo,=20 We (Thomas andI) are not answering a different question - at least I was not= . Maybe the notation used by Thomas made you think so. Still it is the case t= hat you start with a bounded S-topos EE-->SS (unnamed)) and then consider a p= oint SS --->EE over SS, whose inverse image you denote by F:EE -->SS. I unde= rstood that. Now there are the following considerations.=20 (a) =46rom EE bounded over SS you get a site CC (with a topology j, say) whi= ch is internal to SS. This gives you, for an object X of EE, the epimorphism= from the appropriate coproduct in EE to X. The remarks Thomas made (at leas= t some of them) correspond to this basic construction you definitely use. I t= otally agree with that. You need an object G of generators and the epi in qu= estion expressed by the diagram Thomas included in his answer, and which you= can also see in page 51-52 of my book with Jonathon Singular Coverings of T= oposes, SLNM 1890, 2006.=20 (b) Now you resort to F:EE ---> SS which is left exact and has an SS-indexed= right adjoint. This is why you may infer that F preserves the given diagram= of an epi into X from a coproduct involving CC, which is again an epi from a= coproduct (with the same indexing "set"!) to FX. Cannot draw these diagrams= in an iPad, at least not easily. Here you argue "as in Set", but the part t= hat needs the interplay between EE and SS us the first one and you cannot av= oid that.=20 Without Joyal-Tierney's Memoir at hand I cannot comment on your assertion ab= out it except by recollection. I will do so in Montreal next week.=20 As for Diaconescu's theorem, it too requires the notion of an internal objec= t of generators, which is one of of his main contributions in lifting a noti= on well understood for Grothendieck toposes over Set to "Grothendieck topose= s" over an arbitrary base topos SS. Another is of course to express the corr= ect lifting of "flatness".=20 I am aware that there are attempts to describe a logic that extends the inte= rnal logic of a topos SS but in which all of this can be expressed including= fibrations over SS and, in the process, getting rid of all the neat constru= ctions involving category theory. In my view, the goal of reducing topos the= ory to a certain "naive constructive set theory", even if succesful, will no= t aid in the formulation of new concepts or their use. As a matter of pride,= logicians may be able to say "we did it", but category theorists in genera= l and topos theorists in particular will not be attracted by it. Hopefully, t= hat is. Finally, everyone knows that the internal logic of a topos is intuit= itionistic But who exhibited the object \Omega which permits such a conclus= ion? Grothendieck calls \Omega "the Lawvere object".=20 Please revise carefully your construction and argument, and then tell me if I= am not right. I close shop now until further notice. Marta Sent from my iPad On 2013-07-27, at 8:18 PM, "Eduardo J. Dubuc" wrote: > 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) =3D EE ---> SS over SS, etc etc. In this context I asked: >=20 >> Consider F: CC ---> SS to be >> the inverse image of a point. Then the family Ff: FC ---> FX=20 >> epimorphic in SS. >>=20 >> My question is: >>=20 >> 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 >=20 >> Given a in FX, take f:C ---> X and c in FC such that a =3D Ff(c). >=20 >=20 > 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. >=20 > 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. >=20 > 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) >=20 > 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) >=20 > I say F: CC ---> SS the inverse image of a point. Abusing notation as > usual, we also write F: EE ---> SS. >=20 > 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. >=20 > I should have realized in the original Thomas answer that he was > thinking in a different question, but did not !. >=20 > All this is mathematics, so I hope it should be completely clarified. >=20 > 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. >=20 > best e.d. >=20 > On 27/07/13 05:56, Marta Bunge wrote: >> Dear Thomas, >>=20 >> 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. >>=20 >> 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. >>=20 >> Best regards, Marta >>=20 >> Sent from my iPad >>=20 >> On 2013-07-27, at 4:33 AM, "Thomas >> Streicher" wrote: >>=20 >>> Dear Eduardo, >>>=20 >>> 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) >>>=20 >>> e X<<--- u^*G -----> G | | | p.b. | V V FJ >>> ----> FI Fu >>>=20 >>> 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. =46rom 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. >>>=20 >>> 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. >>>=20 >>> 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). >>>=20 >>> 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) =3D 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. >>>=20 >>> 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. >>>=20 >>> Best regards, Thomas >=20 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]