Final functor

A functor $F:\mathcal{C}\to \mathcal{D}$ is final when every comma category $(B\downarrow F)$ is nonempty and connected. Colimits are unchanged after restriction along a final functor.

The finality property of a functor means every required comma category is nonempty and connected. It is the condition defining a final functor; the displayed criterion uses categorical connected components.

Let $F:\mathcal{I}\to \mathcal{J}$ be final and $D:\mathcal{J}\to \mathcal{C}$. A cocone ${\lambda }_i:D(Fi)\to X$ extends uniquely to $D$: for $j\in \mathcal{J}$, choose $(i,u:j\to Fi)$ in $(j\downarrow F)$ and set ${\bar{\lambda }}_j={\lambda }_{i}D(u)$. Connectedness makes this independent of the choice. Consequentlywhenever either side is constructed by this universal property.