Dear Eduardo, 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. If you want a statement valid 'externally', you should instead use generalized elements in SS and epimorphic families involving their domains. I hope this helps. Best regards, Olivia
-----Messaggio originale----- Da: Eduardo J. Dubuc [mailto:edubuc@dm.uba.ar] Inviato: mercoledì 24 luglio 2013 00:45 A: Categories list Oggetto: categories: disjoint_coproducts_?
Hello, I have the following question:
Assume a topos SS as the base topos, and work in this topos as in naive set theory (without choice or excluded middle). Take a Grothendieck topos EE
SS with a site of definition CC. 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. 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):
Given a in FX, take f:C ---> X and c in FC such that a = Ff(c).
We can break this question in two:
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).
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.
greetings e.d.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]