Kerodon

Proof of Proposition 7.1.4.13. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories. Assume that $U$ is a coreflective localization functor: we will show that, for every object $D \in \operatorname{\mathcal{D}}$, there exists a $U$-initial object $C \in \operatorname{\mathcal{C}}$ and an isomorphism $D \rightarrow U(C)$ in $\operatorname{\mathcal{D}}$ (the converse follows from Lemma 7.1.4.14). Using Proposition 6.3.3.6, we see that there exists a functor $F: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and a natural isomorphism $\eta : \operatorname{id}_{\operatorname{\mathcal{D}}} \rightarrow U \circ F$ which is the unit of an adjunction between $F$ and $U$. In particular, for every object $D \in \operatorname{\mathcal{D}}$, we have an isomorphism $\eta _{D}: D \rightarrow U(C)$ for $C = F(D)$. We will complete the proof by showing that the object $C$ is $U$-initial. Fix an object $X \in \operatorname{\mathcal{C}}$; we wish to show that the functor $U$ induces a homotopy equivalence of Kan complexes $\rho : \operatorname{Hom}_{\operatorname{\mathcal{C}}}( F(D), X ) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( (U \circ F)(D), U(X) )$. Since $\eta _{D}: D \rightarrow (U \circ F)(D)$ is an isomorphism, this is equivalent to the requirement that the composite map

is a homotopy equivalence of Kan complexes, which follows from our assumption that $\eta $ is the unit of an adjunction (Proposition 6.2.1.17). $\square$