A few weeks ago, I went to the Semantics of Proofs and Programs workshop at the Institut Henri Poincaré in Paris. There were many fascinating talks there, and the workshop was very enjoyable.
At some point, Giuseppe Rosolini mentioned Dana Scott‘s equilogical spaces. I had loved this construction since I’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.
Equilogical spaces.
The categorical of equilogical spaces is a very natural category, and it is Cartesian closed (and a bit more). Here is the definition:
- An equilogical space is a pair (X, ≡) where X is a T0 space and ≡ is an equivalence relation on X.
I will almost always write ≡ for the ambient equivalence relation, irrespective of the space we are in.
You may think of (X, ≡) as saying we really wish to contemplate the quotient X/≡, but we do not really carry out any quotienting. Similarly to formal balls, we might call these objects formal quotients.
- It is tempting to define a morphism of equilogical spaces f : (X, ≡) → (Y, ≡) as a continuous map f from X to Y. It is only sensible to require f to be equivariant, namely to be such that if x≡x’ then f(x)≡f(x’).
However, in the formal quotient interpretation, you would not like to distinguish between two equivariant continuous maps f, f’ : X → Y that map every element to distinct but equivalent elements.
In other words, say that two maps f, f’ : X → Y are equivalent if and only if, for every x in X, f(x)≡f’(x).
We then define the morphisms of equilogical spaces from (X, ≡) to (Y, ≡) as those equivalence classes of equivariant continuous maps from X to Y. I will usually do as if morphisms were equivariant continuous maps, but I’ll have to remind you that these morphisms are understood modulo equivalence, from time to time.
That is it! Let us write Equ for the resulting category, of equilogical spaces and equivalence classes of equivariant continuous maps. At first sight, Equ is very close to Top0, the category of T0 topological spaces, and I would not have been surprised to learn that they are equivalent… but they are not, since one is Cartesian-closed and the other is not.
Equ is a larger category than Top0, in the following sense. Top0 embeds into Equ through the functor Inj that maps every topological space X to (X, =), and every continuous map f : X → Y to the (one-element) equivalence class of f.
Conversely, there is a functor Q : Equ → Top0 that maps every formal quotient (X, ≡) to the actual quotient space X/≡. The composition Q o Inj is the identity, and there is natural transformation from the identity functor on Equ to Inj o Q (at object (X, ≡), it maps x in X to its equivalence class modulo ≡). Putting all this together, Inj is right adjoint to Q, so, equating Top0 with its image in Equ, we see that Top0 is a reflective subcategory of Equ (see p.183).
Limits, colimits.
Equ has all products. The product ∏i in I (Xi, ≡i) is the obvious one, (∏i in I Xi, ≡), where ≡ is the equivalence relation defined by: (xi)i in I ≡ (x’i)i in I if and only if xi ≡i x’i for every i in I.
Equ has all equalizers, too. The equalizer of f, g : (X, ≡) → (Y, ≡) is the subspace [f≡g] of X of those points x such that f(x)≡g(x), with equivalence relation the restriction of that of (X, ≡) to the subset [f=g]. In general, the equalizers in Equ are the ≡-satured subspaces, with the obvious definition of subspace (a topological subspace with the restriction of the equivalence relation); ≡-saturated means that any element that is ≡-equivalent to one of the subspace is also in the subspace.
Since Equ has all products and all equalizers, it is complete.
Equ also has all coproducts, and they are also the obvious ones. The coproduct ∐i in I (Xi, ≡i) is the obvious one, (∐i in I Xi, ≡), where ≡ is the equivalence relation defined by: (i, x) ≡ (i’, x’) if and only if i=i’ and x ≡i x’.
The main difference with Top is with coequalizers. In Top, the coequalizers are the quotient maps. The coequalizers are rather different in Equ. We build them now. As a consequence, Equ will be cocomplete.
Coequalizers.
A coequalizer of f, g : (X, ≡) → (Y, ≡) in Equ is by definition an (equivalence class) of equivariant continuous maps h : (Y, ≡) → Z for some equilogical space Z, such that h o f = h o g (up to equivalence), and which is universal with this property.
A good candidate for h and Z is as follows. Let R be the symmetric relation on Y defined by y R y’ if and only if y=f(x) and y’=g(x) for some x in X. If h exists, then h(y)≡h(y’) for every pair y, y’ in Y with y R y’. It follows that the same relation holds for every pair y, y’ in Y such that y (≡ ∪ R)* y’. The relation (≡ ∪ R)* is the reflexive transitive closure of the union of the two relations. In other words, x (≡ ∪ R)* x’ if and only if there are 2n+1 points, for some natural number n, x0, x1, …, x2n+1, such that x ≡ x0 R x1 ≡ … R x2n-1 ≡ x2n R x2n+1 ≡ x’.
The equilogical space Z = (Y, (≡ ∪ R)*) is, together with (the equivalence class of) the identity map from Y to Z, the coequalizer of f and g in Equ. The previous paragraph is the beginning of the argument that proves it.
In Top, the coequalizers are the quotient maps. We do not take any topological quotients here! After all, this is why we took formal quotients instead of actual quotients as objects of Equ.
Coequalizers… and Cartesian closure.
In any category, any morphism that occurs as a coequalizer is necessarily epi, but the converse may fail. It is customary to call regular epi the maps that occur as coequalizers of some parallel pair of morphisms. In Top, the regular epis are exactly the quotient maps, while every surjective continuous map is epi.
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 q : A → B is a regular epi, then q x idC : A x C → B x C is also a regular epi. Indeed, _ x C is a left adjoint functor since C is exponential by Cartesian closure, left adjoints preserve colimits [see p.176], and coequalizers are special colimits.
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… Doing Exercise 5.4.29 is still interesting, and will help to get a better grasp of what is happening with topological spaces.
In Equ, just like in Top, product with any object C also preserves coproducts. From the construction of coequalizers in Equ, we see that product with C in Equ preserves coequalizers, too. (This fails in Top.) It follows that product with C preserves all colimits.
This is a necessary condition for the _ x C functor to be left adjoint, hence for C to be exponentiable. There is a handy theorem of category theory, Freyd’s General Adjoint Functor Theorem, which states that the functors F from a cocomplete category C to a category D that are left adjoints are exactly those which preserve all colimits and satisfy a so-called solution set condition. The latter is a bit subtle, and I don’t want to bother you with it. Be aware that if you follow the link above, you’ll have to reverse the direction of all arrows.
Anyway, all this means that we are just one step away from proving that Equ 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. (By the way, Exercise 5.4.29 essentially asks you to prove Freyd’s theorem in the special case of the _ x C functor on Top.)
Algebraic complete lattices with PERs.
The argument by Bauer et al. that Equ 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. See Bauer et al. [2] for all missing details.
The starting point of this construction is given in Proposition 9.3.5 of the book. Let S be Sierpiński space, OX be the complete lattice of open subsets of X. If X is T0, then the map ηS : X → SOX, defined by ηS(x) = (χU (x))U in OX for every x in X, is an embedding. I called SOX the powerset construction, because it is isomorphic to the powerset P(OX) of OX, with the Scott topology of the inclusion ordering. I will prefer the latter view of the powerset construction: then, ηS : X → P(OX) maps x to the collection of open neighborhoods of x.
Now, P(OX) 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 X.
If we start from an equilogical space (X, ≡) instead of just a T0 space X, this endows P(OX) with an additional structure: an equivalence relation on a subset of P(OX). Indeed, we can equate X with a subspace of P(OX), and the equivalence relation ≡ defines an equivalence relation on the corresponding subset.
An equivalence relation on a subset of a set X is called a partial equivalence relation (PER) on X. I will usually write such relations as ≃ instead of ≡.
PERs are usually defined in another way. This alternative definition is very simple and natural: a PER ≃ on X is a symmetric transitive relation on X, which we do not require to be reflexive. Any equivalence relation ≡ on a subset A of X yields a PER ≃ (according to the new definition), defined by x ≃ y if and only if x and y are both in A and x ≡ y. Conversely, a PER ≃ on X defines an equivalence relation on its domain, where the domain of ≃ is by definition the set of points such that x ≃ x. PERs are a classical tool in logic.
Given an equilogical space (X, ≡), (P(OX), ≃) is an algebraic complete lattice with a PER on it, provided we define ≃ by: the domain of ≃ is Im ηS, and ηS(x) ≃ ηS(x’) if and only if x ≡ x’. In other words, identifying X with a subspace of P(OX), ≃ is just the equivalence relation ≡ on the subset X.
Call PERCLat the category of algebraic complete lattices L with a PER ≃ on it. (Bauer et al. call it PEqu, which I find a little confusing.)
The morphisms are a bit subtle — again. Given two algebraic complete lattices with PERs (L, ≃) and (L‘, ≃’), the dcpo [L → L’] of all continuous maps from L to L’ is again an algebraic complete lattice. (This can be seen by using Exercise 5.7.18, which says that [L → L’] is a Scott domain, and one sees easily that also has a top element, hence that it is an algebraic complete lattice.)
One may define a PER ≅ on [L → L’] by f ≅ f’ if and only if, for every pair of elements x, x’ in L such that x ≃ x‘, we have f(x) ≃’ f’(x’). The domain of this PER is, by definition, the set of equivariant maps from L to L’; a continuous map f from L to L’ is equivariant if and only if f(x) ≃’ f(x’) whenever x ≃ x‘. Now, the morphisms from L to L’ are the equivalence classes of equivariant maps, modulo ≅.
Of course, we have just lifted the whole notion of morphisms in Equ to PERCLat through ηS. One can show that the two categories Equ and PERCLat are equivalent. (I will relegate the argument in an appendix), and that the latter is Cartesian closed.
The latter is a simple extension of the fact that the category of algebraic complete lattices is Cartesian closed: the exponential object from (L, ≃) to (L‘, ≃’) in PERCLat is ([L → L’], ≅), where ≅ was just defined.
It follows that Equ is Cartesian closed, too.
So what does the exponential object from (X, ≡) to (Y, ≡’) look like in Equ? We find the equivalent objects in PERCLat, and these are (P(OX), ≃) and (P(OY), ≃’) , where ≃ is defined from ≡ and ≃’ is defined from ≡’ in the usual way. The exponential object from (P(OX), ≃) to (P(OY), ≃’) in PERCLat is ([P(OX) → P(OY)], ≅), where ≅ is defined as above: f ≅ f’ if and only if, for every pair of elements A, A’ in P(OX) such that A ≃ A‘, we have f(A) ≃’ f’(A’). Going back to Equ, the exponential object (Y, ≡’)(X, ≡) is then (dom ≅, ≅), where dom ≅ is equipped with the subspace topology induced from the Scott topology on [P(OX) → P(OY)]. There does not seem to be any simpler description of it, as far as I know. Might this be related to the Isbell topology, for example? I do not know, and I have been too lazy to check it out.
Application App : (Y, ≡’)(X, ≡) x (X, ≡) → (Y, ≡’) is (the equivalence class of) the map that sends an ≅-equivariant continuous map f in [P(OX) → P(OY)] and x in X to f(ηS(x)) — or rather, to the unique point y in Y such that ηS(y) = f(ηS(x)).
The currification Λ(f) of f : (Z, ∼) x (X, ≡) → (Y, ≡’) is (the equivalence class of) the map that sends z in Z to (the equivalence class of) P(O (f (z, _))). The latter rather barbaric notation (see appendix) stands for the equivariant continuous map from P(OX) to P(OY) that sends each set A of open subsets of X to the family of open subsets V of Y such that {x in X | f (z, x) in V} is in A. Gasp. At least it all works out.
Filter spaces.
We now have two rather different families of Cartesian closed categories that contain Top0: Equ, which was the topic of this post… and filter spaces, which were the topic of Filters II. Is there any connection between the two kinds?
This question was solved by Reinhold Heckmann [3]. I’ll talk about this in a later post. There you’ll notice that Heckmann introduces a new, even fancier category of so-called assemblies over algebraic complete lattices. Those generalize our complete algebraic lattices with PERs in such a way that the new category contains not just the T0 spaces, but all of Top.
— Jean Goubault-Larrecq (July 30th, 2014
[1] Dana S. Scott. Data types as lattices. Technical Monograph PRG-5, Oxford University Computing Laboratory, 1976.
[2] Andrej Bauer, Lars Birkedal, and Dana S. Scott. Equilogical Spaces. Theoretical Computer Science 315(1), 5 May 2004, 35-59. (Submitted as early as 1998, as far as I know.)
[3] Reinhold Heckmann. On the Relationship between Filter Spaces and Equilogical Spaces. 1998. Available on the Web.
Appendix: Equ and PERCLat are equivalent categories.
There is a functor F : Equ → PERCLat, which maps the equilogical space (X, ≡) to the algebraic complete lattice with PER (P(OX), ≃), where ≃ is the PER which we have already mentioned: the domain of ≃ is Im ηS, and ηS(x) ≃ ηS(x’) if and only if x ≡ x’. Given a morphism of equilogical spaces f : (X, ≡) → (Y, ≡), there is a Scott continuous map P(Of) : P(OX) → P(OY), defined as mapping a set A of open subsets of X to f[A] = {U open | f-1(U) is in A}. (Yes, this is the same formula as for the image filter. This is certainly no accident.) This map is equivariant, just because f respects the equivalence relation ≡. The functor F maps f : (X, ≡) → (Y, ≡) to the equivalence class of P(Of).
Conversely, there is a functor G : PERCLat → Equ, which maps any algebraic complete lattice with a PER (L, ≃) to the equilogical space (dom ≃, ≃). Here dom ≃ is the domain of ≃, seen as a subspace of L, where L has the Scott topology; and in (dom ≃, ≃), the second component ≃ is shorthand for the restriction of ≃ to dom ≃ (an equivalence relation). Given any equivariant map f : (L, ≃) → (L‘, ≃’), f restricts to a continuous map from (dom ≃, ≃) to (dom ≃’, ≃’), as a consequence of equivariance. Moreover, any two equivalent equivariant maps f, f’ : (L, ≃) → (L‘, ≃’) define the same restriction to (dom ≃, ≃). This is an immediate consequence of the definition of ≅ on [L → L’].
One can check that F and G define an equivalence of categories. The embedding ηS : X → P(OX) defines an isomorphism between (X, ≡) and G o F (X, ≡), and it is natural in X. Conversely, the fact that F o G (L, ≃) is naturally isomorphic to (L, ≃) is a bit more surprising. Bauer et al. [2] say that this is directly from the definition. I’ll let you do the exercise. Once you’ve done all the checking (but no sooner), you’ll realize Bauer et al. are right. Oh, by the way, do not forget that morphisms are equivalence classes of continuous maps. This is crucial: to show that f o g is an identity morphism in Equ or in PERCLat, it is enough to show that it maps every element x, not to x itself, but to an equivalent element.