Constructive algebraic geometry

I was just watching Andrej Bauer's lecture Five Stages of Accepting Constructive Mathematics, and he mentioned that in the constructive setting we cannot guarantee that every ideal is contained in a maximal ideal---since that obviously requires Zorn's Lemma (or is equivalent to Zorn's Lemma, perhaps?)---so we need to approach algebraic geometry from a different point of view, such as locales.

I am curious how algebraic geometry looks from this constructive point of view, and if there are any good references on this subject?

I'm fairly new to constructive mathematics, though I have been lured in by Kock's synthetic differential geometry, and I'm starting to read the HoTT book.

• Lombardi's and Quitté's book Commutative algebra: Constructive methods. Finite projective modules gives a quite involved look at what the commutative algebra part looks like constructively. This may give you some idea of what takes the place of maximal ideals and such. It is not focused on algebraic geometry though. Nov 15, 2017 at 12:36
• Here is a way to talk about the Zariski spectrum without ever mentioning prime ideals: it is the right adjoint to the global sections functor from locally ringed spaces to commutative rings. If we replace locally ringed spaces with locally ringed locales, for the right definition of "locally ringed" (there is a definition which does not refer to stalks) then we should get a constructively meaningful construction, which may or may not agree with the locale whose closed sets are the ideals. Nov 15, 2017 at 18:22
• (read "whose close subspaces are radical ideals") Nov 15, 2017 at 20:20
• @AbdelmalekAbdesselam : Maybe, but 'Algorithmic' would be a really terrible name for something that accept the full law of excluded middle. Algoritmically speaking its fine to assume that for exemple elements of the ring you work with satisfies (a=b) or not (a=b), but if I gave you a sequence of element of the ring or a function P, decide if "there exist x such that $P(x)=0$" or "$P(x) \neq0$ for all x" is not algorithmic, the case where P is a polynomial in several integer variables is the typical algoritmically undecidable problem ! Nov 16, 2017 at 19:20
• @AbdelmalekAbdesselam Not sure, names for this sort of things often comes from (one of) the semantics you have in mind for them, and I don't know an interesting semantics for this system. So in waiting for a good semantics (which as far I'm concern also mean " a reason to work in this system" ) I would call it just ZF+DC. There are various names that already exists if you add to this system some axioms which contradict full choice (the sort of things that are true in Solovay model) like "Dream mathematics" ncatlab.org/nlab/show/dream+mathematics Nov 16, 2017 at 20:33

Let me wrote a quick introduction to this idea:

1) Locales

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.

2) The localic Zariski spectrum

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.

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.

3) Internal logic

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.

• Excellent answer, and I do recommend Ingo's work. Nov 15, 2017 at 16:02
• Small correction: the frame of opens of the Zariski spectrum is the (opposite of the) poset of radical ideals, not all ideals Nov 15, 2017 at 19:37
• @ಠ_ಠ You're welcome. I just corrected a lots of details and added some precision and new examples. Nov 15, 2017 at 21:10
• @SimonHenry By the way, do you happen to know where I could find the interpretation of "random real numbers" using locales? It sounds very interesting.
– ಠ_ಠ
Nov 15, 2017 at 22:06
• In the work of Alec Simpson mostly like homepages.inf.ed.ac.uk/als/Research/Sources/mrs.pdf and some other work of him. Although I believe there are several (non equivalent) variations on this idea (the most obvious being to consider fully additive measure instead of $\sigma$-additive which is more natural in locale theory), some of them being treated elsewhere. I'll add more precision If I can remember... Nov 15, 2017 at 22:34