Lemma 114.19.1. Notation and assumptions as above. Let $p : X_ A \to X$ denote the projection. Given $A'$ denote $p' : X_{A'} \to X$ the projection. The functor $p'_*$ induces an equivalence of categories between

1. the category $\textit{Lift}(\mathcal{F}, A')$, and

2. the category $\textit{Lift}(p_*\mathcal{F}, A')$.

Proof. FIXME. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).