Supremum is Coproduct in Order Category
Jump to navigation
Jump to search
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$