Kerodon

Proof. Combining Example 4.1.2.4, Remark 4.1.2.6, and Remark 4.4.3.2, we deduce that the inclusion map $\operatorname{\mathcal{C}}^{\simeq } \hookrightarrow \operatorname{\mathcal{C}}$ is an inner fibration; in particular, $\operatorname{\mathcal{C}}^{\simeq }$ is an $\infty $-category. The repleteness is immediate from the definition (since $\operatorname{\mathcal{C}}^{\simeq }$ contains every isomorphism in $\operatorname{\mathcal{C}}$). $\square$

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

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$

Proof. The implications $(1) \Rightarrow (2) \Rightarrow (4)$ and $(1) \Rightarrow (3) \Rightarrow (4)$ follow from Example 4.2.1.5, Proposition 4.4.2.11, and Example 4.4.1.11 (and do not require the assumption that $\operatorname{\mathcal{D}}$ is a Kan complex). We will complete the proof by showing that $(4) \Rightarrow (1)$. Our assumption that $\operatorname{\mathcal{D}}$ is a Kan complex guarantees that every morphism in $\operatorname{\mathcal{D}}$ is an isomorphism. Since $q$ is conservative, it follows that every morphism in $\operatorname{\mathcal{C}}$ is an isomorphism. We can therefore identify $q$ with the induced map $q^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$, which is Kan fibration by virtue of Proposition 4.4.3.7. $\square$

Proof. Combine Corollaries 4.4.3.8 and 4.2.3.20. $\square$

Proof. Apply Proposition 4.4.3.7 to the isofibration $\operatorname{\mathcal{C}}\rightarrow \Delta ^{0}$. $\square$

Proof. The assumption that $\operatorname{\mathcal{C}}_0$ is replete guarantees that the inclusion map $\iota : \operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$ is an isofibration (Example 4.4.1.12). Applying Proposition 4.4.3.7, we deduce that the inclusion $\operatorname{\mathcal{C}}_0^{\simeq } \hookrightarrow \operatorname{\mathcal{C}}^{\simeq }$ is a Kan fibration, so that $\operatorname{\mathcal{C}}_0^{\simeq }$ is a summand of $\operatorname{\mathcal{C}}^{\simeq }$ by virtue of Example 3.1.1.4. $\square$

Proof. If $u$ is an isomorphism, then it belongs to the image of the inclusion functor $\operatorname{\mathcal{C}}^{\simeq } \hookrightarrow \operatorname{\mathcal{C}}$. Since the core $\operatorname{\mathcal{C}}^{\simeq }$ is a Kan complex, this proves that $(1) \Rightarrow (2)$. Conversely, if we can write $u = F( \overline{u} )$ for some functor $F: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ where $\operatorname{\mathcal{E}}$ is a Kan complex, then Remark 1.5.1.6 guarantees that $u$ is an isomorphism in $\operatorname{\mathcal{C}}$ (since $\overline{u}$ is automatically an isomorphism in $\operatorname{\mathcal{E}}$, by virtue of Proposition 1.4.6.10). This proves that $(2) \Rightarrow (1)$.

The implication $(3) \Rightarrow (2)$ is immediate. We will complete the proof by showing that $(2)$ implies $(3)$. Let $\operatorname{\mathcal{E}}$ be a Kan complex, let $F: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a functor, and let $\overline{u}$ be an edge of $\operatorname{\mathcal{E}}$ satisfying $F( \overline{u} ) = u$. Let us identify $\overline{u}$ with a morphism of simplicial sets $\Delta ^1 \rightarrow \operatorname{\mathcal{E}}$. By virtue of Proposition 3.1.7.1, this morphism factors as a composition $\Delta ^1 \xrightarrow {v} \operatorname{\mathcal{E}}' \xrightarrow {q} \operatorname{\mathcal{E}}$, where $v$ is anodyne and $q$ is a Kan fibration. Since $\operatorname{\mathcal{E}}$ is a Kan complex and $q$ is a Kan fibration, the simplicial set $\operatorname{\mathcal{E}}'$ is a Kan complex (Remark 3.1.1.11). Because $\Delta ^1$ is weakly contractible and $v$ is a weak homotopy equivalence, the Kan complex $\operatorname{\mathcal{E}}'$ is contractible. We can then write $u = F'(v)$ where $F' = F \circ q$. $\square$

Proof. Let $F: X \rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets. To show that $F$ factors through the core $\operatorname{\mathcal{C}}^{\simeq } \subseteq \operatorname{\mathcal{C}}$, we must show that for every edge $u: x \rightarrow y$ of the Kan complex $X$, the image $F(u)$ is an isomorphism in $\operatorname{\mathcal{C}}$. This follows from Remark 1.5.1.6, since $u$ is automatically an isomorphism in the $\infty $-category $X$ (Proposition 1.4.6.10). $\square$

Proof. Combine Corollary 4.4.3.11 with Proposition 4.4.3.17. $\square$

Proof. Since $q$ is an isofibration, it is an inner fibration. It follows that the morphism $q'$ is also an inner fibration (Remark 4.1.1.5). Since $\operatorname{\mathcal{D}}'$ is an $\infty $-category, the simplicial set $\operatorname{\mathcal{C}}'$ is also an $\infty $-category (Remark 4.1.1.9). This proves $(1)$.

Let $\operatorname{\mathcal{E}}$ denote the fiber product $\operatorname{\mathcal{C}}^{\simeq } \times _{ \operatorname{\mathcal{D}}^{\simeq } } \operatorname{\mathcal{D}}'^{\simeq }$, which we regard as a simplicial subset of $\operatorname{\mathcal{C}}' = \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}'$. It follows from Proposition 4.4.3.7 that $q$ restricts to a Kan fibration $q^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$. The projection map $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}'^{\simeq }$ is a pullback of $q^{\simeq }$, and is therefore also a Kan fibration. Since $\operatorname{\mathcal{D}}'^{\simeq }$ is a Kan complex (Corollary 4.4.3.11), it follows that $\operatorname{\mathcal{E}}$ is a Kan complex (Remark 3.1.1.11). Applying Corollary 4.4.3.18, we deduce that $\operatorname{\mathcal{E}}$ is contained in the core $\operatorname{\mathcal{C}}'^{\simeq } \subseteq \operatorname{\mathcal{C}}'$, which proves that the diagram (4.17) is a pullback square. Since $q^{\simeq }$ is a Kan fibration, it is also a homotopy pullback square (Example 3.4.1.3). This proves assertion $(2)$, and assertion $(3)$ is an immediate consequence.

To complete the proof of $(4)$, it will suffice to show that the morphism $q'$ satisfies condition $(\ast )$ of Definition 4.4.1.4. Let $Y'$ be an object of $\operatorname{\mathcal{C}}'$ and let $\overline{u}': \overline{X}' \rightarrow q'(Y')$ be an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}'$; we wish to show that $\overline{u'}$ can be written as $q'( u')$ for some isomorphism $u': X' \rightarrow Y'$ in the $\infty $-category $\operatorname{\mathcal{C}}'$. By virtue of $(3)$, this is equivalent to showing that $F'(\overline{u}')$ can be written as $q(u)$ for some isomorphism $u: X \rightarrow F(Y)$ in the $\infty $-category $\operatorname{\mathcal{C}}$, which follows from our assumption that $q$ is an isofibration. $\square$

Proof. Apply Corollary 4.4.3.19 in the special case $\operatorname{\mathcal{D}}' = \{ D\} $. $\square$

Proof. Since $q$ is an inner fibration, the simplicial set $\operatorname{\mathcal{C}}_{D}$ is an $\infty $-category (Remark 4.1.1.6). It will therefore suffice to show that every morphism $f$ in $\operatorname{\mathcal{C}}_{D}$ is an isomorphism (Proposition 4.4.2.1). By virtue of Corollary 4.4.3.20, this is equivalent to the requirement that $f$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$. This follows from our assumption that $q$ is conservative, since $q(f) = \operatorname{id}_{D}$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}$. $\square$

Proof of Proposition 4.4.3.22. Let $\sigma : Y \rightarrow \operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq }$ be a morphism of simplicial sets, which we identify with a diagram $F: X \times Y \rightarrow \operatorname{\mathcal{C}}$. To show that $\sigma $ factors through the monomorphism $\theta $, it will suffice to show that $F$ factors through the core $\operatorname{\mathcal{C}}^{\simeq } \subseteq \operatorname{\mathcal{C}}$. Equivalently, we wish to show that for every edge $(u,v): (x,y) \rightarrow (x',y')$ in the product simplicial set $X \times Y$, the morphism $F(u,v): F(x,y) \rightarrow F(x',y')$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$. Note that $F(u,v)$ can be identified with a composition of morphisms

in the $\infty $-category $\operatorname{\mathcal{C}}$. Since the collection of isomorphisms in $\operatorname{\mathcal{C}}$ is closed under composition (Remark 1.4.6.3), it will suffice to show that $F(u,\operatorname{id}_{y} )$ and $F( \operatorname{id}_{x'}, v)$ are isomorphsms in $\operatorname{\mathcal{C}}$. In the first case, this follows from Proposition 4.4.3.17 (applied to the morphism $F|_{ X \times \{ y\} }$), since $X$ is a Kan complex. In the second case, it follows from our assumption that $\sigma $ factors through the core $\operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq } \subseteq \operatorname{Fun}(X,\operatorname{\mathcal{C}})$ (and therefore carries the edge $v: y \rightarrow y'$ to an isomorphism in the diagram $\infty $-category $\operatorname{Fun}(X,\operatorname{\mathcal{C}})$). $\square$