Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 10.2.3.14 (Uniqueness of Images). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}})$ spanned by those $2$-simplices

\[ \xymatrix@R =50pt@C=50pt{ & Y_0 \ar [dr]^{i} & \\ X \ar [ur]^{q} \ar [rr]^{f} & & Y } \]

which exhibit $Y_0$ as an image of $f$ (see Remark 10.2.3.3). Then the restriction functor

\[ D: \operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \quad \quad \sigma \mapsto d^{2}_{1}( \sigma ) \]

is a trivial Kan fibration from $\operatorname{Fun}'(\Delta ^2, \operatorname{\mathcal{C}})$ to the full subcategory $\operatorname{Fun}'( \Delta ^1, \operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$ spanned by those morphisms $f: X \rightarrow Y$ which admit an image in $\operatorname{\mathcal{C}}$.

Proof. Combining Lemma 10.2.3.10 with Theorem 9.1.8.2, we deduce that the functor $D$ is fully faithful, and therefore induces an equivalence from $\operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}})$ to the full subcategory $\operatorname{Fun}'(\Delta ^1, \operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$. To complete the proof, it will suffice to show that $D$ is an isofibration (Proposition 4.5.5.20). This follows from Corollary 4.4.5.3, since $\operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}})$ is a replete subcategory of $\operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}})$ (see Corollary 10.2.2.12 and Remark 9.2.4.24). $\square$