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