Kerodon

Proof. We will prove the first assertion; the proof of the second is similar. We proceed as in the proof of Proposition 4.3.6.4. Let us first regard the anodyne morphism $f$ as fixed, and let $T$ be the collection of all morphisms $g$ of simplicial sets for which $\theta _{f,g}$ is left anodyne. Then $T$ weakly saturated (in the sense of Definition 1.5.4.12). We wish to prove that $T$ contains every monomorphism of simplicial sets. By virtue of Proposition 1.5.5.14, we are reduced to proving that the morphism $\theta _{f,g}$ is left anodyne in the special case where $g$ is the boundary inclusion $\operatorname{\partial \Delta }^{q} \hookrightarrow \Delta ^{q}$ for some $q \geq 0$.

Let us now regard $g: \operatorname{\partial \Delta }^ q \hookrightarrow \Delta ^ q$ as fixed, and let $S$ denote the collection of all morphisms of simplicial sets for which $\theta _{f,g}$ is left anodyne. To complete the proof, we must show that $S$ contains every anodyne morphism of simplicial sets. As before, we note that $S$ is weakly saturated. It will therefore suffice to show that $S$ contains every horn inclusion $\Lambda ^{p}_{i} \hookrightarrow \Delta ^ p$ when $p > 0$ and $0 \leq i \leq p$. In other words, we are reduced to checking that the pushout-join

is left anodyne. This is clear, since $\theta _{f,g}$ can be identified with the horn inclusion $\Lambda ^{p+1+q}_{i} \hookrightarrow \Delta ^{p+1+q}$ by virtue of Lemma 4.3.6.16. $\square$

Proof. We will prove the first assertion; the proof of the second is similar. Assume that $q$ is a left fibration; we wish to show that the map $X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)}$ is a Kan fibration. Equivalently, we wish to show that every lifting problem

admits a solution, provided that the left vertical map $A \rightarrow A'$ is anodyne. Unwinding the definitions, we see that this can be rephrased as a lifting problem

This problem admits a solution, since the vertical map on the left is left anodyne (Proposition 4.3.7.1) and $q$ is a left fibration. $\square$

Proof. Apply Proposition 4.3.7.2 in the special case $K_0 = \emptyset $. $\square$

Proof. Apply Proposition 4.3.7.2 in the special case $S = \Delta ^{0}$. $\square$

Proof. Apply Corollary 4.3.7.4 in the special case $K_0 = \emptyset $ (or Corollary 4.3.7.3 in the special case $S = \Delta ^{0}$). $\square$

Proof. We will prove the first assertion; the proof of the second is similar. Assume that $q$ is a right fibration and that the inclusion $K_0 \hookrightarrow K$ is anodyne. We wish to show that the map $X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)}$ is a trivial Kan fibration. Equivalently, we wish to show that every lifting problem

admits a solution, provided that the left vertical map $A \rightarrow A'$ is a monomorphism. Unwinding the definitions, we see that this can be rephrased as a lifting problem

This problem admits a solution, since the vertical map on the left is right anodyne (Proposition 4.3.7.1) and $q$ is a right fibration. $\square$

Proof. Apply Proposition 4.3.7.6 in the special case $S = \Delta ^{0}$. $\square$

Proof. We will prove the first assertion (the second follows by a similar argument). Let $T$ be the collection of all morphisms $f$ of simplicial sets for which $f^{\triangleright }$ is right anodyne. We wish to show that every monomorphism belongs to $T$. Since the collection $T$ is weakly saturated, it will suffice to show that every boundary inclusion $f: \operatorname{\partial \Delta }^ n \hookrightarrow \Delta ^ n$ belongs to $T$ (Proposition 1.5.5.14). In this case, we can identify $f^{\triangleright }$ with the with the horn inclusion $\Lambda ^{n+1}_{n+1} \hookrightarrow \Delta ^{n+1}$ (see Example 4.3.3.28). $\square$

Proof. We will prove the first assertion; the second follows by a similar argument. Fix a vertex $x \in X$, so that the inclusion morphism $\iota : X \star Y' \hookrightarrow X \star Y$ factors as a composition

The morphism $\iota '$ is a pushout of the inclusion $Y'^{\triangleleft } \hookrightarrow Y^{\triangleleft }$, and is left anodyne by virtue of Lemma 4.3.7.8. It will therefore suffice to show that $\iota ''$ is left anodyne. This is a special case of Proposition 4.3.7.1, since the inclusion map $\{ x\} \hookrightarrow X$ is a weak homotopy equivalence (by virtue of our assumption that $X$ is weakly contractible) and therefore anodyne (by virtue of Corollary 3.3.7.7). $\square$

Proof. We will prove the first assertion; the second follows by a similar argument. To show that the morphism $X_{/f} \rightarrow S_{/(q \circ f)}$ is a trivial Kan fibration, we must prove that every lifting problem

admits a solution. Unwinding the definitions, we can rephrase this as a lifting problem

This lifting problem admits a solution, since $q$ is assumed to be a right fibration and the left vertical map is right anodyne (Proposition 4.3.7.9). $\square$

Proof. Apply Corollary 4.3.7.13 in the special case $S = \Delta ^{0}$. $\square$

Proof. To show that the map $X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)}$ is a trivial Kan fibration, we must show that every lifting problem every lifting problem

admits a solution, provided that the left vertical map $A \rightarrow A'$ is a monomorphism. Unwinding the definitions, we see that this can be rephrased as a lifting problem

This problem admits a solution, since the vertical map on the left is a monomorphism (Proposition 4.3.7.1) and $q$ is a trivial Kan fibration. $\square$

Proof. Apply Proposition 4.3.7.15 in the special case $K_0 = \emptyset $. $\square$

Proof. Apply Proposition 4.3.7.15 in the special case $S = \Delta ^{0}$. $\square$

Proof. Apply Corollary 4.3.7.16 in the special case $S = \Delta ^{0}$ (or Corollary 4.3.7.18 in the special case $K_0 = \emptyset $). $\square$