The Stacks project

Proof. The set is open by definition (see Definition 37.62.2). Let $S' \to S$ be a morphism of schemes. Set $X' = S' \times _ S X$, $Y' = S' \times _ S Y$, and denote $f' : X' \to Y'$ the base change of $f$. Let $x' \in X'$ be a point such that $f'$ is Koszul at $x'$. Denote $s' \in S'$, $x \in X$, $y' \in Y'$ , $y \in Y$, $s \in S$ the image of $x'$. Note that $f$ is locally of finite presentation, see Morphisms, Lemma 29.21.11. Hence we may choose an affine neighbourhood $U \subset X$ of $x$ and an immersion $i : U \to \mathbf{A}^ n_ Y$. Denote $U' = S' \times _ S U$ and $i' : U' \to \mathbf{A}^ n_{Y'}$ the base change of $i$. The assumption that $f'$ is Koszul at $x'$ implies that $i'$ is a Koszul-regular immersion in a neighbourhood of $x'$, see Lemma 37.62.3. The scheme $X'$ is flat and locally of finite presentation over $S'$ as a base change of $X$ (see Morphisms, Lemmas 29.25.8 and 29.21.4). Hence $i'$ is a relative $H_1$-regular immersion over $S'$ in a neighbourhood of $x'$ (see Divisors, Definition 31.22.2). Thus the base change $i'_{s'} : U'_{s'} \to \mathbf{A}^ n_{Y'_{s'}}$ is a $H_1$-regular immersion in an open neighbourhood of $x'$, see Divisors, Lemma 31.22.1 and the discussion following Divisors, Definition 31.22.2. Since $s' = \mathop{\mathrm{Spec}}(\kappa (s')) \to \mathop{\mathrm{Spec}}(\kappa (s)) = s$ is a surjective flat universally open morphism (see Morphisms, Lemma 29.23.4) we conclude that the base change $i_ s : U_ s \to \mathbf{A}^ n_{Y_ s}$ is an $H_1$-regular immersion in a neighbourhood of $x$, see Descent, Lemma 35.23.32. Finally, note that $\mathbf{A}^ n_ Y$ is flat and locally of finite presentation over $S$, hence Divisors, Lemma 31.22.7 implies that $i$ is a (Koszul-)regular immersion in a neighbourhood of $x$ as desired. $\square$