A locale is a sort of "formal topological space", which "may not have enough points to separate its open sets". For instance, there is a "locale of all real numbers that are both rational and irrational", which of course has no points at all (since there are no such numbers), but as a locale it is a nontrivial structure.

Locales are often better-behaved than topological spaces in constructive mathematics (i.e. in the absence of the law of excluded middle). For instance, there is a "locale of formal real numbers" $R_f$ whose sublocale $[0,1]_f$ is always compact, despite that the Heine-Borel theorem for the space $[0,1]$ may fail constructively. Classically, $R_f$ has enough points, but constructively it may not — though unlike the example above it of course has lots of points, indeed its points are dense in it. (See for instance P.T. Johnstone's book Stone spaces, or section D4.7 in Sketches of an Elephant.)

My question is: suppose $f:R_f \to R_f$ is a continuous map of locales, such that $f(x)>0$ for all points $x$ of $R_f$ (i.e. for all actual real numbers $x$); does it follow (constructively) that $f$ factors through the "locale of formal positive real numbers"?

The latter means the open sublocale of $R_f$ defined by the open subset $(0,\infty)$. Note that denseness of the points of $R_f$ is insufficient to answer "yes", since a function can be positive on a dense subset but zero at some other points.


1 Answer 1


I think the answer is no. Work in a recursive context; eg the effective topos. Consider a (uniformly continuous) function $f:R\to R$ such that $f(x)>0$ for all $x$, but we don't have a positive infimum. This is standard (use the Kleene tree). Now consider the embedding of pointwise spaces into locales; the work by Palmgren A constructive and functorial embedding of locally compact metric spaces into locales. Then you have a function as requested, but if it factors through the positive formal reals, then we have a positive infimum. The result is proved here and recalled in the introduction of this paper

  • $\begingroup$ How do you extend the map $f$ from reals to the locale of reals? Or this something that Erik does? $\endgroup$ Jul 30, 2015 at 21:40
  • $\begingroup$ Yes, that's what Erik does, (following Vickers). From the abstract: "a full and faithful functor M from the category of locally compact metric spaces and continuous functions into the category of formal topologies (or equivalently locales)" $\endgroup$ Jul 31, 2015 at 6:36
  • $\begingroup$ Deleted my last comment which was confused. This is excellent, thank you! $\endgroup$ Aug 28, 2015 at 17:04
  • $\begingroup$ Does Erik's work assume countable choice? $\endgroup$ Aug 28, 2015 at 17:04

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.