Isomorphism of Preorders

definition example

Let $(P,{\le }_P)$ and $(Q,{\le }_Q)$ be preorders. A monotone function $f:P\to Q$ is an isomorphism if there is a monotone $g:Q\to P$ with $f;g={\mathrm{id}}_P$ and $g;f={\mathrm{id}}_Q$, i.e. $p=g(f(p))$ and $q=f(g(q))$. $g$ is the inverse of $f$. If an isomorphism exists, $P$ and $Q$ are isomorphic. An isomorphism of preorders is “basically just a relabeling of the elements”.

Sources: 7 Sketches Definition 1.75, Example 1.76, Remark 1.74; this is the special case of Isomorphism in the Category of Preorders.

Example 1.76. The preorders $P$ ($a\le b,c\le d\le e$ with $b,c$ incomparable), $Q$ ($v,w\le x\le y\le z$-shaped) and $R$ (same as $Q$ but with an extra drawn arrow $x\to z$) are all isomorphic; the extra arrow is implied by transitivity, so $Q$ and $R$ are literally the same preorder.

A Galois Connection is a “relaxed isomorphism”: replacing $\le$ by $=$ in $p\le g(f(p))$, $f(g(q))\le q$ recovers this definition. Compare Equivalence of Categories, of which isomorphism of skeletal preorders is a special case: two preorders are equivalent as categories iff their poset reflections are isomorphic.

LeanHaskell

#check (OrderIso ℕ ℕ)     -- α ≃o β : an order-preserving bijection with order-preserving inverse
#check @OrderIso.symm

data OrderIso a b = OrderIso (Monotone a b) (Monotone b a)
-- laws: the two composites are identities