Dear Steve, On Thu, May 31, 2018 at 10:40:41AM +0100, Steve Vickers wrote:
Does algebraic geometry provide an analogous construction that could lead to the point-free R? Can the locally ringed space be topologized (point-free) so that the copy of R has its usual topology?
very interesting question. I feel that the following remarks have some relevance. * Algebraic geometers do consider an analogue of the usual spectrum construction for topological rings: the "formal spectrum". Unfortunately, the theory is only developed for actual topological rings, not point-free versions of them. * One can define a point-free notion of a spectrum for apartness rings (ring objects in the category of sets-equipped-with-apartness-relation). This secretly comes up in algebraic geometry: Let X be a scheme. Inside the topos Sh(X), there is the ring O_X to which we can apply the usual point-free spectrum construction. We might hope that this just yields the one-point space; but unless X was zero-dimensional to begin with, this hope is false. In fact, the externalization of this construction is a locally ringed locale which comes equpped with a morphism of ringed locales to (X,O_X); but this morphism is not a morphism of *locally* ringed locales. The solution to this problem is to observe that O_X, being a local ring, has canonically the structure of an apartness ring. The variant of the spectrum construction for apartness rings applied to it yields the one-point space (i.e. (X,O_X) itself from the external point of view), as one would expect. * Both the problem and the solution can be generalized a bit. Let X be a scheme. Let A be an O_X-algebra. Then algebraic geometers consider the "relative spectrum of A", which is always a locally ringed locale over X and will be a scheme if A is quasicoherent. As before, it's not true that one can obtain the relative spectrum simply by carrying out the usual point-free spectrum construction internally in Sh(X). A variant is needed. A description of these variants of the usual construction can be found in Section 12 of https://rawgit.com/iblech/internal-methods/master/notes.pdf. However, I don't know yet a natural generalization of these constructions which could be directly helpful to your project -- they are tailored to apartness rings and to algebras over local rings. While it's certainly better to view the reals as an apartness ring instead of an ordinary ring, information has still been lost from the point-free version of the reals. Cheers, Ingo [For admin and other information see: http://www.mta.ca/~cat-dist/ ]