Given a topological space with topology , the specialization order is defined by either of the following two equivalent conditions:
if and only if belongs to the closure of ; we say that is a specialisation of .
if and only if
(Note: some authors use the opposite ordering convention.)
is if and only if its specialisation order is a partial order. is iff its specialisation order is equality. is (like but without ) iff its specialisation order is an equivalence relation. (See separation axioms.)
Given a continuous map between topological spaces, it is order-preserving relative to the specialisation order. Thus, we have a faithful functor from the category of of topological spaces to the category of preordered sets.
In the other direction, to each proset we may associate a topological space whose elements are those of , and whose open sets are precisely the upward-closed sets with respect to the preorder. This topology is called the specialization topology. This defines a functor
i \colon ProSet \to Top
which is a full embedding; the essential image of this functor is the category of Alexandroff spaces (spaces in which an arbitrary intersection of open sets is open). Hence the category of prosets is equivalent to the category of Alexandroff spaces.
In fact, we have an adjunction , making a coreflective subcategory of . In particular, the counit evaluated at a space ,
i(Spec(X)) \to X,
is the identity function at the level of sets, and is continuous because any open of is upward-closed with respect to , according to the second equivalent condition of the definition of the specialization order.
This adjunction restricts to an adjoint equivalence between the categories and of finite prosets and finite topological spaces. The unit and counit are both identity functions at the level of sets, so we in fact have an equivalence between these categories as concrete categories.