Kerodon

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

Proposition 4.4.3.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty$-categories. Then the induced map $F^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$ is a Kan fibration.

Proof. Fix integers $n > 0$ and $0 \leq i \leq n$; we wish to show that every lifting problem

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{i} \ar [r]^-{\sigma _0} \ar [d] & \operatorname{\mathcal{C}}^{\simeq } \ar [d]^{F^{\simeq }} \\ \Delta ^ n \ar [r]^-{\overline{\sigma }} \ar@ {-->}[ur]^{\sigma } & \operatorname{\mathcal{D}}^{\simeq } }$

admits a solution. In the case $n=1$, this follows either from our definition of isofibration (in the case $i=1$) or from Corollary 4.4.1.8 (in the case $i=0$). We may therefore assume that $n \geq 2$. We claim that $\sigma _0$ can be extended to an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ satisfying $F(\sigma ) = \overline{\sigma }$. If $0 < i < n$, this follows from the fact that $F$ is an inner fibration. The extremal cases $i=0$ and $i=n$ follow from Proposition 4.4.2.13 (applied to the inner fibration $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and its opposite $F^{\operatorname{op}}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}}$). To complete the proof, it will suffice to show that $\sigma$ carries each edge of $\Delta ^ n$ to an isomorphism in $\operatorname{\mathcal{C}}$. For $n > 2$, this is automatic (since the horn $\Lambda ^{n}_{i}$ contains every edge of $\Delta ^ n$). In the case $n=2$ it follows from the two-out-of-three property for isomorphisms in $\operatorname{\mathcal{C}}$ (Remark 1.4.6.3). $\square$