# Künneth formula for de Rham cohomology with respect to an integrable connection

I am reading through https://stacks.math.columbia.edu/tag/0FM9 which proves that for $$X,Y$$ schemes over some base $$S$$ and $$X \times _S Y \overset{p}{\rightarrow} X$$ resp. $$X \times _S Y \overset{q}{\rightarrow} Y$$ the projection morphisms, there is an isomorphism of complexes $$\mathrm{Tot}(p^{-1} \Omega^{\bullet}_{X/S} \otimes_{f^{-1}\mathcal{O}_S} q^{-1} \Omega^{\bullet}_{Y/S}) \rightarrow \Omega_{X\times_S Y} ^{\bullet},$$ where $$f:X \times_S Y \rightarrow S$$ is the structure map. Now, I am wondering whether we can show something like this for de Rham complexes with respect to integrable connections, i.e. let $$(E, \nabla_E)$$ and $$(F,\nabla_F)$$ be vector bundles over $$\mathcal{O}_X$$ and $$\mathcal{O}_Y$$ with integrable connections. We then get an integrable connection $$p^{\ast}\nabla_E \otimes q^{\ast}\nabla_F$$ on $$p^{\ast}E \otimes q^{\ast}F$$ do we have an isomorphism of complexes $$\mathrm{Tot}(p^{-1}(E \otimes \Omega^{\bullet}_{X/S}) \otimes_{f^{-1}\mathcal{O}_S} q^{-1}(F \otimes \Omega^{\bullet}_{Y/S})) \rightarrow p^{\ast}E \otimes q^{\ast}F \otimes \Omega_{X\times_S Y} ^{\bullet},$$ with the differentials induced by the connections?

EDIT: There seem to be some problems with this StacksPorject section since 0FLS is wrong. Nevertheless, the isomorphism of complexes should still exist if we replace all inverse image functors by pull-backs and tensor over $$\mathcal{O}_{X\times_S Y}$$ instead of $$f^{-1}\mathcal{O}_S$$.

Note that an $$\mathcal{O}_X$$-coherent sheaf is a D-module if and only it is a vector bundle with integrable connection. You can recover the D-module structure from your connection as follows: given $$\mathscr{E} \to \Omega_X^1\otimes\mathscr{E}$$ you can recover the D-module, i.e. the action of the tangent bundle via $$\mathcal{T}_X\otimes \mathscr{E} \to \mathcal{T}_X\otimes\Omega_X^1\otimes\mathscr{E} \to \mathscr{E}$$. For the sake of being pedantic, you can also check from Section 1.3 of the same book that for smooth morphisms, $$f^*\scr{E}$$ as a D-module will be the one coming from $$(f^*\mathscr{E}, f^*\nabla)$$. Now it should be the compatibility of de Rham fuctor with exterior product as in Theorem 0.1 of Saito. Perhaps for vector bundle with integrable connectoins Saito's theorem 0.1 was known before him?
As commented below this argument works for $$S = \operatorname{Spec}\mathbb{C}$$.
• Do you mean Proposition 1.5.18? In any way this only seems to deal with the case of schemes over $\mathbb{C}$, right? – Joachim Nov 15 '20 at 19:33
• Sorry I tagged the wrong paper of Saito. ems-ph.org/journals/… and indeed, this is dealing with the case $S=\mathbb{C}$. – guest0803 Nov 15 '20 at 19:54