July 2013 - Categories - categories.org.au

Partial functor
by David Leduc 17 Mar '15

17 Mar '15

Hi, A partial functor from C to D is given by a subcategory S of C and a functor from S to D. What is the appropriate notion of natural transformation between partial functors that would allow to turn small categories, partial functors and those "natural transformations" into a bicategory? The difficulty is that two partial functors from C to D might not have the same definition domain. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 6

Research positions
by Maria Manuel Clementino 26 Feb '14

26 Feb '14

5-YEAR RESEARCH POSITIONS The Centre for Mathematics of the University of Coimbra (CMUC) invites applications for five 5-year research positions in all areas of Mathematics. Applicants should have a PhD in Mathematics and at least three years of post-doctoral experience, with an international-level publication record and demonstrated ability to perform independent research. Preference will be given to candidates working in one of the areas in which the members of CMUC are currently active. A very good command of English is required. The appointments will be made for three years, renewable for two more. Successful applicants are expected to develop research within the areas of interest of CMUC. They should also contribute to graduate studies, supervising students from the Department of Mathematics. The basic salary is equivalent to the index 195 of the Portuguese research career (in the order of 42 500 euros a year), in accordance with the Ciência 2008 guidelines http://alfa.fct.mctes.pt/apoios/contratacaodoutorados/edital2008 Benefits include private health insurance and social security. Applicants should send • cover sheet (available from www.mat.uc.pt/cmuc/coversheet.pdf) including names and contact information of three persons who can provide a letter of recommendation • curriculum vitae (publication list included) • a 5-year research proposal (2 pages max), emphasizing their own research goals as pdf files to cmuc(a)mat.uc.pt. The subject of the e-mail message must include the job reference C2008 FCTUC CMUC v15-v19. The deadline for applications is *September 10, 2008.* ------------------------------ More information can be found at www.mat.uc.pt

1 1

Re: Reply to Eduardo Dubuc
by Eduardo J. Dubuc 30 Jul '13

30 Jul '13

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"<streicher(a)mathematik.tu-darmstadt.de> 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/ ]

2 3

Re: Reply to Eduardo Dubuc
by Thomas Streicher 29 Jul '13

29 Jul '13

Dear David, indeed Michael's work is an alternative to the AST approach taylored towards a setting where it is forbidden to speak of equality of sets. He doesn't construct the category of classes around a topos but rather works with Kripke Joyal semantics for it. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Re: Reply to Eduardo Dubuc
by Marta Bunge 28 Jul '13

28 Jul '13

Eduardo, 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 that you start with a bounded S-topos EE-->SS (unnamed)) and then consider a point SS --->EE over SS, whose inverse image you denote by F:EE -->SS. I understood that. Now there are the following considerations. (a) From EE bounded over SS you get a site CC (with a topology j, say) which 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 least some of them) correspond to this basic construction you definitely use. I totally agree with that. You need an object G of generators and the epi in question 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 Toposes, SLNM 1890, 2006. (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 that needs the interplay between EE and SS us the first one and you cannot avoid that. Without Joyal-Tierney's Memoir at hand I cannot comment on your assertion about it except by recollection. I will do so in Montreal next week. As for Diaconescu's theorem, it too requires the notion of an internal object of generators, which is one of of his main contributions in lifting a notion well understood for Grothendieck toposes over Set to "Grothendieck toposes" over an arbitrary base topos SS. Another is of course to express the correct lifting of "flatness". I am aware that there are attempts to describe a logic that extends the internal 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 constructions involving category theory. In my view, the goal of reducing topos theory to a certain "naive constructive set theory", even if succesful, will not 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 general and topos theorists in particular will not be attracted by it. Hopefully, that is. Finally, everyone knows that the internal logic of a topos is intuititionistic But who exhibited the object \Omega which permits such a conclusion? Grothendieck calls \Omega "the Lawvere object". 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" <edubuc(a)dm.uba.ar> 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) = 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 >> 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"<streicher(a)mathematik.tu-darmstadt.de> 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/ ]

1 0

disjoint_coproducts_bis_?
by Eduardo J. Dubuc 28 Jul '13

28 Jul '13

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. A) Three answers respond to the intended interpretation of my question and say the same, that the arguing is correct. 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. It is mysterious however for what stands the symbol "*" ? 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. This is very clear. 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. This seems somehow less clear, the wording "(possibly infinitary) disjuntions" opens the door for a misunderstanding, and should be explained. 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. Now, two new postings to the list made me think it is pertinent to clarify and expand the question: Answering Olivia 3), Thomas Streicher writes: 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 And Olivia answers: 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 Well, it seems to me things are now mixed up, and I will intent to clarify, expecting also to be not quite right. First, I said in my original posting and in mathoverflow: "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." "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. I give two examples: 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." 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." 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). For the validity of all this only (e.g. Boileau-Joyal) is needed (no theory of indexed categories or fibrations, etc). Then, thats it !, the arguing is correct !, why bother more ?, as answers 1) 2) and 3) point out. Well, it seems I still need some more reassuring facts. I quote a (private, but since then Thomas has written to the list, I feel he would not object) knowledgeable answer by Thomas 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. 1) Does it make sense to take E = COPRODUCT_{all f: C ---> X, all C in CC} FC ? We have g: E ---> FX an epimorphism, so we can take c in E such that a = 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. Then we would need the validity of: 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. Then, this justify that the arguing is correct, according with 1) and 2). From this I figured out and wrote (privately to Thomas) 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. and he answered "right!". But he also writes later in the Mail: 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. 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). So, this seems to be no objection to the validity of the arguing in my original question. 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. And now, I rise a new question to the list: B) 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). Why bother ? Take for example Diaconescu Theorem, Can we reason as follows ?: 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. e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Lambekfest Sept 21, 2013 (Preliminary announcement)
by Robert Seely 28 Jul '13

28 Jul '13

On Saturday, 21 September at the CRM (Centre de Recherches Mathematiques, Universite de Montreal) we are holding a one-day not-quite-birthday-bash workshop, celebrating the career of Prof Joachim (Jim) Lambek, FRSC. (Jim was 90 last December.) Jim Lambek has been a profoundly inspirational mathematician for more than 60 years, and has made ground-breaking contributions to a number of fields, including algebra, linguistics, theoretical physics, and logic and proof theory. Lambek's work on (categorical approaches to) linguistics, to theoretical physics, and to logic and proof theory will be represented by talks during the meeting. There will be a reception at the CRM following the talks. There is a preliminary listing of this meeting on the CRM's website http://www.crm.umontreal.ca/cal/en/jour20130921.html Further information about the CRM (e.g. how to get there, hotels, etc) may be found on their website http://www.crm.umontreal.ca/en/ . A more detailed announcement (and website) will be made later. The speakers will be: 1. W. Buszkowski (Poznan) 2. C. Casadio (Chieti) / M. Sadrzadeh (Queen Mary) 3. B. Coecke (Oxford) 4. M. Makkai (McGill) 5. M. Moortgat (Utrecht) 6. P. Scott (Ottawa) 7. P. Selinger (Dalhousie) -- <rags(a)math.mcgill.ca> <www.math.mcgill.ca/rags> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Reply to Eduardo Dubuc
by Thomas Streicher 27 Jul '13

27 Jul '13

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/ ]

1 0

Re: Reply to Eduardo Dubuc
by Eduardo J. Dubuc 27 Jul '13

27 Jul '13

On 26/07/13 17:08, Thomas Streicher wrote: >>> 2) If on the other hand you work in a topos EE that is bounded >>> over SS, then you cannot work "as in Sets" concerning >>> constructions in EE that involve SS. Here it is necessary to >>> resort to either the "teoria delle categorie sopra un topos di >>> base" (indexed categories) or to the theory of fibrations. >>> >>> [[1===1]] >>> Concerning your question, let me point out that, although you >>> pretend to work entirely inside SS, you do not, as your >>> construction involves EE. It certainly makes sense, since EE is >>> locally small, and CC is small ( meaning internal to SS). What I >>> want to warn you about is how you proceed from there without >>> resorting to EE as a bounded SS- topos. > > I fully subscribe to this, That's what I also wanted to say but > formulated less clearly. > > The saying that "toposes correspond to naive set theory without > principle and excluded middle" is right only if "naive set theory" > is identified with higher order logic. But in "naive category > theory" you all the time have to quantify over families of objects > and morphisms of a category where these collections don't form sets. > In particular, you have to quantify over all objects of the base > topos which you can't do inside the base topos. > > As Marta has said one has to resort to fibered/indexed reasoning > which also cannot be (fully) expressed in the internal language of > the base topos. > > [[2===2]] > As I wrote to Eduardo in a non-public mail I consider > the "naive set theory" style arguments one often find in the > literature as kind of "blueprints" for the precise fibered/indexed > arguments. > > An alternative is using Algebraic Set Theory which allows one to > build around every topos EE a category of classes in such a way that > EE appears as internal to it. This, among other things, is the aim of > a recent paper by Awodey, Butz, Simpson and myself which has is to > appear at APAL and a preliminary version of which can be obtained > from Alex's homepage > (http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models.pdf) > > Sorry for speaking pro domo but it is relevant here when one wants > to fully stay within an internal language. > > Thomas Thanks Marta an Thomas, I am learning a lot !. I would like to comment in the items marked [[1===1]] and [[2===2]] of your answers. It seems to me now that the argument in my question does not need any theory of indexing categories. See, concerning [1===1] above I can say: My construction does not involve EE. It involves an internal site CC in SS, a functor CC ---> SS, a coproduct in SS indexed by an object in SS, and a SINGLE object X in EE, which is sheaf CC^op ---> SS. All this involves ONLY SS, and no forbiden quantifications are used. So the internal logic of SS should suffice. Concerning [2===2], you are probably right in many cases, precisely cases that I distrust because I feel the authors are not carefully enough (this due to my ignorance together with a tendency to be as Saint Thomas, "have to see to belive"). But in other cases not. For example, the entire paper Joyal-Tierney, An extension of the galois theory of grothendieck, Memoirs 309, is no "blue print" for nothing, it is in final form, very careful, and entirely justified (even their change of base) without any need of fibered/indexed arguments, as they say, (e.g. Boileau-Joyal) suffices. For example, they consider p: EE ---> SS, and say p_* sends sup-lattices to sup-lattices, they consider a left adjoint p^# (between the categories of sup-lattices) and stablish an isomorphism Hom(L, p_*(M)) = p_*Hom(p^#(L), M) in SS and say "expresses the (strong) adjointness p^# --| p_*" (page 44). They use "strong", no mention at all to "indexed adjoint", and this isomorphism is just a definition of strong. But, is not true that a topos p: EE ---> SS is canonically indexed and that for many things you can proceed tacitly without need to mention any theory of indexed categories ?. Even for constructions in EE ?. For example, a family in EE indexed by I in SS is just an arrow X ---> p*I, and the COPRODUCT_{i \in I} X_i in EE is just X. Please, do not think I am against fibered/indexed arguments, I can not be either against or in favor, since I do not know the theory. After your answers I understand now the theory is useful when you need to use quantifications not avaiable in the internal logic of a topos and other things of this sort. Best Eduardo. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Reply to Eduardo Dubuc
by Marta Bunge 27 Jul '13

27 Jul '13

> Dear Eduardo, > > Thank you for keeping me au courant. Difficult as it is to write in my iPad, I want to tell you my position and what I think of your question. > > My position (as that of any topos theorist) is that > > 1) If you work in an elementary topos SS, then it is true that you can do so "as in Sets", provided you do not use excluded middle ( as the internal logic is intuitionistic) or use Choice (as the set theory intrinsic to SS is constructive). > > 2) If on the other hand you work in a topos EE that is bounded over SS, then you cannot work "as in Sets" concerning constructions in EE that involve SS. Here it is necessary to resort to either the "teoria delle categorie sopra un topos di base" (indexed categories) or to the theory of fibrations. > > Concerning your question, let me point out that, although you pretend to work entirely inside SS, you do not, as your construction involves EE. It certainly makes sense, since EE is locally small, and CC is small ( meaning internal to SS). What I want to warn you about is how you proceed from there without resorting to EE as a bounded SS- topos. > I apologize for previous (private) irrelevant remarks as I misunderstood your question - until now, that is. > > Concerning Diaconescu's theorem, AC implies Booleaness can be done "as in Sets" but the proof is not trival. If you mean the theorem which gives a characterization of bounded SS-toposes as a classifying topos, it requires fibrations over SS. > > Regards, > Marta > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1