Order embedding and order isomorphism

Let $(P,{\le }_P)$ and $(Q,{\le }_Q)$ be posets (Partial order and partially ordered set).

A function $f:P\to Q$ is an order embedding when for all $x,y\in P$

$x{\le }_{P}y⟺f(x){\le }_{Q}f(y)\mathrm{.}$

An order embedding is automatically injective: $f(x)=f(y)$ gives $f(x){\le }_{Q}f(y)$ and $f(y){\le }_{Q}f(x)$, hence $x{\le }_{P}y$ and $y{\le }_{P}x$, hence $x=y$ by antisymmetry (Partial order and partially ordered set).

An order isomorphism is a surjective order embedding, equivalently a bijection $f:P\to Q$ with $x{\le }_{P}y⟺f(x){\le }_{Q}f(y)$ for all $x,y\in P$. The posets $P$ and $Q$ are order isomorphic, written $P\cong Q$, when an order isomorphism $P\to Q$ exists.

• The condition is an equivalence, not an implication. A bijection satisfying only $x{\le }_{P}y\Rightarrow f(x){\le }_{Q}f(y)$ need not be an order isomorphism: let $P=\{a,b\}$ carry the discrete order, in which $a$ and $b$ are incomparable, and let $Q=\{0,1\}$ carry $0<1$. The bijection $a\mapsto 0$, $b\mapsto 1$ preserves every relation of $P$, because $P$ has none beyond reflexivity, yet its inverse does not preserve $0<1$.
• For total orders the implication form does suffice. If $P$ and $Q$ are totally ordered and $f:P\to Q$ is a bijection with $x{<}_{P}y\Rightarrow f(x){<}_{Q}f(y)$, then $f$ is an order isomorphism: given $f(x){<}_{Q}f(y)$, the alternative $y{\le }_{P}x$ would give $f(y){\le }_{Q}f(x)$, which is impossible. Since a well-order is total (Well-order and well-ordered set), a strictly increasing bijection between well-orders is automatically an order isomorphism.
• Strict form. An order isomorphism satisfies $x{<}_{P}y⟺f(x){<}_{Q}f(y)$, because it is injective and preserves both $\le$ and $=$ in both directions.
• The identity is an order isomorphism, the inverse of an order isomorphism is one, and a composite of two is one. Hence $\cong$ is reflexive, symmetric and transitive on any set of posets. It is not a relation on "all posets", since there is no set of all posets.
• Order isomorphisms transport well-ordering. If $f:P\to Q$ is an order isomorphism and $(P,{\le }_P)$ is a well-order (Well-order and well-ordered set), so is $(Q,{\le }_Q)$: totality transfers because $f$ is a surjective embedding, and a nonempty $S\subseteq Q$ has $f^{-1}[S]$ nonempty, whose least element $\mathrm{\ell }$ is carried by $f$ to a least element of $S$. This transfer is used repeatedly below and is the reason order isomorphism, rather than mere bijection, is the right notion of sameness here.
• Order isomorphisms respect initial segments. If $f:P\to Q$ is an order isomorphism and $x\in P$, then $f$ carries $\{y\in P:y{<}_{P}x\}$ onto $\{z\in Q:z{<}_{Q}f(x)\}$: the strict form gives the inclusion one way, and surjectivity gives it the other, since $z{<}_{Q}f(x)$ has the form $z=f(y)$ with $y{<}_{P}x$. Consequently the restriction of $f$ to that set is again an order isomorphism.
• Functions, bijections, ordered pairs and Cartesian products are built in this library, at A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain, Injection, surjection, bijection, The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,b\}\}$ and The Cartesian product $A\times B:=\{z\in \mathcal{P}(\mathcal{P}(A\cup B)):\mathrm{\exists }a\in A\mathrm{\exists }b\in Bz=(a,b)\}$; "subset" and "union" are built alongside them. This item fixes only the order-theoretic terminology on top of that vocabulary.