Proof.
By Discriminants, Lemma 49.11.7 for every $x \in X$ we can find $d \geq 1$ and a commutative diagram
\[ \xymatrix{ Y \ar[d] & V \ar[d] \ar[l] \ar[r] & V_ d \ar[d] \ar[r] & Y_ d = \mathop{\mathrm{Spec}}(B_ d) \ar[d] \\ X & U \ar[l] \ar[r] & U_ d \ar[r] & X_ d = \mathop{\mathrm{Spec}}(A_ d) } \]
such that $x \in U \subset X$ is affine open, $V = f^{-1}(U)$ and $V = U \times _{U_ d} V_ d$. Write $U = \mathop{\mathrm{Spec}}(A)$ and $V = \mathop{\mathrm{Spec}}(B)$ and observe that $B = A \otimes _{A_ d} B_ d$ and recall that $B_ d = A_ d e_1 \oplus \ldots \oplus A_ d e_ d$. Suppose we have $a_1, \ldots , a_ r \in A$ and $b_1, \ldots , b_ s \in B$. We may write $b_ j = \sum a_{j, l} e_ d$ with $a_{j, l} \in A$. Set $N = r + sd$ and consider the factorizations
\[ \xymatrix{ V \ar[r] \ar[d] & V' = \mathbf{A}^ N \times V_ d \ar[r] \ar[d] & V_ d \ar[d] \\ U \ar[r]& U' = \mathbf{A}^ N \times U_ d \ar[r] & U_ d } \]
Here the horizontal lower right arrow is given by the morphism $U \to U_ d$ (from the earlier diagram) and the morphism $U \to \mathbf{A}^ N$ given by $a_1, \ldots , a_ r, a_{1, 1}, \ldots , a_{s, d}$. Then we see that the functions $a_1, \ldots , a_ r$ are in the image of $\Gamma (U', \mathcal{O}_{U'}) \to \Gamma (U, \mathcal{O}_ U)$ and the functions $b_1, \ldots , b_ s$ are in the image of $\Gamma (V', \mathcal{O}_{V'}) \to \Gamma (V, \mathcal{O}_ V)$. In this way we see that for any finite collection of elements1 of the groups
\[ \Gamma (V, \Omega ^ i_{Y/\mathbf{Z}}),\quad i = 0, 1, 2, \ldots \quad \text{and}\quad \Gamma (U, \Omega ^ j_{X/\mathbf{Z}}),\quad j = 0, 1, 2, \ldots \]
we can find a factorizations $V \to V' \to V_ d$ and $U \to U' \to U_ d$ with $V' = \mathbf{A}^ N \times V_ d$ and $U' = \mathbf{A}^ N \times U_ d$ as above such that these sections are the pullbacks of sections from
\[ \Gamma (V', \Omega ^ i_{V'/\mathbf{Z}}),\quad i = 0, 1, 2, \ldots \quad \text{and}\quad \Gamma (U', \Omega ^ j_{U'/\mathbf{Z}}),\quad j = 0, 1, 2, \ldots \]
The upshot of this is that to check $\text{d} \circ \Theta _{Y/X} = \Theta _{Y/X} \circ \text{d}$ it suffices to check this is true for $\Theta _{V'/U'}$. Similarly, for property (2) of the lemma.
By Discriminants, Lemmas 49.11.4 and 49.11.5 the scheme $U_ d$ is smooth and the morphism $V_ d \to U_ d$ is étale over a dense open of $U_ d$. Hence the same is true for the morphism $V' \to U'$. Since $\Omega _{U'/\mathbf{Z}}$ is locally free and hence $\Omega ^ p_{U'/\mathbf{Z}}$ is torsion free, it suffices to check the desired relations after restricting to the open over which $V'$ is finite étale. Then we may check the relations after a surjective étale base change. Hence we may split the finite étale cover and assume we are looking at a morphism of the form
\[ \coprod \nolimits _{i = 1, \ldots , d} W \longrightarrow W \]
with $W$ smooth over $\mathbf{Z}$. In this case any local properties of our construction are trivial to check (provided they are true). This finishes the proof of (1) and (2).
Finally, we observe that (3) follows from (2) because $\Omega _{Y/S}$ is the quotient of $\Omega _{Y/\mathbf{Z}}$ by the submodule generated by pullbacks of local sections of $\Omega _{S/\mathbf{Z}}$.
$\square$
Comments (2)
Comment #5436 by Shogōki on
Comment #5662 by Johan on