Kerodon

Proof. We will show that $\widetilde{h}$ satisfies the hypotheses of Variant 8.4.6.9:

$(0)$

The $\infty $-category $\widehat{\operatorname{\mathcal{C}}}_{ / f }$ is $\mathbb {K}$-cocomplete: that is, it admits $K$-indexed colimits, for each $K \in \mathbb {K}$. This follows from Corollary 7.1.4.21, since the $\infty $-category $\widehat{\operatorname{\mathcal{C}}}$ is $\mathbb {K}$-cocomplete.

$(1)$

The functor $\widetilde{h}$ is fully faithful. This is a special case of Remark 4.6.2.7, since the diagram (8.60) is a categorical pullback square and the functor $h$ is fully faithful.

$(2)$

Choose an uncountable regular cardinal $\kappa $ such that $\widehat{\operatorname{\mathcal{C}}}$ and $\widehat{\operatorname{\mathcal{C}}}_{/f}$ are locally $\kappa $-small, and each simplicial set $K \in \mathbb {K}$ is essentially $\kappa $-small. Choose an object $\widetilde{C} \in \widetilde{\operatorname{\mathcal{C}}}$ having image $C \in \operatorname{\mathcal{C}}$, and let

\[ \mathscr {F}: \widehat{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\mathcal{S}}^{< \kappa } \quad \quad \widetilde{\mathscr {F}}: \widehat{\operatorname{\mathcal{C}}}_{/f} \rightarrow \operatorname{\mathcal{S}}^{< \kappa } \]

be functors corepresented by the objects $X = h(C)$ and $\widetilde{X} = \widetilde{h}( \widetilde{C} )$, respectively. For every simplicial set $K \in \mathbb {K}$, the functor $\mathscr {F}$ preserves $K$-indexed colimits, and we must show that $\widetilde{ \mathscr {F} }$ has the same property. Choose a colimit diagram $\widetilde{g}: K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{C}}}_{/f}$; we wish to show that $\widetilde{\mathscr {F}} \circ \widetilde{g}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{S}}^{< \kappa }$. Let $g: K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{C}}}$ denote the composition of $\widetilde{g}$ with the projection map. Then $g$ is a colimit diagram in $\widehat{\operatorname{\mathcal{C}}}$ (Corollary 7.1.4.21), so $\mathscr {F} \circ g$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{S}}^{< \kappa }$. Define

\[ \operatorname{\mathcal{E}}= K^{\triangleright } \times _{ \widehat{\operatorname{\mathcal{C}}} } \widehat{\operatorname{\mathcal{C}}}_{X/} \quad \quad \widetilde{\operatorname{\mathcal{E}}} = K^{\triangleright } \times _{ \widehat{\operatorname{\mathcal{C}}} } \widehat{\operatorname{\mathcal{C}}}_{X/}. \]

Using Proposition 5.6.6.21, we see that $\mathscr {F} \circ g$ and $\widetilde{\mathscr {F}} \circ \widetilde{g}$ are covariant transport representations for the left fibrations $\operatorname{\mathcal{E}}\rightarrow K^{\triangleleft }$ and $\overline{\operatorname{\mathcal{E}}} \rightarrow K^{\triangleleft }$, respectively. Our assumption that $\mathscr {F} \circ g$ is a colimit diagram guarantees that the inclusion map $K \times _{ K^{\triangleleft } } \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}$ is left cofinal, and we wish to show that the inclusion map $K \times _{ K^{\triangleleft } } \widetilde{\operatorname{\mathcal{E}}} \hookrightarrow \widetilde{\operatorname{\mathcal{E}}}$ is also left cofinal (Corollary 7.4.3.14). This follows from Proposition 7.2.3.12, since the tautological map $\widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}$ is a pullback of the projection map $(\widehat{\operatorname{\mathcal{C}}}_{X/})_{/f} \rightarrow \widehat{\operatorname{\mathcal{C}}}_{X/}$, and therefore a right fibration (Proposition 4.3.6.1).

$(3)$

Let $\widehat{\operatorname{\mathcal{C}}}'_{/f}$ denote the smallest replete full subcategory of $\widehat{\operatorname{\mathcal{C}}}_{/f}$ which contains the essential image of $\widetilde{h}$ and is closed under the formation of $K$-indexed colimits for $K \in \mathbb {K}$. We wish to show that $\widehat{\operatorname{\mathcal{C}}}'_{/f} = \widehat{\operatorname{\mathcal{C}}}_{/f}$. Let $\widehat{\operatorname{\mathcal{C}}}' \subseteq \widehat{\operatorname{\mathcal{C}}}$ denote the full subcategory spanned by those objects $X \in \widehat{\operatorname{\mathcal{C}}}$ having the property that every object $\widetilde{X} \in \widehat{\operatorname{\mathcal{C}}}_{/f}$ lying over $X$ belongs to $\widehat{\operatorname{\mathcal{C}}}_{/f}^{0}$. We will complete the proof by showing that $\widehat{\operatorname{\mathcal{C}}}' = \widehat{\operatorname{\mathcal{C}}}$. Since the diagram (8.60) is a categorical pullback square, $\widehat{\operatorname{\mathcal{C}}}'$ contains the essential image of the functor $h$. It will therefore suffice to show that $\widehat{\operatorname{\mathcal{C}}}'$ is closed under the formation of $K$-indexed colimits, for each $K \in \mathbb {K}$. Fix a colimit diagram $g: K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{C}}}$ carrying the cone point of $K^{\triangleright }$ to an object $X \in \widehat{\operatorname{\mathcal{C}}}$. Assume that $g|_{K}$ factors through $\widehat{\operatorname{\mathcal{C}}}'$; we wish to show that $X$ also belongs to $\widehat{\operatorname{\mathcal{C}}}'$. Let $\widetilde{X}$ be an object of $\widehat{\operatorname{\mathcal{C}}}_{/f}$ lying over $X$. Since the inclusion of the cone point into $K^{\triangleright }$ is right anodyne (Example 4.3.7.11), we can lift $g$ to a diagram $\widetilde{g}: K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{C}}}_{/f}$ carrying the cone point to $\widetilde{X}$ (Proposition 4.2.4.5). The assumption that $g|_{K}$ factors through $\widehat{\operatorname{\mathcal{C}}}'$ guarantees that $\widetilde{g}|_{K}$ factors through $\widehat{\operatorname{\mathcal{C}}}_{/f}^{0}$. Since $g$ is a colimit diagram, $\widetilde{g}$ is also a colimit diagram (Corollary 7.1.4.21). It follows that $\widetilde{X}$ belongs to $\widehat{\operatorname{\mathcal{C}}}'_{/f}$. Allowing the object $\widetilde{X}$ to vary, we conclude that $X$ belongs to $\widehat{\operatorname{\mathcal{C}}}'$, as desired.