* disjoint_coproducts_?
@ 2013-07-23 22:45 Eduardo J. Dubuc
2013-07-24 11:04 ` R: disjoint_coproducts_? Olivia Caramello
0 siblings, 1 reply; 3+ messages in thread
From: Eduardo J. Dubuc @ 2013-07-23 22:45 UTC (permalink / raw)
To: Categories list
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/ ]
^ permalink raw reply [flat|nested] 3+ messages in thread
* R: disjoint_coproducts_?
2013-07-23 22:45 disjoint_coproducts_? Eduardo J. Dubuc
@ 2013-07-24 11:04 ` Olivia Caramello
2013-07-25 11:33 ` disjoint_coproducts_? Thomas Streicher
0 siblings, 1 reply; 3+ messages in thread
From: Olivia Caramello @ 2013-07-24 11:04 UTC (permalink / raw)
To: 'Eduardo J. Dubuc', 'Categories list'
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/ ]
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: disjoint_coproducts_?
2013-07-24 11:04 ` R: disjoint_coproducts_? Olivia Caramello
@ 2013-07-25 11:33 ` Thomas Streicher
0 siblings, 0 replies; 3+ messages in thread
From: Thomas Streicher @ 2013-07-25 11:33 UTC (permalink / raw)
To: Olivia Caramello; +Cc: 'Eduardo J. Dubuc', 'Categories list'
> 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/ ]
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2013-07-25 11:33 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-07-23 22:45 disjoint_coproducts_? Eduardo J. Dubuc
2013-07-24 11:04 ` R: disjoint_coproducts_? Olivia Caramello
2013-07-25 11:33 ` disjoint_coproducts_? Thomas Streicher
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).