Kerodon

Proof. We will prove the first assertion; the second follows by a similar argument. Assume first that $f$ is left anodyne. Then $f$ is a monomorphism (Remark 4.2.4.4). For every left fibration of simplicial sets $\widetilde{B} \rightarrow B$, the restriction map $\theta : \operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B} )$ is a pullback of the map

and is therefore a trivial Kan fibration (Proposition 4.2.5.4). In particular, $u$ is a homotopy equivalence (Proposition 3.1.6.10). Allowing $\widetilde{B}$ to vary, we conclude that $f$ is left cofinal.

We now prove the converse. Assume that $f$ is a left cofinal monomorphism; we wish to show that $f$ is left anodyne. By virtue of Proposition 4.2.4.5, it will suffice to show that every lifting problem

admits a solution, provided that $q$ is a left fibration of simplicial sets. Let us regard the morphism $g$ as fixed, and consider the restriction map

Since $f$ is a monomorphism, the morphism $\theta $ is a left fibration (Proposition 4.2.5.1). Since the target simplicial set $\operatorname{Fun}_{ / B }( A, X \times _{S} B)$ is a Kan complex (Corollary 4.4.2.5), it follows that $\theta $ is a Kan fibration (Corollary 4.4.3.8). Our assumption that $f$ is left cofinal guarantees that $\theta $ is a homotopy equivalence, and therefore a trivial Kan fibration (Proposition 3.2.7.2). In particular, it is surjective at the level of vertices, which guarantees that (7.8) admits a solution. $\square$

Proof. We first prove $(1)$. Let $X$ be a Kan complex. Then the projection map $X \times B \rightarrow B$ is a Kan fibration (Remark 3.1.1.6), and therefore both a left and a right fibration (Example 4.2.1.5). Consequently, if $f$ is either left cofinal or right cofinal, the induced map

is a homotopy equivalence of Kan complexes. Allowing $X$ to vary, we conclude that $f$ is a weak homotopy equivalence.

We now prove $(2)$. Assume that $B$ is a Kan complex and that $f$ is a weak homotopy equivalence; we will show that $f$ is left cofinal (the proof that $f$ is right cofinal is similar). Let $q: \widetilde{B} \rightarrow B$ be a left fibration. Since $B$ is a Kan complex, $q$ is a Kan fibration (Corollary 4.4.3.8); in particular, $\widetilde{B}$ is a Kan complex. Applying Corollary 3.1.3.4, we obtain a commutative diagram of Kan complexes

where the vertical maps are Kan fibrations (Corollary 3.1.3.2). Our assumption that $f$ is a weak homotopy equivalence guarantees that the horizontal maps are homotopy equivalences (Proposition 3.1.6.17). Applying Proposition 3.2.8.1, we deduce that the map $\operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B})$ is also a homotopy equivalence. $\square$

Proof. Let $q: \widetilde{C} \rightarrow C$ be a left fibration of simplicial sets, and let

be the morphisms given by precomposition with $g$ and $f$. Our assumption that $f$ is left cofinal guarantees that $f^{\ast }$ is a homotopy equivalence. It follows that $g^{\ast }$ is a homotopy equivalence if and only if $f^{\ast } \circ g^{\ast }$ is a homotopy equivalence (Remark 3.1.6.7). $\square$

Proof. Combine Propositions 7.2.1.6 and 7.2.1.3. $\square$

Proof. Combine Proposition 7.2.1.6 with Example 7.2.1.4. $\square$

Proof. We will show that $f$ is left cofinal; the proof that $f$ is right cofinal is similar. Let $q: \widetilde{B} \rightarrow B$ be a left fibration; we wish to show that composition with $f$ induces a homotopy equivalence $f^{\ast }: \operatorname{Fun}_{/B}(B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B})$. Applying Corollary 5.6.7.3 (and Remark 5.6.7.4), we deduce that there exists a pullback diagram of simplicial sets

where $Q$ is a left fibration of $\infty $-categories. Let $\operatorname{Fun}( A[W^{-1}], \operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}(A,\operatorname{\mathcal{C}})$ spanned by those diagrams which carry each edge of $W$ to an isomorphism in $\operatorname{\mathcal{C}}$ (Notation 6.3.1.1), and define $\operatorname{Fun}( A[W^{-1}], \widetilde{\operatorname{\mathcal{C}}} )$ similarly. We have a commutative diagram of $\infty $-categories

where the vertical maps on both sides are left fibrations (Corollary 4.2.5.2). Since $Q$ is a left fibration of $\infty $-categories, it is conservative (Proposition 4.4.2.11), so the right side of the diagram is a pullback square. In particular, the vertical map in the middle is also a left fibration. Our assumption that $f$ exhibits $B$ as a localization of $A$ with respect to $W$ guarantees that the left horizontal maps are equivalences of $\infty $-categories. Applying Corollary 4.5.2.32, we conclude that the map of fibers

is an equivalence of $\infty $-categories, and therefore a homotopy equivalence of Kan complexes (Example 4.5.1.13). $\square$

Proof. Combine Theorem 6.3.7.1 (and Variant 6.3.7.17) with Corollary 7.2.1.11. $\square$

Proof. Combine Proposition 7.2.1.10 with Example 6.3.1.12. $\square$

Proof. If $q$ is a trivial Kan fibration, then it is both a left fibration and a right fibration (Example 4.2.1.5). Moreover, $q$ is also a categorical equivalence of simplicial sets (Proposition 4.5.3.11), hence left and right cofinal by virtue of Corollary 7.2.1.13. This proves the implications $(3) \Rightarrow (1)$ and $(3) \Rightarrow (2)$.

We will complete the proof by showing that $(1) \Rightarrow (3)$ (the proof of the implication $(2) \Rightarrow (3)$ is similar). Assume that $q$ is a left cofinal left fibration. Then composition with $q$ induces a homotopy equivalence of Kan complexes $\operatorname{Fun}_{/S}( S, X) \rightarrow \operatorname{Fun}_{/S}(X,X)$. In particular, the morphism $q$ admits a section $f: S \rightarrow X$ such that $\operatorname{id}_{X}$ and $f \circ q$ belong to the same connected component of $\operatorname{Fun}_{/S}(X,X)$. For each vertex $s \in S$, let $X_{s} = \{ s\} \times _{S} X$ be the fiber of $q$ over $s$. Then the identity map $\operatorname{id}: X_{s} \rightarrow X_{s}$ is homotopic to the constant map $X_{s} \rightarrow \{ f(s) \} \hookrightarrow X_{s}$. It follows that the Kan complex $X_{s}$ is contractible. Allowing $s$ to vary, we conclude that the left fibration $q$ is a trivial Kan fibration (Proposition 4.4.2.14). $\square$

Proof. Suppose first that we can write $f = f'' \circ f'$, where $f'$ is left anodyne and $f''$ is a trivial Kan fibration. Proposition 7.2.1.3 guarantees that $f'$ is left cofinal, and Proposition 7.2.1.5 guarantees that $f''$ is left cofinal. Applying Proposition 7.2.1.6, we conclude that $f$ is also left cofinal.

We now prove the converse. Assume that $f: X \rightarrow Z$ is left cofinal. Applying Proposition 4.2.4.7, we can write $f$ as a composition $X \xrightarrow {f'} Y \xrightarrow {f''} Z$, where $f'$ is left anodyne and $f''$ is a left fibration. Then $f'$ is also left cofinal (Proposition 7.2.1.3). Applying Proposition 7.2.1.6, we deduce that $f''$ is left cofinal. It then follows from Corollary 7.2.1.14 that $f''$ is a trivial Kan fibration. $\square$

Proof. By virtue of Corollary 7.2.1.15, we may assume that $f$ factors as a composition $X \xrightarrow {g} Y \xrightarrow {h} Z$, where $g$ is left anodyne and $h$ is a trivial Kan fibration. Setting $Y' = Y {\coprod }_{X} X'$, we can expand (7.9) to a commutative diagram

Note that the square on the left is a pushout diagram in which the horizontal maps are monomorphisms, and therefore a categorical pushout diagram (Example 4.5.4.12). Applying Proposition 4.5.4.8, we deduce that the square on the right is also a categorical pushout diagram. Since $h$ is a categorical equivalence (Proposition 4.5.3.11), it follows that $h'$ is also a categorical equivalence (Proposition 4.5.4.10). In particular, $h'$ is left cofinal (Corollary 7.2.1.13). The morphism $g'$ is left anodyne (since it is a pushout of $g$), and is therefore also left cofinal (Proposition 7.2.1.3). Applying Proposition 7.2.1.6, we deduce that $f' = h' \circ g'$ is also left cofinal. $\square$

Proof. For every morphism of simplicial sets $f: X \rightarrow Z$, let $X \xrightarrow {f'} Q(f) \xrightarrow {f''} Y$ be the factorization of Proposition 4.2.4.7, so that $f'$ is left anodyne, $f''$ is a left fibration, and the construction $f \mapsto Q(f)$ is a functor which commutes with filtered colimits. Using Propositions 7.2.1.5, 7.2.1.6, and Corollary 7.2.1.14, we see that $f$ is left cofinal if and only if the morphism $f'': Q(f) \rightarrow Z$ is a trivial Kan fibration. Since the collection of trivial Kan fibrations is closed under filtered colimits (Remark 1.5.5.3), it follows that the collection of left cofinal morphisms is also closed under filtered colimits. $\square$

Proof. Combine Corollary 7.2.1.17 with Proposition 7.2.1.3. $\square$

Proof. By virtue of Corollary 7.2.1.15, the morphism $f$ factors as a composition $X \xrightarrow {f'} Y \xrightarrow {f''} Z$, where $f'$ is left anodyne and $f''$ is a trivial Kan fibration. It follows that $f \times \operatorname{id}_{K}$ factors as a composition

We now note that $f' \times \operatorname{id}_{K}$ is left anodyne (Proposition 4.2.5.3) and $f'' \times \operatorname{id}_{K}$ is a trivial Kan fibration (Remark 1.5.5.2). Applying Corollary 7.2.1.15, we deduce that $f \times \operatorname{id}_{K}$ is left cofinal. $\square$

Proof. Factoring $f \times f'$ as a composition

the desired result follows by combining Corollary 7.2.1.19 with Proposition 7.2.1.6. $\square$

Proof. Since $g$ is a categorical equivalence, the construction $\widetilde{C} \mapsto B \times _{C} \widetilde{C}$ induces a bijection from equivalence classes of left fibrations over $C$ to equivalence classes of left fibrations over $B$ (Corollary 5.6.0.6). It follows that $f$ is left cofinal if and only if it satisfies the following condition:

$(\ast )$

For every left fibration $q: \widetilde{C} \rightarrow C$, the restriction map $f^{\ast }: \operatorname{Fun}_{/C}(B, \widetilde{C} ) \rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C} )$ is a homotopy equivalence of Kan complexes.

It will therefore suffice to show that, for every left fibration $q: \widetilde{C} \rightarrow C$, the restriction map $f^{\ast }: \operatorname{Fun}_{/C}(B, \widetilde{C} ) \rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C} )$ is a homotopy equivalence if and only if the restriction map $(g \circ f)^{\ast }: \operatorname{Fun}_{/C}( C, \widetilde{C})\rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C})$ is a homotopy equivalence. This is clear, since our assumption that $g$ is a categorical equivalence guarantees that the restriction map $g^{\ast }: \operatorname{Fun}_{/C}(C, \widetilde{C}) \rightarrow \operatorname{Fun}_{/C}(B, \widetilde{C} )$ is a homotopy equivalence (Corollary 7.2.1.13). $\square$

Proof. By virtue of Proposition 7.2.1.21, the morphism $f$ is left cofinal if and only if the composite morphism $g' \circ f$ is left cofinal. Similarly, Proposition 7.2.1.6 guarantees that $f'$ is left cofinal if and only if $f' \circ g$ is left cofinal. We conclude by observing that $g' \circ f = f' \circ g$. $\square$

Proof. Let $\operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ be the full subcategory spanned by the isomorphisms of $\operatorname{\mathcal{C}}$ (see Example 4.4.1.14). Let $\operatorname{ev}_0, \operatorname{ev}_1: \operatorname{Isom}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the morphisms given by evaluation at the vertices $0,1 \in \Delta ^1$, so that $\operatorname{ev}_0$ and $\operatorname{ev}_1$ are trivial Kan fibrations (Corollary 4.4.5.10). Fix an isomorphism of $f_0$ with $f_1$, which we identify with a diagram $F: K \rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}})$ satisfying $\operatorname{ev}_0 \circ F = f_0$ and $\operatorname{ev}_1 \circ F = f_1$. Applying Corollary 7.2.1.22 to the diagram

we deduce that $f_0$ is left cofinal if and only if $F$ is left cofinal. By the same reasoning, this is equivalent to the condition that $f_1$ is left cofinal. $\square$