# Kerodon

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

Theorem 7.2.5.5. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category. Then $\operatorname{\mathcal{C}}$ is filtered (in the sense of Definition 7.2.4.3) if and only if the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is homotopy filtered (in the sense of Definition 7.2.5.1), when regarded as an $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched category by means of Construction 4.6.8.13.

Proof of Theorem 7.2.5.5. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category and suppose that the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is homotopy filtered; we wish to show that $\operatorname{\mathcal{C}}$ is filtered (the reverse implication follows from Lemma 7.2.5.12). By virtue of Lemma 7.2.5.13, it will suffice to show that for every integer $n \geq 0$, every morphism of simplicial sets $f: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{C}}$ can be extended to a morphism $\overline{f}: (\operatorname{\partial \Delta }^ n)^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. For $n = 0$, this follows from our assumption that $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is nonempty. We will therefore assume that $n > 0$. By virtue of Lemma 7.2.5.15, we may assume without loss of generality that the restriction $f_{-} = f|_{ \Delta ^{n-1} }$ is the constant map taking the value $X$ for some object $X \in \operatorname{\mathcal{C}}$. Set $Y = f(n)$ and let $\operatorname{Hom}_{\operatorname{\mathcal{C}}}^{\mathrm{R}}(X,Y) = \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Y}$ denote the right-pinched morphism space of Construction 4.6.5.1, so that we can identify $f|_{ \Lambda ^{n}_{n} }$ with a morphism of simplicial sets $g: \operatorname{\partial \Delta }^{n-1} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}^{\mathrm{R}}(X,Y)$. Invoking assumption $(\ast _ n)$ of Definition 7.2.5.1, we deduce that there exists a morphism $v: Y \rightarrow Z$ in $\operatorname{\mathcal{C}}$ for which the composite map

$\operatorname{\partial \Delta }^{n-1} \xrightarrow {g} \operatorname{Hom}_{\operatorname{\mathcal{C}}}^{\mathrm{R}}(X,Y) \hookrightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \xrightarrow {[v] \circ } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z)$

is nullhomotopic. Since the projection map $\operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/Y}$ is a trivial Kan fibration (Corollary 4.3.6.13), we can lift $g$ to a morphism $\widetilde{g}: \operatorname{\partial \Delta }^{n-1} \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f}$. Combining Propositions 5.2.8.7 and 4.6.8.16, we deduce that the diagram of Kan complexes

$\xymatrix@R =50pt@C=50pt{ \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Y} \ar [d]^{\iota _{X,Y}^{\mathrm{R}}} & \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \ar [r] \ar [l] & \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z} \ar [d]^{\iota ^{\mathrm{R}}_{X,Z}} \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \ar [rr]^{[v] \circ } & & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) }$

commutes up to homotopy, where $\iota _{X,Y}^{\mathrm{R}}$ and $\iota _{X,Z}^{\mathrm{R}}$ are the right-pinch inclusion morphisms of Construction 4.6.5.6. Since $\iota ^{\mathrm{R}}_{X,Z}$ is a homotopy equivalence (Proposition 4.6.5.9), it follows that the composite map $\operatorname{\partial \Delta }^{n-1} \xrightarrow {\widetilde{g}} \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/Z}$ is nullhomotopic, and can therefore be extended to an $(n-1)$-simplex $g': \Delta ^{n-1} \rightarrow \operatorname{\mathcal{C}}_{/Z}$ (Proposition 3.2.6.11). Unwinding the definitions, we can identify $\widetilde{g}$ and $g'$ with morphisms $(\Lambda ^{n}_{n})^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ and $( \Delta ^{n-1 })^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$, which can be amalgamated to a single morphism $\overline{f}: ( \operatorname{\partial \Delta }^{n} )^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ extending $f$. $\square$