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@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/ ]
Dear Eduardo, Indeed I misunderstood what you wrote. My comments were on an arbitrary geometric morphism F -| U : EE -> SS. You, however, speak about a geometric morphism F -| U : SS -> EE where EE = Sh(CC,JJ) with the site (CC,JJ) living in SS. Then we know that F is determined by the restriction along Yoneda giving rise to a functor CC -> SS which you call F. Since CC is internal to SS we can speak about your F within SS. But you also mention X in EE. So we can't fully stay within the internal language of SS. But we may consider for X in EE the canonical map c_X = \coprod_{C:CC,f : hom(C,X)} ---> X which is epic for the reason given by Marta and me. Since F : EE -> SS is a left adjoint F(c_X) is epic, too. But we also have to exploit that F considered as a fibered functor is cocartesian, i.e. preserves internal sums. So you statement can be formulated in the internal language of SS when X is fixed externally (since EE over SS is locally small). But for proving it one has to go to the indexed/fibrational level. At least I don't see any other way. Best, Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 28/07/13 13:50, Thomas Streicher wrote:
Dear Eduardo,
Indeed I misunderstood what you wrote. My comments were on an arbitrary geometric morphism F -| U : EE -> SS. You, however, speak about a geometric morphism F -| U : SS -> EE where EE = Sh(CC,JJ) with the site (CC,JJ) living in SS. Then we know that F is determined by the restriction along Yoneda giving rise to a functor CC -> SS which you call F. Since CC is internal to SS we can speak about your F within SS. But you also mention X in EE. So we can't fully stay within the internal language of SS. But we may consider for X in EE the canonical map
c_X = \coprod_{C:CC,f : hom(C,X)} ---> X [==1==]
which is epic for the reason given by Marta and me. Since F : EE -> SS is a left adjoint F(c_X) is epic, too. But we also have to exploit that F considered as a fibered functor is cocartesian, i.e. preserves internal sums. So you statement can be formulated in the internal language of SS when X is fixed externally (since EE over SS is locally small). But for proving it one has to go to the indexed/fibrational level. At least I don't see any other way.
Best, Thomas
Thanks Thomas (and Marta, this is in reply to both), things are now more clear to me, and I understand that (as you explain via the indexed/fibrational level) the arguing in the notation of the internal language of the topos SS is not only correct but appropriately validated. Have an internal site CC in SS, a sheaf X in EE = sh(CC), and a point with inverse image F: EE ---> SS (X and F are fixed but arbitrary). The arguing in question was: Given a in FX, take f:C ---> X and c in FC such that a = Ff(c). Note: f:C ---> X stands for f in X(C). The validity follows from an epimorphism: COPRODUCT_{f: C ---> X, C in CC} FC ---> FX whose existence you explain via the indexed/fibrational level. Now, is there something wrong in the following ? (To explain I will have to write things that I know you know very well): The site CC actually is an internal category with object of objects C_o, object of arrows C_1, and some structure, The presheaf X actually is an arrow X ---> C_o (internally X = COPRODUCT_{C in C_o} X(C)), with a right action as usual. The point (externalized as a functor EE ---> SS actually corresponds to an internal functor which (again) is an arrow F ---> C_o (internally F = COPRODUCT_{C in C_o} X(C)) with a left action as usual. By the very construction of the object F(X) (single F and single X) as a colimit in SS we have an epimorphism in SS: COPRODUCT_{f: C ---> X, C in CC} FC ---> FX which is COPRODUCT_{f in X(C), C in CC} FC ---> FX, and we are done. This is just notation for some purely external categorical constructions in SS, and no use of machinery at the indexed/fibrational level. Of course, we can say X ---> C_o is a family indexed by C_o, etc. but this is just parlance (no technical meaning) leading to the internal language notation justified by e.g. Joyal-Boileau). Notice also that F can be any covariant functor, not necessarily flat (in which case the resulting external functor F: EE ---> SS will not be a point). Finally, notice also that the epic we not use in this last arguing (that I marked [==1==] above) is actually an epic in the category of presheaves and it is preserved by F by the very construction of F(X), whether or not F is a point. best Eduardo. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Eduardo, I understand your point better now. For you FX is already given as the respective colimit. This was shown by Celeyrette in his 1974 Th'ese directed by B'enabou (Ch.VI Theorem de Kan where you also find a proof of Diaconescu's theorem over arbitrary bases). But you have to rely on a theorem characterizing colimits of small diagrams in SS from which it follows that the source tupling (in the sense of internal sums) of the cone is epic. Even if you think it is splitting hairs you cannot express the property of being epic in SS within the internal language of SS. You can express in the internal language of SS that a map is surjective and show externally that SS validates f being surjective iff f is epic in SS. (For expressing "epic" in SS one would have to quantify over all objects in SS which one cannot do in the internal language of SS.) So my conclusion is that the argument you give is ok for most purposes. What I wrote above (and previously) gives some additional justification of its correctness. I will be offline till next weekend and therefore have no time to continue a discussion with many mails back and forth. Moreover, I think things have been clarified to quite some extent. Best, Thomas PS "purely external categorical construction in SS" is a contradiction in terms formulations like these have given me the impression that you have wrong reason for a correct result [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Eduardo J. Dubuc -
Thomas Streicher