On internal functions and arrows in a Topos

Question

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:

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

Consider the following formulae on $\lambda$:

ed): ($\bigvee_{y\in Y} \;\lambda\langle x,y \rangle = 1$),

uv): ($\lambda\langle x,y \rangle \wedge \lambda\langle x,y' \rangle \leq i^*[[y = y']]$).

Let $\theta: X \times Y \to Map(X,\,Y)$ be the universal locale furnished with such an arrow

(that is, $\forall \lambda \; \exists ! \; \varphi^* : Map(X,Y) \to G \;\; \varphi^* \theta = \lambda$)

Gavin Wraith in "Localic Groups", Cahiers de Top. et Geom. Diff. Vol XXII-1 (1981) defines an object

$Points(G) = LocalMorphisms(G,\, \Omega) \subset \Omega^G$ and says that it is clear that:

a) $Points(Map(X,\,Y)) = Y^X$.

From this it follows that:

b) There is a bijection $X \times Y \to \Omega \;\equiv\; X \to Y$ (where the arrow on the right satisfy ed) and uv))

QUESTION 1] I ask for a convincing proof of a), or better, a proof of the weaker ? b).

Concerning b), consider the following conditions on a relation $R \subset X \times Y$:

exed) $\pi_1: R \to X$ is an epimorphism.

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

Then, using that epis are strict it follows using standard category theory:

$R$ satisfy exed) and exuv) $\Leftrightarrow$ $\exists ! \; f: X \to Y$ such that $R = \Gamma_f$ (the Graph of $f$)

Thus, b) will follow if we can prove :

$R$ satisfy exed) and exuv) $\Leftrightarrow$ $\varphi_R$ satisfy ed) and uv) ($\varphi_R$ $=$ characteristic function).

This is more related with the formula

uv'): ($\; \lambda (x, y) \wedge \lambda ( x', y') \wedge i^*[[x = x']] \leq i [[y = y']] $ )

SUBQUESTION] Are uv) and uv') equivalent ?

QUESTION 2]

Consider now a geometric morphism $f: \mathcal{F} \to \mathcal{E}$. We have a bijection

$X \times Y \to f_*\Omega_\mathcal{E} \;\; \equiv \;\; f^*X \times f^*Y \to \Omega_\mathcal{E}$.

I want to know if the arrows satisfying ed) and uv) correspond under this bijection.

Answer 1

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.

Subquestion] these are provably equivalent in first order constructive logic.

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.

Answer 2

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.

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

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

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.