Upper semicontinuity of proper fibre dimension

By [F1] the morphism $f$ is of finite type; fix $s\in S$. By [F5] the base change $X_s\to \mathrm{Spec}\kappa (s)$ is of finite type, hence quasi-compact by [F4], so $X_s$ is covered by finitely many affine opens $\mathrm{Spec}{A}_i$ with each $A_i$ a finite-type $\kappa (s)$-algebra by [F4]; each $A_i$ is Noetherian by [F10], hence each $\mathrm{Spec}{A}_i$ is a Noetherian topological space by [F10], and a space with a finite open cover by Noetherian subspaces is Noetherian (a descending chain of closed subsets restricts to a descending chain in each chart and therefore stabilises).

For $n\ge 0$ put $U_n=\{x\in X:$ the fibre $X_{f(x)}$ has local dimension at most $n$ at $x\}$ and $Z_n=X\setminus U_n$. Then $U_n$ is open in $X$: indeed, by [F4] it suffices to check this on an affine chart $U=\mathrm{Spec}B$ mapping into an affine $V=\mathrm{Spec}A$ with $A\to B$ finite type, and for a point $x\in U$ corresponding to $\mathfrak{q}\in \mathrm{Spec}B$ the fibre of $U\to V$ at the corresponding $\mathfrak{p}=\mathfrak{q}\cap A$ is $\mathrm{Spec}(B{\otimes }_A\kappa (\mathfrak{p}))$ by [F3], an open subscheme of $X_{f(x)}$ with the same local dimension at $x$ by [F7]; if this local dimension is $m\le n$, then clause 2 of [F8] applied with $n$ replaced by $m$ gives an open neighbourhood of $\mathfrak{q}$ inside $U$ on which the fibre local dimension is at most $m\le n$, so $U_n\cap U$ is a union of such neighbourhoods and is open.

For every $s\in S$ one has $\dim X_s={\sup }_{x\in X_s}{\dim }_x{X}_s$: the inequality ${\dim }_x{X}_s\le \dim X_s$ holds because $X_s$ itself is an open neighbourhood of $x$ and ${\dim }_x{X}_s$ is the infimum over such neighbourhoods [F7]; conversely, given a strict chain $Z_0⊊\cdots ⊊Z_d$ of nonempty irreducible closed subsets of $X_s$ and a point $x\in Z_0$, every open neighbourhood $W$ of $x$ in $X_s$ gives nonempty irreducible open subspaces $W\cap Z_0\subseteq \cdots \subseteq W\cap Z_d$ which are strictly increasing (if $W\cap Z_i=W\cap Z_{i+1}$, then this set is a nonempty open subset of the irreducible space $Z_{i+1}$ and hence dense in it by [F9], while it is contained in the closed subset $Z_i\subseteq Z_{i+1}$, whence $Z_{i+1}=Z_i$, a contradiction), so $\dim W\ge d$ and ${\dim }_x{X}_s\ge d$; taking the supremum over chains and using [F6] gives the reverse inequality.

For every $s\in S$ and every integer $d\ge 0$: $\dim X_s>d$ if and only if there is $x\in X_s$ with ${\dim }_x{X}_s>d$; this is immediate from the identification of step 1.3, the left-hand condition being the supremum of the numbers ${\dim }_x{X}_s$ exceeding $d$. In particular the empty fibre, of dimension $-\mathrm{\infty }$ by [F6], satisfies neither condition.

For every $d\ge 0$ the equality $\{s\in S:\dim X_s>d\}=f(Z_d)$ holds: if $\dim X_s>d$, step 2.1 supplies $x\in X_s$ with ${\dim }_x{X}_s>d$, and $x\in Z_d$ because the local dimension of $X_{f(x)}=X_s$ at $x$ exceeds $d$; conversely $x\in Z_d$ has $f(x)=s$ and $\dim X_s\ge {\dim }_x{X}_s>d$ by step 1.3.

By step 1.2 the set $Z_d$ is closed in $X$, and $f$ is a closed map by [F2], so $f(Z_d)$ is closed in $S$; by step 3.1 the set $\{s:\dim X_s>d\}$ is closed for every $d\ge 0$, and since $\dim X_s$ takes values in $\mathbb{N}\cup \{-\mathrm{\infty }\}$ [F6] one has $\{s:\dim X_s\ge n\}=\{s:\dim X_s>n-1\}$ for every $n\ge 1$.

For $n\ge 1$ the set $\{s:\dim X_s\ge n\}$ is closed by step 4.1, and for $n=0$ it equals $f(X)$, the image of the closed set $X$, which is closed by [F2]; hence the set is closed for every $n\ge 0$, which is the theorem. The Axiom of Choice [F11] is used exactly through the cited local fibre-dimension lemma [F8] and the cited algebra results [F10] that carry it, and no further choice is made. [F2, F6, F10, F11, step 4.1] $\mathrm{\square }$