Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Assume a topos $\mathcal{S}$ as the base topos, and we work in this topos as in naive set theory (without choice or excluded middle). Take a Grothendieck topos $\mathcal{E} \to \mathcal{S}$ with a site of definition $\mathcal{C}$. As usual in the literature consider that $\mathcal{C}$ has objects, and that these objects are objects of $\mathcal{E}$ which are generators in the sense that given any $X \in \mathcal{E}$ the family of all $f: C \to X$ all $C$ in $\mathcal{C}$ is epimorphic.

Consider $F: \mathcal{E} \to \mathcal{S}$ to be the inverse image of a point. Then the family $Ff: FC \to FX$ is epimorphic in $\mathcal{S}$. My question is the following:

Can I do the following ? (meaning, is it correct the following arguing, certainly valid if $\mathcal{S}$ is the topos of sets):

Given $a \in FX$, take $f: C \to X$ and $c \in FC$ such that $a = Ff(c)$

This is related to the validity in $\mathcal{S}$ of the following:

Given $x \in \coprod_{i \in I}{S_i}$, then $x \in S_i$ for some $i \in I$.

share|improve this question
    
Looks valid to me: I would possibly expand it to: $\coprod_C FC \to FX$ is an epimorphism, therefore for any $a\colon\ast\to FX$ there exists $c\colon\ast\to \coprod_C FC$ lifting $a$, and since coproducts in $S$ are disjoint, $c$ factors through some component $FC$ and you're done. –  David Roberts Jul 23 '13 at 22:20
    
Thanks David, question now is: Can I belive it ?. I guess it is a question to get used to. –  Eduardo Dubuc Jul 23 '13 at 22:54

2 Answers 2

This argument looks OK as long as everything is understood to be in the internal logic of $\mathcal S$. In particular, the implicit existential quantifiers "there exists $C$ and there exists $c$" should be understood internally (i.e., as local existence); similarly for the quantifier "for some $i\in I$".

(By the way, I assume that when you regard objects of $\mathcal C$ as objects of $\mathcal E$, you implicitly identify any $C$ with the associated sheaf of the presheaf represented by $C$.)

share|improve this answer

Thanks David and Andreas, your answers were just what I needed even to formulate correctly the question. On spite of my comment to David's answer, I am quite convinced now that the arguing is correct. If CC is an internal site in SS, the expression $\{all \; f: C \to X,\; all \;C \;in\; CC\}$ I guess it determines an object in SS which legitimates the index in the coproduct expression. Then as David says, disjointness finishes to validate the arguing.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.