Order isomorphism

In the mathematical field of order theory, an order isomorphism is a special kind of monotone function that constitutes a suitable notion of isomorphism for partially ordered sets (posets). Whenever two posets are order isomorphic, they can be considered to be "essentially the same" in the sense that either of the orders can be obtained from the other just by renaming of elements. Two strictly weaker notions that relate to order isomorphisms are order embeddings and Galois connections.
Definition.
Formally, given two posets formula_1 and formula_2, an order isomorphism from formula_1 to formula_2 is a bijective function formula_5 from formula_6 to formula_7 with the property that, for every formula_8 and formula_9 in formula_6, formula_11 if and only if formula_12. That is, it is a bijective order-embedding.
It is also possible to define an order isomorphism to be a surjective order-embedding. The two assumptions that formula_5 cover all the elements of formula_7 and that it preserve orderings, are enough to ensure that formula_5 is also one-to-one, for if formula_16 then (by the assumption that formula_5 preserves the order) it would follow that formula_18 and formula_19, implying by the definition of a partial order that formula_20.
Yet another characterization of order isomorphisms is that they are exactly the monotone bijections that have a monotone inverse.
An order isomorphism from a partially ordered set to itself is called an order automorphism.
When an additional algebraic structure is imposed on the posets formula_1 and formula_2, a function from formula_1 to formula_2 must satisfy additional properties to be regarded as an isomorphism. For example, given two partially ordered groups (po-groups) formula_25 and formula_26, an isomorphism of po-groups from formula_27 to formula_28 is an order isomorphism that is also a group isomorphism, not merely a bijection that is an order embedding.
Order types.
If formula_5 is an order isomorphism, then so is its inverse function.
Also, if formula_5 is an order isomorphism from formula_1 to formula_2 and formula_39 is an order isomorphism from formula_2 to formula_41, then the function composition of formula_5 and formula_39 is itself an order isomorphism, from formula_1 to formula_41.
Two partially ordered sets are said to be order isomorphic when there exists an order isomorphism from one to the other. Identity functions, function inverses, and compositions of functions correspond, respectively, to the three defining characteristics of an equivalence relation: reflexivity, symmetry, and transitivity. Therefore, order isomorphism is an equivalence relation. The class of partially ordered sets can be partitioned by it into equivalence classes, families of partially ordered sets that are all isomorphic to each other. These equivalence classes are called order types.