In Johnstone's Stone Spaces it is proved that the category of profinite partial orders is (equivalent to) the category of ordered Stone spaces (also called Priestley spaces) and that the obvious embedding from finite partial orders into Priestley spaces is the pro-completion of finite partial orders.

Main question: Does it follow that there exists a profinite completion functor from partial orders to Priestley spaces?

If yes, is there an explicit construction of the profinite completion of a partial order?

For example, does anyone know what does the profinite completion of the partial order $(\omega,=)$ look like?

Moreover, profinite quasi-orders are the the Priestley quasi-orders, i.e. quasi-ordered Stone spaces such that if $x\not\leq y$ then there is a clopen downset $D$ such that $y\in D$ and $x\not\in D$. I have the same questions about the profinite completion of a quasi-order. In this context, does one gain anything by considering quasi-order instead of partial orders?

For the record I asked this question on MathSE, here.

I gave it a try:

Let $\mathbf{Po}$ be the category of posets with monotone maps, $\mathbf{PrSp}$ the category of Priestley spaces. Then let $U:\mathbf{PrSp}\to \mathbf{Po}$ be the forgetful functor. The profinite completion functor $P:\mathbf{Po}\to\mathbf{PrSp}$ would be the left adjoint of $U$. Let $\mathbf{DLat}$ be the category of bounded distributive lattices. Now by Birkhoff duality $\mathbf{DLat}_\text{fin}$ is dual to $\mathbf{Po}_\text{fin}$ and Priestley duality is that $\mathbf{DLat}=\text{Ind-}\mathbf{DLat}_\text{fin}$ is dual to $\mathbf{PrSp}=\text{Pro-}\mathbf{Po}_\text{fin}$. Let $D:\mathbf{Po}\to \mathbf{DLat}$ be the contravariant functor sending a po $P$ to the lattice $\mathcal{D}(P)$ of its downsets, and a monotone map $f:P\to Q$ to the preimage map $f^{-1}:\mathcal{D}(Q)\to\mathcal{D}(P)$. Let $H:\mathbf{DLat}\to \mathbf{PrSp}$ be the contravariant functor in Priestley duality. Now we claim that $P:\mathbf{Po}\to \mathbf{PrSp}$ can be defined as $P=H\circ D$.

Sketch of the proof

Let $Q$ be a partial order and $\langle p_{i,j}:Q_i\to Q_j \rangle$ the cofiltered diagram of its finite po quotients. Let $P(Q)=\lim_i Q_i$ be the limit in the category of Priestley spaces, each $Q_i$ considered discrete of course, and $i_Q:Q\to P(Q)$ the natural monotone mapping. Using Birkhoff duality, we may consider the diagram $\langle h_j,i:D_j\to D_i\rangle$ in $\mathbf{DLat}_\text{fin}$ dual to $\langle p_i:Q\to Q_i \rangle$ and its colimit $D=\text{colim}_j D_j$ in $\mathbf{DLat}$. This distributive lattice is just the lattice $\mathcal{D}(Q)$ of downsets of $Q$. Indeed $D$ is the union of all downsets of $Q$ of the form $p^{-1}(E)$ for a monotone map $p:Q\to F$ with $F$ finite and $E$ downset of $F$. But for every downset $D$ of $Q$ the characteristic function $\chi_D:Q\to 2$ is monotone (where $2=\{0<1\}$) and $\chi^{-1}(1)=D$. It follows by Priestley duality that the Priestley space $P(Q)=\lim_i Q_i$ is dual to the lattice $\mathcal{D}(Q)$. From this point of view we get that $i_Q:Q\to P(Q)$, $q\mapsto \{D\in \mathcal{D}(Q)\mid q\in D\}$ is the unit of the adjunction.

Now let $f:Q\to X$ be a monotone map into a Priestley space $X$. Then $X$ is dual to the lattice $\mathcal{CD}(X)$ of clopen downsets of $X$ under Priestley duality. Since $f$ is monotone the preimage map goes $f^{-1}:\mathcal{D}(X)\to\mathcal{D}(Q)$ and restricts to a homomorphism $f^{-1}:\mathcal{CD}(X)\to\mathcal{D}(Q)$ whose Priesltey dual is a monotone continuous map $\bar{f}:P(Q)\to X$. Clearly we have $\bar{h}\circ i_Q=h$.

Hence the functor $P:\mathbf{Po}\to\mathbf{PrSp}$, $Q\mapsto P(Q)$ and for a monotone $f:Q\to R$ in $\mathbf{Po}$ then $P(f):P(Q)\to P(R)$ is the Priestley dual map of $f^{-1}:\mathcal{D}(R)\to\mathcal{D}(Q)$, is dual to the forgetful functor $U:\mathbf{PrSp}\to \mathbf{Po}$.