The notion of final $(\infty,1)$-functor (also called a cofinal $(\infty,1)$-functor) is the generalization of the notion of final functor from category theory to (∞,1)-category-theory.
An (∞,1)-functor $p : K' \to K$ is final precisely if precomposition with $p$ preserves (∞,1)-colimit:
if $p$ is final then for $F : K \to C$ any (∞,1)-functor we have
when either of these (∞,1)-colimits exist.
(final morphism of simplicial set)
A morphism $p : S \to T$ of simplicial sets is final if for every right fibration $X \to T$ the induced morphism of simplicial sets
is a homotopy equivalence.
So in the overcategory $sSet/T$ a final morphism is an object such that morphisms out of it into any right fibration are the same as morphisms out of the terminal object into that right fibration.
This definition is originally due to Andre Joyal. It appears as HTT, def 4.1.1.1.
This is equivalent to the following definition, in terms of the model structure for right fibrations:
The morphism $p : S \to T$ is final precisely if the terminal morphism $(p \to *) = \left( \array{ S &&\to&& T \\ & {}_{\mathllap{}}\searrow && \swarrow_{=} \\ && T } \right)$ in the overcategory $sSet_T$ is a weak equivalence in the model structure for right fibrations on $sSet_T$.
This is HTT, prop. 4.1.2.5.
If $T$ is a Kan complex then $p : S \to T$ is final precisely if it is a weak equivalence in the standard model structure on simplicial sets.
This is HTT, cor. 4.1.2.6.
(preservation of undercategories and colimits)
A morphism $p : K' \to K$ of simplicial sets is final precisely if for every quasicategory $C$
and equivalently precisely if
… and for every $F : K \to C$ the morphism
of under quasi-categories induced by composition with $p$ is an equivalence of (∞,1)-categories.
This is HTT, prop. 4.1.1.8.
The following result is the $(\infty,1)$-categorical analog of what is known as Quillen’s Theorem A.
(recognition theorem for final $(\infty,1)$-functors)
A morphism $p : K \to C$ of simplicial sets with $C$ a quasi-category is final precisely if for each object $c \in C$ the comma-object $c/p := c/C \times_C K$ is weakly contractible.
More explicitly, the comma object in question here is the pullback
where $c/C$ is the under quasi-category under $c$.
This is due to Andre Joyal. A proof appears as HTT, prop. 4.1.3.1.
The following says that up to equivalence, the cofinal maps of simplicial sets are the right anodyne morphisms
A map of simplicial sets is cofinal precisely if it factors as a right anodyne map followed by a trivial fibration.
This is (Lurie, cor. 4.1.1.12).
The inclusion $\ast \to \mathcal{C}$ of a terminal object is final.
By theorem the inclusion of the point is final precisely if for all $c \in \mathcal{C}$, the (∞,1)-categorical hom-space $\mathcal{C}(c,\ast)$ is contractible. This is the definition of $\ast$ being terminal.
A (weak) localization $f: \mathcal{C} \to \mathcal{D}$ is both initial and final.
This appears, for example, as (Cisinski, 7.1.10).
Consider the inclusion of the walking span-category, into the result of adjoining an initial object $t$:
One readily sees that for each object on the right, its comma category over this inclusion has contractible nerve, whence Theorem implies that this inclusion is a final $\infty$-functor.
As an application of the finality of (1), observe that for $\mathcal{C}$ an (∞,1)-category and $T \in \mathcal{C}$ an object, (∞,1)-colimits in the under-(∞,1)-category
are given by the $\infty$-colimit in $\mathcal{C}$ itself of the given cone of the original diagram, with tip $X$ (by this Prop.): For
a small diagram, we have
(when either $\infty$-colimit exists).
Now for $\mathcal{I}$ the walking span diagram on the left of (1), this means that homotopy cofiber products in $\mathcal{C}^{T/}$ are computed as $\infty$-colimits in $\mathcal{C}$ of diagrams of the shape on the right of (1). But since the inclusion in (1) is final, these are just homotopy cofiber products in $\mathcal{C}$.
Explicitly: Given
regarded as a span in $\mathcal{C}^T$, hence with underlying objects
we have:
In particular, if $(B,\phi_B) \;\coloneqq\; (T,id_T)$ is the initial object in $\mathcal{C}^{T/}$, in which case the cofiber product is just the coproduct
we find that the coproduct in the co-slice category is the co-fiber product under the given tip object in the underlying category
For $K \in$ sSet a simplicial set, write $\Delta_{/K}$ for its category of elements, called here the category of simplices of the simplicial set:
an object of $\Delta_{/K}$ is a morphism of simplicial sets of the form $\Delta^n \to K$ for some $n \in \mathbb{N}$ (hence an $n$-simplex of $K$) and a morphism is a commuting diagram
Moreover, write
for the non-full subcategory on the non-degenerate simplices.
When the simplicial set $K$ is non-singular, i.e. every face of a non-degenerate simplex is still non-degenerate, then the category $\Delta_{/K}^{nd}$ is a poset and it coincides with the barycentric subdivision of $K$.
Suppose $K$ is a non-singular simplicial set. Then the inclusion
is a cofinal morphism of quasi-categories.
This appears as (Lurie, variant 4.2.3.15).
For every simplicial set $K$ there exists a cofinal map
This is (Lurie, prop. 4.2.3.14).
If the simplicial set $K$ is singular, it is not in general true that the inclusion $N(\Delta_{/K}^{nd}) \hookrightarrow N(\Delta_{/K})$ is final. For a counter-example, see (Hovey, 9).
For every simplicial set $K$, evaluation at the initial vertex
is both initial and final.
This appears as (Shah, 12.2) and also follows from the fact that this map is a weak localization (Cisinski, 7.3.15).
This can be used to establish a Bousfield-Kan formula for homotopy colimits; see (Shah, 12.3).
final $(\infty,1)$-functor
Section 4.1 of
Section 6 of
Dan Dugger, A primer on homotopy colimits (pdf)
Mark Hovey, item 9 of Errata to Model Categories (pdf)
Jay Shah Parametrized higher categories and higher algebra: Expose II- Indexed homotopy limits and colimits.
Denis-Charles Cisinski Higher Categories and Homotopical Algebra.
Last revised on July 3, 2020 at 10:37:52. See the history of this page for a list of all contributions to it.