Lemma 37.62.13. Let
be a commutative diagram of morphisms of schemes. Assume $S$ is locally Noetherian, $Y \to S$ is locally of finite type, $Y$ is regular, and $X \to S$ is a local complete intersection morphism. Then $f : X \to Y$ is a local complete intersection morphism and $Y \to S$ is Koszul at $f(x)$ for all $x \in X$.