Giraud's proper base change for Gerbes - Elimination of Noetherian hypotheses

Question

I was looking through Giraud's book Cohomologie Non-abelienne, and there is a very nice theorem that Giraud proves in the Noetherian case (Cohomologie Non-Abelienne VII.2.2):

Let $f:X\to Y$ be a proper map of schemes with $Y$ locally Noetherian. Then for any map $i:A\to Y$, let $X_A$ denote the pullback equipped with projections $\pi_X:X_A\to X$ and $\pi_A:X_A\to A$. Then if $F$ is a constructible étale stack on $X$, the component of the base-change transformation $$\beta_F: i^\ast f_\ast F \to π_{A,\ast} \pi_X^\ast F$$ at $F$ is an equivalence.

By standard reductions, it suffices to prove this in the case where $Y$ is a strict Henselian ring and $A\to Y$ is the inclusion of the special point. In this case, it becomes equivalent to showing that the natural map $\Gamma_X(F)\to \Gamma_{X_A}(F\rvert_{X_A})$ is an equivalence of groupoids for all constructible étale stacks $F$ on $X$.

It also follows from proper base-change for constructible sheaves of sets and the obstruction theory of $1$-sheaves that we can reduce to the case where $F$ is a constructible gerbe.

Unfortunately, the proof seems to use Noetherianness in a tricky way, where the key step of the proof seems to be a Noetherian induction argument on closed subsets (see loc. cit. VII.2.2.14-15). My intuition is that there should be some way to apply absolute approximation to reduce to the Noetherian case, but I have no idea how to approximate Henselian pairs (or if they even have Noetherian approximations in general).

Can these Noetherian hypotheses be eliminated? If so, how? Is there anywhere in the literature to take a look?

Answer 1

Edit/Warning: I just realized that I accidentally put $A$ here everywhere instead of $Y$. Since I don't want to bother rewriting the comments I left below, I'm just noting this in advance.

Ok, I think I have this by a sequence of reductions: First, prove the case where our proper map is $P^n_A\to A$. In this case, we can directly apply absolute Noetherian approximation to the base $A$, so we're done by Giraud and 3-for-2. Then, we also have the case where $X$ is projective over $A$ because proper basechange for closed immersions is obvious (using 2-topos theory, for example).

Since projective maps now satisfy basechange for constructible 1-sheaves, we can show that projective surjective maps are universal effective descent maps for constructible 1-sheaves (universal effective descent for constructible 0-sheaves implies universal descent for constructible 1-sheaves, and projective base-change for constructible 1-sheaves and universal descent for constructible 1-sheaves together imply universal effective descent for constructible 1-sheaves).

Now in the general case, apply Chow's lemma to find a proper cover $X^\prime\to X$ by an $X^\prime,$ which embeds as a closed subscheme of $P^n_A$. We then also see that $X^\prime \to P^n_A \times_A X = P^n_X$ is also a closed immersion, so now use the theorem for the projective map $X^\prime \to A$ and use effective descent for the map $X^\prime \to X$, so we're done.

The key point seems to be that you have to apply Noetherian approximation early on rather than later on.