Slice Category of Order Category

Theorem

Let $\mathbf P$ be a order category, and denote its ordering by $\preceq$.

Let $p \in \mathbf P_0$ be an object of $\mathbf P$.

Then:

$\mathbf P \mathbin / p \cong p^\preceq$

where:

$\mathbf P \mathbin / p$ is the slice of $\mathbf P$ over $p$

$p^\preceq$ is the order category defined by the weak lower closure of $p$.

The objects of $\mathbf P \mathbin / p$ are morphisms $q \to p$ of $\mathbf P$.

The morphisms are $q \to r$ fitting into a commutative diagram:

$\quad\quad \begin{xy}\xymatrix@C=1em{ q \ar[rr] \ar[rd] & & r \ar[ld] \\ & p }\end{xy}$

Define a functor $U: \mathbf P \mathbin / p \to \mathbf P$ by:

$U \left({q \to p}\right) := q$

$U \left({q \to r}\right) := q \to r$

Because there is at most one morphism $q \to p$ for each $q$, $U$ is injective on objects.

That $U$ is faithful is trivial.

That is, $\mathbf P \mathbin / p$ is isomorphic to the image of $U$.

Now the objects of the image of $U$ in $\mathbf P$ are those $q$ such that $q \preceq p$.

That is, the image of $U$ has as objects $p^\preceq$.

By Commutative Diagram in Preorder Category, every morphism $q \to r$ in $p^\preceq$ fits into a commutative triangle as above.

Thus all morphisms of $p^\preceq$ are in the image of $U$, so that $p^\preceq$ is precisely the image of $U$.

Hence the result.

$\blacksquare$