Lemma 37.73.2. Let $f : X \to Y$ be a locally quasi-finite morphism of finite presentation. Let $w : X \to \mathbf{Z}$ be a weighting of $f$. Then the level sets of the function $\int _ f w$ are locally constructible in $Y$.

Proof. By Lemma 37.72.1 formation of the function $\int _ f w$ commutes with arbitrary base change and by Lemma 37.72.3 after base change we still have a weighthing. This means that if we can find $Y' \to Y$ surjective and of finite presentation, then it suffices to prove the result after base change to $Y'$, see Morphisms, Theorem 29.22.3.

The question is local on $Y$ hence we may assume $Y$ is affine. Then $X$ is quasi-compact and quasi-separated (as $f$ is of finite presentation). Suppose that $X = U \cup V$ are quasi-compact open. Then we have

$\textstyle {\int }_ f w = \textstyle {\int }_{f|_ U} w|_ U + \textstyle {\int }_{f|_ V} w|_ V - \textstyle {\int }_{f|_{U \cap V}} w|_{U \cap V}$

Thus if we know the result for $w|_ U$, $w|_ V$, $w|_{U \cap V}$ then we know the result for $w$. By the induction principle (Cohomology of Schemes, Lemma 30.4.1) it suffices to prove the lemma when $X$ is affine.

Assume $X$ and $Y$ are affine. We may choose an open immersion $X \to T$ where $T \to Y$ is finite, see Lemma 37.42.3. Because we may still base change with a suitable $Y' \to Y$ we can use Morphisms, Lemma 29.48.6 to reduce to the case where all residue field extensions induced by the morphism $T \to Y$ (and a foriori induced by $X \to Y$) are trivial. In this situation $\int _ f w$ is just taking the sums of the values of $w$ in fibres. The level sets of $w$ are locally constructible in $X$ (Lemma 37.73.1). The function $w$ only takes a finite number of values by Properties, Lemma 28.2.7. Hence we conclude by Morphisms, Theorem 29.22.3 and some elementary arguments on sums of integers. $\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).