From mboxrd@z Thu Jan 1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org
X-Spam-Level:
X-Spam-Status: No, score=0.5 required=5.0 tests=DATE_IN_PAST_24_48,
RCVD_IN_MSPIKE_H2 autolearn=no autolearn_force=no version=3.4.4
Received: (qmail 22257 invoked from network); 25 Jan 2023 16:53:54 -0000
Received: from smtp2.mta.ca (198.164.44.75)
by inbox.vuxu.org with ESMTPUTF8; 25 Jan 2023 16:53:54 -0000
Received: from rr.mta.ca ([198.164.44.159]:39910)
by smtp2.mta.ca with esmtp (Exim 4.80)
(envelope-from )
id 1pKj1p-0001E7-DT; Wed, 25 Jan 2023 12:53:41 -0400
Received: from majordomo by rr.mta.ca with local (Exim 4.92.1)
(envelope-from )
id 1pKj0y-0002oy-F7
for categories-list@rr.mta.ca; Wed, 25 Jan 2023 12:52:48 -0400
From: Steven Vickers
To: Vaughan Pratt
CC: "categories@mta.ca"
Subject: categories: Re: Terminology for point-free topology?
Date: Tue, 24 Jan 2023 11:45:04 +0000
References:
In-Reply-To:
Accept-Language: en-US
Content-Language: en-US
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-2022-jp"
Content-Transfer-Encoding: quoted-printable
Precedence: bulk
Reply-To: Steven Vickers
Message-Id:
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
Sent: Monday, January 23, 2023 11:17 PM
To: Steven Vickers (Computer Science)
Cc: 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 =1B$B"*=1B(B k.
A good picture for internal logic in E is often to imagine E as sheaves ove=
r 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 ge=
neral E. Then geometric constructions, such as binary product a x x, are ca=
lculated fibrewise. The subobject classifier k is not geometric, but your m=
aps 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 rig=
ht conditions on r, it should correspond to a bundle map, from the local ho=
meomorphism for a to the more general bundle for x. That is why we're appro=
ximating a bundle by a local homeomorphism. There is a best possible approx=
imation, the discrete coreflection, or the "set of points" as calculated in=
ternally in E, but my example with B =3D Sierpinski shows it can be badly d=
eficient even for straightforward bundles.
I must stress that the ability to treat bundles as internal spaces is a won=
derful feature of point-free topology, something to be treasured, so one sh=
ouldn'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 f=
or most purposes."
Would that be the dense point?
No.
You'll see more discussion of this in my arXiv notes, but perhaps I can exp=
lain the generic point in computer science terms as a formal parameter.
Suppose you're working in a programming language L, and you write a procedu=
re 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 fr=
eely 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 par=
ameter a:T.
Note that a may itself be in the scope of some other formal parameter, henc=
e 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 f=
ollows from being of type T, and the actual parameters a as being more spec=
ific. The same idea applies to the generic point in a classifying topos.
Instead of types and elements, we have geometric theories and models. For i=
nstance T might be the geometric theory of Dedekind sections, and then a mo=
del is a real number. The classifying topos Set[x:T] is the geometric mathe=
matics 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 substi=
tution we get a functor Set[x:T] -> Set[x':T'] that preserves geometric str=
ucture (essentially: colimits and finite limits). It has a right adjoint, a=
nd 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 t=
opos 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 con=
struct. 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. (A=
re 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/ ]