Lemma 17.2.6. If \(q\colon F \to S\) is an \(\Rr \)-cocartesian fibration, the functor \(\pi _q\colon E_{\Rr }(q) \to F\) preserves \(\Rr \)-cocartesian morphisms. Moreover, given a morphism \(g\colon F \to F'\) in \((\Cat _\infty )^{\Rr \mathrm {-cocart}}_{/S}\), the Beck–Chevalley transformation \[ \pi _{q'} E_{\Rr }(g) \xrightarrow {\eta } \pi _{q'} E_{\Rr }(g) i_q \pi _q \simeq \pi _{q'} i_{q'} g \pi _q \xrightarrow {\epsilon } g \pi _q \] is a natural isomorphism. In particular, the following diagram commutes:
Proof. First consider an \(\Rr \)-cocartesian morphism \[ (e,r\colon x \to y) \longrightarrow (e,r'r\colon x \to y') \] in \(E_{\Rr }(q)\). The functor \(\pi _q\) sends it to the induced morphism \(r_!e \to (r'r)_!e\). Both the composite \(e \to r_!e \to (r'r)_!e\) and its first factor are \(q\)-cocartesian, so the second factor is \(q\)-cocartesian by Lemma 23.1.14. Thus \(\pi _q\) preserves \(\Rr \)-cocartesian morphisms.
It suffices to show that the transformation is a pointwise isomorphism for every individual object \((e,r\colon x \to y)\) in \(E_{\Rr }(q)\). Let \(\hat {r}_e\colon e \to e'\) be a \(q\)-cocartesian lift of \(r\) in \(F\), and let \(\hat {r}_{g(e)}\colon g(e) \to e''\) be a \(q\)-cocartesian lift of \(r\) in \(F'\). The universal property of \(\hat {r}_{g(e)}\) then induces a map \(e'' \to g(e')\). But since \(g\) preserves \(\Rr \)-cocartesian morphisms, the map \(g(e) \to g(e')\) is already an \(\Rr \)-cocartesian morphism, hence the map \(e'' \to g(e')\) is an isomorphism in \(F'\). Unwinding the definitions of the counit of the adjunction \(\pi _{q'} \dashv i_{q'}\) reveals that this map is precisely the map \((\pi _{q'} E_{\Rr }(g))(e,r) \to (g \pi _q)(e,r)\), finishing the proof. □
Generated from the authoritative LaTeX source.