Prestreams and d-spaces

Let me make an incursion into the realm of directed algebraic topology. I will not talk about the algebraic topological part per se, merely about an apparently silly question: how to best model topological spaces with a notion of direction (of time, if you will) on it?

There are numerous applications. The one I know best is from concurrency theory [1]. For example, imagine you have two processes running concurrently. Each one has a local notion of time, which you may think as a real number between 0 and 1. Then the space of configurations of those two processes is [0,1]². The initial configuration is (0,0), and the final configuration is (1,1). Naturally, [0,1]² is a topological space, but it also has a natural direction of time, which one can model as the pointwise ordering on [0,1]². Processes can only go forward in time, and therefore the trajectories which we are interested in are not just any path on [0,1]², but monotonic paths. A path on a topological space X is a continuous map γ : [0,1] → X (here and everywhere in this post, [0,1] will have its metric topology, certainly not its Scott topology) and we are interested in those that are also monotonic.

There are other applications. One that is often cited is general relativity [2], although I cannot say much about it.

Anyway, what should be a model for topological spaces with a direction of time? Obviously that should be a topological space with an ordering on it, right? Or perhaps a pospace (see Definition 9.1.11 in the book), namely a topological space with a compatible ordering, where compatible means that the graph of the ordering is closed in the product topology.

Yes, of course… but we would also like to be able to model looping behaviors, such as the following directed circle:

Topologically, this should be just the usual circle. But time is meant to advance counterclockwise, and that is not an ordering. In fact, if you try to model this as a preordering, you will soon discover that every point is less than or equal to any other point, which is definitely not what you want.

One may model the desired notion of direction of time on the directed circle by a cyclic order. That is a ternary relation of betweenness between points. I will not consider this here, as directed algebraic topology also needs to consider more complicated spaces, including directed spheres, directed tori, and so on. There are many models for that kind of thing: cubical sets and precubical sets, Lisbeth Fajstrup, Eric Goubault, and Martin Raussen’s notion of local pospace, Krzysztof Ziemiański’s order simplicial complexes, Philippe Gaucher’s flows, Marco Grandis’ inequilogical spaces, etc. I would like to concentrate on two, apparently very different models: Marco Grandis’ d-spaces [3], and Sanjeevi Krishnan’s prestreams [4]. The topic of the latter paper is really about streams, but prestreams are simpler, and I will address streams another time.

Emmanuel Haucourt discovered that there is an adjunction between the categories dTop of d-spaces and the category PreStr of streams [5], and it which is idempotent. I would like to give an idea of how all that is defined and works. This adjunction is also one between dTop and the subcategory Str of streams, which in my opinion is more interesting than PreStr, but, as I said, this will be for another time.

Grandis’ d-spaces

A very simple model of directed spaces was introduced by Marco Grandis in [3]. It is probably the one that is used most often today. This is just a topological space with an collection of paths, satisfying some elementary axioms.

Let me recall that a path on a topological space X is just a continuous map γ : [0,1] → X. We say that it is a path from γ(0) to γ(1). I will always equip [0,1] with its usual metric topology; not its Scott topology, remember.

You may imagine drawing the set of points γ(t), 0≤t≤1, on a piece of paper, and this will give you the picture of a curve inside the space X. However, you should keep in mind that a path is not just a space of points on a curve, but also a parametrization of this curve: we know which point is obtained when t=0, which is obtained when t=1, and also at all other possible values of t.

A reparametrization of a path γ is any path of the form γ o φ, where φ is a monotonic, continuous map from [0,1] to [0,1]. Clearly, γ and γ o φ define the same curve, but with different parametrizations. Note that we do not require φ to be bijective. In particular, φ may decide to be constant on some subintervals of [0,1]; φ may also fail to be surjective, so that, for example, γ composed with the map t ↦ 1/3+1/6.t is a reparametrization of γ, which serves as the subpath of γ from γ(1/3) to γ(1/2).
The concatenation γ₁;γ₂ of two paths γ₁ : [0,1] → X and γ₂ : [0,1] → X is only defined if the final endpoint γ₁(1) of γ₁ coincides with the initial endpoint γ₂(0) of γ₂, and is the function that maps every t in the first half [0,½] of the interval [0,1] to γ₁(2t), and every t in the second half, [½,1], to γ₂(2t–1). This is what you would expect: follow the path γ₁ then γ₂. The concatenation is defined with a somewhat arbitrary parametrization; we might decide to follow γ₁ from 0 to 1/3 and γ₂ from 1/3 to 1 instead, for example, but that does not matter, because one can reparametrize. (Side story: concatenation, as we have defined it, is not associative. Why? However, taking paths up to the smallest equivalence relation that equates paths with their reparametrizations, concatenation is associative on equivalence classes. This will be unimportant in the rest of this post, but you may want to know.)

A d-space is a pair (X, dX), where X is a topological space, and dX is a collection of paths on X, called the d-paths, such that:

dX is closed under reparametrization: for every d-path γ in dX, all its reparametrizations γ o φ are in dX;
dX is closed under concatenation: for any two d-paths γ₁ and γ₂ in dX such that γ₁;γ₂ is defined, γ₁;γ₂ is a d-path in dX;
dX contains all the constant paths, namely all the constant maps from [0,1] to X.

Examples of d-spaces

Here are a few examples:

The directed circle is just the set of complex numbers of modulus 1, namely the numbers of the form e^iθ, θ ∈ R, with the subspace topology induced by the inclusion in C. The directed paths are exactly the maps t ↦ e^iφ(t), where φ is any monotonic, continuous map from [0,1] to R.
The standard directed line segment I^→ is [0,1], with its usual topology, and whose directed paths are exactly the monotonic continuous maps φ from [0,1] to [0,1].
Every topological space can be given the discrete d-path structure, where every path whatsoever is considered to be a d-path.
Every topological space can be given the indiscrete d-path structure, where the only d-paths are the constant paths.
The product of two d-spaces (X, dX) and (Y, dY) is the space X × Y, together with the collection of paths γ : [0,1] → X × Y such that π₁ o γ is a d-path in X (an element of dX) and π₂ o γ is a d-path in Y (an element of dY), where π₁ and π₂ are first and second projections, respectively. This is product in the category dTop of d-spaces (see below).
The staircase product of (X, dX) and (Y, dY) is also X × Y, with the smallest collection of d-paths formed from constants paths, horizontal d-paths (paths of the form t ↦ (γ(t),y) where γ ∈ dX and y ∈ Y), vertical d-paths (paths of the form t ↦ (x,γ(t)) where x ∈ X and γ ∈ dX), and closed under concatenation and reparametrization. All the d-paths in the staircase product are d-paths in the product, but the converse is wrong: the d-paths in the staircase product are finite concatenations of bits of d-paths going up and of d-paths going right, but no curvy or diagonal d-paths of the product is in the staircase product.

The category dTop of d-spaces

There is a category dTop of d-spaces. Its morphisms f : (X, dX) → (Y, dY) are the continuous maps f : X → Y that map d-paths to d-paths, namely such that for every γ ∈ dX, f o γ ∈ dY.

The category dTop is complete. We have described the binary products above. General products are defined similarly. The pullback of two morphisms of d-spaces f : (X, dX) → (Z, dZ) and g : (Y, dY) → (Z, dZ) is given by their topological pullback, namely the set {(x,y) | x ∈ X, y ∈ Y, f(x)=g(y)} with the subspace topology induced from X × Y, and the d-paths in that pullback are just the d-paths in the product X × Y that remain inside {(x,y) | x ∈ X, y ∈ Y, f(x)=g(y)}.

The category dTop is also cocomplete. Coproducts are very easy to build, and I will leave them to you as an exercise. You can build general colimits as quotients of (wide) coproducts. The quotient of a d-space (X, dX) by an equivalence relation ≡ on X is the topological quotient X/≡, with a slightly complicated collection of d-paths. The easiest way to describe it is as follows. There is a (continuous) quotient map q : X → X/≡, and d(X/≡) is the collection of (reparametrizations of) finite concatenations of paths of the form q o γ, where γ ranges over dX. In other words, a d-path from q(x) to q(y) in X/≡ is given by n d-paths in X, from x₁ to y₁, from x₂ to y₂, …, from x_n to y_n respectively, and such that x≡x₁, y₁≡x₂, y₂≡x₃, …, y_n≡y.

There is a general categorical reason why dTop is both complete and cocomplete, and why limits and colimits are computed as they are: the forgetful functor from dTop to Top is topological. This is an amazing notion, which I may decide to talk about some time. In the meantime, have a look at [6], Sections 21 and 22, if you are interested.

Prestreams

Streams are another model of directed topological spaces, proposed by Sanjeevi Krishnan [4]. If you are into sheaf theory, you will find them very natural: they are essentially cosheaves of preordered sets. If you are not, you may have a hard time understanding them at first sight.

Let me recommend my own paper [7] on the subject, and let me apologize for any apparent boasting from my part; I have spent some time in writing [7] to try and explain what prestreams and streams are, how you compute limits and colimits in the corresponding categories, and so on. (Oh, by the way, there were two mistakes in the published version of the paper, so be sure to download the HAL version. That version also states explicitly where and what those mistakes were.)

Since streams are complicated, we will concentrate on the simpler notion of prestreams here. Streams are just certain particular prestreams.

A prestream is a pair (X, (⊑_U)_{U ∈ OX}) consisting of a topological space X and a precirculation, namely a collection of preorderings ⊑_U on U, one for each open subset U of X. (I write OX for the lattice of open subsets of X.) We also require the following monotonicity property:

If U ⊆ V, then for all points x, y of U such that x ⊑_U y, we also have x ⊑_V y.

The preorderings ⊑_U encode directions of time that are local to U, for each open set U. Let us consider the directed circle again:

First look at a small open set U, such as the open segment of arc ]A, B[ shown in bold between points A and B. On that small open set U, you would like ⊑_U to be the ordering depicted by the arrow: x ⊑_U y if and only if one can go from x to y, between A and B, by traveling counterclockwise.

This works similarly for all the other open segments in bold, with arrows on their sides.

However, if X is the whole circle S₁^→, the monotonicity requirement implies that ⊑_X contains all the preorderings ⊑_U, where U ranges over all the arc segments, such as ]A, B[. This implies that any point x must be lower in the ⊑_X preordering than any point y that you can reach by traveling counterclockwise… but this is the case for all points y. So ⊑_X must be the trivial preordering that declares every point less than or equal to any point.

Examples of prestreams

Let me give a few other examples of prestreams.

First, the actual definition of the directed circle, as a prestream S₁^→: this is the space of complex numbers of modulus 1, namely the numbers of the form e^iθ, θ ∈ R, with the subspace topology induced by the inclusion in C, as in the d-space case. The important thing is how you define ⊑_U, and this is subtle, so watch out.
For every open subset U, for all x, y in U, we let x ⊑_U y if and only if we can write x as e^iθ, y as e^iθ’, with θ≤θ’, and (the important part!) such that for every t in the interval [θ, θ’], e^it is in U. In other words, there is a whole segment connecting x to y in the counterclockwise direction that is included in U. This is actually a stream, not just a prestream… and in fact a Haucourt stream, a notion I will introduce (way) below.
Every topological space X equipped with a preordering ≤ defines a prestream by declaring that ⊑_U is the restriction of ≤ to U for every open subset U of X. (This will turn out to be almost never a stream.)
If you apply the previous construction to [0,1] with its usual ordering, you will obtain a prestream. One would expect that, if you take the quotient of that prestream in the category PreStr of prestreams (see below) obtained by equating 0 and 1, you would obtain a form of the directed circle. But you would be disappointed: the result is just the circle with the trivial preordering that declares that every point is below any point. (One reason why we should prefer streams over prestreams… that will be another time!)
Here is a better (and fundamental) construction of the directed line segment. This is the analogue of the d-space I^→; hence we keep the same name and the same notation. The carrier of I^→ is the usual unit interval [0,1]. The precirculation is defined as follows: for every open subset U of [0,1], for all x, y in U, x ⊑_U y if and only if x≤y and the whole segment [x,y] is included in U. Note the analogy with S₁^→: in fact, S₁^→ is the quotient of I^→ in PreStr. (I^→ is also a Haucourt stream, hence a stream.)
Every topological space can be given the discrete precirculation, where ⊑_U is the trivial preordering on U that makes every point below any other point. This is a special case of a preordered topological space (see second bulleted item above), where the preordering is the trivial one.
Every topological space can be given the indiscrete precirculation, where ⊑_U is just equality. This is again a preordered topological space, with equality as preordering.

The category PreStr of prestreams

There is a category PreStr of prestreams. Its morphisms f : (X, (⊑_U)_U ∈ OX) → (Y, (⪯_V)_V ∈ OY) are the continuous maps f: X → Y that are locally monotonic, namely such that for every open subset V of Y, for all points x, y in U≝f^–1(V), if x ⊑_U y then f(x) ⪯_V f(y).

Just as with dTop, the forgetful functor that sends every prestream to its carrier is topological, and that immediately shows that PreStr is complete and cocomplete. You will probably have to trust me on that.

As an illustration, here is how one builds the product of two prestreams (X, (⊑_U)_U ∈ OX) and (Y, (⪯_V)_V ∈ OY). Its carrier is the topological product X × Y. For every open subset W of X × Y, its first projection π₁[W] ≝ {x ∈ X | ∃y ∈ Y, (x,y) ∈ W} is an open subset U of X, and its second projection π₂[W] is an open subset V of Y. Then the preordering ≤_W on W is given by: (x,y) ≤_W (x’,y’) if and only if x ⊑_U y and x’ ⪯_V y’.

That may sound like a reasonable definition. However, that is really a strange notion of product. In order to decide whether (x,y) ≤_W (x’,y’), one needs to compare (x,y) and (x’,y’) in the product preordering ⊑_U × ⪯_V. In particular, one compares (x,y) and (x’,y’) inside W exactly as one compares them in the smallest rectangle that encloses W, namely U × V. That is strange, because one would expect ≤_W to only depend of what happens inside W, not in the smallest rectangle that encloses W. The notion of products of streams will be more natural, but streams are more complex.

Let me also mention how you build quotients in PreStr. Let (X, (⊑_U)_U ∈ OX) be a prestream, and let ≡ be an equivalence relation on X. The quotient prestream (Y, (⪯_V)_V ∈ OY) is built as follows. First, Y is the quotient space X/≡. Let q : X → Y be the quotient map. Given any open subset V of Y, let U≝q^–1(V). Then, for all points y, y’ of V, we declare that y ⪯_V y’ if and only if there are finitely many points x₁, x’₁, x₂, x’₂, …, x_n, x’_n in U such that x₁ ⊑_U x’₁ ≡ x₂ ⊑_U x’₂ ≡ … ≡ x_n ⊑_U x’_n, and q(x₁)=y, q(x’_n)=y’. Note the resemblance with quotients in dTop: we alternate between moves where we travel from x_i to a larger point x’_i in U (relatively to ⊑_U), and sideways moves, where we replace a point x’_i by an equivalent point x_i+1.

Building prestreams from d-spaces: the functor S

There is a general way of building a prestream from a d-space. Given any d-space (X, dX), we define a precirculation (⊑_U)_U ∈ OX on X by letting x ⊑_U y (for all points x and y of U) if and only if there is a d-path γ ∈ dX from x to y (namely, such that γ(0)=x and γ(1)=y) and whose image is entirely included in U.

We write S(X, dX) for the resulting prestream, or just S(X).

Please pay attention to the second condition on γ: the image of γ should be entirely contained in U, namely, γ(t) should be in U for every t in [0,1]. That should ring a bell: this is how we defined the prestream S₁^→, as well as the prestream I^→. In fact, I simply defined the directed circle prestream S₁^→ as the image of the directed circle d-space S₁^→ through S, and the directed line segment prestream I^→ as the image of the directed line segment d-space I^→ through S.

What we have defined is the object part of a functor S : dTop → PreStr. Its action on morphisms is as follows. Given any d-space morphism f : (X, dX) → (Y, dY), we realize that f is continuous (by definition) and locally monotonic with respect to the precirculations on S(X, dX) and S(Y, dY). Explicitly, let (⊑_U)_U ∈ OX be the precirculation on the prestream S(X, dX) and (⪯_V)_V ∈ OY be the precirculation on S(Y, dY). For every open subset V of Y, let U≝f^–1(V). Given any two points x, x’ of U such that x ⊑_U x’, by definition there is a d-path γ ∈ dX from x to y whose image is entirely included in U. Since f is a d-space morphism, f o γ is a d-path (in dY), and this is a d-path from f(x) to f(y) whose image is included in the image of U by f, hence in V.

It turns out that S preserves all colimits. Quotients in both dTop and PreStr are coequalizers (as in Top), so it is no wonder that one can obtain the directed circle as a quotient of the directed line segment in both.

The reason that S preserves all colimits is because it left adjoint to a functor D, which we now build.

Building d-spaces from prestreams: the functor D

In the reverse direction, let (X, (⊑_U)_U ∈ OX) be any prestream. We define a d-space D(X, (⊑_U)_U ∈ OX), or just D(X) for short, as follows. The carrier of D(X) is simply X, and we need to define its set of d-paths. This is relatively subtle, and exhibits the fundamental rôle played by the directed line segment in the theory.

We say that a path γ : [0,1] → X is a d-path in D(X) if and only if γ is a directed path in the prestream (X, (⊑_U)_U ∈ OX), namely if and only if γ defines a prestream morphism from the directed line segment prestream I^→ to (X, (⊑_U)_U ∈ OX). Explicitly, a directed path is a continuous map γ from [0,1] to X such that, for every open subset U of X, for all points s, t in [0,1] such that s ≤ t and the whole interval [s,t] is included in γ^–1(U), γ(s) ⊑_U γ(t).

I will let you check by yourselves that all the constant paths are directed paths, that the concatenation of two directed paths is a directed path, and that directed paths are closed under reparametrization.

Beware! On dipaths and directed paths

This definition is subtle, because one might have thought of a simpler notion. The alternate notion of a dipath is that of a continuous map γ from [0,1] to X such that, for every open subset U of X, for all points s ≤ t in γ^–1(U), γ(s) ⊑_U γ(t). Instead, with a directed path we only require γ(s) ⊑_U γ(t) if s, t are in γ^–1(U), s ≤ t, and every point between s and t is also in γ^–1(U). A dipath is a prestream morphism from the preordered topological space ([0,1], ≤), seen as prestream, to (X, (⊑_U)_U ∈ OX).

We will not take dipaths as d-paths, and perhaps the simplest reason is because dipaths, contrarily to directed paths, are not closed under concatenation. Indeed, let us imagine two dipaths γ₁ from x to y and γ₂ from y to z in X, and an open subset of X containing γ₁(½) and γ₂(½) but not y. You need to show that γ₁(½) ⊑_U γ₂(½), but how would you do that? The only imaginable way you could prove it would be by showing that γ₁(½) ⊑_U γ₁(1) = y = γ₂(0) ⊑_U γ₂(½), but you cannot, since y is not in U. (No such problem occurs with directed paths, since you would start from the assumption that U contains all the points γ₁(t) for ½≤t≤1 and all the points γ₂(t) for 0≤t≤½, and in particular y.)

Hence, remember: on D(X), d-path = directed path ≠ dipath.

Here is an actual counterexample, showing that concatenations of dipaths may fail to be dipaths.

Let X be the three point space {0, 1, ⊥}, with the Scott topology of the ordering that makes ⊥ least, and 0 and 1 incomparable above it. Its open subsets are the empty set, {0}, {1}, {0,1}, and the whole space.
Let dX consist of all paths on X, namely all continuous functions from [0,1], with its usual metric topology, to X. There are a lot of them, do not worry.
We consider the prestream S(X, dX).
Note that any path γ from 0 to 1 in X must go through ⊥: γ^–1({0}) and γ^–1({1}) are disjoint open subsets of [0,1], hence cannot cover [0,1], since [0,1] is connected; therefore γ(t)=⊥ for some t in [0,1]. Similarly, any path from 1 to 0 must go through ⊥. This implies that the preordering ⊑_U on U≝{0,1} must be the equality relation. Remember indeed that x ⊑_U y if and only if there is a d-path (simply a path, here) from x to y whose image is entirely included in U, and we have just shown that this cannot happen if x=0 and y=1, or if x=1 and y=0.
In particular, there is no dipath from 0 to 1 in S(X, dX). Indeed, for U≝{0,1}, s≝0, t≝1, such a dipath γ would need to satisfy γ(0)=0 ⊑_U 1=γ(1). There is no dipath from 1 to 0 either.
Let us fix any a ∈ [0,1]. There is a dipath γ₁ from 0 to ⊥, defined as mapping every element of [0,a[ to 0 and every element of [a,1] to ⊥.
Indeed, this is continuous, because the inverse image of any open set that contains 0 but not ⊥ is the open set [0,a[, and all the other inverse images are either empty or the whole of [0,1].
In order to show that is a dipath, we consider any open subset V of X, and we check that for all s ≤ t in [0,1] such that γ₁(s) and γ₁(t) are in V, then γ₁(s) ⊑_V γ₁(t), namely that there is a d-path (simply a path) from γ₁(s) to γ₁(t) whose image is entirely included in V.
This is obvious if γ₁(s) = γ₁(t). Otherwise, γ₁(s)=0 and γ₁(t)=⊥, so V contains both 0 and ⊥, and the subpath u ↦ γ₁(s+(t–s)u) (or just γ₁ itself) is a d-path from 0 to ⊥ whose image is entirely contained in V.
This proof actually shows that 0 ⊑_V ⊥. I will let you check that ⊑_V on any open set V containing both 0 and ⊥ is trivial, namely that it makes every element less than or equal to any other element of V.
Similarly, there is a dipath γ₂ from ⊥ to 1, defined as mapping every element of [0,a] to ⊥ and every element of ]a,1] to 1.
Every dipath is a directed path, and directed paths are closed under concatenation. Hence, the concatenation γ₁;γ₂ is a directed path, but it cannot be a dipath, since as we have seen earlier, there is no dipath from 0 to 1.

The adjunction S ⊣ D

Let us return to the construction of D(X). Let me remind you that we defined the d-paths in D(X) as the directed paths in X, namely the prestream morphism from I^→ to (X, (⊑_U)_U ∈ OX), or equivalently, as the paths γ : [0,1] → X such that, for every open subset U of X, for all points s, t in [0,1] such that s ≤ t and the whole interval [s,t] is included in γ^–1(U), γ(s) ⊑_U γ(t).

As one would expect, this is the object part of a functor D from PreStr to dTop. On morphisms, it simply maps every prestream morphism f : (X, (⊑_U)_U ∈ OX) → (Y, (⪯_V)_V ∈ OY) to f itself. We need to check that for every d-path γ on D(X), f o γ is a d-path on D(Y). In other words, we wish to verify that for every prestream morphism γ from I^→ to (X, (⊑_U)_U ∈ OX), f o γ is a prestream morphism from I^→ to (Y, (⪯_V)_V ∈ OY), and that is obvious.

Given a d-space (X, dX), let us look at D(S(X)). The carrier of D(S(X)) is just X, and a d-path in D(S(X)) is a path γ : [0,1] → X such that, for every open subset U of X, for all points s, t in [0,1] such that s ≤ t and the whole interval [s,t] is included in γ^–1(U), [γ(s) ⊑_U γ(t), namely:] there is a d-path γ’ from γ(s) to γ(t) whose image is entirely included in U. If γ is a d-path itself, this property is satisfied: it suffices to define γ’ as the subpath u ↦ γ₁(s+(t–s)u). This defines a morphism η_X : X → D(S(X)), which is just the identity on carriers.

The morphism η_X is natural in X, and will be the unit of our future adjunction S ⊣ D.

We say that the d-space (X, dX) is complete if and only if η_X is an isomorphism of d-spaces, namely if and only if for every path γ : [0,1] → X, for every open subset U of X, for all points s, t in [0,1] such that s ≤ t and the whole interval [s,t] is included in γ^–1(U), there is a d-path γ’ from γ(s) to γ(t) whose image is entirely included in U (not necessarily a subpath of γ), then γ itself is a d-path. The notion and the name “complete” are due to Ziemiański [8, Definition 2.7], and the notion was introduced independently by Haucourt [5], as the objects of the category called dT* there.

I will let you check that D(Y) is a complete d-space for every prestream Y. This is one half of Proposition 5.10 of [5], which states that D o S o D = D. If you do it by yourself, try not to get lost in the various notions and constructions!

In the other direction, given a prestream (X, (⊑_U)_U ∈ OX), S(D(X)) is a prestream whose carrier is X, and whose precirculation (⊑’_U)_U ∈ OX is obtained as follows: for every open subset U of X, for all points x and y of U, x ⊑’_U y if and only if:

there is a d-path γ from x to y in D(X) whose image is entirely included in U;
equivalently, there is a directed path γ from x to y whose image is entirely included in U;
equivalently, there is a path γ from x to y whose image is entirely included in U, and such that for every open subset V of X, for all points s, t in [0,1] such that s ≤ t and the whole interval [s,t] is included in γ^–1(V), γ(s) ⊑_V γ(t). (Wow, what a definition! As an exercise, show that you can restrict V to be included in U, and that this would give an equivalent definition.)

Although that sounds complicated, at least we see that if x ⊑’_U y then x ⊑_U y: if x ⊑’_U y, then there is a path γ from x to y as above, and letting s≝0, t≝1, and V≝U, γ(s) ⊑_V γ(t)—namely, x ⊑_U y. Hence the identity map defines a prestream morphism ε_X : S(D(X)) → X. This is natural in X, and will be the counit of the adjunction S ⊣ D.

I have called Haucourt streams those prestreams X such that ε_X is an isomorphism of prestreams [7]; they are the objects of the subcategory St* introduced by Haucourt in [5]. They are exactly those prestreams in which, for every open subset U, for all points x and y of U, x ⊑_U y if and only if there is a directed path γ from x to y whose image is entirely included in U. In other words, x ⊑_U y is witnessed by the existence of a directed path from x to y in U.

Every prestream of the form S(Y), for any d-space Y, is a Haucourt stream, as one can check by oneself. This is also the other half of Proposition 5.10 of [5].

We have almost completed our proof the S is left adjoint to D, with unit η and counit ε. It only remains to verify that ε_S₍_X₎ o S(η_X) is the identity on S(X) and that D(ε_X) o η_D₍_X₎ is the identity on D(X). This is obvious, since the functions underlying the unit and counit morphisms are identity maps.

I have mentioned that D(X) is a complete d-space for every prestream X, in other words, that η_D₍_X₎ is an isomorphism, for every prestream X. An adjunction F ⊣ U such that the unit at every object of the form U(-) is an isomorphism is called an idempotent adjunction. This has many other equivalent definitions. (The one I have taken is item 7 of Definition 1.1 of the nCatLab article.) Those equivalent definitions yield:

S(η_X) is an isomorphism of prestreams, for every d-space X;
ε_S₍_X₎ is an isomorphism of prestreams, for every d-space X;
D(ε_S₍_X₎) is an isomorphism of d-spaces, for every d-space X, namely D o S is an idempotent monad;
D(S(η_X)) = η_D₍_S₍_X)) for every d-space X;
D(S(η_D₍_X₎)) = η_D₍_S_(D(_X))) for every prestream X;
D(ε_X) is an isomorphism of d-spaces, for every prestream X;
(η_D₍_X₎ is an isomorphism of d-spaces, for every prestream X, already mentioned)
S(η_D₍_X₎) is an isomorphism of prestreams, for every prestream X, namely S o D is an idempotent comonad;
S(D(ε_X)) = ε_S₍_D₍_X)) for every prestream X;
S(D(ε_S₍_X₎)) = ε_S₍_D₍_S₍_X))) for every d-space X.

In particular, the adjunction S ⊣ D restricts to an adjoint equivalence between the full subcategory of objects in the range of D (the complete d-spaces) and the full subcategory of objects in the range of S (the Haucourt streams).

Finally, we have reached the following conclusion.

Theorem [5]. There is an idempotent adjunction S ⊣ D between dTop and PreStr, which restricts to an adjoint equivalence between the full subcategory of complete d-spaces and Haucourt streams.

Conclusion

We haven’t touched the subject of streams at all. I’ll talk about them another time. Be reassured: every Haucourt stream is a stream, as its name indicates. Streams are a tad more general. More importantly, they are cosheaves of preordered sets, and I’ll try to say some of the things that this implies. I will also explain what products in the categories of streams and of Haucourt streams look like. They are more complicated than for prestreams, but they are also a lot more natural.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen. Directed Algebraic Topology and Concurrency. ISBN 978-3-319-15398-8.
Roger Penrose, Techniques of Differential Topology in Relativity, Conference Board of the Mathematical Sciences, Regional Conference Series in Applied Mathematics, vol. 7, SIAM, Philadelphia, USA, 1972.
Marco Grandis. Directed Algebraic Topology: Models of Non-Reversible Worlds. New Mathematical Monographs 13, Cambridge University Press, 2009. ISBN-13 978-0-521-76036-2.
Sanjeevi Krishnan. A convenient category of locally preordered spaces. Applied Categorical Structures, 17(5):445–466, 2009.
Emmanuel Haucourt. Streams, d-spaces, and their fundamental categories. Electronic Notes in Theoretical Computer Science 283, pages 111–151, 2012.
Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories. The joy of cats. John Wiley and Sons, Inc., 1990. Online version available here.
Jean Goubault-Larrecq. Exponentiable streams and prestreams. Applied Categorical Structures 22, pages 515–549, 2014. The published version, available from Springer Link, contains two mistakes, which are repaired in the HAL report.
Krzysztof Ziemiański. A cubical model for path spaces in d-simplicial complexes. Topology and its Applications 159(8), pages 2127–2145, 2012.

— Jean Goubault-Larrecq (July 25th, 2021)