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 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.
A poset may be understood as a set with extra structure.
Given a set , a partial order on is a (binary) relation with the following properties:
reflexivity: always;
transitivity: if , then ;
antisymmetry: if , then .
A poset is a set equipped with a partial order.
A poset is precisely a proset satisfying the extra condition that implies that .
In dependent type theory, the identity type 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 and the condition :
A partial order is a preorder with an equivalence of types for all and .
Equivalently, one could inductively define a function
on reflexivity of the identity type by reflexivity of the preorder
Then, a partial order is a preorder such that the defined function is an equivalence of types for all and .
In either case, since the preorder is valued in propositions, the antisymmetry axiom ensures that the partial order is an h-set.
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 , there is at most one morphism from to
if there is a morphism from to and a morphism from to (which by the above implies that and are isomorphic), then .
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 and imply , 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.)
The morphisms of partially ordered sets are monotone functions; a monotone function from a poset to a poset is a function from to (seen as structured sets) that preserves :
Equivalently, it is a functor from to (seen as certain categories).
In this way, posets form a category Pos.
A (closed bounded) interval in a poset is a set of the form
A poset is locally finite if every closed bounded interval is finite.
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 is a finite set is called locally finite or a causet.
A poset with a bounding countable subset is called -bounded. That is, the poset is -bounded above if there exists a sequence (where is a natural number or infinity) such that for every in the poset there is an with . (The poset is -bounded below if we have instead.) Note that every bounded poset is -bounded, but not conversely. Note that some authorities require ; this makes a difference only for the empty poset (we say it is -bounded, they say it is not).
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.
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..
For a poset, write for the topological space whose underlying set is the underlying set of and whose open subsets are the upward closed subsets of : those subsets with the property that
This is called the Alexandroff topology on .
For a poset, there is a natural equivalence
between the category of sheaves on the locale and the category of copresheaves on .
For more see Alexandroff topology.
Every poset is a Cauchy complete category. Posets are the Cauchy completions of prosets. (Rosolini)
In homotopy type theory, every type with a partial order in a univalent universe is a poset. (Tosun, Ahrens, North, Shulman, Tsementzis)
Let be the category of finite posets and order-preserving functions, and let be the category of finite distributive lattices and lattice homomorphisms. These are contravariantly equivalent, thanks to the presence of an ambimorphic object:
Proposition. The opposite category of is equivalent to :
One direction of this equivalence is given by the hom-functor
where is the 2-element poset with and for any , is the distributive lattice of poset morphisms from to . The other direction is given by
where is the 2-element distributive lattice and for any , is the poset of distributive lattice morphisms from to .
This Birkhoff duality is (in one form or another) mentioned in many places; the formulation in terms of hom-functors may be found in
The functorial nature of the correspondence means that morphisms of finite posets (i.e. order-preserving maps) naturally correspond to morphisms of finite distributive lattices (i.e. order-preserving maps that also respect meet and join).
It follows from Birkhoff’s representation theorem that every finite distributive lattice can be seen as a lattice of sets (i.e. sets with join and meet given by union and intersection) – in particular, sets whose elements are the join-irreducible elements of the lattice. Furthermore, a good intuition for why this duality holds is that either an element is generated as the join of existing elements, or it is join-irreducible. Hence given any existing poset, we can simply add all missing joins, and also a bottom (i.e. the nullary join). By general results (the adjoint functor theorem for posets) this suffices to ensure that all meets exist as well. This is analogous to the free colimit completion of a category, and indeed Birkhoff representation can be seen as a very special case of the Yoneda lemma as applied to (0,1)-category theory (i.e., order theory), since (0,1)-presheaves are functors into Bool rather than Set and hence correspond to lower sets.
Birkhoff duality does not hold for infinite posets.
The function algebra of rational-valued functions on any set is a partial order.
The function algebra of Cauchy real-valued functions on is a partial order. In fact, it is the Cauchy completion of the function algebra of rational-valued functions on .
More generally, if is a vector space on the rational numbers with a quadratic form, then is a partial order, and its Cauchy completion is a vector space of same dimension on the Cauchy real numbers with a quadratic form. In particular, the Cauchy complex numbers and the Gaussian rationals are partial orders.
In a logic with implications, the set of propositions is partially ordered with respect to the implication as a relation.
Cauchy completion of prosets and posets is discussed in
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:
Roman Bruckner, Christoph Pegel, Cofibrant objects in the Thomason Model Structure, [arXiv:0808.4108]
Roman Bruckner, Abstract Homotopy Theory and the Thomason Model Structure, PhD thesis, Bremen 2016 [gbv:46-00105527-15, pdf]
On the Birkhoff duality between finite posets and finite distributive lattices
Garrett Birkhoff, Rings of sets. Duke Mathematical Journal, 3(3):443–454, 1937.
Bas Spitters, Cubical sets and the topological topos (arXiv:1610.05270)
Last revised on April 11, 2025 at 01:13:54. See the history of this page for a list of all contributions to it.