The Stacks project

Proof. The existence follows from general category theoretic arguments (insert future reference here), but we will also give a direct construction as this construction will be useful in the future proofs. We will freely use the notation introduced in the proof of Lemma 18.33.2. Given any differential operator $D : \mathcal{F} \to \mathcal{G}$ we obtain an $\mathcal{O}_2$-linear map $L_ D : \mathcal{O}_2[\mathcal{F}] \to \mathcal{G}$ sending $[m]$ to $D(m)$. If $D$ has order $0$ then $L_ D$ annihilates the local sections

where $g_0$ is a local section of $\mathcal{O}_2$ and $m, m'$ are local sections of $\mathcal{F}$. If $D$ has order $1$, then $L_ D$ annihilates the local sections

where $f$ is a local section of $\mathcal{O}_1$, $g_0, g_1$ are local sections of $\mathcal{O}_2$, and $m, m'$ are local sections of $\mathcal{F}$. If $D$ has order $k$, then $L_ D$ annihilates the local sections $[m + m'] - [m] - [m']$, $f[m] - [fm]$, and the local sections

Conversely, if $L : \mathcal{O}_2[\mathcal{F}] \to \mathcal{G}$ is an $\mathcal{O}_2$-linear map annihilating all the local sections listed in the previous sentence, then $m \mapsto L([m])$ is a differential operator of order $k$. Thus we see that $\mathcal{P}^ k_{\mathcal{O}_2/\mathcal{O}_1}(\mathcal{F})$ is the quotient of $\mathcal{O}_2[\mathcal{F}]$ by the $\mathcal{O}_2$-submodule generated by these local sections. $\square$