The Stacks project

Proof. We have constructed the map $\Omega ^\bullet _{X/S} \to \Omega ^\bullet _{L^\star /S, 0}$ above.

Construction of $\text{Res} : \Omega ^\bullet _{L^\star /S, 0} \to \Omega ^\bullet _{X/S}[-1]$. Let $U \subset X$ be an open and let $s \in \mathcal{L}(U)$ and $s' \in \mathcal{L}^{\otimes -1}(U)$ be sections such that $s' s = 1$. Then $s$ gives an invertible section of the sheaf of algebras $(L^\star \to X)_*\mathcal{O}_{L^\star }$ over $U$ with inverse $s' = s^{-1}$. Then we can consider the $1$-form $\text{d}\log (s) = s' \text{d}(s)$ which is an element of $\Omega ^1_{L^\star /S, 0}(U)$ by our construction of the grading on $\Omega ^1_{L^\star /S}$. Our computations on affines given below will show that $1$ and $\text{d}\log (s)$ freely generate $\Omega ^\bullet _{L^\star /S, 0}|_ U$ as a right module over $\Omega ^\bullet _{X/S}|_ U$. Thus we can define $\text{Res}$ over $U$ by the rule

for all $\omega ', \omega \in \Omega ^\bullet _{X/S}(U)$. This map is independent of the choice of local generator $s$ and hence glues to give a global map. Namely, another choice of $s$ would be of the form $gs$ for some invertible $g \in \mathcal{O}_ X(U)$ and we would get $\text{d}\log (gs) = g^{-1}\text{d}(g) + \text{d}\log (s)$ from which the independence easily follows. Finally, observe that our rule for $\text{Res}$ is compatible with differentials as $\text{d}(\omega ' + \text{d}\log (s) \wedge \omega ) = \text{d}(\omega ') - \text{d}\log (s) \wedge \text{d}(\omega )$ and because the differential on $\Omega ^\bullet _{X/S}[-1]$ sends $\omega '$ to $-\text{d}(\omega ')$ by our sign convention in Homology, Definition 12.14.7.

Local computation. We can cover $X$ by affine opens $U \subset X$ such that $\mathcal{L}|_ U \cong \mathcal{O}_ U$ which moreover map into an affine open $V \subset S$. Write $U = \mathop{\mathrm{Spec}}(A)$, $V = \mathop{\mathrm{Spec}}(R)$ and choose a generator $s$ of $\mathcal{L}$. We find that we have

Computing differentials we see that

and therefore taking exterior powers we obtain

Taking degree $0$ parts we find

and the proof of the lemma is complete. $\square$