# Proof of Lemma 5.1.5.3 in Jacob Lurie's HTT.

I am currently trying to understand the following proof in Higher Topos Theory.

I am fine with almost all of the argument, except with the claim that $$\mathcal{E}^1$$ is a deformation retract of $$\mathcal{E}$$. While I feel like this is true, I am unable to prove it properly, i.e writing down a well-defined morphism of simplicial sets $$r : \mathcal{E} \to \mathcal{E}^1$$ along with a homotopy witnessing it as a deformation retract.

An object (i.e a $$0$$-simplex) of $$\mathcal{E}^1$$ is just a map $$C \to X$$ in $$\mathcal{P}(S)$$, while an object of $$\mathcal{E}$$ is

• Either a couple $$(v, C \to X)$$ where $$v$$ is the cone point of $$(\mathcal{C}_{/X})^\rhd$$.
• Either a couple $$(B \to X, C \to B)$$ where $$B$$ is in $$\mathcal{C}$$.

The "obvious way" to produce a map $$C \to X$$ out of this kind of data would be to send $$(v, C \to X)$$ to $$C \to X$$ and $$(B \to X, C \to B)$$ to a composition $$C \to B \to X$$. My issue with this approach is that I am using composition internal to $$\mathcal{P}(S)$$, which is only weakly defined, and I do not know how to produce a full map of simplicial sets using it. The same problem arises when trying to work out higher-dimensional simplices.

I can show that $$\mathcal{E}^1 \to \mathcal{E}^0$$ is a weak homotopy equivalence by viewing it as a pullback of the initial (hence left anodyne) map $$\{\mathrm{id}_{\mathcal{P}(S)}\} \hookrightarrow \mathcal{P}(S)_{C/ }$$ by the right fibration (hence proper map) $$\mathcal{C}_{/X} \to \mathcal{C}$$. I can not make this argument work for $$\mathcal{E}^1 \to \mathcal{E}$$, unless the map $$(\mathcal{C}_{/X})^\rhd \to \mathcal{P}(S)$$ is proprer. I have no idea wether this can be expected or not.

Using a similar kind of argument (pulling back the right anodyne map $$\{v\} \to (\mathcal{C}_{/X})^\rhd$$ along the left fibration $$\mathcal{P}(S)_{C/ } \to \mathcal{P}(S)$$), I can show that $$\mathcal{E}^0$$ indeed has the same homotopy type as $$\mathcal{E}$$ and that it is the homotopy type of $$\mathrm{Map}_{\mathcal{P}(S)}(C, X)$$ but this argument does not say that this equivalence is induced by $$\mathcal{E}^0 \to \mathcal{E}$$.

Is there a simple argument to show that $$\mathcal{E}^1 \to \mathcal{E}$$ is a weak homotopy equivalence, or even to show directly that $$\mathcal{E}^0 \to \mathcal{E}$$ is a weak homotopy equivalence?

Update: It seems to me that one can show directly that $$\mathcal{E}^0$$ is a deformation retract of $$\mathcal{E}$$, and that the homotopies do not use composition internal to $$\mathcal{P}(S)$$. However, I am not yet been able to write the homotopy either, and would appreciate any hint or construction that would help defining such a map.

I think you are right in following intuitions at the zero level, but I strongly recommend you not to use simplex by simplex constructions and use abstract stuff to create maps, as you were doing.

My first intuition was the following (see HTT 1.2.2 for definitions):

• $$\mathcal{E}$$ can be contracted to the cone point in the first component, yielding $$\text{Hom}^L_{\mathcal{P}(S)}(C,X)$$;
• $$\mathcal{E}_0$$ can be contracted in the second component (because the overcategory has a final object) to yield exactly $$\mathcal{E}^1 = \text{Hom}^R_{\mathcal{P}(S)}(C,X)$$;

The very non obvious thing is then to find a deformation retraction from $$\text{Hom}^L \to \text{Hom}^R$$, which I am not quite sure it exist; so we should change approach. On the other side, we can contract the second component on $$\{1_C\}$$ because it is initial, yielding a deformation retraction

$$\mathcal{E} \to (\mathcal{C}_{/X})^{\triangleright} \times_{\mathcal{P}(S)} \{1_C\}$$

But the cone point is sent to $$X \in \mathcal{P}(S)$$ and will never contribute to the pullback, so the latter is equal to $$\mathcal{E}^1$$! This happens unless $$X=C$$, but in this case the inclusion $$\mathcal{C}_{/C} \to (\mathcal{C}_{/C})^{\triangleright}$$ is a deformation retraction by sending the cone point to $$1_C$$.

I don't know which lemma to invoke here so we just verify on simplices: an $$n$$ simplex $$\Delta^n \to (\mathcal{C}_{/X})^{\triangleright} \times_{\mathcal{P}(S)} \{1_C\}$$ is the same as a map $$\phi : \Delta^{k+1} \to \mathcal{C}$$ for some $$-1 \le k \le n$$ so that $$\phi(k+1) = X, \ \ \ \phi|_{\{0, \ldots, k\}} * X : \Delta^n \to \mathcal{C}$$ is constantly $$C$$, where $$X$$ above denotes the constant $$=X$$ simplex $$\Delta^{n-k-1} \to \mathcal{P}(S)$$. In order for this to happen, we must have $$n-k-1 = -1$$ because $$X \neq C$$, i.e. $$n=k$$. But $$n$$ simplices $$\phi: \Delta^{n+1} \to \mathcal{C}$$ such that $$\phi(n+1) = X, \ \ \ \phi|_{\{0, \ldots, n\}} = C$$ are exactly the simplices coming from $$\mathcal{C}_{/X} \times_{\mathcal{P}(S)} \{1_C\}$$.

Remark. I implicitly used above that maps $$\Delta^n \to A^{\triangleright}$$ are the same as maps $$\phi:\Delta^k \to A$$ with $$-1 \le k \le n$$, and under a simplicial map $$F: A^{\triangleright} \to B$$ such simplex is sent to $$F( \phi)* F(v)* \ldots * F(v)$$; here $$v$$ is the cone point and $$F(v)$$ is repeated $$n-k-1$$ times. This is just another way of stating that

$$(A^{\triangleright})_n = (A * \Delta^0 ) = A_n \cup (\Delta^0)_n \cup \bigcup_{i+j = n-1} A_i \times (\Delta^0)_j$$

Using the convenient convention that $$\Delta^{-1} = \emptyset$$, so that $$A_{-1}$$ has just one element (the empty map).

• Thank you for your answer! I agree with the fact that the cone point does not contribute to the pullback. Can you explain why you can freely contract the second component in the pullback while keeping the first inchanged? It looks like you're following the approach I mentionned at the end of my paragraph starting with "I can show that ...". My issue was that to deduce that I can contract the second component of $\mathcal{E}$ in the pullback, I would need some properness-like property of $(\mathcal{C}/X)^{\rhd} \to \mathcal{P}(S)$ so that the pullback of a left anodyne map by this remains so. – Robin Carlier Jan 14 at 8:10
• I would say that pulling back gives a (simplicial) functor $\text{sSet}_{/\mathcal{P}(S) } \to \text{sSet}_{/(C/X)^{\triangleright} }$ . As long as you have a deformation retraction of $\mathcal{P}(S) _{C/}$ to ${1_C}$ over $\mathcal{P}(S)$, applying the functor you will obtain a deformation retraction of the pullback. This is true: just write the diagram of deformating to the initial element and you will see everything commutes :) – Andrea Marino Jan 14 at 9:21
• An analogy with algebra of why you don't need properness. Say you have a ring morphism $A\to B$, and consider the base change $(-) \otimes_A B : \text{Ch}(A) \to \text{Ch}(B)$ of chain complexes. This sends homotopy equivalent complexes to homotopy equivalent complexes, because you can just apply the function to all the morphisms involved. On the other side, it's not true in general that they send quasi isomorphisms to quasi isomorphisms; for this to happen you would need $A\to B$ flat (in analogy with the properness hypothesis you were looking for). Does it make sense? I hope it does :) – Andrea Marino Jan 14 at 9:31
• The analogy with algebra makes a lot of sense, thank you! I never thought of properness that way and I must thank you for this! I agree that if we have a deformation retract over $\mathcal{P}(S)$, then it's done. But is the retraction $\mathcal{P}(S)_{C/} \to 1_C$ really happening over $\mathcal{P}(S)$? An object of $C \to X$ in $\mathcal{P}(S)_{C/}$ is sent to $X$, and the map $\{1_C\} \to \mathcal{P}(S)$ sends the unique object to $C$. It looks to me there is no map $\mathcal{P}(S)_{C/} \to 1_C$ over $\mathcal{P}(S)$. Am I missing something? – Robin Carlier Jan 14 at 9:47
• Ok, your argument is really sound but then I thought "we should relax something in order for this retraction to be possible". Luckily, there is already a 'relax' parameter we have not implemented: a 1-cell in $sSet_{C/}$ is a 2-cell in $sSet$; you specified edges and vertices, but we still can choose the interior. The latter correspond to a homotopy $h: \mathcal{P}(S)_{C/} \times \Delta^1 \to \mathcal{P}(S)$. Now the two maps $(C \to X) \mapsto C$ and $(C \to X) \mapsto X$ are homotopic via the morphism $C\to X$. Hope I saved the day - never sure with HTT technicalities! – Andrea Marino Jan 14 at 10:43