Re: Point-free affine real line?

[Vaughan Pratt <pratt@cs.stanford.edu>]

  > 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/ ]