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/ ]
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/ ]
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.
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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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
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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
Eduardo J. Dubuc -
Olivia Caramello -
Thomas Streicher