Lemma 37.62.1. Let $S$ be a scheme. Let $U$, $P$, $P'$ be schemes over $S$. Let $u \in U$. Let $i : U \to P$, $i' : U \to P'$ be immersions over $S$. Assume $P$ and $P'$ smooth over $S$. Then the following are equivalent

$i$ is a Koszul-regular immersion in a neighbourhood of $x$, and

$i'$ is a Koszul-regular immersion in a neighbourhood of $x$.

**Proof.**
Assume $i$ is a Koszul-regular immersion in a neighbourhood of $x$. Consider the morphism $j = (i, i') : U \to P \times _ S P' = P''$. Since $P'' = P \times _ S P' \to P$ is smooth, it follows from Divisors, Lemma 31.22.9 that $j$ is a Koszul-regular immersion, whereupon it follows from Divisors, Lemma 31.22.12 that $i'$ is a Koszul-regular immersion.
$\square$

## Comments (1)

Comment #8552 by Hayama Kazuma on

There are also: