Kerodon

Proof. The equivalence $(1) \Leftrightarrow (2)$ follows from Proposition 4.6.9.16, the equivalence $(2) \Leftrightarrow (3)$ from Corollary 5.1.7.16 (and Proposition 5.1.7.5). Corollary 4.3.6.12 guarantees that $u$ is a left fibration. In particular, it is an isofibration, so the equivalence $(3) \Leftrightarrow (4)$ is a special case of Proposition 4.5.5.20. The equivalence $(4) \Leftrightarrow (5)$ follows by unwinding definitions. $\square$

Proof. Set $\operatorname{\mathcal{D}}= \operatorname{\mathcal{C}}_{f/} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}'$ and $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}_{X/} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}'$. Our assumption that $f$ exhibits $Y$ as a $\operatorname{\mathcal{C}}'$-reflection of $X$ guarantees that the restriction map $u: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ is a trivial Kan fibration (Proposition 6.2.2.10). We wish to show that the analogous restriction map

is also trivial Kan fibration. Let us regard $\overline{f}$ as a morphism of simplicial sets $\Delta ^1 \star K \rightarrow \operatorname{\mathcal{C}}$, which we can identify with a diagram $\overline{q}: K \rightarrow \operatorname{\mathcal{D}}$. Under this identification, $\overline{u}$ corresponds to the map $\operatorname{\mathcal{D}}_{ / \overline{q} } \rightarrow \operatorname{\mathcal{E}}_{ / u \circ \overline{q} }$ induced by $u$, which is a trivial Kan fibration by virtue of Corollary 4.3.7.17. $\square$

Proof. Let $\overline{X}$ be an object of the slice $\infty $-category $\operatorname{\mathcal{C}}_{/q}$; we wish to show that there exists a morphism $\overline{f}: \overline{X} \rightarrow \overline{Y}$ which exhibits $\overline{Y}$ as a $\operatorname{\mathcal{C}}'_{/q}$-reflection of $\overline{X}$. Let $X$ denote the image of $\overline{X}$ in the $\infty $-category $\operatorname{\mathcal{C}}$. Since $\operatorname{\mathcal{C}}'$ is a reflective subcategory of $\operatorname{\mathcal{C}}$, we can choose a morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ which exhibits $Y$ as a $\operatorname{\mathcal{C}}'$-reflection of $X$. By virtue of Corollary 6.2.2.11, it will suffice to show that $f$ can be lifted to a morphism $\overline{f}: \overline{X} \rightarrow \overline{Y}$ in $\operatorname{\mathcal{C}}_{/q}$. Unwinding the definitions, we can rewrite this as a lifting problem

which admits a solution by virtue of the fact that the right vertical map is a trivial Kan fibration (Proposition 6.2.2.10). $\square$

Proof. Assume that $\operatorname{\mathcal{C}}'$ is a reflective subcategory of $\operatorname{\mathcal{C}}$; we will show that there exists a functor $L: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}'$ and a natural transformation $\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow L$ which exhibits $L$ as a $\operatorname{\mathcal{C}}'$-reflection functor (the reverse implication is immediate from the definitions). Let $\operatorname{\mathcal{E}}$ be the full subcategory of $\operatorname{\mathcal{C}}\times \Delta ^1$ spanned by those objects $(X,i)$ having the property that if $i=1$, then $X$ belongs to the full subcategory $\operatorname{\mathcal{C}}'$. Let $\pi : \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ denote the projection map. Let $\widetilde{u}: (X,0) \rightarrow (Y,1)$ be a morphism in $\operatorname{\mathcal{E}}$, corresponding to a morphism $u: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ for which the target $Y$ belongs to $\operatorname{\mathcal{C}}'$. By virtue of Corollary 5.1.2.3, the morphism $\widetilde{u}$ is $\pi $-cocartesian if and only if $u$ exhibits $Y$ as a $\operatorname{\mathcal{C}}'$-reflection of $X$. Consequently, our assumption that $\operatorname{\mathcal{C}}'$ is a reflective subcategory of $\operatorname{\mathcal{C}}$ guarantees that $\pi $ is a cocartesian fibration of $\infty $-categories. Applying Proposition 5.2.2.8, we deduce that there exists a functor

and a morphism $\widetilde{\eta }: \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow L$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ which carries each object $X \in \operatorname{\mathcal{C}}$ to a $\pi $-cocartesian morphism $(X,0) \rightarrow (L(X),1)$ in $\operatorname{\mathcal{E}}$. Composing with the projection map $\pi : \operatorname{\mathcal{E}}\rightarrow \Delta ^1$, we obtain a natural transformation $\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow L$ in $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$ which exhibits $L$ as a $\operatorname{\mathcal{C}}'$-reflection functor. $\square$

Proof. We first show that $(1)$ implies $(2)$. Let $X$ be an object of $\operatorname{\mathcal{C}}$, so that $\eta $ determines a morphism $\eta _{X}: X \rightarrow L(X)$. For every object $Y \in \operatorname{\mathcal{C}}'$, Proposition 6.2.1.17 guarantees that composition with the homotopy class $[\eta _ X]$ induces an isomorphism

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. It follows that $\eta _{X}$ exhibits $L(X)$ as a $\operatorname{\mathcal{C}}'$-reflection of $X$. Allowing $X$ to vary, we conclude that $\eta $ exhibits $L$ as a $\operatorname{\mathcal{C}}'$-reflection functor.

We now show that $(2)$ implies $(3)$. Assume that, for every object $X \in \operatorname{\mathcal{C}}$, the morphism $\eta _ X: X \rightarrow L(X)$ exhibits $L(X)$ as a $\operatorname{\mathcal{C}}'$-reflection of $X$. Note that we have a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{C}}$, obtained by applying the natural transformation $\eta $ to the morphism $\eta _{X}: X \rightarrow L(X)$. For each object $Y \in \operatorname{\mathcal{C}}$, we obtain a commutative diagram of sets

If $Y$ belongs to the subcategory $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$, then the vertical maps and the upper horizontal map in this diagram are bijective. It follows that the lower horizontal map is bijective as well. Allowing $Y$ to vary, we deduce that the homotopy class $[ L(\eta _ X) ]$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}'$, so that $L( \eta _ X )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}'$. In the special case where $X$ belongs to $\operatorname{\mathcal{C}}'$, Example 6.2.2.4 guarantees that $\eta _ X$ is already an isomorphism before applying the functor $L$.

We now show that $(3)$ implies $(1)$. Note that $\eta $ determines natural transformations

If condition $(3)$ is satisfied, then Theorem 4.4.4.4 guarantees that $\eta '$ and $\eta ''$ are isomorphisms in the $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}}' )$ and $\operatorname{Fun}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{C}})$, respectively. Invoking the criterion of Proposition 6.1.4.6, we conclude that $\eta $ is the unit of an adjunction. $\square$

Proof of Proposition 6.2.2.13. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be a full subcategory. It follows from Proposition 6.2.2.17 that the inclusion functor $\operatorname{\mathcal{C}}' \hookrightarrow \operatorname{\mathcal{C}}$ admits a left adjoint if and only if there exists a functor $L: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}'$ and a natural transformation $\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow L$ which exhibits $L$ as a $\operatorname{\mathcal{C}}'$-reflection functor. By virtue of Lemma 6.2.2.16, this is equivalent to the requirement that $\operatorname{\mathcal{C}}'$ is a reflective subcategory of $\operatorname{\mathcal{C}}$. The analogous characterization of coreflective subcategories follows by a similar argument. $\square$

Proof. Let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be the essential image of $G$. If $G$ is fully faithful, then it induces an equivalence $\operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}'$ (Corollary 4.6.2.23). The equivalence $(1) \Leftrightarrow (2)$ follows by applying Proposition 6.2.2.13 to the subcategory $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$, and the implication $(2) \Rightarrow (3)$ follows by applying Proposition 6.2.2.17 to the subcategory $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$. To show that $(3) \Rightarrow (2)$, we observe that if a natural isomorphism $\epsilon : F \circ G \xrightarrow {\sim } \operatorname{id}_{\operatorname{\mathcal{D}}}$ is the counit of an adjunction, then $G$ restricts to an equivalence of $\operatorname{\mathcal{D}}$ with a full subcategory of $\operatorname{\mathcal{C}}$ (Proposition 6.2.1.13), and is therefore fully faithful. The equivalence $(3) \Leftrightarrow (4)$ is a special case of Proposition 6.1.4.7. $\square$

Proof. Suppose that conditions $(1)$ and $(2)$ are satisfied; we will show that $F$ is an equivalence of $\infty $-categories (the converse is immediate from the definitions). Combining assumption $(2)$ with Corollary 6.2.2.19, we can choose a functor $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and a natural isomorphism $\epsilon : F \circ G \xrightarrow {\sim } \operatorname{id}_{\operatorname{\mathcal{D}}}$ which is the counit of an adjunction between $F$ and $G$. Let $\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow G \circ F$ be a natural transformation which is compatible up to homotopy with $\epsilon $, in the sense of Definition 6.2.1.1. For each object $C \in \operatorname{\mathcal{C}}$, the morphism $\eta _{C}$ fits into a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{D}}$, where $\epsilon _{ F(C) }$ and $\operatorname{id}_{ F(C) }$ are isomorphisms. It follows that $F( \eta _ C )$ is also an isomorphism in $\operatorname{\mathcal{D}}$. Applying assumption $(1)$, we deduce that $\eta _{C}$ is an isomorphism in $\operatorname{\mathcal{C}}$. Allowing the object $C$ to vary (and invoking the criterion of Theorem 4.4.4.4), we deduce that $\eta $ is also a natural isomorphism, so that $F$ and $G$ are homotopy inverse to one another. $\square$

Proof. The implication $(2) \Rightarrow (1)$ follows from Proposition 6.2.2.17. Conversely, suppose that condition $(1)$ is satisfied, and let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by those objects of the form $L(X)$ for $X \in \operatorname{\mathcal{C}}$. Assumption $(1)$ guarantees that $\eta _{Y}$ is an isomorphism for each $Y \in \operatorname{\mathcal{C}}'$, so that $\eta $ exhibits $L$ as a $\operatorname{\mathcal{C}}'$-reflection functor by virtue of Proposition 6.2.2.17. $\square$

Proof. We first show that, if $f: X \rightarrow Y$ is a morphism of $\operatorname{\mathcal{E}}$ satisfying conditions $(1)$ and $(2)$, then $f$ exhibits $Y$ as a $\operatorname{\mathcal{E}}'$-reflection of $X$. It follows from condition $(2)$ that $U(Y)$ belongs to $\operatorname{\mathcal{C}}'$, so that $Y$ belongs to $\operatorname{\mathcal{E}}'$. It will therefore suffice to show that for each object $Z \in \operatorname{\mathcal{E}}$, precomposition with $f$ induces a homotopy equivalence $\theta : \operatorname{Hom}_{\operatorname{\mathcal{E}}}(Y,Z) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$. Let us abuse notation by identifying $\theta $ with the restriction map $\{ f\} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y) } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y,Z) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$, so that we have a commutative diagram of Kan complexes

Assumption $(1)$ guarantees that this diagram is a homotopy pullback square (Proposition 5.1.2.1), and assumption $(2)$ guarantees that $\overline{\theta }$ is a homotopy equivalence of Kan complexes. Applying Corollary 3.4.1.5, we conclude that $\theta $ is also a homotopy equivalence.

We now show that $\operatorname{\mathcal{E}}'$ is a reflective subcategory of $\operatorname{\mathcal{E}}$. Fix an object $X \in \operatorname{\mathcal{E}}$. Since $\operatorname{\mathcal{C}}'$ is a reflective subcategory of $\operatorname{\mathcal{C}}$, there exists a morphism $\overline{f}: U(X) \rightarrow \overline{Y}$ in $\operatorname{\mathcal{C}}$ which exhibits $\overline{Y}$ as a $\operatorname{\mathcal{C}}'$-reflection of $U(X)$. Since $U$ is a cocartesian fibration, we can write $\overline{f} = U(f)$ for some $U$-cocartesian morphism $f: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$. By construction, the morphism $f$ satisfies conditions $(1)$ and $(2)$, and therefore exhibits $Y$ as an $\operatorname{\mathcal{E}}'$-reflection of $X$.

To complete the proof, it will suffice to show that if $h: X \rightarrow Z$ is another morphism which exhibits $Z$ as a $\operatorname{\mathcal{E}}'$-reflection of $X$, then $h$ also satisfies conditions $(1)$ and $(2)$. By virtue of Remark 6.2.2.3, there exists a $2$-simplex

of $\operatorname{\mathcal{E}}$, where $g: Y \rightarrow Z$ is an isomorphism of $\operatorname{\mathcal{E}}'$. In particular, $g$ is $U$-cocartesian (Proposition 5.1.1.9), so that $h$ satisfies $(1)$ by virtue of Corollary 5.1.2.4. Since $U(g)$ is an isomorphism in $\operatorname{\mathcal{C}}'$, condition $(2)$ follows from Remark 6.2.2.3. $\square$