The Stacks project

Proof. Our assumption is that for every $y \in Y$ and local equation $f \in \mathcal{O}_{X, y}$ of $Y$ we have

for some module $M$ with $f$-torsion free exterior powers $\wedge ^ p(M)$. It follows that

Below we will tacitly use these facts. In particular the sheaves $\Omega ^ p_{X/S}$ have no nonzero local sections supported on $Y$ and we have a canonical inclusion

see More on Flatness, Section 38.42. Let $U = \mathop{\mathrm{Spec}}(A)$ be an affine open subscheme such that $Y \cap U = V(f)$ for some nonzerodivisor $f \in A$. Let us consider the $\mathcal{O}_ U$-submodule of $\Omega ^ p_{X/S}(Y)|_ U$ generated by $\Omega ^ p_{X/S}|_ U$ and $\text{d}\log (f) \wedge \Omega ^{p - 1}_{X/S}$ where $\text{d}\log (f) = f^{-1}\text{d}(f)$. This is independent of the choice of $f$ as another generator of the ideal of $Y$ on $U$ is equal to $uf$ for a unit $u \in A$ and we get

which is a section of $\Omega _{X/S}$ over $U$. These local sheaves glue to give a quasi-coherent submodule

Let us agree to think of $\Omega ^ p_{Y/S}$ as a quasi-coherent $\mathcal{O}_ X$-module. There is a unique surjective $\mathcal{O}_ X$-linear map

defined by the rule

for all opens $U$ as above and all $\eta ' \in \Omega ^ p_{X/S}(U)$ and $\eta \in \Omega ^{p - 1}_{X/S}(U)$. If a form $\eta $ over $U$ restricts to zero on $Y \cap U$, then $\eta = \text{d}f \wedge \eta ' + f\eta ''$ for some forms $\eta '$ and $\eta ''$ over $U$. We conclude that we have a short exact sequence

for all $p$. We still have to define the differentials $\Omega ^ p_{X/S}(\log Y) \to \Omega ^{p + 1}_{X/S}(\log Y)$. On the subsheaf $\Omega ^ p_{X/S}$ we use the differential of the de Rham complex of $X$ over $S$. Finally, we define $\text{d}(\text{d}\log (f) \wedge \eta ) = -\text{d}\log (f) \wedge \text{d}\eta $. The sign is forced on us by the Leibniz rule (on $\Omega ^\bullet _{X/S}$) and it is compatible with the differential on $\Omega ^\bullet _{Y/S}[-1]$ which is after all $-\text{d}_{Y/S}$ by our sign convention in Homology, Definition 12.14.7. In this way we obtain a short exact sequence of complexes as stated in the lemma. $\square$