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$.
Proof
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.
Hence by Functor is Embedding iff Faithful and Injective on Objects, $U$ is an embedding.
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$
Sources
- 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous) ... (next): $\S 1.6.4$