MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 ?


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.

share|cite|improve this question

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.

share|cite|improve this answer
Left exact functors preserve posets, and $\Omega_F$ is an internal poset in $\mathcal F$. The lattice structures of $\mathcal E(X\times Y,f_*\Omega)$ and $\mathcal F(f^*X\times f^*Y,\Omega)$ coincide because they are the result of applying naturally isomorphic left exact functors -- $\mathcal E(X\times Y,f_*-)$ and $\mathcal F(f^*X\times f^*Y,−)$ -- to the same poset. This equivalence in natural in $X$ and $Y$. Now joins have a universal property relative in terms of the order, and therefore must commute with the isomorphism. – Wouter Stekelenburg Jun 27 '12 at 17:54
Clear enough, thank you very much. – Eduardo J. Dubuc Jul 2 '12 at 17:40
To see that $\pi_0: L\to X$ is a monomorphism, consider its kernel pair $l,r:Z\to L\times L$. Now $\pi_0\circ l =\pi_0\circ r$ by definition, and $\pi_1\circ l = \pi_1\circ r$ by uv), because the morphism $(\pi_0\circ l,\pi_1\circ l,\pi_1\circ r): Z\to X\times Y\times Y$ represents the subobject $\{ (x,y,y')| \lambda(x,y)\land\lambda(x,y') \}$. Because $\pi_i\circ l = \pi_i\circ r$, $l=r$. To conclude: every parallel pair $f,g:W\to L$ such that $\pi_0\circ f= \pi_0\circ g$ factors uniquely through $l,r$. Therefore every such pair satisfies $f=g$. – Wouter Stekelenburg Mar 25 '13 at 9:51

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.

share|cite|improve this answer

Your Answer


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.