{"id":428,"date":"2014-07-30T22:00:26","date_gmt":"2014-07-30T20:00:26","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=428"},"modified":"2022-11-19T15:31:41","modified_gmt":"2022-11-19T14:31:41","slug":"equilogical-spaces","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=428","title":{"rendered":"Equilogical spaces"},"content":{"rendered":"<p>A few weeks ago, I went to the <a title=\"Semantics of proofs and programs\" href=\"https:\/\/www.ihp.fr\/fr\/ceb\/trimester\/proofs\/workshop3\">Semantics of Proofs and Programs workshop<\/a> at the Institut Henri Poincar\u00e9 in Paris. There were many fascinating talks there, and the workshop was very enjoyable.<\/p>\n<p>At some point, <a title=\"Giuseppe Rosolini\" href=\"https:\/\/www.disi.unige.it\/person\/RosoliniG\/\">Giuseppe Rosolini<\/a> mentioned <a title=\"Dana Scott\" href=\"https:\/\/www.cs.cmu.edu\/~scott\/\">Dana Scott<\/a>&#8216;s equilogical spaces. I had loved this construction since I&#8217;ve learned about it, so let me talk about it. Apparently, Dana Scott had mentioned the idea already in 1976 [1, Section 7], and it did not catch on. It was resurrected in work by Andrej Bauer, Lars Birkedal and Dana Scott [2] more than 20 years later.<\/p>\n<p><strong>Equilogical spaces.<\/strong><\/p>\n<p>The categorical of equilogical spaces is a very natural category, and it is Cartesian closed (and a bit more). Here is the definition:<\/p>\n<ul>\n<li>An equilogical space is a pair (<em>X<\/em>, \u2261) where <em>X<\/em> is a T<sub>0<\/sub> space and \u2261 is an equivalence relation on <em>X<\/em>.<br \/>\nI will almost always write \u2261 for the ambient equivalence relation, irrespective of the space we are in.<br \/>\nYou may think of (<em>X<\/em>, \u2261) as saying we really wish to contemplate the quotient <em>X<\/em>\/\u2261, but we do not really carry out any quotienting. Similarly to formal balls, we might call these objects <em>formal quotients<\/em>.<\/li>\n<\/ul>\n<ul>\n<li>It is tempting to define a morphism of equilogical spaces <em>f<\/em> : (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261) as a continuous map <em>f<\/em> from <em>X<\/em> to <em>Y<\/em>. It is only sensible to require <em>f<\/em> to be <em>equivariant<\/em>, namely to be such that if <em>x<\/em>\u2261<em>x&#8217;<\/em> then <em>f<\/em>(<em>x<\/em>)\u2261<em>f<\/em>(<em>x&#8217;<\/em>).<br \/>\nHowever, in the formal quotient interpretation, you would not like to distinguish between two equivariant continuous maps <em>f<\/em>, <em>f&#8217;<\/em> : <em>X<\/em> \u2192 <em>Y<\/em> that map every element to distinct but equivalent elements.<br \/>\nIn other words, say that two maps <em>f<\/em>, <em>f&#8217;<\/em> : <em>X<\/em> \u2192 <em>Y<\/em> are <em>equivalent<\/em> if and only if, for every <em>x<\/em> in <em>X<\/em>, <em>f<\/em>(<em>x<\/em>)\u2261<em>f&#8217;<\/em>(<em>x<\/em>).<br \/>\nWe then define the morphisms of equilogical spaces from (<em>X<\/em>, \u2261) to (<em>Y<\/em>, \u2261) as those <em>equivalence classes<\/em> of equivariant continuous maps from <em>X<\/em> to <em>Y<\/em>.\u00a0 I will usually do as if morphisms were equivariant continuous maps, but I&#8217;ll have to remind you that these morphisms are understood modulo equivalence, from time to time.<\/li>\n<\/ul>\n<p>That is it! Let us write <strong>Equ<\/strong> for the resulting category, of equilogical spaces and equivalence classes of equivariant continuous maps.\u00a0 At first sight,\u00a0<strong>Equ<\/strong> is very close to <strong>Top<\/strong><sub>0<\/sub>, the category of T<sub>0<\/sub> topological spaces, and I would not have been surprised to learn that they are equivalent&#8230; but they are not, since one is Cartesian-closed and the other is not.<\/p>\n<p><strong>Equ<\/strong> is a larger category than <strong>Top<\/strong><sub>0<\/sub>, in the following sense. <strong>Top<\/strong><sub>0<\/sub> embeds into <strong>Equ<\/strong> through the functor Inj that maps every topological space <em>X<\/em> to (<em>X<\/em>, =), and every continuous map <em>f<\/em> : <em>X<\/em> \u2192 <em>Y<\/em> to the (one-element) equivalence class of <em>f<\/em>.<br \/>\nConversely, there is a functor Q : <strong>Equ<\/strong> \u2192 <strong>Top<\/strong><sub>0<\/sub> that maps every formal quotient (<em>X<\/em>, \u2261) to the actual quotient space <em>X<\/em>\/\u2261. The composition Q o Inj is the identity, and there is natural transformation from the identity functor on <strong>Equ<\/strong> to Inj o Q (at object (<em>X<\/em>, \u2261), it maps <em>x<\/em> in <em>X<\/em> to its equivalence class modulo \u2261). Putting all this together, Inj is right adjoint to Q, so, equating <strong>Top<\/strong><sub>0<\/sub> with its image in <strong>Eq<\/strong><strong>u<\/strong>, we see that <strong>Top<\/strong><sub>0<\/sub> is a reflective subcategory of <strong>Eq<\/strong><strong>u<\/strong> (see p.183).<\/p>\n<p><strong>Limits, colimits.<\/strong><\/p>\n<p><strong>Equ<\/strong> has all products. The product \u220f<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> (<em>X<em><sub>i<\/sub><\/em><\/em>, \u2261<em><sub>i<\/sub><\/em>) is the obvious one, (\u220f<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> <em>X<em><sub>i<\/sub><\/em><\/em>, \u2261), where \u2261 is the equivalence relation defined by: (<em>x<sub>i<\/sub><\/em>)<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> \u2261 (<em>x&#8217;<sub>i<\/sub><\/em>)<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> if and only if <em>x<sub>i<\/sub><\/em> \u2261<em><sub>i<\/sub><\/em> <em>x&#8217;<sub>i<\/sub><\/em> for every <em>i<\/em> in <em>I<\/em>.<\/p>\n<p><strong>Equ<\/strong> has all equalizers, too. The equalizer of <em>f<\/em>, <em>g<\/em> : (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261) is the subspace [<em>f<\/em>\u2261<em>g<\/em>] of <em>X<\/em> of those points <em>x<\/em> such that <em>f<\/em>(<em>x<\/em>)\u2261<em>g<\/em>(<em>x<\/em>), with equivalence relation the restriction of that of (<em>X<\/em>, \u2261) to the subset [<em>f<\/em>=<em>g<\/em>]. In general, the equalizers in <strong>Equ<\/strong> are the \u2261-satured subspaces, with the obvious definition of subspace (a topological subspace with the restriction of the equivalence relation); \u2261-saturated means that any element that is \u2261-equivalent to one of the subspace is also in the subspace.<\/p>\n<p>Since <strong>Equ<\/strong> has all products and all equalizers, it is complete.<\/p>\n<p><strong>Equ<\/strong> also has all coproducts, and they are also the obvious ones. The coproduct \u2210<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> (<em>X<em><sub>i<\/sub><\/em><\/em>, \u2261<em><sub>i<\/sub><\/em>) is the obvious one, (\u2210<em><sub>i<\/sub><\/em><sub> in <\/sub><em><sub>I<\/sub><\/em> <em>X<em><sub>i<\/sub><\/em><\/em>, \u2261), where \u2261 is the equivalence relation defined by: (<em>i<\/em>, <em>x<\/em>) \u2261 (<em>i&#8217;<\/em>, <em>x&#8217;<\/em>) if and only if i=<em>i&#8217;<\/em> and <em>x<\/em> \u2261<em><sub>i<\/sub><\/em> <em>x&#8217;.<\/em><\/p>\n<p>The main difference with <strong>Top<\/strong> is with coequalizers. In <strong>Top<\/strong>, the coequalizers are the quotient maps. The coequalizers are rather different in <strong>Equ<\/strong>. We build them now.\u00a0 As a consequence, <strong>Equ<\/strong> will be cocomplete.<\/p>\n<p><strong>Coequalizers<\/strong>.<\/p>\n<p>A coequalizer of <em>f<\/em>, <em>g<\/em> : (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261) in <strong>Equ<\/strong> is by definition an (equivalence class) of equivariant continuous maps <em>h<\/em> : (<em>Y<\/em>, \u2261) \u2192 <em>Z<\/em> for some equilogical space <em>Z<\/em>, such that <em>h<\/em> o <em>f<\/em> = <em>h<\/em> o <em>g<\/em> (up to equivalence), and which is universal with this property.<\/p>\n<p>A good candidate for <em>h<\/em> and <em>Z<\/em> is as follows.\u00a0 Let <em>R<\/em> be the symmetric relation on <em>Y<\/em> defined by <em>y R y&#8217;<\/em> if and only if <em>y<\/em>=<em>f<\/em>(<em>x<\/em>) and <em>y&#8217;<\/em>=<em>g<\/em>(<em>x<\/em>) for some <em>x<\/em> in <em>X.<\/em>\u00a0 If <em>h<\/em> exists, then <em>h<\/em>(<em>y<\/em>)\u2261<em>h<\/em>(<em>y&#8217;<\/em>) for every pair\u00a0<em>y<\/em>,\u00a0y&#8217; in\u00a0<em>Y<\/em> with <em>y R y&#8217;<\/em>.\u00a0 It follows that the same relation holds for every pair <em>y<\/em>,\u00a0y&#8217; in\u00a0Y such that\u00a0<em>y <\/em>(\u2261 \u222a <em>R<\/em>)* <em>y&#8217;<\/em>.\u00a0 The relation\u00a0(\u2261 \u222a <em>R<\/em>)* is the reflexive transitive closure of the union of the two relations. In other words, <em>x\u00a0<\/em>(\u2261 \u222a <em>R<\/em>)* <em>x&#8217;<\/em> if and only if there are 2<em>n<\/em>+1 points, for some natural number <em>n<\/em>, <em>x<sub>0<\/sub><\/em>, <em>x<sub>1<\/sub><\/em>, &#8230;, <em>x<sub>2n+1<\/sub><\/em>, such that <em>x<\/em> \u2261 <em>x<sub>0<\/sub><\/em>\u00a0<em>R<\/em> <em>x<sub>1<\/sub><\/em> \u2261 &#8230;\u00a0<em>R<\/em> <em>x<sub>2n-1<\/sub><\/em> \u2261 <em>x<sub>2n<\/sub><\/em>\u00a0<em>R<\/em> <em>x<sub>2n+1<\/sub><\/em> <em>\u2261 x&#8217;<\/em>.<\/p>\n<p>The equilogical space <em>Z<\/em> = (<em>Y<\/em>, (\u2261 \u222a <em>R<\/em>)*) is, together with (the equivalence class of) the identity map from <em>Y<\/em> to <em>Z<\/em>, the coequalizer of <em>f<\/em> and <em>g<\/em> in <strong>Equ<\/strong>.\u00a0 The previous paragraph is the beginning of the argument that proves it.<\/p>\n<p>In <strong>Top<\/strong>, the coequalizers are the quotient maps.\u00a0 We do not take any topological quotients here!\u00a0 After all, this is why we took <em>formal<\/em> quotients instead of actual quotients as objects of <strong>Equ<\/strong>.<\/p>\n<p><strong>Coequalizers&#8230; and Cartesian closure.<\/strong><\/p>\n<p>In any category, any morphism that occurs as a coequalizer is necessarily epi, but the converse may fail. It is customary to call <em>regular epi<\/em> the maps that occur as coequalizers of some parallel pair of morphisms.\u00a0 In <strong>Top<\/strong>, the regular epis are exactly the quotient maps, while every surjective continuous map is epi.<\/p>\n<p>This leads us to Cartesian closure. It is category theoretic folklore that, in a Cartesian closed category, regular epis are closed under products with isos. That is, if <em>q<\/em> : <em>A<\/em> \u2192 <em>B<\/em> is a regular epi, then <em>q<\/em> x id<em><sub>C<\/sub><\/em> : <em>A<\/em> x <em>C<\/em> \u2192 <em>B<\/em> x <em>C<\/em> is also a regular epi. Indeed, _ x <em>C<\/em> is a left adjoint functor since <em>C<\/em> is exponential by Cartesian closure, left adjoints preserve colimits [see p.176], and coequalizers are special colimits.<\/p>\n<p>This is the deep reason behind Exercise 5.4.29. Oops, I just gave you a proof of it! And a much shorter one, too&#8230; Doing Exercise 5.4.29 is still interesting, and will help to get a better grasp of what is happening with topological spaces.<\/p>\n<p>In <strong>Equ<\/strong>, just like in <strong>Top<\/strong>, product with any object <em>C<\/em> also preserves coproducts.\u00a0 From the construction of coequalizers in <strong>Equ<\/strong>, we see that product with <em>C<\/em> in Equ preserves coequalizers, too.\u00a0 (This fails in <strong>Top<\/strong>.)\u00a0 It follows that product with <em>C<\/em> preserves all colimits.<\/p>\n<p>This is a necessary condition for the _ x <em>C<\/em> functor to be left adjoint, hence for <em>C<\/em> to be exponentiable. There is a handy theorem of category theory, Freyd&#8217;s <a title=\"General Adjoint Functor Theorem\" href=\"https:\/\/ncatlab.org\/nlab\/show\/adjoint+functor+theorem\">General Adjoint Functor Theorem<\/a>, which states that the functors <em>F<\/em> from a cocomplete category <strong><em>C<\/em><\/strong> to a category <strong><em>D<\/em><\/strong> that are left adjoints are exactly those which preserve all colimits and satisfy a so-called <em>solution set condition<\/em>. The latter is a bit subtle, and I don&#8217;t want to bother you with it.\u00a0 Be aware that if you follow the link above, you&#8217;ll have to reverse the direction of all arrows.<br \/>\nAnyway, all this means that we are just one step away from proving that <strong>Equ<\/strong> is Cartesian closed. Since the solution set condition is tricky, and eventually the General Adjoint Functor Theorem would give little information as to what exponentials look like, we follow the route that Bauer, Birkedal and Scott took.\u00a0 (By the way, Exercise 5.4.29 essentially asks you to prove Freyd&#8217;s theorem in the special case of the _ x <em>C<\/em> functor on <strong>Top<\/strong>.)<\/p>\n<p><strong>Algebraic complete lattices with PERs.<\/strong><\/p>\n<p>The argument by Bauer <em>et al. <\/em>that <strong>Equ<\/strong> is Cartesian closed goes through a brilliant construction: we build an equivalent category, which will easily be seen to be Cartesian closed. This is how Dana Scott came up with equilogical spaces in the first place, from what I understand.\u00a0 See Bauer <em>et al.<\/em> [2] for all missing details.<\/p>\n<p>The starting point of this construction is given in Proposition 9.3.5 of the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>. Let <strong>S<\/strong> be Sierpi\u0144ski space, <strong>O<\/strong><em>X<\/em> be the complete lattice of open subsets of <em>X<\/em>. If <em>X<\/em> is T<sub>0<\/sub>, then the map \u03b7<strong><sub>S<\/sub><\/strong> : <em>X<\/em> \u2192 <strong>S<\/strong><sup><strong>O<\/strong><em>X<\/em><\/sup>, defined by \u03b7<strong><sub>S<\/sub><\/strong>(x) = (\u03c7<em><sub>U<\/sub><\/em> (x))<em><sub>U<\/sub><\/em><sub> in <\/sub><sub>OX<\/sub> for every <em>x<\/em> in <em>X<\/em>, is an embedding. I called <strong>S<\/strong><sup><strong>O<\/strong><em>X<\/em><\/sup> the powerset construction, because it is isomorphic to the powerset <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) of <strong>O<\/strong><em>X<\/em>, with the Scott topology of the inclusion ordering. I will prefer the latter view of the powerset construction: then, \u03b7<strong><sub>S<\/sub><\/strong> : <em>X<\/em> \u2192 <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) maps <em>x<\/em> to the collection of open neighborhoods of <em>x<\/em>.<\/p>\n<p>Now, <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) has all sorts of nice properties. Notably, it is an algebraic complete lattice. The finite elements are just the finite sets of open subsets of <em>X<\/em>.<\/p>\n<p>If we start from an equilogical space (<em>X<\/em>, \u2261) instead of just a T<sub>0<\/sub> space <em>X<\/em>, this endows <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) with an additional structure: an equivalence relation on a subset of <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>). Indeed, we can equate <em>X<\/em> with a subspace of <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), and the equivalence relation \u2261 defines an equivalence relation on the corresponding subset.<\/p>\n<p>An equivalence relation on a subset of a set <em>X<\/em> is called a <em>partial equivalence relation<\/em> (<em>PER<\/em>) on <em>X<\/em>. I will usually write such relations as \u2243 instead of \u2261.<\/p>\n<p>PERs are usually defined in another way. This alternative definition is very simple and natural: a PER \u2243 on <em>X<\/em> is a symmetric transitive relation on <em>X<\/em>, which we do not require to be reflexive. Any equivalence relation \u2261 on a subset <em>A<\/em> of <em>X<\/em> yields a PER \u2243 (according to the new definition), defined by <em>x<\/em> \u2243 <em>y<\/em> if and only if <em>x<\/em> and <em>y<\/em> are both in <em>A<\/em> and x \u2261 <em>y<\/em>. Conversely, a PER \u2243 on <em>X<\/em> defines an equivalence relation on its <em>domain<\/em>, where the domain of \u2243 is by definition the set of points such that <em>x<\/em> \u2243 <em>x<\/em>. PERs are a classical tool in logic.<\/p>\n<p>Given an equilogical space (<em>X<\/em>, \u2261), (<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), \u2243) is an algebraic complete lattice with a PER on it, provided we define \u2243 by: the domain of \u2243 is Im \u03b7<strong><sub>S<\/sub><\/strong>, and \u03b7<strong><sub>S<\/sub><\/strong>(<em>x<\/em>) \u2243 \u03b7<strong><sub>S<\/sub><\/strong>(<em>x&#8217;<\/em>) if and only if <em>x \u2261<\/em> <em>x&#8217;<\/em>. In other words, identifying <em>X<\/em> with a subspace of <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), \u2243 is just the equivalence relation \u2261 on the subset <em>X<\/em>.<\/p>\n<p>Call <strong>PERCLat<\/strong> the category of algebraic complete lattices <em>L<\/em> with a PER \u2243 on it.\u00a0 (Bauer <em>et al.<\/em> call it <strong>PEqu<\/strong>, which I find a little confusing.)<\/p>\n<p>The morphisms are a bit subtle \u2014 again. Given two algebraic complete lattices with PERs (<em>L<\/em>, \u2243) and (<em>L<\/em>&#8216;, \u2243&#8217;), the dcpo [<em>L<\/em> \u2192 <em>L&#8217;<\/em>] of all continuous maps from <em>L<\/em> to <em>L&#8217;<\/em> is again an algebraic complete lattice. (This can be seen by using Exercise 5.7.18, which says that [<em>L<\/em> \u2192 <em>L&#8217;<\/em>] is a Scott domain, and one sees easily that also has a top element, hence that it is an algebraic complete lattice.)<br \/>\nOne may define a PER \u2245 on [<em>L<\/em> \u2192 <em>L&#8217;<\/em>] by <em>f<\/em> \u2245 <em>f&#8217;<\/em> if and only if, for every pair of elements <em>x<\/em>, <em>x&#8217;<\/em> in <em>L<\/em> such that <em>x<\/em> \u2243 <em>x<\/em>&#8216;, we have <em>f<\/em>(<em>x<\/em>) \u2243&#8217; <em>f&#8217;<\/em>(<em>x&#8217;<\/em>). The domain of this PER is, by definition, the set of <em>equivariant<\/em> maps from <em>L<\/em> to <em>L&#8217;<\/em>; a continuous map <em>f<\/em> from <em>L<\/em> to <em>L&#8217;<\/em> is equivariant if and only if <em>f<\/em>(<em>x<\/em>) \u2243&#8217; <em>f<\/em>(<em>x&#8217;<\/em>) whenever <em>x<\/em> \u2243 <em>x<\/em>&#8216;. Now, the morphisms from <em>L<\/em> to <em>L&#8217;<\/em> are the equivalence classes of equivariant maps, modulo \u2245.<\/p>\n<p>Of course, we have just lifted the whole notion of morphisms in <strong>Equ<\/strong> to <strong>PERCLat<\/strong> through \u03b7<strong><sub>S<\/sub><\/strong>. One can show that the two categories <strong>Equ<\/strong> and <strong>PERCLat<\/strong> are equivalent.\u00a0 (I will relegate the argument in an appendix), and that the latter is Cartesian closed.<br \/>\nThe latter is a simple extension of the fact that the category of algebraic complete lattices is Cartesian closed: the exponential object from (<em>L<\/em>, \u2243) to (<em>L<\/em>&#8216;, \u2243&#8217;) in <strong>PERCLat<\/strong> is ([<em>L<\/em> \u2192 <em>L&#8217;<\/em>], \u2245), where \u2245 was just defined.<\/p>\n<p>It follows that <strong>Equ<\/strong> is Cartesian closed, too.<\/p>\n<p>So what does the exponential object from (<em>X<\/em>, \u2261) to (<em>Y<\/em>, \u2261&#8217;) look like in <strong>Equ<\/strong>? We find the equivalent objects in <strong>PERCLat<\/strong>, and these are (<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), \u2243) and (<strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>), \u2243&#8217;) , where \u2243 is defined from \u2261 and \u2243&#8217; is defined from \u2261&#8217; in the usual way. The exponential object from (<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), \u2243) to (<strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>), \u2243&#8217;) in <strong>PERCLat<\/strong> is ([<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) \u2192 <strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>)], \u2245), where \u2245 is defined as above: <em>f<\/em> \u2245 <em>f&#8217;<\/em> if and only if, for every pair of elements <em>A<\/em>, <em>A&#8217;<\/em> in <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) such that <em>A<\/em> \u2243 <em>A<\/em>&#8216;, we have <em>f<\/em>(<em>A<\/em>) \u2243&#8217; <em>f&#8217;<\/em>(<em>A&#8217;<\/em>).\u00a0 Going back to <strong>Equ<\/strong>, the exponential object (<em>Y<\/em>, \u2261&#8217;)<sup>(X, \u2261)<\/sup> is then (dom \u2245, \u2245), where dom \u2245 is equipped with the subspace topology induced from the Scott topology on [<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) \u2192 <strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>)]. There does not seem to be any simpler description of it, as far as I know.\u00a0 Might this be related to the Isbell topology, for example?\u00a0 I do not know, and I have been too lazy to check it out.<\/p>\n<p>Application App : (<em>Y<\/em>, \u2261&#8217;)<sup>(X, \u2261)<\/sup> x (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261&#8217;) is (the equivalence class of) the map that sends an \u2245-equivariant continuous map <em>f<\/em> in [<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) \u2192 <strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>)] and <em>x<\/em> in <em>X<\/em> to <em>f<\/em>(\u03b7<strong><sub>S<\/sub><\/strong>(<em>x<\/em>)) \u2014 or rather, to the unique point <em>y<\/em> in <em>Y<\/em> such that \u03b7<strong><sub>S<\/sub><\/strong>(<em><em>y<\/em><\/em>)<em> = f<\/em>(\u03b7<strong><sub>S<\/sub><\/strong>(<em>x<\/em>)).<\/p>\n<p>The currification \u039b(<em>f<\/em>) of <em>f<\/em> : (<em>Z<\/em>, \u223c) x (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261&#8217;) is (the equivalence class of) the map that sends <em>z<\/em> in <em>Z<\/em> to (the equivalence class of) <strong>P<\/strong>(<strong>O<\/strong> (<em>f<\/em> (<em>z<\/em>, _))).\u00a0 The latter rather barbaric notation (see appendix) stands for the equivariant continuous map from <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) to <strong>P<\/strong>(<strong>O<\/strong><em>Y<\/em>) that sends each set <em>A<\/em> of open subsets of <em>X<\/em> to the family of open subsets <em>V<\/em> of <em>Y<\/em> such that {<em>x<\/em> in <em>X<\/em> | <em><em>f<\/em> <\/em>(<em><em>z<\/em>, x<\/em>) in <em>V<\/em>} is in <em>A<\/em>.\u00a0 Gasp.\u00a0 At least it all works out.<\/p>\n<p><strong>Filter spaces.<\/strong><\/p>\n<p>We now have two rather different families of Cartesian closed categories that contain <strong>Top<\/strong><sub>0<\/sub>: <strong>Equ<\/strong>, which was the topic of this post&#8230; and filter spaces, which were the topic of <a title=\"Filters, part II: filter spaces\" href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=283\">Filters II<\/a>.\u00a0 Is there any connection between the two kinds?<\/p>\n<p>This question was solved by Reinhold Heckmann [3].\u00a0 I&#8217;ll talk about this in a later post.\u00a0 There you&#8217;ll notice that Heckmann introduces a new, even fancier category of so-called assemblies over algebraic complete lattices.\u00a0 Those generalize our complete algebraic lattices with PERs in such a way that the new category contains not just the T<sub>0<\/sub> spaces, but all of <strong>Top<\/strong>.<\/p>\n<p style=\"text-align: right;\">\u2014 <a href=\"https:\/\/www.lsv.ens-paris-saclay.fr\/~goubault\/?l=en\" rel=\"attachment wp-att-993\">Jean Goubault-Larrecq<\/a>\u00a0(July 30th, 2014<img loading=\"lazy\" decoding=\"async\" class=\"wp-image-993 alignright\" src=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/wp-content\/uploads\/2016\/08\/jgl-2011.png\" alt=\"jgl-2011\" width=\"32\" height=\"44\" \/><\/p>\n<p>[1] Dana S. Scott. <em>Data types as lattices<\/em>. <a title=\"Data types as lattices\" href=\"https:\/\/www.cs.ox.ac.uk\/files\/3287\/PRG05.pdf\">Technical Monograph PRG-5<\/a>, Oxford University Computing Laboratory, 1976.<\/p>\n<p>[2] Andrej Bauer, Lars Birkedal, and Dana S. Scott. <em>Equilogical Spaces<\/em>. Theoretical Computer Science 315(1), 5 May 2004, 35-59. (Submitted as early as 1998, as far as I know.)<\/p>\n<p>[3]\u00a0 Reinhold Heckmann.\u00a0 <em>On the Relationship between Filter Spaces and Equilogical Spaces<\/em>.\u00a0 1998.\u00a0 Available <a title=\"On the Relationship between Filter Spaces and Equilogical Spaces\" href=\"https:\/\/rw4.cs.uni-sb.de\/~heckmann\/papers\/fil.ps.gz\">on the Web<\/a>.<\/p>\n<p><strong>Appendix: Equ and PERCLat are equivalent categories.<\/strong><\/p>\n<p>There is a functor <em>F<\/em> : <strong>Equ<\/strong> \u2192 <strong>PERCLat<\/strong>, which maps the equilogical space (<em>X<\/em>, \u2261) to the algebraic complete lattice with PER (<strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>), \u2243), where \u2243 is the PER which we have already mentioned: the domain of \u2243 is Im \u03b7<strong><sub>S<\/sub><\/strong>, and \u03b7<strong><sub>S<\/sub><\/strong>(<em>x<\/em>) \u2243 \u03b7<strong><sub>S<\/sub><\/strong>(<em>x&#8217;<\/em>) if and only if <em>x \u2261<\/em> <em>x&#8217;<\/em>. Given a morphism of equilogical spaces <em>f<\/em> : (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261), there is a Scott continuous map <strong>P<\/strong>(<strong>O<\/strong><em>f<\/em>) : <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) <strong>\u2192 P<\/strong>(<strong>O<\/strong><em>Y<\/em>), defined as mapping a set A of open subsets of <em>X<\/em> to <em>f<\/em>[<em>A<\/em>] = {<em>U<\/em> open | <em>f<\/em><sup>-1<\/sup>(<em>U<\/em>) is in <em>A<\/em>}. (Yes, this is the same formula as for the image filter. This is certainly no accident.) This map is equivariant, just because <em>f<\/em> respects the equivalence relation \u2261. The functor <em>F<\/em> maps <em>f<\/em> : (<em>X<\/em>, \u2261) \u2192 (<em>Y<\/em>, \u2261) to the equivalence class of <strong>P<\/strong>(<strong>O<\/strong><em>f<\/em>).<\/p>\n<p>Conversely, there is a functor <em>G<\/em> : <strong>PERCLat<\/strong> \u2192 <strong>Equ<\/strong>, which maps any algebraic complete lattice with a PER (<em>L<\/em>, \u2243) to the equilogical space (dom \u2243, \u2243). Here dom \u2243 is the domain of \u2243, seen as a subspace of <em>L<\/em>, where <em>L<\/em> has the Scott topology; and in (dom \u2243, \u2243), the second component \u2243 is shorthand for the restriction of \u2243 to dom \u2243 (an equivalence relation). Given any equivariant map <em>f<\/em> : (<em>L<\/em>, \u2243) \u2192 (<em>L<\/em>&#8216;, \u2243&#8217;), <em>f<\/em> restricts to a continuous map from (dom \u2243, \u2243) to (dom \u2243&#8217;, \u2243&#8217;), as a consequence of equivariance. Moreover, any two equivalent equivariant maps <em>f<\/em>, <em>f&#8217;<\/em> : (<em>L<\/em>, \u2243) \u2192 (<em>L<\/em>&#8216;, \u2243&#8217;) define the same restriction to (dom \u2243, \u2243). This is an immediate consequence of the definition of \u2245 on [<em>L<\/em> \u2192 <em>L&#8217;<\/em>].<\/p>\n<p>One can check that <em>F<\/em> and <em>G<\/em> define an equivalence of categories. The embedding \u03b7<strong><sub>S<\/sub><\/strong> : <em>X<\/em> \u2192 <strong>P<\/strong>(<strong>O<\/strong><em>X<\/em>) defines an isomorphism between (<em>X<\/em>, \u2261) and <em>G<\/em> o <em>F<\/em> (<em>X<\/em>, \u2261), and it is natural in <em>X<\/em>. Conversely, the fact that <em>F<\/em> o <em>G<\/em> (<em>L<\/em>, \u2243) is naturally isomorphic to (<em>L<\/em>, \u2243) is a bit more surprising.\u00a0 Bauer <em>et al.<\/em> [2] say that this is directly from the definition.\u00a0 I&#8217;ll let you do the exercise.\u00a0 Once you&#8217;ve done all the checking (but no sooner), you&#8217;ll realize Bauer <em>et al.<\/em> are right.\u00a0 Oh, by the way, do not forget that morphisms are <em>equivalence classes<\/em> of continuous maps.\u00a0 This is crucial: to show that <em>f<\/em> o <em>g<\/em> is an identity morphism in <strong>Equ<\/strong> or in <strong>PERCLat<\/strong>, it is enough to show that it maps every element <em>x<\/em>, not to <em>x<\/em> itself, but to an equivalent element.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>A few weeks ago, I went to the Semantics of Proofs and Programs workshop at the Institut Henri Poincar\u00e9 in Paris. There were many fascinating talks there, and the workshop was very enjoyable. At some point, Giuseppe Rosolini mentioned Dana &hellip; <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=428\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"open","ping_status":"open","template":"","meta":{"_crdt_document":"","footnotes":""},"class_list":["post-428","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/428","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=428"}],"version-history":[{"count":32,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/428\/revisions"}],"predecessor-version":[{"id":5964,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/428\/revisions\/5964"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=428"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}