Kerodon

Proof. The equivalence $(1) \Leftrightarrow (2)$ is tautology, the implication $(2) \Rightarrow (3)$ follows from Proposition 8.5.6.17 (and Example 8.5.7.3), and the implication $(3) \Rightarrow (4)$ is immediate. We will complete the proof by showing that $(4)$ implies $(1)$. Assume that $e$ is homotopy idempotent, so that there exists a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ whose boundary is indicated in the diagram

Let $\operatorname{Spine}[\operatorname{\mathbf{Z}}]$ denote the $1$-dimensional simplicial set of Notation 8.5.4.12, and let $T_{\sigma }: \operatorname{Spine}[\operatorname{\mathbf{Z}}] \rightarrow \operatorname{\mathcal{C}}_{X/}$ be the morphism of simplicial sets which carries each vertex of $\operatorname{Spine}[\operatorname{\mathbf{Z}}]$ to $e$ (regarded as an object of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{X/}$) and each nondegenerate edge of $\operatorname{Spine}[\operatorname{\mathbf{Z}}]$ to $\sigma $ (regarded as a morphism of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{X/}$). We will identify $T_{\sigma }$ with a diagram $\overline{T}_{e}: \operatorname{Spine}[\operatorname{\mathbf{Z}}]^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$, where the restriction $\overline{T}_{e}|_{ \operatorname{Spine}[\operatorname{\mathbf{Z}}] }$ is the diagram $T_{e}: \operatorname{Spine}[\operatorname{\mathbf{Z}}] \rightarrow \operatorname{\mathcal{C}}$ of Notation 8.5.6.11. Let us further identify $\overline{T}_{e}$ with an object $\overline{X}$ of the slice $\infty $-category $\operatorname{\mathcal{C}}_{ / T_{e} }$, lying over the object $X \in \operatorname{\mathcal{C}}$. By virtue of assumption $(4)$, the $\infty $-category $\operatorname{\mathcal{C}}_{ / T_{e} }$ has a final object $\overline{Y}$, lying over a some object $Y \in \operatorname{\mathcal{C}}$. We can therefore choose a morphism $\overline{r}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{\mathcal{C}}_{ / T_{e} }$, having some image $r: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$. The morphism $\overline{r}$ can be identified with a diagram $\Delta ^1 \star \operatorname{Spine}[\operatorname{\mathbf{Z}}] \rightarrow \operatorname{\mathcal{C}}$, which we display informally as

By construction, the restriction of this diagram to the middle column witnesses the equality $[i(0)] \circ [r] = [e]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$. To show that the homotopy class $[e]$ is a split idempotent, it will suffice to show that $[r] \circ [i(0)]$ is the identity morphism $[ \operatorname{id}_{Y} ]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$. Since the morphism $[i(0)]$ admits a left inverse, it will suffice to show that equality holds after postcomposition with $[i(0)]$. This follows from the calculation