Lemma 17.2.3. For every functor \(p\colon E \to S\), the functor \(E_{\Rr }(p)\) is an \(\Rr \)-cocartesian fibration, and for every functor \(f\colon E \to E'\) over \(S\) with structure map \(p'\colon E' \to S\), the induced functor \(E_{\Rr }(f)\colon E_{\Rr }(p) \to E_{\Rr }(p')\) over \(S\) is an \(\Rr \)-cocartesian functor.
Proof. First note that the target functor \(t\colon \Ar _{\Rr }(S) \to S\) is an \(\Rr \)-cocartesian fibration: given an object \((r\colon x \to y) \in \Ar _{\Rr }(S)\) (i.e., a morphism in \(\Rr \)) and a morphism \(r'\colon y \to y'\) in \(\Rr \), a \(t\)-cocartesian lift of \(r'\) starting in \(r\) is given by the commutative square
In particular, we see that a morphism in \(\Ar _{\Rr }(S)\) over \(r' \in \Rr \) is \(t\)-cocartesian if and only if its image under the source functor \(s\colon \Ar _{\Rr }(S) \to S\) is an isomorphism in \(S\).
The general case is similar: given an object \((e,r\colon x \to y)\) in \(E_{\Rr }(p)\) and a morphism \(r'\colon y \to y'\) in \(\Rr \), an \(\Rr \)-cocartesian lift is given by the map \((e,r\colon x \to y) \to (e, r'r\colon x \to y')\) in \(E_{\Rr }(p)\). Indeed, the hom anima in the pullback \(E_{\Rr }(p)\) is the corresponding pullback of the hom animae in \(E\) and \(\Ar _{\Rr }(S)\), and this morphism is the identity on the \(E\)-component. Its cocartesian property therefore follows from that of the displayed morphism in \(\Ar _{\Rr }(S)\).
Note that these morphisms leave the \(E\)-component fixed. In particular, it is clear that the functor \(E_{\Rr }(f)\colon E_{\Rr }(p) \to E_{\Rr }(p')\) over \(S\) is an \(\Rr \)-cocartesian functor for every \(f\colon E \to E'\) over \(S\). □
Generated from the authoritative LaTeX source.