nLab preorder

Redirected from "proset".
Contents

Context

(0,1)(0,1)-Category theory

Graph theory

Relations

Homotopy type theory

Contents

Idea

A preorder or a quasi-order is like a partial order, but without the “antisymmetry” requirement that xyx \leq y and yxy \leq x implies x=yx = y.

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

Definition

As a set with a relation

A preorder or quasiorder on a set SS is a reflexive and transitive relation, generally written \leq. A preordered set, or proset, is a set equipped with a preorder. (This should not be confused with a pro-set, i.e. a pro-object in Set.)

As a graph

A preordered set is a loop digraph (V,E,s:EV,t:EV)(V, E, s:E \to V, t:E \to V), with functions refl:VErefl:V \to E and

tr:{(f,g)E×E|t(f)= Vs(g)}Etr:\{(f,g) \in E \times E \vert t(f) =_V s(g)\} \to E

such that

  • for every aVa \in V, s(refl(a))= Eas(refl(a)) =_E a
  • for every aVa \in V, t(refl(a))= Eat(refl(a)) =_E a
  • for every fEf \in E, s(tr(g,f))= Es(f)s(tr(g,f)) =_E s(f)
  • for every fEf \in E, t(tr(g,f))= Et(g)t(tr(g,f)) =_E t(g)
  • for every fEf \in E, tr(f,refl(s(f)))= Eftr(f, refl(s(f))) =_E f
  • for every fEf \in E, tr(refl(t(f)),f)= Eftr(refl(t(f)), f) =_E f
  • for every fEf \in E, gEg \in E, and hEh \in E such that t(f)= Vs(g)t(f) =_V s(g) and t(g)= Vs(h)t(g) =_V s(h), tr(h,tr(g,f))= Etr(tr(h,g),f)tr(h,tr(g,f)) =_E tr(tr(h,g),f)

As a category

Equivalently, a preordered set is a (strict) thin category: a strict category such that for any pair of objects x,yx, y, there is at most one morphism from xx to yy. The existence of such a morphism corresponds to the truth of the relation xyx \leq y. In other words, it's a (strict) category enriched over the cartesian monoidal category of truth values (a (0,1)-category).

In homotopy type theory

In homotopy type theory, we must be careful to distinguish preorders (on a homotopy type of arbitrary h-level) and preordered sets (which apply to an h-set). When translating ordinary, set-level mathematics to HoTT, preordered sets are almost always what is wanted. A preorder on a type AA consists of:

  • For each pair of elements a,b:Aa, b : A, a proposition aba \le b;

  • For every a:Aa : A, a witness of reflexivity refl a:aa\operatorname{refl}_a : a \le a

  • For every a,b,c:Aa, b, c : A, p:abp : a \le b and q:bcq : b \le c, a witness of transitivity trans a,b,c(p,q):ac\operatorname{trans}_{a,b,c}(p, q) : a \le c.

Note that, as usual, the quantifiers “for each” and “for every” should be interpreted as applications of the corresponding dependent function types. Every homotopy type AA has an h-set of possible preordered structures, but the sum of all possible structures has h-level bounded by AA‘s.

Properties

Relation to partial orders

Any preordered set is equivalent to a poset. This is a special case of the theorem that every category has a skeleton, but (if you define ‘equivalence’ weakly enough) this case does not require the axiom of choice.

If the foundations have quotient sets, then every preorder has a quotient set equivalent to a poset. Let (P,)(P, \leq) be a preorder. Define the equivalence relation \sim on PP for all elements a,bPa, b \in P as ab:=(ab)(ba)a \sim b := (a \leq b) \wedge (b \leq a). Then the quotient set P/P / \sim is a poset. This is the 0-truncated version of the fact that because every precategory has a core pregroupoid and every pregroupoid has a Rezk completion into a groupoid, every precategory has a Rezk completion into a category.

Note that while in homotopy type theory, preorders can be applied to general types (thus the need for differentiating between preorders and preordered sets), partial orders necessarily apply to sets: Any map p:(ab)(ba)(a=b)p : (a \le b) \wedge (b \le a) \to (a = b) is necessarily a fibrewise equivalence (fixing aa and quantifying over bb), since it induces an equivalence of total spaces. Thus, the codomain type (a=b)(a = b) is a proposition, since the domain (ab)(ba)(a \le b) \wedge (b \le a), being a product of propositions, is a proposition.

Relation to thin categories

In set-theoretic foundations, a preordered set is the same as a thin category (a category in which any two parallel morphisms are equal), and it is partially ordered just when it is skeletal. Thus, asking for a preordered set to be partially ordered may seem to break the principle of equivalence of category theory. However, as remarked above, a thin category always has a skeleton which is a poset; so working with posets up to isomorphism is the same as working with preordered sets up to equivalence. In other words, if xyx \le y and yxy \le x, so that xx and yy are isomorphic, we may as well say that they are equal (since they are isomorphic in only one way).

Another way to say this is that the nerve simplicial set of a preorder, which is necessarily a Segal space or category object in an (infinity,1)-category in SetGrpdSet \hookrightarrow \infty Grpd, is in addition a complete Segal space or genuine category object in SetSet if the preorder is in fact a partial order. For more on this perspective see at Segal space – Examples – In Set.

If we distinguish between isomorphism and equality of elements in a preordered set (hence considering preordered sets up to isomorphism, rather than up to equivalence), then this is equivalent to considering the corresponding thin category to also be a strict category. When treated in this sense, preordered sets are not equivalent to posets.

On the other hand, in non-set-theoretic foundations where not every category need have an underlying set (i.e. need not be a strict category in any canonical way) — such as homotopy type theory or preset theories — a preordered set defined as “a set with a relation \leq …” is automatically a strict category, with a notion of equality of objects coming from the given set. By contrast, in this case a thin category (as opposed to a more general category) does have a canonical structure of strict category in which equality of objects means isomorphism, but not every strict thin category is canonical in this sense. In this case, partially ordered sets correspond to thin categories (with canonical strict-category structures), while preordered sets correspond to thin categories with arbitrary strict-category structures.

Construction of preorders from any binary relation

(See also codensity monad, guarded quantification.)

Theorem

Given sets AA and BB and a binary relation R(x,y)R(x, y) between AA and BB, then the relation

T(x,y)w:B.R(x,w)R(y,w)T(x, y) \coloneqq \forall w:B.R(x, w) \implies R(y, w)

is a preorder on AA.

Proof

We work in dependent type theory, where implication is denoted by the function type PQP \to Q and universal quantification is denoted by the dependent product type x:AP(x)\prod_{x:A} P(x). Thus, the type family T(x,y)T(x, y) is represented as

T(x,y) w:BR(x,w)R(y,w)T(x, y) \coloneqq \prod_{w:B} R(x, w) \to R(y, w)

A binary relation in dependent type theory is a type family x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) such that each R(x,y)R(x, y) is an h-proposition. Since R(x,w)R(x, w) and R(y,w)R(y, w) are both h-propositions, and h-propositions are closed under function types and dependent product types, T(x,y)T(x, y) is also valued in h-propositions, and is a binary relation.

In addition, for all elements x:Ax:A, there is an element

refl T(x): w:BR(x,w)R(x,w)\mathrm{refl}_{T}(x):\prod_{w:B} R(x, w) \to R(x, w)

defined by the identity function on R(x,w)R(x, w)

refl T(x)(w)id R(x,w)\mathrm{refl}_{T}(x)(w) \coloneqq \mathrm{id}_{R(x, w)}

and for all elements x:Ax:A, y:Ay:A, and z:Az:A, there is a function

trans T(x,y,z):( w:BR(x,w)R(y,w))×( w:BR(y,w)R(z,w))( w:BR(x,w)R(z,w))\mathrm{trans}_{T}(x, y, z):\left(\prod_{w:B} R(x, w) \to R(y, w)\right) \times \left(\prod_{w:B} R(y, w) \to R(z, w)\right) \to \left(\prod_{w:B} R(x, w) \to R(z, w)\right)

defined by composition of the functions f(w):R(x,w)R(y,w)f(w):R(x, w) \to R(y, w) and g(w):R(y,w)R(z,w)g(w):R(y, w) \to R(z, w) dependent upon element w:Bw:B:

trans T(x,y,z)(f,g)(w)g(w)f(w)\mathrm{trans}_{T}(x, y, z)(f, g)(w) \coloneqq g(w) \circ f(w)

Since the type

w:BR(x,w)R(y,w)\prod_{w:B} R(x, w) \to R(y, w)

is a binary relation valued in h-propositions which satisfies reflexivity and transitivity, it is a preorder.

Preorder reflection

The 2-category of preorders (more precisely, that of thin categories) is reflective in Cat. The reflector preserves the objects and declares xyx \leq y if there exists an arrow from xx to yy.

Cauchy completion

Proposition

Internal to any regular category every poset is a Cauchy complete category.

This appears as (Rosolini, prop. 2.1).

Proposition

Internal to any exact category the Cauchy completion of any preorder exists and is its poset reflection?.

This appears as (Rosolini, corollary. 2.3).

References

Cauchy completion for preorders is discussed in

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

Last revised on December 25, 2023 at 00:59:01. See the history of this page for a list of all contributions to it.