2 tag added
1

# On internal functions and arrows in a Topos

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.