Corollary 3.35.
Let \(n\geq0\) and let \(f\colon X \to Y\) be \(n\)-connected. Then the functor \(f^*\colon (T_{/Y})_{\leq n-1} \to (T_{/X})_{\leq n-1}\) is an equivalence.
Proof
Full faithfulness of \(f^*\) was proved in Proposition 3.18.For essential surjectivity, we may replace \(T\) by \(T_{/Y}\) and assume \(Y = *\). Given an \((n-1)\)-truncated morphism \(U \to X\), we must show that it is in the image of the functor \((-) \times X\colon T_{\leq n-1} \to (T_{/X})_{\leq n-1}\). We claim that the map \(U \to \tau_{n-1} U \times X\) is an isomorphism. By the factorization system from Proposition 3.18, it suffices to show it is both \((n-1)\)-truncated and \((n-1)\)-connected.
- The map is \((n-1)\)-truncated since it lives over \(X\), and both maps to \(X\) are \((n-1)\)-truncated. The claim follows by left cancellation.
- To see it is \((n-1)\)-connected, note that it factors as \[U \longrightarrow U \times X \longrightarrow \tau_{n-1} U \times X.\]The first map is \((n-1)\)-connected, as it is a base change of the diagonal \(X \to X \times X\), which is \((n-1)\)-connected by the theorem. The second map is \((n-1)\)-connected since it is a base change of the map \(U \to \tau_{n-1} U\).