On internal functions and arrows in a Topos - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T09:15:35Z http://mathoverflow.net/feeds/question/100539 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/100539/on-internal-functions-and-arrows-in-a-topos On internal functions and arrows in a Topos Eduardo Dubuc 2012-06-24T18:42:16Z 2012-07-02T17:41:40Z <p>I am not an expert on elementary topos (meaning by this to work with the internal language in a Grothendiek topos) and I rather be told than struggle with the following:</p> <p>Consider an elementary topos $\mathcal{E}$, a locale $G$, the unique locale morphism $i^*: \Omega \to G$, and any arrow $\lambda: X \times Y \to G$:</p> <p>Consider the following formulae on $\lambda$:</p> <p>ed): ($\bigvee_{y\in Y} \;\lambda\langle x,y \rangle = 1$), </p> <p>uv): ($\lambda\langle x,y \rangle \wedge \lambda\langle x,y' \rangle \leq i^*[[y = y']]$).</p> <p>Let $\theta: X \times Y \to Map(X,\,Y)$ be the universal locale furnished with such an arrow </p> <p>(that is, $\forall \lambda \; \exists ! \; \varphi^* : Map(X,Y) \to G \;\; \varphi^* \theta = \lambda$)</p> <p>Gavin Wraith in "Localic Groups", Cahiers de Top. et Geom. Diff. Vol XXII-1 (1981) defines an object </p> <p>$Points(G) = LocalMorphisms(G,\, \Omega) \subset \Omega^G$ and says that it is clear that:</p> <p>a) $Points(Map(X,\,Y)) = Y^X$.</p> <p>From this it follows that:</p> <p>b) There is a bijection $X \times Y \to \Omega \;\equiv\; X \to Y$ (where the arrow on the right satisfy ed) and uv))</p> <p>QUESTION 1] I ask for a convincing proof of a), or better, a proof of the weaker ? b).</p> <p>Concerning b), consider the following conditions on a relation $R \subset X \times Y$:</p> <p>exed) $\pi_1: R \to X$ is an epimorphism.</p> <p>exuv) The family $y = \pi_2 (x, y): C \to R \to Y$ is a compatible family with respect to the family $x = \pi_1 (x, y): C \to R \to X$. (indexed by all $(x, y): C \to R$)</p> <p>Then, using that epis are strict it follows using standard category theory:</p> <p>$R$ satisfy exed) and exuv) $\Leftrightarrow$ $\exists ! \; f: X \to Y$ such that $R = \Gamma_f$ (the Graph of $f$)</p> <p>Thus, b) will follow if we can prove :</p> <p>$R$ satisfy exed) and exuv) $\Leftrightarrow$ $\varphi_R$ satisfy ed) and uv) ($\varphi_R$ $=$ characteristic function).</p> <p>This is more related with the formula </p> <p>uv'): ($\; \lambda (x, y) \wedge \lambda ( x', y') \wedge i^*[[x = x']] \leq i [[y = y']]$ )</p> <p>SUBQUESTION] Are uv) and uv') equivalent ? </p> <p>QUESTION 2] </p> <p>Consider now a geometric morphism $f: \mathcal{F} \to \mathcal{E}$. We have a bijection </p> <p>$X \times Y \to f_*\Omega_\mathcal{E} \;\; \equiv \;\;<br> f^*X \times f^*Y \to \Omega_\mathcal{E}$. </p> <p>I want to know if the arrows satisfying ed) and uv) correspond under this bijection.</p> http://mathoverflow.net/questions/100539/on-internal-functions-and-arrows-in-a-topos/100572#100572 Answer by Wouter Stekelenburg for On internal functions and arrows in a Topos Wouter Stekelenburg 2012-06-25T08:09:01Z 2012-06-27T11:41:44Z <p>Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.</p> <p>Subquestion] these are provably equivalent in first order constructive logic.</p> <p>Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal F(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.</p> http://mathoverflow.net/questions/100539/on-internal-functions-and-arrows-in-a-topos/100640#100640 Answer by Eduardo Dubuc for On internal functions and arrows in a Topos Eduardo Dubuc 2012-06-25T23:21:32Z 2012-07-02T17:41:40Z <p>Thanks, your answer was useful (specially to Question 2) and clarify many things to me, but nevertheless I still am in lack of what I wanted to know in Question 1. </p> <p>Question1] ed) means that $\pi_0$ is an epimorphism, less evidently, uv) means that it is a monomorphism. Precisely I would like to have a hint of how to prove this. Out of an internal formula you derive an external statement. I had the statements exed) and exuv) and wanted to know how do you prove that they follow from ed) and un). I can prove by standard category theory that exed) and exuv) are equivalent to $\pi_0$ being an isomorphism, but I am still in darkness about how using ed) and uv) as hypothesis on $\lambda: X \times Y \to \Omega$, I can produce an arrow $\lambda: X \to Y$ to work with. Of course, I have a relation $R \subset X \times Y$, and all I need is to prove that $\pi_0$ is an isomorphism. But, how I can prove (or explain) this ?, more convincingly that writing "it just says so".</p> <p>Question2] A reference to or proof that the bijection $\mathcal{E}(X \times Y, f_* \Omega) \cong \mathcal{F}(f^* X \times f^* Y, \Omega)$ is a locale isomorphism ?. </p> <p>Concerning my original question2, it is still necessary to argue how using that being the bijection a locale isomorphism it follows that arrows which satisfy ed) and uv) correspond. </p>