Kerodon

Remark 7.3.7.2. In the situation of Theorem 7.3.7.1, suppose that the functor $F^{0} = F|_{ \operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}}$ admits a $V$-left Kan extension $F': \operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$ satisfying $V \circ F' = V \circ F$. Then the converse of Theorem 7.3.7.1 is also true: if $f$ is $V'$-left Kan extended from $\operatorname{\mathcal{A}}^{0}$, then $F$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$. To prove this, it will suffice to show that the functors $F$ and $F'$ are isomorphic (Remark 7.3.3.17). This is clear: we can identify $F'$ with a functor $f': \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ satisfying $V' \circ f' = V' \circ f$, and Theorem 7.3.7.1 guarantees that $f'$ is $V'$-left Kan extended from $\operatorname{\mathcal{A}}^{0}$. Since the functors $f$ and $f'$ coincide on $\operatorname{\mathcal{A}}^{0}$, they are isomorphic by virtue of Theorem 7.3.6.14.