categories: Re: Terminology for point-free topology?

[Steven Vickers <s.j.vickers.1@bham.ac.uk>]

Dear Vaughan,

The idea of generic point as dense point looks misconceived to me. I'll say  more below. First, however, can I check we're in line with intro/extrovert? When I discussed the circle, was I using them with the same metaphorical content as you had in mind?

More below.

Steve.

________________________________
From: Vaughan Pratt <pratt@cs.stanford.edu>
Sent: Monday, January 23, 2023 11:17 PM
To: Steven Vickers (Computer Science) <s.j.vickers.1@bham.ac.uk>
Cc: categories@mta.ca <categories@mta.ca>
Subject: Re: categories: Terminology for point-free topology?


In my case the problem I'm having with Chu(E,k) is that I have no intuition  about E-enriched categories.  A given Chu space (a,r,x) would have a and x  each be an object of E, with x a frame defined by inclusion.  What I can't  picture is r: a x x → k.

A good picture for internal logic in E is often to imagine E as sheaves over some B, with the objects as local homeomorphisms to B. That might sound a  bit point-set, but Joyal and Tierney showed how to make sense of it for general E. Then geometric constructions, such as binary product a x x, are calculated fibrewise. The subobject classifier k is not geometric, but your maps r are just subobjects of a x x, and those too can be seen fibrewise.

Actually, frames aren't geometric either, but J&T showed that the internal frames correspond to more general bundles over B. When you build in the right conditions on r, it should correspond to a bundle map, from the local homeomorphism for a to the more general bundle for x. That is why we're approximating a bundle by a local homeomorphism. There is a best possible approximation, the discrete coreflection, or the "set of points" as calculated internally in E, but my example with B = Sierpinski shows it can be badly deficient even for straightforward bundles.

I must stress that the ability to treat bundles as internal spaces is a wonderful feature of point-free topology, something to be treasured, so one shouldn't be tempted to treat such straightforward bundles as pathological on  the grounds of their "non-spatiality".

"In fact the generic point in the topos of sheaves, on its own, is enough for most purposes."

Would that be the dense point?

No.

You'll see more discussion of this in my arXiv notes, but perhaps I can explain the generic point in computer science terms as a formal parameter.

Suppose you're working in a programming language L, and you write a procedure with a formal parameter x of type T. Within the scope of the declaration  x:T, you are no longer working in pure L, but in L with an element of T freely adjoined. Call it L[x:T]. The freeness lies in the fact that whatever you construct with x can be transported, by substitution, to any actual parameter a:T.

Note that a may itself be in the scope of some other formal parameter, hence in some L[x':T']. Substituting a for x transports any construction in L[x:T] into one in L[x':T'], so, in some sense you get a homomorphism L[x:T] -> L[x':T'].

Now think of x as "generic", in that it has no properties other than what follows from being of type T, and the actual parameters a as being more specific. The same idea applies to the generic point in a classifying topos.

Instead of types and elements, we have geometric theories and models. For instance T might be the geometric theory of Dedekind sections, and then a model is a real number. The classifying topos Set[x:T] is the geometric mathematics of Set with a model of T freely adjoined - that is pretty much what the universal property of classifying toposes tells us. If we have a model a of T, and it could be in some other topos, say Set[x':T'], then by substitution we get a functor Set[x:T] -> Set[x':T'] that preserves geometric structure (essentially: colimits and finite limits). It has a right adjoint, and hence we get a geometric morphism. That's a generalized point of Set[x:T] - its generalized points are equivalent to models of T.

Note also that, for a locale, that classifying topos is equivalent to the topos of sheaves.

I hope this helps clarify the fact that the generic point does not live in Set, but in a different topos Set[x:T] that is more or less a syntactic construct. Its sufficiency as a point on its own lies in the fact that it can be instantiated as any other more specific point.

I can't see any way in which it is helpful to see it as a "dense" point. (Are you trying to think of it as a "thickened" point where a circle meets a tangent? I don't think that analogy goes anywhere.)



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]