R: disjoint_coproducts_?

["Olivia Caramello" <oc233@hermes.cam.ac.uk>]

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