disjoint_coproducts_?

disjoint_coproducts_?

[Eduardo J. Dubuc]

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

R: disjoint_coproducts_?

[Olivia Caramello]

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

Re: disjoint_coproducts_?

[Thomas Streicher]

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