Pos.yaml

id: Pos
name: category of posets
notation: $\Pos$
objects: partially ordered sets (aka posets), i.e. sets equipped with a reflexive, transitive, antisymmetric relation
morphisms: order-preserving functions
description: Even though there are many similarities with $\Prost$, the main difference is that the forgetful functor $\Pos \to \Set$ has no right adjoint.
nlab_link: https://ncatlab.org/nlab/show/Pos

tags:
  - order theory

related:
  - FinOrd
  - Prost

satisfied_properties:
  - property: locally small
    proof: There is a forgetful functor $\Pos \to \Set$ and $\Set$ is locally small.

  - property: locally finitely presentable
    proof: See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Example 1.10.

  - property: cartesian closed
    proof: For posets $P,Q$ we endow $\Hom(P,Q)$ with the partial order in which $f \leq g$ holds iff $f(p) \leq g(p)$ for all $p \in P$. The universal evaluation map is $\Hom(P,Q) \times P \to Q$, $(f,p) \mapsto f(p)$, it is order-preserving, and it satisfies the universal property.

  - property: semi-strongly connected
    proof: Every non-empty poset is weakly terminal (by using constant maps).

  - property: generator
    proof: The singleton poset $1$ is a generator, since morphisms $1 \to P$ correspond to the elements of $P$.

  - property: cogenerator
    proof: 'We prove that the poset $\{0 < 1\}$ is a cogenerator: Let $P$ be a poset and $a,b \in P$ be two elements such that $f(a) = f(b)$ for all order-preserving maps $f : P \to \{0 < 1 \}$. This means that $a$ and $b$ lie in the same upper sets. In particular, $b$ lies in the upper set generated by $a$, meaning $a \leq b$, and similarly we deduce $b \leq a$. Thus, $a = b$.'

  - property: infinitary extensive
    proof: '[Sketch] Since <a href="/category/Set">$\Set$</a> is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.'

  - property: coregular
    proof: See <a href="https://math.stackexchange.com/questions/5130295" target="_blank">MSE/5130295</a>.

unsatisfied_properties:
  - property: skeletal
    proof: This is trivial.

  - property: balanced
    proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$).

  - property: regular
    proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.

  - property: Malcev
    proof: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.'

  - property: co-Malcev
    proof: 'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \Pos \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton poset and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.'

  - property: regular subobject classifier
    proof: Assume that there is a regular subobject classifier $\Omega$, so that (by the classification of regular monomorphisms) $\Hom(P,\Omega)$ is isomorphic to the set of subsets of $P$. By taking $P = \{0\}$ we see that $\Omega$ has $2$ elements, so that either $\Omega \cong \{0,1\}$ (discrete) or $\Omega \cong \{0 < 1\}$. By taking $P = \{0 < 1\}$ we see that $\Omega$ has four pairs $(x,y)$ with $x \leq y$. But $\{0,1\}$ has only two and $\{0 < 1\}$ has only three such pairs.

  - property: cofiltered-limit-stable epimorphisms
    proof: Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.

  - property: effective cocongruences
    proof: |-
      Let $X$ be $\IR$ with the standard (total) order, and let $E$ be the poset with underlying set $\IR \times \{ 0, 1 \}$ and partial order such that $(x, m) \le (y, n)$ if and only if $x < y$ or $(x, m) = (y, n)$. The two maps $\IR \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\IP, \le)$, the induced equivalence relation on the set of order-preserving functions $\IR \to \IP$ is that $f \sim g$ if and only if $f(x) \le g(y)$ and $g(x) \le f(y)$ whenever $x < y$. This relation is clearly reflexive and symmetric; for transitivity, if $f \sim g$ and $g \sim h$, then whenever $x < y$, we have $f(x) \le g(\frac{x+y}{2}) \le h(y)$ and similarly $h(x) \le g(\frac{x+y}{2}) \le f(y)$, showing that $f \sim h$.
      On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of <a href="/content/effective-congruence-quotients">this result</a>, $E$ would be the cokernel pair of the equalizer of the two maps $\IR \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.

special_objects:
  initial object:
    description: empty poset
  terminal object:
    description: singleton poset
  coproducts:
    description: disjoint union with the obvious partial order that leaves the distinct summands incomparable
  products:
    description: direct products with the evident partial order

special_morphisms:
  isomorphisms:
    description: bijective functions that are order-preserving and order-reflecting
    proof: This is easy.
  monomorphisms:
    description: injective order-preserving functions
    proof: The same proof as for <a href="/category/Set">$\Set$</a> can be used.
  epimorphisms:
    description: surjective order-preserving functions
    proof: 'Clearly, surjective maps are epimorphisms. Conversely, assume that $f : P \to Q$ is an order-preserving map which is not surjective. Choose $q \in Q \setminus f(P)$. The order-preserving maps $Q \to \{0 < 1\}$ correspond to the upper sets in $Q$, and composing them with $f$ corresponds to taking their $f$-preimages. Consider the two upper sets $Q_{> q}$ and $Q_{\geq q}$. Their $f$-preimages are the same since $q \notin f(P)$. Therefore, $f$ is not an epimorphism.'
  regular monomorphisms:
    description: embeddings
    proof: 'Every regular monomorphism is an embedding by the explicit construction of equalizers. For the converse, let $i : P \to Q$ be an embedding, which we may assume to be an inclusion. Consider the cokernel pair $C \coloneqq Q \cup_P Q$. It exists because the category has pushouts, but we can (and need to) describe it more concretely: As a set, $C$ is a disjoint union of $P$ and two copies of $Q \setminus P$. The elements will be denoted by $p,q_1,q_2$. The $i$th inclusion map $Q \to C$ maps $p \in P$ to itself and $q \in Q \setminus P$ to $q_i$. The ordering is directly induced by $Q$: We have $p \leq p''$ in $C$ iff $p \leq p''$ in $P$, we have $p \leq q_i$ iff $p \leq q$ in $Q$, etc. One verifies that this indeed defines a partial order, and by construction the two maps $Q \rightrightarrows C$ are order-preserving and have equalizer $P$.'