1
$\begingroup$

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$.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – David Roberts
    Jul 23, 2013 at 22:20
  • $\begingroup$ Thanks David, question now is: Can I belive it ?. I guess it is a question to get used to. $\endgroup$ Jul 23, 2013 at 22:54

2 Answers 2

1
$\begingroup$

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$.)

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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