# Does an isomorphism induce an order isomorphism?

Let $\mathfrak{A}$ is a poset. For $a, b \in \mathfrak{A}$ we will denote $a \curlyvee b$ if only if there is a non-least element $c$ such that $c \leqslant a \wedge c \leqslant b$.

Let $\mathfrak{A}$ and $\mathfrak{B}$ are posets. A pointfree funcoid from $\mathfrak{A}$ to $\mathfrak{B}$ is a pair $\left( \alpha ; \beta \right)$ of functions $\alpha \in \mathfrak{B}^{\mathfrak{A}}$ and $\beta \in \mathfrak{A}^{\mathfrak{B}}$ such that $\alpha \left( x \right) \curlyvee y \Leftrightarrow \beta \left( y \right) \curlyvee x$ for every $x \in \mathfrak{A}$, $y \in \mathfrak{B}$.

I denote $\left\langle \left( \alpha ; \beta \right) \right\rangle = \alpha$ for every pointfree funcoid $\left( \alpha ; \beta \right)$.

Composition $\left( \alpha_1 ; \beta_1 \right) \circ \left( \alpha_0 ; \beta_0 \right)$ of funcoids $\left( \alpha_0 ; \beta_0 \right)$ and $\left( \alpha_1 ; \beta_1 \right)$ is defined by the formula: $$\left( \alpha_1 ; \beta_1 \right) \circ \left( \alpha_0 ; \beta_0 \right) = \left( \alpha_1 \circ \alpha_0 ; \beta_0 \circ \beta_1 \right) .$$ The category of pointfree funcoids is the category whose objects are small posets, whose morphisms are pointfree funcoids between these posets, the composition is the composition of pointfree funcoids.

It is easy to verify that it is indeed a category.

Question: If $f$ is an isomorphism of the category of pointfree funcoids then $\left\langle f \right\rangle$ is an order isomorphism?

You can read more about funcoids (a tool for general topology) here.

-

Obviously $\left\langle f \right\rangle$ is increasing.

We have: $\left\langle f \right\rangle \circ \left\langle f^{- 1} \right\rangle = \left\langle f \circ f^{- 1} \right\rangle = \left\langle \operatorname{id}^{\mathsf{\operatorname{FCD}}}_{\mathfrak{B}} \right\rangle =\operatorname{id}_{\mathfrak{B}}$ and $\left\langle f^{- 1} \right\rangle \circ \left\langle f \right\rangle = \left\langle f^{- 1} \circ f \right\rangle = \left\langle \operatorname{id}^{\mathsf{\operatorname{FCD}}}_{\mathfrak{A}} \right\rangle = \operatorname{id}_{\mathfrak{A}}$. Thus $\left\langle f \right\rangle$ is a bijection.

$\left\langle f \right\rangle$ is increasing and bijective. Consequently $\langle f\rangle$ is an order isomorphism.

-
Err, the condition that $\langle f \rangle$ is increasing seems not always true for every pointfree funcoid. We should additionally require this condition. I will check this. –  porton Jul 21 '12 at 14:55