Proposition 17.2.7 (Free adjunction of \(\Rr \)-cocartesian lifts). The functor \[ E_{\Rr }\colon (\Cat _\infty )_{/S}\to (\Cat _\infty )^{\Rr \mathrm {-cocart}}_{/S} \] from Lemma 17.2.3 is left adjoint to the forgetful functor, with unit given by \(i_{p}\colon E \to E_{\Rr }(p)\) and counit given by \(\pi _{q}\colon E_{\Rr }(q) \to F\). More precisely, given a functor \(p\colon E \to S\) and an \(\Rr \)-cocartesian fibration \(q\colon F \to S\), precomposition with \(i_{p}\) induces an equivalence \[ \Fun _{/S}^{\Rr \mathrm {-cocart}}\bigl (E_{\Rr }(p),F\bigr ) \iso \Fun _{/S}(E,F), \] with inverse sending \(f\colon E\to F\) to \(\pi _{q}\circ E_{\Rr }(f)\).
Proof. Consider first a morphism \(f\colon E \to F\) in \((\Cat _\infty )_{/S}\). We must show that the composite \[ E \xrightarrow {i_p} E_{\Rr }(p) \xrightarrow {E_{\Rr }(f)} E_{\Rr }(q) \xrightarrow {\pi _q} F \] is naturally isomorphic to \(f\). To this end, observe that by naturality of the map \(i_p\colon E \to E_{\Rr }(p)\) in \(p\), the composite of the first two maps is given by \(E \xrightarrow {f} F \xrightarrow {i_q} E_{\Rr }(q)\), naturally in \(f\). The desired equivalence is then induced by the counit map \(\pi _q \circ i_q \iso \id _F\) of the adjunction \(\pi _q \dashv i_q\), which is an equivalence by full faithfulness of \(i_q\).
Next, consider a morphism \(g\colon E_{\Rr }(p) \to F\) in \((\Cat _\infty )^{\Rr \mathrm {-cocart}}_{/S}\). We must show that the composite \[ E_{\Rr }(p) \xrightarrow {E_{\Rr }(i_p)} E_{\Rr }(E_{\Rr }(p)) \xrightarrow {E_{\Rr }(g)} E_{\Rr }(q) \xrightarrow {\pi _q} F \] is naturally isomorphic to \(g\). By Lemma 17.2.6, the composite of the last two maps is naturally equivalent to the composite \(E_{\Rr }(E_{\Rr }(p)) \xrightarrow {\pi _{E_{\Rr }(p)}} E_{\Rr }(p) \xrightarrow {g} F\); note that the natural isomorphism given there is natural in \(g\). The map \(\pi _{E_{\Rr }(p)}\) is given by composition in \(\Rr \): it sends a tuple \(((e,r\colon x \to y), r'\colon y \to z)\) to \((e, r'r\colon x \to z)\). In particular, if \(r = \id _y\) is the identity, this results in \((e, r'\colon y \to z)\). It follows that the composite \(\pi _{E_{\Rr }(p)} \circ E_{\Rr }(i_p)\) is naturally equivalent to \(\id _{E_{\Rr }(p)}\). This finishes the proof of the second statement of the proposition.
The first statement immediately follows from the second one by passing to groupoid cores on both sides, so that the left-hand side becomes \(\Hom _{(\Cat _\infty )^{\Rr \mathrm {-cocart}}_{/S}}(E_{\Rr }(p),F)\), while the right-hand side becomes \(\Hom _{(\Cat _\infty )_{/S}}(E,F)\). □
Generated from the authoritative LaTeX source.