I posted this question on MSE a few days ago, but got no response (despite a bounty). I hope it will get more answers here, but I'm afraid it might not be appropriate as I'm not sure it's actually research-level. Please do tell me if it's not appropriate and if possible tell me how to modify the question so that it may become appropriate (if such modifications exist)

I recently saw a video of a presentation of Andrej Bauer here about constructive mathematics; and there are two examples of locales he mentions that strike me : he explains quickly what the space of random reals might be, by saying that it's the locale of reals that are in every measure $1$ subset of $[0,1]$ (for instance): as he says, of course there are no such reals, but that should not stop us from considering the space of these reals, which may have interesting topological properties even if it has no points.

Similarly in a constructive setting (or classical setting without AC) some rings may have no prime/maximal ideals, and so their spectrum as usually conceived is uninteresting. But that should not stop us from studying the space of prime/maximal ideals with the Zariski topology, even if it has no points.

My questions are related to these examples specifically and to generalizations:

Is the first example of random reals in any way connected to the random reals one mentions in forcing ? e.g. is forcing to add some random reals in any way connected to considering the topos of sheaves on the locale of random reals ?

Has the second example been extensively studied ? What sort of properties can we get from the study of this "Zariski locale" ?

Is there some form of general theory of locales as spaces of imaginary points ? For instance is this how one usually sees locales intuitively; or better is there some actual theory (more than a heuristic) of constructing pointless (or with few points) spaces of objects that we'd like to exist but don't actually exist ? This is very vague so I'll give a further example of what one might envision: if two first-order structures $A$ and $B$ aren't isomorphic but $A\cong_p B$, we might want to study the space of isomorphisms of $A$ and $B$, which would ideally be a pointless locale. One could say something similar about generic filters of a poset when one is trying to do some forcing : from the point of view of the small model, these generic filters don't exist: we could envision a space of generic filters. In these four cases we have some objects that don't exist (random reals, maximal ideals, isomorphisms) but that we can define and that in some very vague sense ought to exist, and so we construct the space of these objects; but it turns out that this space can have no points at all: is there a general theory of this sort of thing ?

These questions are very vague so I hope they're appropriate. I'll appreciate answers with references, but I'd also very much like answers that themselves provide some intuition (though a bit more technical than what I've expressed in the question), and some thoughts.

  • $\begingroup$ What does $A\cong_p B$ mean? Does it denote elementary equivalence of structures? $\endgroup$ – Qfwfq Jul 20 '18 at 20:30
  • $\begingroup$ I wasn't sure whether it was standard notation. It means they're finitely partially isomorphic, i.e. there are many finite partial isomorphisms between them (many in the sense that you can always enlarge a finite domain or a finite codomain of a finite partial isomorphism to any larger finite domain or codomain). Some authors describe it as "$A$ is isomorphic to $B$, except if they're not; but then it's for stupid reasons, such as cardinality". In particular it's easy to see that this is the same as "there exists a forcing extension where they're isomorphic" @Qfwfq $\endgroup$ – Max Jul 20 '18 at 21:24
  • $\begingroup$ I see. I had never heard of this notion before (not a logician speaking...). I know I'll be asking a slightly off topic thing but could you make a concrete example of such a pair of structures being "not isomorphic just for stupid reasons"? $\endgroup$ – Qfwfq Jul 20 '18 at 22:32
  • 1
    $\begingroup$ @Qfwfq : $\mathbb{Q}$ and any dense, linear order without endpoints. It's known that if this second order is countable, then it is in fact isomorphic to $\mathbb{Q}$. If it's not countable though, then by collapsing its cardinal to $\aleph_0$ in a forcing extension makes it isomorphic to $\mathbb{Q}$ $\endgroup$ – Max Jul 21 '18 at 8:29
  • $\begingroup$ Even in classical mathematics, one of the main approach to algebraic geometry is not about spaces, but about toposes, which are already defined in this "point free" manner. $\endgroup$ – Hurkyl Jul 22 '18 at 6:27

I can only answer some of your questions.

Yes, the Zariski locale is extensively studied. It's one of the ways of setting up scheme theory in a constructive context: Don't define schemes as locally ringed spaces, but as locally ringed locales. The locally ringed locale $\mathrm{Spec}(A)$ always enjoys the universal property we expect of it, namely that morphisms $X \to \mathrm{Spec}(A)$ of locally ringed locales are in one-to-one correspondence with ring homomorphisms $A \to \mathcal{O}_X(X)$. (Only) if the Boolean Prime Ideal Theorem is available (a slightly weaker form of the axiom of choice), one can show that the Zariski locale has enough points. In this case it's isomorphic to the locale induced from the classical topological space of prime ideals (equipped with the Zariski topology).

(Note that the preceding paragraph assumes that you define the Zariski locale of a ring $A$ to be the locale of prime filters of $A$, not the locale of prime ideals. (A prime filter is a direct axiomatization of what's classically simply the complement of a prime ideal.) The locale of prime ideals also exists, but does not coincide with the true Zariski locale; classically, it is isomorphic to the topological space of prime ideals equipped with the constructible topology.)

Yes, there is a general theory of locales as spaces of imaginary points. Briefly, to any propositional geometric theory $T$ (roughly speaking, a collection of axioms of a certain form, such as the axioms of a prime ideal or of a prime filter), there is a classifing locale $\mathrm{Set}[T]$. The points of this locale are exactly the $\mathrm{Set}$-based models of $T$ (that is, the actual prime ideals or the actual prime filters). It can happen that there are no such models, yet still the theory $T$ is consistent. In this case the classifying local doesn't have any points, yet still is not the trivial locale.

Any locale $X$ is the classifying locale of some propositional geometric theory, a theory which deserves the name "theory of points of $X$".

The theory of classifying locales indeed allows you to construct spaces (locales) of things which aren't expected to exist, just by writing down the axioms of the hypothetical objects. A particularly tantalizing example is the locale of surjections from $\mathbb{N}$ to $\mathbb{R}$. There are no such surjections, of course, therefore this locale doesn't have any points. But it's still nontrivial. The topos of sheaves over this locale contains an epimorphism from $\underline{\mathbb{N}}$, the constant sheaf with stalks $\mathbb{N}$, to $\underline{\mathbb{R}}$; this epimorphism could be named the "walking surjection from $\mathbb{N}$ to $\mathbb{R}$", as any such surjection in any topos is a pullback of this one.

(The reals starred in the preceding paragraph only for dramatic purposes. The previous paragraph stays correct if $\mathbb{R}$ is substituted by any inhabited set. The described construction has been used, as one of a series of reduction steps, in Joyal and Tierney's celebrated monograph An Extension of the Galois Theory of Grothendieck.)

An excellent entry point to the business of locales as spaces of ideal points is a very accessible expository note by Steve Vickers. (When you've finished with this one, be sure to check out his further surveys, all available on his webpage, for instance this one.)

  • $\begingroup$ Thank you very much for a great answer. Could you add a bit of clarification concerning the classifying locale ? $\endgroup$ – Max Jul 21 '18 at 17:00
  • 5
    $\begingroup$ Nice answer. So, it looks like you belive that there is no surjection from $\mathbb{N}$ to $\mathbb{R}$. $\endgroup$ – Andrej Bauer Jul 21 '18 at 21:39

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this how peoples in topos theory/categorical logic understand it. And it makes the connection with those "locales of imaginary points" very clear.

It should be equivalent to the classical description..

Let say I want to construct some forcing extension that add one "thing" where "thing" can be for example "a random real number", "a generic real", "a surjection $\mathbb{N} \twoheadrightarrow X$" for some fixed set $X$, "a non-principal ultrafilter", a "generic filter"...

The first step is to look at the "space of all thing", i.e. the classifying locales of the theory of "thing". So "thing" has to be a nice (geometric) notion so that such a classyfing space exists.

Depending on whether your ground model of ZFC already have "things" this locale can have points or not. (of course the most interesting case is when it does not)

Then I need to check that this classifying locale of 'things' is non trivial. There are a lots of way to do that, and it really depends on the type of 'thing' you consider, though a very common technics to do that is the "Localic Bair category theorem" which says that an arbitrary intersection of dense sublocales is a dense sublocales. Of course this can fail. This happen for example if "things" are surjection $F \twoheadrightarrow \mathbb{N}$ with $F$ a fixed finite set.

If this locale is non-empty, I can look at the category of sheaves over it. It is a topos, and hence it admits something called "internal logic" which makes into a new "set theoretical universe" in which you have a canonical "thing". I refer you to classical books on topos theory for that notion (Moerdijk & MacLane "sheaves in geometry and logics, The volume 3 of Borceux's "Handbook of categorical algebra" are both very classical and very good. Chapter three of Collin McLarty "Elementary categories, elementary toposes" is also very focused on categorical logic so give a shorter introduction to the topic).

This is not quite the end of the story because this new "mathematical universes" is not quite a model of ZF for two reasons:

  • It corresponds to a "structural set theory" whereas ZF is a "material set theory" (to use the terminology of Mike Shulman's excellent paper that I recommend). This means that it is not based on the $\in$ relation, but rather on functions between sets. Fortunately the paper I just mention present some constructions (the "Cole-Mitchell-Osius" construction) that allow to go from a structural set theory to a material set theory, basically by looking at the class of all trees.

  • It might not satisfies the axiome of chocie or the law of excluded middle. But fortunately there is a nice topos theoretic construction which given a locale $L$ (or a more general Grothendieck topos) produces a covering of $L$ by a boolean locale $B$. The internal logic of that boolean locale also has a "thing" and this times satisfies the law of excluded middle and, if your ground model satisfies choice, the axiom of choice.

So to sum up, the forcing extension adding a "thing" is obtained hes the Cole-Mitchell-Osius construction applied to the category of sheaves of a boolean cover of the classifying locale of things. Of course, if you are already doing topos theory or cartegorical logic, you don't really care about getting a model of ZFC exactly, so you tend to get ride of the Cole-Mitchell-Osius construction, and even often of the boolean cover, and so you remeber the slogan that "forcing = sheaves over classyfing spaces".

For example for some structure $A$ and $B$, "being isomorphic in a forcing extention" is exactly the same as saying that the locale of isormorphisms between $A$ and $B$ is non-trivial.


Here are some comments on intuition. You can think of locales as being analogous to affine schemes and frames as being analogous to commutative rings; from this point of view the existence of locales with few or no points is no more surprising than the existence of affine schemes with few or no global points (morphisms from $\text{Spec } \mathbb{Z}$). In fact we have the following table of analogies:

  • Frame : commutative ring
  • Locale : affine scheme
  • Coproducts / joins : addition
  • Products / meets : multiplication
  • Open of a locale : function on an affine scheme
  • Point of a locale : global point of an affine scheme
  • Sierpinski space : affine line


Now, consider the following construction: there is an affine scheme which deserves to be called the "classifying scheme of square roots of $-1$," in that morphisms from $\text{Spec } R$ into this affine scheme correspond to square roots of $-1$ in $R$. Of course this scheme is just $\text{Spec } \mathbb{Z}[x]/(x^2 + 1)$. Note that it has no points, in the sense of no morphisms from $\text{Spec } \mathbb{Z}$, because $-1 \in \mathbb{Z}$ has no square roots. However, the "theory of a square root of $-1$" is nevertheless "consistent," in the sense that $\mathbb{Z}[x]/(x^2 + 1)$ is not the zero ring, and this "theory" does have "models," just in more complicated rings than $\mathbb{Z}$.

The quotation marks are meant to emphasize the following analogies between presenting a commutative ring by generators and relations and presenting a locale as the classifying locale of a propositional geometric theory:

  • Propositional geometric theory : collection of variables and polynomial identities between them
  • Model of a theory : collection of elements of a commutative ring satisfying some polynomial identities
  • Classifying locale of a theory : Spec of a commutative ring presented by generators and relations

Somewhat more explicitly, when we present a commutative ring by generators and relations as $\mathbb{Z}[x_1, \dots x_n]/(f_1, \dots f_m)$, the resulting affine scheme has the universal property that maps from $\text{Spec } R$ into it correspond exactly to solutions of the system of equations $f_1 = \dots = f_m$ in $R$. This is exactly analogous to the universal property of the classifying locale of a theory.


I consider locales as spaces with imaginary points where these imaginary points exist in larger set theoretic universes. In fact, locales should be thought of as spaces with imaginary points where in larger universes the points may still be imaginary, but there is eventually a large enough universe where the points will all appear as concrete objects. There are many examples of such spaces with imaginary points such as the space of all points in every dense open set, the space of all $\omega_{1}$-length branches on an Aronszajn tree or more generally the space of all threads in an empty inverse limit of sets, and the set of all generic ultrafilters on a poset. In all of these examples, one can associate a frame with these spaces with imaginary points. Furthermore, forcing can add the desired imaginary object, and forcing can also add points to locales without disrupting the locale too much. With that being said, extending a frames to a non-forcing extension can make all of the resulting frames homeomorphic and thus while these extensions add points, these extensions also collapse all of the differences between the frames.

Suppose that $M$ is a model definable with parameters in $V$. $M$ does not need to be a model of ZFC, ZF or much of anything for that matter. Furthermore, $M$ does not need to be well-founded. Suppose now that $$M\models\text{$L$ is a frame}.$$ Then $L$ will still be a distributive lattice in $V$. We say that an ideal $I\subseteq L$ is an $M$-ideal if whenever $R\in M,R\subseteq I$, we have $\bigvee R\in I$. Let $L^{+V}$ be the set of all $M$-ideals $I\subseteq L$. Then $L^{+V}$ is a frame in $V$. The way to interpret this frame without resorting to ideals is to observe that $L^{+V}$ is the smallest frame in $V$ containing $L$ such that if $C\subseteq L,C\in M$, then $\bigvee^{L^{+V}}C=\bigvee^{L}C$.

The theory of extending frames to larger universes behaves remarkably well when we limit our scope to the forcing extensions. Since complete Boolean algebras are special kinds of frames and are essential to point-free topology, it makes most sense to study the interpretation of frames in forcing extensions using the Boolean-valued model approach to forcing. I call this theory Boolean-valued pointfree topology. The downside to Boolean-valued pointfree topology is that it only works with forcing extensions and not with other extensions.

Suppose that $L$ is a frame and $B$ is a complete Boolean algebra which is a subframe of $L$. Then $L$ can be considered as a $B$-valued structure where we set $\|x\leq y\|$ to be the largest element $b\in B$ where $x\wedge b\leq y\wedge b$ and where we set $\|x=y\|$ to be the largest element $b\in B$ where $x\wedge b=y\wedge b$. Since $L$ is a $B$-valued structure closed under complete mixing, we can consider $L$ as an object in the forcing extension $V^{B}$ and $$V^{B}\models\text{$L$ is a frame}.$$

$\textbf{Theorem:}$ Suppose that $P$ is one of the properties: regularity, complete regularity, paracompactness, ultraparacompactness, zero-dimensionality. Then $L$ satisfies $P$ if and only if $$V^{B}\models\text{$L$ satisfies $P$}.$$

Now, if $L$ is a frame and $B$ is a complete Boolean algebra, then $B$ is a subframe of the frame coproduct $L\oplus B$. Therefore, $L\oplus B$ is a $B$-valued structure and $$V^{B}\models\text{$L\oplus B$ is a frame}.$$ It turns out that $L\oplus B$ is the correct way to interpret a frame $L$ as a frame in $V^{B}$ and the $L\oplus B$ is the Boolean-valued structure that corresponds to the $L^{+V[G]}$ construction. The following results illustrate the soundness of this construction.

$\textbf{Theorem:}$ Suppose that $P$ is one of the following properties: Compactness, locally connected connectedness, compact connectedness, regularity. Then $L$ satisfies property $P$ if and only if $$V^{B}\models\text{$L\oplus B$ satisfies property $P$}.$$

Passing to forcing extensions improves the topological properties of the spaces.

$\textbf{Theorem:}$ Suppose that $P$ is one of the following properties: Paracompactness, ultraparacompactness, complete regularity, zero-dimensionality, second countability. If $L$ satisfies property $P$, then $$V^{B}\models\text{$L\oplus B$ satisfies property $P$ as well}.$$

Now, if $L$ is a frame, then the points in $L$ are the frame homomorphisms $\phi:L\rightarrow 2$. One can extend this definition of a point to Boolean-valued models where we define a $B$-valued point to be a frame homomorphism $\phi:L\rightarrow B$. It turns out that the frame homomorphisms $\phi:L\rightarrow B$ form a $B$-valued structure where we set $\|\phi=\theta\|$ to be the largest $b\in B$ where $\phi(x)\wedge b=\theta(x)\wedge b$ for each $b\in B$. This definition of a point is coherent with the theory that we have developed since the frame homomorphisms $\phi:L\rightarrow B$ correspond with the $\dot{x}\in V^{B}$ such that $$V^{B}\models\text{$\dot{x}$ is a point in the frame $L\oplus B$}.$$

If $L$ is a frame, then let $B_{L}=\{x\in L|x^{**}=x\}$. Then $B_{L}$ is the smallest dense sublocale of the frame $L$, and $B_{L}$ is a complete Boolean algebra. The mapping $\phi:L\rightarrow B_{L}$ is a frame homomorphism. Therefore, forcing eventually adds points to every frame. For the regular frames, we can do much better than simply adding a few points using forcing just to satisfy the critics of point-free topology.

$\textbf{Theorem:}$ Suppose that $L$ is a regular frame. Then there is a complete Boolean algebra $B$ such that $$V^{B}\models\text{$L\oplus B$ is Polish space}.$$

Therefore, we should not think of point-free topology as just the study of spaces with imaginary points, but point-free topology is the study of spaces that will eventually become Polish spaces (unless you like lower separation axioms). Not only does Boolean-valued point-free topology justify point-free topology, but Boolean-valued point-free topology also justifies the separation axiom regularity since the regular frames will eventually become Polish spaces.

To be continued.

I am going to get back to this answer later with more details that describe what happens when the model $M$ is not a ground model of $V$ and in particular when $M$ is not well-founded in $V$. I will need more time to think about frames in these ill-founded models.


Since your question is kind of vague, I'll answer the question that I think you're asking:

The theory of generalized spaces usually goes a bit beyond locales, namely to Grothendieck topoi. Locales are a reflective subcategory of Grothendieck topoi, so you can think of Grothendieck topoi as a true generalization of locales. There are many examples of topoi that don't arise from topological spaces that occur frequently in geometry, for example, the topoi of sheaves of sets on the Étale and Nisnevich sites.

I am not a logician, but I think that the examples you're looking for are all usually stated in this language of topoi. Proving that these topoi are the sheaves on a localic site is usually how people think of such things.

Reference: https://ncatlab.org/nlab/show/locale#RelationToToposes

This is covered in great detail in Johnstone's Sketches of an elephant


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.