nLab partial order




A partial order on a set is a way of ordering its elements to say that some elements precede others, but allowing for the possibility that two elements may be incomparable without being the same. This is the fundamental notion in order theory.

By regarding the ordering \leq as the existence of a unique morphism, preorders may be regarded as certain categories (namely, thin categories). This category is sometimes called the order category associated to a partial order; see below for details.


As a set with extra structure

A poset may be understood as a set with extra structure.

Given a set SS, a partial order on SS is a (binary) relation \leq with the following properties:

A poset is a set equipped with a partial order.

As a preorder with antisymmetry

A poset is precisely a proset satisfying the extra condition that xyxx \leq y \leq x implies that x=yx = y.

In dependent type theory

In dependent type theory, the identity type x=yx = y representing equality is not necessarily valued in h-propositions. As a result, a naive translation of the set theoretic definition of a partial order from a preorder above doesn’t work. Instead, one has to postulate an equivalence of types between the identity type x=yx = y and the condition xyxx \leq y \leq x:

A partial order is a preorder XX with an equivalence of types antisym(x,y):(x= Xy)(x<y)×(y<x)\mathrm{antisym}(x, y):(x =_X y) \simeq (x \lt y) \times (y \lt x) for all x:Xx:X and y:Xy:X.

Equivalently, one could inductively define a function

x:X,y:XidToOrd(x,y):(x= Xy)(x<y)×(y<x)x:X, y:X \vdash \mathrm{idToOrd}(x, y):(x =_X y) \to (x \lt y) \times (y \lt x)

on reflexivity of the identity type by reflexivity of the preorder

idToSymCon(x,x)(id X(x))refl (x)\mathrm{idToSymCon}(x, x)(\mathrm{id}_X(x)) \coloneqq \mathrm{refl}_{\leq}(x)

Then, a partial order is a preorder such that the defined function idToOrd(x,y)\mathrm{idToOrd}(x, y) is an equivalence of types for all x:Xx:X and y:Xy:X.

antisym: x:X y:XisEquiv(idToOrd(x,y))\mathrm{antisym}:\prod_{x:X} \prod_{y:X} \mathrm{isEquiv}(\mathrm{idToOrd}(x, y))

In either case, since the preorder is valued in propositions, the antisymmetry axiom ensures that the partial order is an h-set.

As a category with extra properties

A poset may be understood as a category with extra property, sometimes called its order category.

A poset is a category such that:

  • for any pair of objects x,yx, y, there is at most one morphism from xx to yy

  • if there is a morphism from xx to yy and a morphism from yy to xx (which by the above implies that xx and yy are isomorphic), then x=yx = y.

Equivalently, this says that a poset is a skeletal thin category, or equivalently a skeletal category enriched over the cartesian monoidal category of truth values or equivalently a skeletal (0,1)-category. (See also at enriched poset).

When we do this, we are soon led to contemplate a slight generalization of partial orders: namely preorders. The reason is that the antisymmetry law, saying that xyx \le y and yxy \le x imply x=yx = y, violates the principle of equivalence in a certain sense. (On the other hand, it does not violate it if taken as a definition of equality.)

Monotone functions

The morphisms of partially ordered sets are monotone functions; a monotone function ff from a poset SS to a poset TT is a function from SS to TT (seen as structured sets) that preserves \leq:

xyf(x)f(y). x \leq y \;\Rightarrow\; f(x) \leq f(y) .

Equivalently, it is a functor from SS to TT (seen as certain categories).

In this way, posets form a category Pos.


A (closed bounded) interval in a poset CC is a set of the form

[x,y]={rC|xry}.[x,y] = \{r\in C|x\le r\le y\}.

A poset is locally finite if every closed bounded interval is finite.

Kinds of posets

A poset with a top element and bottom element is called bounded. (But note that a subset of a poset may be bounded without being a bounded as a poset in its own right.) More generally, it is bounded above if it is has a top element and bounded below if it has a bottom element.

A poset with all finite meets and joins is called a lattice; if it has only one or the other, it is still a semilattice.

A poset in which every finite set has an upper bound (but perhaps not a least upper bound, that is a join) is a directed set.

As remarked above, a poset in which each interval [x,y][x,y] is a finite set is called locally finite or a causet.

A poset with a bounding countable subset is called σ\sigma-bounded. That is, the poset is σ\sigma-bounded above if there exists a sequence (x n) n=1 N(x_n)_{n=1}^{N} (where NN is a natural number or infinity) such that for every yy in the poset there is an x mx_m with yx my \leq x_m. (The poset is σ\sigma-bounded below if we have x myx_m \leq y instead.) Note that every bounded poset is σ\sigma-bounded, but not conversely. Note that some authorities require N=N = \infty; this makes a difference only for the empty poset (we say it is σ\sigma-bounded, they say it is not).

In higher category theory

A poset can be understood as a (0,1)-category. This suggests an obvious vertical categorification of the notion of poset to that of n-poset.


Extension to linear order


On a finite set, every partial order may be extended to a linear order.

For non-finite sets this still holds with the axiom of choice.

See at linear extension of a partial order this Prop..

Locales from posets – Alexandroff topology


For PP a poset, write Up(P)Up(P) for the topological space whose underlying set is the underlying set of PP and whose open subsets are the upward closed subsets of PP: those subsets UPU \subset P with the property that

((xU)and(xy))(yU). ((x \in U) and (x \leq y)) \Rightarrow (y \in U) \,.

This is called the Alexandroff topology on PP.


This construction naturally extends to a full and faithful functor.

Up:Up : Poset \to Top \to Locale.


For PP a poset, there is a natural equivalence

Sh(Up(P))[P,Set] Sh(Up(P)) \simeq [P,Set]

between the category of sheaves on the locale Up(P)Up(P) and the category of copresheaves on PP.

For more see Alexandroff topology.

Cauchy completion

Every poset is a Cauchy complete category. Posets are the Cauchy completions of prosets. (Rosolini)

In univalent universes

In homotopy type theory, every type with a partial order in a univalent universe is a poset. (Tosun, Ahrens, North, Shulman, Tsementzis)



Cauchy completion of prosets and posets is discussed in

  • G. Rosolini, A note on Cauchy completeness for preorders (pdf)

Here are some references on directed homotopy theory:

  • Marco Grandis, Directed homotopy theory, I. The fundamental category (arXiv)

  • Tim Porter, Enriched categories and models for spaces of evolving states, Theoretical Computer Science, 405, (2008), pp. 88–100.

  • Tim Porter, Enriched categories and models for spaces of dipaths. A discussion document and overview of some techniques (pdf)

Posets in univalent universes in homotopy type theory are discussed in

  • Ayberk Tosun, Formal Topology in Univalent Foundations pdf

  • Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle (abs:2102.06275)

On posets that are cofibrant objects in the Thomason model structure:

Last revised on October 1, 2023 at 11:38:18. See the history of this page for a list of all contributions to it.