Lemma 23.7.6. Let $R \to S$ be a local ring map of Noetherian local rings. Let $I \subset R$ and $J \subset S$ be ideals with $IS \subset J$. If $R \to S$ is flat and $S/\mathfrak m_ RS$ is regular, then the following are equivalent

1. $J$ is generated by a regular sequence and $S/J$ has finite tor dimension as a module over $R/I$,

2. $J$ is generated by a regular sequence and $\text{Tor}^{R/I}_ p(S/J, R/\mathfrak m_ R)$ is nonzero for only finitely many $p$,

3. $I$ is generated by a regular sequence and $J/IS$ is generated by a regular sequence in $S/IS$.

Proof. If (3) holds, then $J$ is generated by a regular sequence, see for example More on Algebra, Lemmas 15.30.13 and 15.30.7. Moreover, if (3) holds, then $S/J = (S/I)/(J/I)$ has finite projective dimension over $S/IS$ because the Koszul complex will be a finite free resolution of $S/J$ over $S/IS$. Since $R/I \to S/IS$ is flat, it then follows that $S/J$ has finite tor dimension over $R/I$ by More on Algebra, Lemma 15.66.11. Thus (3) implies (1).

The implication (1) $\Rightarrow$ (2) is trivial. Assume (2). By More on Algebra, Lemma 15.77.6 we find that $S/J$ has finite tor dimension over $S/IS$. Thus we can apply Lemma 23.7.5 to conclude that $IS$ and $J/IS$ are generated by regular sequences. Let $f_1, \ldots , f_ r \in I$ be a minimal system of generators of $I$. Since $R \to S$ is flat, we see that $f_1, \ldots , f_ r$ form a minimal system of generators for $IS$ in $S$. Thus $f_1, \ldots , f_ r \in R$ is a sequence of elements whose images in $S$ form a regular sequence by More on Algebra, Lemmas 15.30.15 and 15.30.7. Thus $f_1, \ldots , f_ r$ is a regular sequence in $R$ by Algebra, Lemma 10.68.5. $\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).