The question about the affine real line represents a challenge to this geometric approach, and I'd like to form a better idea of whether it is simply a difficult problem, or a fundamental limitation to my approach.
An affine space over any given field differs *k* from a vector space over *k* only in its algebraic structure, not its topological structure. Whereas the algebraic operations of a vector space over *k* consist of all finitary linear combinations with coefficients drawn from *k*, those of an affine space consist of the subset of those combinations whose coefficients sum to unity, the barycentric combinations. Since the former includes the constant 0 as a linear combination while the latter does not, a consequence is that 0 is a fixpoint of linear transformations but not of affine transformations, whence the latter can include the translations. This is equally true whether *k* is the rationals or the reals. So whatever method you use to obtain the real line from the rational line should also produce the affine real line from the affine rational line. The relevance of the equational theory I gave in my previous message is that it is equivalent to the equational theory of affine spaces over the rationals yet does not require a separate theory of the rationals. The insight here is that the polynomials formed from the operations 2b - a and all finitary centroid operations, one for each positive finite arity, are precisely the barycentric linear combinations with rational coefficients. The real line is a model of this theory but lacks the usual topology that expands its algebraic operations to include linear combinations with all real coefficients. I cannot conceive how the absence of the linear combinations whose coefficients don't sum to unity could be an obstacle for you. Vaughan Pratt On Fri, Jun 1, 2018 at 3:11 AM, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
Dear Johannes,
"Point-free" is as opposed to "point-set" - there is no assumption that the real numbers form a set. Instead, they are taken to be the models of a (geometric) theory of Dedekind sections of the rationals (which do form a set). More generally, a point-free space is one where the points are defined as models of a propositional geometric theory. The topology is then defined intrinsically, opens being the geometric propositions.
My motivation for this comes from topos theory. In any elementary topos, each point-free space does in fact have a set (object) of points. Topologically, it amounts to approximating bundles by local homeomorphisms. However, that construction is not geometric - preserved by inverse image functors, and by pullback of bundles -, so the point-set version is not robust under change of base. There are advantages to staying within the geometric fragment of elementary topos logic, and I am exploring how far that can be taken. I also now have other semantics using arithmetic universes, where the point-set versions simply don't exist.
If it helps, the point-free real line in an elementary topos E is the localic geometric morphism p: F -> E got from F as topos of sheaves of the internal locale of formal reals in E. If E is an S-topos, then you can do this generically over S to get R as the S-classifier for Dedekind sections, and then p is just the bipullback E x_S R. A point-set R would be some local homeomorphism over E (then equipped separately with a topology), but in general it is not got as a bipullback of a local homeomorphism over S.
The question about the affine real line represents a challenge to this geometric approach, and I'd like to form a better idea of whether it is simply a difficult problem, or a fundamental limitation to my approach. To put it another way, am I following in Grothendieck's footsteps in the way I think of toposes, or am I mishandling his ideas in ways that have no bearing on what he was trying to do?
All the best,
Steve.
On 01/06/2018 10:22, huebschm@math.univ-lille1.fr wrote:
Dear Steve
I am not sure whether I understand. What precisely do you mean by "point-free"?
On Thu, 31 May 2018, Steve Vickers wrote:
Algebraic geometry defines the affine line over a field k as an affine scheme, the spectrum of k[X]. It includes a copy of k, each element a being present as the irreducible polynomial X-a, with local ring the ring of fractions got by inverting polynomials f(X) such that f(a) is non-zero.
You can carry this out for the real line R, but it is very much R as a set, and the copy of R in the underlying space of the spectrum has the discrete topology.
The standard approach leads to the Zariski topology.
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?
I've run into various problems.
1. It is not obvious to me that R[X] exists point-free. By that I mean that, without presupposing a set R[X], or using non-geometric constructions, I can't see how to define a geometric theory whose models are the polynomials. The problem comes with trying to pin down the requirement that all but finitely many of the coefficients of a polynomial must be zero. You cannot continuously define the degree of a polynomial, because the function R -> N, a |-> degree(aX + 1), is not continuous.
That suggests the construction as Spec(R[X]) might have to be adjusted. Is there still some locally ringed space that does the trick?
2. The "structure sheaf" cannot be a sheaf. We hope its fibres are point-free local rings, but, whatever they are, they must be R-algebras and so cannot have the discrete topology. The space is locally ringed by some bundle other than a sheaf (local homeomorphism).
3. The usual local rings, got as rings of fractions as described above, may be problematic point-free in the same way as R[X] is. I don't know what would do instead. The power series ring R[[X]]?
The power series ring recovers a single point ("formal geometry" in the sense of Grothendieck, Gelfand-Kazhdan, Kontsevich, etc.).
Best Johannes
(At least as fibre over 0.) It does have the property of inverting those polynomials f for which f(0) is non-zero. And it can be defined point-free, as R^N. (However, the finitely presented approximations R[X|X^n = 0] happily exist point-free.)
Thanks for any references you can provide,
Steve.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]