Supremum is Coproduct in Order Category

Theorem

Let $\mathbf P$ be an order category with ordering $\preceq$.

Let $p, q \in P_0$, and suppose they have some supremum $r = \sup \left\{{p, q}\right\}$.

Then $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.

Proof

Let $\mathbf P^{\text{op}}$ be the dual category of $\mathbf P$.

From Dual of Order Category, it is the order category corresponding to the dual ordering $\succeq$.

From Dual Pairs (Order Theory), it follows that in $\mathbf P^{\text{op}}$:

$r = \inf \left\{{p, q}\right\}$

where $\inf$ denotes infimum.

By Infimum is Product in Order Category, $r$ is the product of $p$ and $q$ in $\mathbf P^{\text{op}}$.

By Dual Pairs (Category Theory), $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.

$\blacksquare$

Also see

• Infimum is Product in Order Category, the dual result

Sources

• 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous): $\S 3.2$: Example $3.7$