Return to Answer

So, the starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For example, one can just says that the poset of open is given by the (opposite) of the poset of radical ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces". And while prime ideal are a little dangerous constructively as they might not exists, ideals are not problematic at all, you always have plenty of them.

So, the starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For example, one can just says that the poset of open is given by the poset of radical ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces". And while prime ideal are a little dangerous constructively as they might not exists, ideals are not problematic at all, you always have plenty of them.

I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk.

They are a small variation on the idea of a topological space, where instead of defining a space by giving a set of points together with a collection of "open subsets" stable under arbitrary unions and finite intersections, one just gives an abstract ordered set of "open subspaces" which should have arbitrary supremums and finite infimums and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame (this is actually the same as a complete Heyting algebra), a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales are defined as just being "the opposite of the category of frames", i.e. a locale is just a frame, and morphisms of locales are morphisms of frame in the other direction.

I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk: They are a small variation on the idea of a topological space, where instead of defining a space by giving a set of points together with a collection of "open subsets" stable under arbitrary unions and finite intersections, one just gives an abstract ordered set of "open subspaces" which should have arbitrary supremums and finite infimums and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame (this is actually the same as a complete Heyting algebra), a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales are defined as just being "the opposite of the category of frames", i.e. a locale is just a frame, and morphisms of locales are morphisms of frame in the other direction.

I do not know if you are already familiar with the notion of locale. They are a small variation on the idea of topological space, where instead of defining a space by giving a set of point together with a collection of "open subset" stable under arbitrary union and finite intersection, one instead just give an abstract order set of "open subset" which should have arbitrary supremum and finite infimum and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame, a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales a defined as just being "the opposite of the category of frame" (so a locale is just a frame, and morphisms of locales are morphism of frame in the other direction).

It is rather easy to go from a topological space to a locales by just remembering the poset of open subspace, and attaching to a continuous map its action on open subset by pre-image. Conversely if one has a locale $X$, one can define a "point" of it as a morphism from the locale corresponding to the one point topological space to $X$, there is a topology on this set of points (generated by the element of the frame corresponding to $X$) and these two construction form an adjunction between frame and topological space, which can be shown to be an equivalence between rather large subcategory (more precisely between "sober topological spaces" and "spatial locales").

There are however some locales which have no points at all. At first you can regard them as pathological monster, but it in fact appears that some of them are extremely natural objects and interesting objects (things like the space of "generic real numbers" or "random real numbers" that Andrej mentioned in his talk, or the "space of bijection" between two infinite set of different cardinality).

Classically, locales and topological spaces are very similar (for example, if you are only interested in complete metric space or locally compact spaces you will not see the differences) but the category of locales is (arguably) slightly better behaved than the category of topological spaces.

Constructively, it is a lot harder to construct "points" of locales. This make the gap between topological spaces and locales considerably larger. And locales become incredibly better behaved than topological spaces.

For example, a lot of classical theorem which requiert the axiom of choices become fully constructive when formulated in terms of locales. This the case for example of the Tychonov theorem, the Hahn Banach theorem, or the Gelfand duality.

For example the idea for the Hahn Banach theorem is that instead of asking for the existence of certain linear form or extension of linear form, we construct a space (a locale) of linear form and show that this is not the empty space (even if it might not have points) and that the map between these spaces induced by restricting to a subspace is always a "surjection" in a good localic sense.

I higlhy recommand to have a look to Peter Johnstone excellent introduction paper to the subject "The point of pointless topology"

The starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For exemple, one can just says that the poset of open is given by the (oposite) of the poset of ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces".

This locales we are constructing is still essentially the "space of prime ideal of the ring" but the question of whether the ring actually has any prime ideal or not become just the question of whether this space has points or not, which a rather unimportant question in locale theory.

This let you go through with the definition of a scheme in a constructive settings. It appears than most classical results of algebraic geometry became constructive when formulating using locales instead of spaces (and replacing statement involving existence of prime or maximal ideal by statement about property of the space of prime ideals similarly to the Hahn banach theorem above). Unfortunately, except very basic things, these are mostly "folk theorem" and do not very often appears in literature (because let's face it, not many algebraic geometer are interested in constructivisme...). With the exception of the work of Ingo Blechschmidt that I mention below.

The last step to this story relies on "internal logic". The idea is that if you work internally in (the topos of sheaves over) the localic Zariski spectrum, then you actually have a "prime ideal of your ring" (more precisely, you have a "localizing system" which satisfies the properties to be the complement of a prime ideal... but taking complement is a dangerous things in constructive mathematics) and this prime ideal is in some sense the universal prime ideal of your ring (proving a property for this internal prime ideal proves property for all prime ideal of your ring) and a large number of proof that relies on the axiom of choice because they says at some point "let M be a maximal/prime ideal of your ring" (for exemple, if you prove that some element is nilpotent because it belongs to all prime ideal) become constructive if, instead of chosing a prime ideal, one move to this internal logic and use the universal one.

This idea of exploiting internal logic in algebraic geometry tend to make everything constructive and has been pushed quite far by Ingo Blechschmidt (you can watch one of his talk here, or read his thesis work here)

To my knowledge the work of Ingo is the only place where you will find a non trivial treatment of algebraic geometry which use this picture.

I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk.

They are a small variation on the idea of a topological space, where instead of defining a space by giving a set of points together with a collection of "open subsets" stable under arbitrary unions and finite intersections, one just gives an abstract ordered set of "open subspaces" which should have arbitrary supremums and finite infimums and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame (this is actually the same as a complete Heyting algebra), a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales are defined as just being "the opposite of the category of frames", i.e. a locale is just a frame, and morphisms of locales are morphisms of frame in the other direction.

It is rather easy to go from a topological space to a locales by just remembering the poset of open subspaces, and attaching to a continuous map its action on open subset by pre-image. Conversely if one has a locale $X$, one can define a "point" of it as a morphism from the locale corresponding to the one point topological space to $X$, there is a topology on this set of points (generated by the element of the frame corresponding to $X$) and these two constructions form an adjunction between locales and topological spaces, which can be shown to be an equivalence between rather large subcategories. More precisely it induces an equivalence between "sober topological spaces" and "spatial locales", where spatial locales are the locales "having enough points" in a precise technical sense.

There are however some locales which have no points at all. At first you can regard them as pathological monster, but it in fact appears that at least some of them are extremely natural and interesting objects (things like the space of "generic real numbers" or "random real numbers" that Andrej mentioned in his talk, or the "space of bijection" between two infinite set of different cardinality whose non triviality is the key points for Cohen forcing to works).

Despite this, classically, locales and topological spaces are very similar (for example, if you are only interested in complete metric spaces or locally compact spaces you will not notice the difference) but the category of locales is overall (arguably) slightly better behaved than the category of topological spaces.

But constructively, it is a lot harder to construct "points" of locales and a lot more locale appears to be non-spatial. This make the gap between topological spaces and locales considerably larger. And in this weaker framework, locales become incredibly better behaved than topological spaces. For example without the law of excluded middle the correct definition of the locale of real number might be non-spatial but is always locally compact, while it is well known that constructively the topological space of real numbers can fail to be locally compact (this is one of the bad things that happen in constructive analysis that Andrej mentioned in his talk). In fact it is known that they agree if and only if the topological space of real number is locally compact.

Similarly, a lot of classical theorem which requiert the axiom of choices become fully constructive when formulated in terms of locales. This the case for example of the Tychonov theorem, the Hahn Banach theorem, or the Gelfand duality.

For example the idea for the Hahn Banach theorem is that instead of asking for the existence of certain linear form or extension of linear form, we construct a space (a locale) of linear form and show that this is not the empty space (even if it might not have points) and that the map between these spaces induced by restricting to a subspace is always a "surjection" in a good localic sense. And this roughly also what happen for the Gelfand duality or the case of ring spectrum that we will discuss below

I highly recommend to have a look to Peter Johnstone excellent non technical introduction paper to the subject "The point of pointless topology" which will expand on what I just said. and probably explains it more clearly.

So, the starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For example, one can just says that the poset of open is given by the (opposite) of the poset of radical ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces". And while prime ideal are a little dangerous constructively as they might not exists, ideals are not problematic at all, you always have plenty of them.

This locale we are constructing is still morally the "space of prime ideal of the ring" but the question of whether the ring actually has any prime ideal or not become just the question of whether this space has points or not, which a rather unimportant question in locale theory.

In fact, if you are familiar with the notion of classifying topos, it is the "space of prime ideal" in the sense that it is the classifying space for prime ideal, more precesely for "prime ideal complement", i.e. subset $O$ of the ring such that ($xy \in O \Rightarrow x \in O \text{ and }y \in O$; $0 \notin O$; $1 \in O$ ; $x+y \in O \Rightarrow x \in O \text{ or } y \in O$) which classically are exactly the complements of prime ideal, and construcively are more important because they are the things you need to get a locale ring when localizing.

This let you go through with the definition of a scheme in a constructive setting. It appears than most classical results of algebraic geometry became constructive when formulated using locales instead of spaces (and replacing statement involving existence of prime or maximal ideal by statement about property of this "space of prime ideals" similarly to the Hahn banach theorem above). Unfortunately, except very basic things, these are mostly "folk theorem" and do not very often appears in literature (because let's face it, not many algebraic geometer are interested in constructivisme...). With the exception of the work of Ingo Blechschmidt that I mention below.

In fact (but that is a personal opinion) I've always found that, for someone already familiar with locale theory, the localic treatment of the basic property of the Zariski spectrum are notably simpler than their usual topological treatment.

The last step to this story relies on the use of "internal logic". The idea is that if you work internally in (the topos of sheaves over) the localic Zariski spectrum, then you actually have a "prime ideal of your ring" (more precisely, you have a "localizing system" which satisfies the properties to be the complement of a prime ideal mentioned above) and this prime ideal is in some sense the universal prime ideal of your ring (proving a property for this internal prime ideal proves property for all prime ideal of your ring) and a large number of proof that relies on the axiom of choice because they says at some point "let M be a maximal/prime ideal of your ring" (for example, if you prove that some element is nilpotent because it belongs to all prime ideal) become constructive if, instead of choosing a prime ideal, you move to this internal logic and use the universal one.

This produces a quite efficient and automatic method to make lots of results of algebra and algebraic geometry constructive.

This idea of exploiting internal logic in algebraic geometry tend to make everything constructive and has been pushed quite far by Ingo Blechschmidt (you can watch one of his talk here, or read his thesis work here)

To my knowledge the work of Ingo is the only place where you will find a non trivial treatment of algebraic geometry which use this picture.

For another example, another place, completely different from prime ideal, where you will use non-constructive things in algebra or algebraic geometry is when you want to talk about algebraic closure of a fields. But it appears that this point of view also provide a solution. In general you cannot construct a single algebraic closure of a given fields, but what you can instead do is to consider the "space of all algebraic closure of the field" in the sense of theory of classifying topsoes. This times this will not even be a locale, but a more general kind of topos, and it appears that this topos is something that have actually been studied a lot by algebraic geometers: indeed, if you start from some ring $R$ and study the "space of all algebraic closure of all residual fields of $R$" defined in a proper way what you get is nothing else than the "small étale topos of $R$". See the work of Gavin Wraith on the subject.