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