From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7819 Path: news.gmane.org!not-for-mail From: "Olivia Caramello" Newsgroups: gmane.science.mathematics.categories Subject: Re: disjoint_coproducts_bis_? Date: Sat, 27 Jul 2013 19:21:26 +0200 Message-ID: References: Reply-To: "Olivia Caramello" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1374970618 14123 80.91.229.3 (28 Jul 2013 00:16:58 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 28 Jul 2013 00:16:58 +0000 (UTC) To: "'Eduardo J. Dubuc'" , "'Categories list'" Original-X-From: majordomo@mlist.mta.ca Sun Jul 28 02:17:01 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 1V3Ef3-0000Jq-B7 for gsmc-categories@m.gmane.org; Sun, 28 Jul 2013 02:16:33 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54796) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3EdO-00012F-UI; Sat, 27 Jul 2013 21:14:50 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3EdQ-0004Cy-1f for categories-list@mlist.mta.ca; Sat, 27 Jul 2013 21:14:52 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7819 Archived-At: Dear Eduardo, Thank you for your clarifications. The fact that you did not use the language of indexed categories or fibrations in formulating your statement, and that you referred to = specific objects and epimorphic families involving the site CC, made me think = that you assumed CC to be a site in the standard sense, rather than a site internal to SS, and hence I answered accordingly. My argument certainly = does not apply in the case of a site internal to SS; in this situation, one should appropriately formalize the statement in the higher-order = internal logic of the topos in question (in which case, the resulting sentence becomes valid in this logic) and use the machinery of indexed categories = or fibrations to 'externalize' it. Concerning your last question, I would like to remark that, in general, = if one is able to interpret a statement M involving certain semantic = notions or constructions as the semantic interpretation of a syntactic statement S = in a system admitting a soundness theorem for such kind of interpretations, = then, if S can be established within the system by purely syntactic means, one = can rely on the soundness theorem to 'canonically' deduce M. Going through a syntactic system to lift results from a given context (playing the role = of a 'standard model' of the system that one keeps in mind when working in = it) to a more general one is a most effective (and conceptually satisfying) = method, as the history of our subject, as well as its most recent developments, show. For instance, following the discovery of the internal language of = a topos, many categorical results about toposes have been established or interpreted as semantic interpretations of syntactic statements provable = in the internal logic. In the case of Diaconescu's Theorem, the route which = has first been taken to establish it over a general base topos has not been = that of designing a 'syntactic' version of it, but rather that of developing appropriate generalizations of the various notions involved in it within = the framework of indexed categories/fibrations. However, I think that it = would be feasible to develop a logical system for doing category theory over a base topos; in this respect, the book "Relative Category Theory and Geometric Morphisms: A Logical Approach" (Oxford Logic Guides) by J. = Chapman and F. Rowbottom might be relevant - its abstract reads as follows:=20 "Topos theory provides an important setting and language for much of mathematical logic and set theory. It is well known that a typed = language can be given for a topos to be regarded as a category of sets. This = enables a fruitful interplay between category theory and set theory. However, = one stumbling block to a logical approach to topos theory has been the = treatment of geometric morphisms. This book presents a convenient and natural = solution to this problem by developing the notion of a frame relative to an elementary topos. The authors show how this technique enables a logical approach to be taken to topics such as category theory relative to a = topos and the relative Giraud theorem. The work is self-contained except that = the authors presuppose a familiarity with basic category theory and topos theory. Logicians, set and category theorists, and computer scientist working in the field will find this work essential reading." Best regards, Olivia =20 =20 > -----Messaggio originale----- > Da: Eduardo J. Dubuc [mailto:edubuc@dm.uba.ar] > Inviato: gioved=EC 25 luglio 2013 23:22 > A: Categories list > Oggetto: categories: disjoint_coproducts_bis_? >=20 > Hi, first many thanks to all who answered my question (in the list and = in > mathoverflow). I feel now the need to further clarify my question = which I > thought was clear enough. >=20 > A) Three answers respond to the intended interpretation of my question = and > say the same, that the arguing is correct. >=20 > 1) Looks valid to me: I would possibly expand it to: > COPRODUCT_{all f: C ---> X, all C in CC} FC ---> FC, is an = epimorphism, > therefore for any a: * ---> FX there exists > c: * ---> COPRODUCT_{all f: C ---> X, all C in CC} FC lifting a, and = since > coproducts in SS are disjoint, c factors through some component FC and > you're done. ? David Roberts. >=20 > It is mysterious however for what stands the symbol "*" ? >=20 > 2) This argument looks OK as long as everything is understood to be in = the > internal logic of SS. In particular, the implicit existential = quantifiers "there > exists C and there exists c" should be understood internally (i.e., as local > existence); similarly for the quantifier "for some i \in I". Andreas Blass. >=20 > This is very clear. >=20 > 3) Your statement is valid internally in SS, that is once formalized = in the > internal language of the topos SS; this can be done in geometric = logic, by > considering a (possibly infinitary) disjunction over all the arrows f: = C ---> X for > C in CC (interpreted by the arrows Ff in SS) and existential quantifications. > Olivia Caramello. >=20 > This seems somehow less clear, the wording "(possibly infinitary) > disjuntions" opens the door for a misunderstanding, and should be > explained. >=20 > Well, I had some other private answers on the negative, and also in = the form > "yes and no". All these answers do not interpret my question the way = it was > intended. They talk about fibrations, coverings, atoms, etc, nothing = to do > with my question. They interpret my question essentially by an = external > view, while it is purely internal. >=20 > Now, two new postings to the list made me think it is pertinent to = clarify and > expand the question: >=20 > Answering Olivia 3), Thomas Streicher writes: >=20 > 4) Since CC is internal to SS which is assumed as different from Set = it doesn't > make sense to consider an infinite disjunction over all arrows > f: C --> X for C in CC. Thomas >=20 > And Olivia answers: >=20 > 5) It seems to me that Eduardo assumed CC to be a site for EE in the classical > sense, i.e. not a site internal to SS but to Set (since he wrote that = "CC has > objects, and that these objects are objects of EE which are generators = in the > sense that given any X in EE, the family of all f: C ---> X, all C in = CC, is > epimorphic"); so an infinite disjunction makes sense in this case. = Olivia >=20 > Well, it seems to me things are now mixed up, and I will intent to clarify, > expecting also to be not quite right. >=20 > First, I said in my original posting and in mathoverflow: >=20 > "As usual in the literature (Joyal-Tierney, Moerdijk, Bunge, and many > more) consider that CC has objects, and that these objects are = objects of EE > which are generators in the sense that given any X in EE, the family = of all f: C > ---> X, all C in CC, is epimorphic." >=20 > "As usual in the literature", Olivia miss this point when she answers Thomas. > Technically speaking I am assuming CC to be an internal site in SS. My > question is purely refered to the validity in the internal language of = the topos > SS. >=20 > I give two examples: >=20 > 6) "Thus, we take the point of view that an arbitrary, but fixed, > (elementary) topos is our basic universe of sets, We work in this = universe as > we would in naive set theory, except that, of course, we cannot use = the > axiom of choice, or the law of excluded middle. This has been shown to = be > correct by various authors (e.g. Boileau-Joyal). > Joyal-Tierney, An extension of the galois theory of grothendieck, = Memoirs > 309." >=20 > 7) "Throughout this paper SS denotes a fixed base topos, all toposes = are > assumed to be Grothendieck toposes over SS, and all geometric = morphisms > are taken to be bounded. Moerdijk, Continuos fibrations and inverse = limits of > toposes Compositio Mathematica 58." >=20 > Then, in these two papers their sites happily have objects, their = objects > happily have elements (as if they were sets, not externally in the = sense of > sections from an object in the site), etc etc. But one has to work carefully, > see for example the definition of open site in 6). >=20 > For the validity of all this only (e.g. Boileau-Joyal) is needed (no theory of > indexed categories or fibrations, etc). >=20 > Then, thats it !, the arguing is correct !, why bother more ?, as = answers 1) 2) > and 3) point out. >=20 > Well, it seems I still need some more reassuring facts. >=20 > I quote a (private, but since then Thomas has written to the list, I = feel he > would not object) knowledgeable answer by Thomas >=20 > 8) my reply would be that given a g.m. F -| U : EE -> SS this corresponds to a > fibration P_F of toposes over SS (P_F is obtained by pulling back the > codomain fibration along F). In the internal language of SS one can = speak > about the fibration P_F only in a restricted way. >=20 > 1) Does it make sense to take >=20 > E =3D COPRODUCT_{all f: C ---> X, all C in CC} FC ? >=20 > We have g: E ---> FX an epimorphism, so we can take c in E such that a = =3D g(c). > Well, the g.m. F -| U : EE -> SS being bounded is already equivalent = to the > existence of a generic family G -> FI. Since P_F is a locally small fibration > (because U has a right adjoint) by Th.10.5 of www.mathematik.tu- > darmstadt.de/~streicher/FIBR/FibLec.pdf your claim 1)follows. See also > footnote 15 on p.78 of loc.cit. Maybe you find > pp.51-52 of Bunge and Funk's book more illuminating in this respect. >=20 > Then we would need the validity of: >=20 > 2) Given x in COPRODUCT_{i in I} S_i , then x in S_i for some i in I. > Depends on how you read this. If you read it externally for a = Grothendieck > topos SS over Set it is wrong if SS is not connected. But the answer = is trivially > YES if you think of (S_i)_{i \in I} as a map S > -> I in SS. But for general toposes SS there is no other meaning of > family of objects in SS indexed by I. >=20 > Then, this justify that the arguing is correct, according with 1) and = 2). >=20 > From this I figured out and wrote (privately to Thomas) >=20 > 9) Thanks for your answer, it confirms that the arguing is correct. > Given an internal site CC in SS, the expression {all f: C ---> X, all = C in CC} > actually determines an object in SS which legitimates the index in the > coproduct expression COPRODUCT_{all f: C ---> X, all C in CC} FC, = then the > answer for 2) is trivially yes as you say. >=20 > and he answered "right!". >=20 > But he also writes later in the Mail: >=20 > 10) The problem rather is that in (the language of) SS you can't = quantify over > such families (nor can you quantify over objects of SS in SS). Well, = there are > possibilities arising from Algebraic Set Theory but that means that = you work > in a category of classes constructed from SS. > In any case reasoning "like in Set" doesn't work for arbitrary base toposes. >=20 > How we should understand this ?. Luckily in my question there is no > quantification of this sort. I understand that you can quantify = (abusing > notation) over objects of SS when these objects are objects of an = internal site > CC, as it is done in 6) and 7). >=20 > So, this seems to be no objection to the validity of the arguing in my original > question. >=20 > I am really sorry if the experts find this long discussion banal, but = I am > posting it since I know it would be useful to many interested non = experts in > the subject. >=20 > And now, I rise a new question to the list: >=20 > B) >=20 > 1) To do many mathematical reasonings and constructions over an = arbitrary > base topos, in several places in the literature classical category = theory (pull- > backs, subobject classifiers, colimits, effective epimorphisms, etc = etc) is > painfully and carefully used (e.g. the books Topos theory, Vol. 10, Academic > Press, London, 1977, or Sheaves in Geometry and Logic, Springer, = 1992). >=20 > Why bother ? >=20 > Take for example Diaconescu Theorem, Can we reason as follows ?: >=20 > 2) This theorem needs no proof, since the proof of the statement with = the > topos of sets as a base topos (SGA4 expose IV, Proposition 4.9.4, = p356, SLN > 269) can be done with an arbitrary base topos since "we work in this universe > as we would in naive set theory". Just check that no use is made of choice, > the excluded middle, quantification over "large" > families or any other non kosher things. >=20 > e.d. >=20 >=20 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]