Proof.
Note that the assumption on $Y' \to Y$ implies that for $y' \in Y'$ mapping to $y \in Y$ the field extension $\kappa (y')/\kappa (y)$ is finitely generated. Hence also all the fibres $X'_{y'} = (X_ y)_{\kappa (y')}$ are locally Noetherian, see Varieties, Lemma 33.11.1. Thus the lemma makes sense. Set $y' = f'(x')$ and $y = f(x)$. Hence we get the following commutative diagram of local rings
\[ \xymatrix{ \mathcal{O}_{X', x'} & \mathcal{O}_{X, x} \ar[l] \\ \mathcal{O}_{Y', y'} \ar[u] & \mathcal{O}_{Y, y} \ar[l] \ar[u] } \]
where the upper left corner is a localization of the tensor product of the upper right and lower left corners over the lower right corner.
Assume $f$ is Gorenstein at $x$. The flatness of $\mathcal{O}_{Y, y} \to \mathcal{O}_{X, x}$ implies the flatness of $\mathcal{O}_{Y', y'} \to \mathcal{O}_{X', x'}$, see Algebra, Lemma 10.100.1. The fact that $\mathcal{O}_{X, x}/\mathfrak m_ y\mathcal{O}_{X, x}$ is Gorenstein implies that $\mathcal{O}_{X', x'}/\mathfrak m_{y'}\mathcal{O}_{X', x'}$ is Gorenstein, see Lemma 48.25.1. Hence we see that $f'$ is Gorenstein at $x'$.
Assume $f$ is flat at $x$ and $f'$ is Gorenstein at $x'$. The fact that $\mathcal{O}_{X', x'}/\mathfrak m_{y'}\mathcal{O}_{X', x'}$ is Gorenstein implies that $\mathcal{O}_{X, x}/\mathfrak m_ y\mathcal{O}_{X, x}$ is Gorenstein, see Lemma 48.25.1. Hence we see that $f$ is Gorenstein at $x$.
Assume $Y' \to Y$ is flat at $y'$ and $f'$ is Gorenstein at $x'$. The flatness of $\mathcal{O}_{Y', y'} \to \mathcal{O}_{X', x'}$ and $\mathcal{O}_{Y, y} \to \mathcal{O}_{Y', y'}$ implies the flatness of $\mathcal{O}_{Y, y} \to \mathcal{O}_{X, x}$, see Algebra, Lemma 10.100.1. The fact that $\mathcal{O}_{X', x'}/\mathfrak m_{y'}\mathcal{O}_{X', x'}$ is Gorenstein implies that $\mathcal{O}_{X, x}/\mathfrak m_ y\mathcal{O}_{X, x}$ is Gorenstein, see Lemma 48.25.1. Hence we see that $f$ is Gorenstein at $x$.
$\square$
Comments (4)
Comment #7719 by Andrew on
Comment #7720 by Johan on
Comment #7721 by Laurent Moret-Bailly on
Comment #7972 by Stacks Project on