$\newcommand{\T}{\mathscr{T}}\newcommand{\C}{\mathscr{C}^\infty}$I've been enjoying Iversen's book on sheaf cohomology. He briefly mentions De Rham cohomology and a sheafy perspective on it but he doesn't mention if the canonical isomorphism is functorial; everyone says that it is, but with the sheaf perspective I'm not so sure. It's not been clear to me or people I've talked to how to even define sheafy De Rham cohomology as a functor. To explain the problem I need to explain his definition first.
Let "smooth manifold" mean the usual but emphasise second-countable, Hausdorff and being without boundary (the latter for convenience and the first two because we need our manifolds to be $\sigma$-compact). All sheaves and sheaf morphisms considered will be of $\Bbb R$-sheaves.
For a smooth manifold $X$, let $\C_X$ denote the sheaf of smooth $\Bbb R$-valued functions. Let $\T_X$ denote the tangential sheaf; this is the sheaf with sections $\T_X(U)$ the vector space of all sheaf morphisms $\phi:\C_X|_U\to\C_X|_U$ with the property that for all open $V\subseteq U$, $\phi_V:\C_X(V)\to\C_X(V)$ is a derivation of $\Bbb R$-algebras. The sheaf action is defined by obvious restriction, and it is obviously a true sheaf.
Now for $p\ge0$ let $\Omega_X^p$ denote the De Rham sheaf, the "sheafy" notion of differential forms. This is the sheaf on $X$ with sections $\Omega^p_X(U)$ defined as the vector space of alternating morphisms of $\C_X|_U$-modules: $$\omega:\T_X|_U\otimes_{\C_X|_U}\T_X|_U\otimes_{\C_X|_U}\cdots\otimes_{\C_X|_U}\T_X|_U\to\C_X|_U$$Where $p$ sheaf tensor products are taken. The exterior derivative may be defined in the usual way and we have a complex of sheaves $\Omega^\bullet_X$ and an obvious injection $\underline{\Bbb R}\to\Omega^\bullet_X$. It can be argued with a local bump function perspective that this is a complex of soft sheaves, and since $X$ is $\sigma$-compact and LCH this means soft sheaves are acyclic for cohomology (as well as compactly supported cohomology). Then standard arguments involving finding a basis for forms on $\Bbb R^n$ and getting antiderivatives find that $\Omega^\bullet_X$ is a resolution of $\underline{\Bbb R}$ (exact iff. exact on stalks).
By abstract nonsense we conclude $H^\bullet(X;\Bbb R)\cong H^\bullet_{dR}(X)$ and $H^\bullet_C(X;\Bbb R)\cong H^\bullet_{dR,C}(X)$.
Now my question is: with this sheafy perspective on $H^\bullet_{dR}$, how is it a functor? Because I would obviously want the sheaf theory to produce a natural isomorphism between the two theories. I know this should be possible since the high and mighty speak of this e.g. Clausen refers to (some similar variant of) sheafy De Rham cohomology as a functor, but doesn't explain how that actually works. I don't know if Iversen's formulation (the presentation of which I've also slightly tweaked) is standard or not.
Classically if I have a smooth $f:X\to Y$ it's very easy to define the derivative $df$ "pointwise". If you have a derivation $D:\C(f^{-1}(W))\to\Bbb R$ you promote it to one $\C(W)\to\Bbb R$ just by assigning $g\mapsto D(g\circ f)$, for any open subset $W$ of $Y$. However Iversen's formulation is founded on vector fields, rather than tangent vectors. Looking around, we can't generally perform a similar construction for pushing forward vector fields; if I have a section $\phi$ of $\T_X(f^{-1}(W))$, I can define a derivation $\C(W)\to\C(f^{-1}(W))$ by precomposition again but I can't push that to something $\C(W)\to\C(W)$. Ideally I should have a sheafy derivative $df:f_\ast\T_X\to\T_Y$, or $\T_X\to f^\ast\T_Y$ or $\T_Y\to f_\ast\T_X$ or whatever the correct variance should be, but I'm struggling to get anything. And then of course if I don't have a derivative I don't have a hope of defining a pullback-of-forms map $\Omega_Y^p\to f_\ast\Omega_X^p$.
And that's what I really need; it can be shown that $f^\ast:H^\bullet(Y;\Bbb R)\to H^\bullet(X;\Bbb R)$ would be computable by (the global sections of) any chain map $F:\Omega^\bullet_Y\to f_\ast\Omega_X^\bullet$ which, in degree zero, equals the precomposition map $f^\ast:\C_Y\to f_\ast\C_X$. But how do I find such a chain map $F$?
Best Answer
$\newcommand{\T}{\mathscr{T}}\newcommand{\C}{\mathscr{C}^\infty}$Thanks to a helpful onlooker, there is a very satisfactory solution making the sheafy definition functorial and agreeing with ordinary cohomology; it probably descends to something equivalent to the classical definition, and I can write it up now. I'm sure the universal derivation perspective offered in comments by Aphelli also works out but I was less sure of the details.
In my question, I lamented the lack of a "derivative". Well, turns out there is one. We don't need to work with tangent vectors and pointwise stuff, we can just locally use Jacobians.
Fix smooth manifolds $X,Y$ and some $F:X\to Y$. Let $F^{-1}$ denote the sheaf theoretic preimage. Observe that precomposition by $F$ yields a map $\C_Y\to F_\ast\C_X$ of $\Bbb R$-sheaves on $Y$, even of $\Bbb R$-algebras, and by adjunction there is a map $F^{-1}\C_Y\to\C_X$ of $\Bbb R$-algebra-sheaves on $X$, making $\C_X$ a $F^{-1}\C_Y$-module. Thus there is a pullback $F^\ast$ of $\C_Y$-modules to $\C_X$-modules, given by: $F^\ast\mathscr{F}:=\C_X\otimes_{F^{-1}\C_Y}F^{-1}\mathscr{F}$.
This has the property that it preserves direct sums and takes tensor products over $\C_Y$ to tensor products over $\C_X$ in a manner preserving multiplication; $F^\ast\mathscr{F}\otimes_{\C_X}F^\ast\mathscr{G}\cong F^\ast(\mathscr{F}\otimes_{\C_Y}\mathscr{G})$ is $\C_X$-multilinear, as it essentially just comes from $\C_X\otimes_{\C_X}\C_X\cong\C_X$.
We seek a derivative $dF:\T_X\to F^\ast\T_Y$. Consider the open cover $\mathfrak{U}$ of $X$ by charts $U$ such that $F(U)$ is contained in a chart $V$ of $Y$ (by continuity this really does cover). Since $F^{-1}(\mathscr{F}|_V)=(F^{-1}\mathscr{F})|_U$ holds, if we choose coordinates on $U,V$ (say $\dim X=n,\dim Y=m$) then $\T_X|_U,\T_Y|_V$ are free of ranks $N,M$ with a global basis given by $\frac{\partial}{\partial x_\mu},\frac{\partial}{\partial y_\nu}$ for $1\le\mu\le N,1\le\nu\le M$; it follows that $F^\ast\T_Y$ is free (as a $\C_X$-module) with basis the $F^{-1}(\partial/\partial y_\nu)$.
Under this identification, to define $dF$ locally on $U$ we need to specify a map $\oplus_{\mu=1}^N\C_X\to\oplus_{\nu=1}^M\C_X$ and this is easily done through the smooth entries of the Jacobian of $F$. Explicitly, $\frac{\partial}{\partial x_\mu}\mapsto\sum_{\nu=1}^M\frac{\partial F_\nu}{\partial x_\mu}\cdot F^{-1}(\partial/\partial y_\nu)$ defines $dF$ on all open subsets of $U$.
The resulting map is independent of the coordinates by Jacobian properties and also of the choice of containing chart $V$ by preimage properties. It then follows these sheaf morphisms $dF|_U,U\in\mathfrak{U}$ are compatible on their intersections, using again the fact "$F^\ast$" behaves well with restriction.
$dF$ could be defined in the same way if one replaced $Y$ with an open $W\subseteq Y$ and $X$ with $F^{-1}(W)$, and $(dF)_{F^{-1}(W)}=d(F|_{F^{-1}(W)})$ would hold true, the definitions would clearly give the same thing.
Now that that's done, given any $n$-form $\omega$ on an open subset $W$ of $Y$ there is a composite: $$\bigotimes_{\C_X|_{F^{-1}(W)}}\T_X|_{F^{-1}(W)}\overset{\otimes dF|F^{-1}(W)}{\longrightarrow}\bigotimes_{\C_X|_{F^{-1}(W)}}F^\ast(\T_Y|_W)\cong F^\ast\left(\bigotimes_{\C_Y|_W}\T_Y|_W\right)\\\overset{F^\ast\omega}{\longrightarrow}F^\ast(\C_Y|_W)\cong\C_X|_{F^{-1}(W)}$$It is fairly clear this composition is an alternating form. It's also a map of $\C_X$-modules as it is at each stage of the composition. We can call this composition $F^\ast\omega$. So, there is a map $\Omega^n_Y(W)\to\Omega^n_X(F^{-1}(W))$, obviously $\Bbb R$-linear, and it does behave well under restriction. We derive a map $F^\ast:\Omega^n_Y\to F_\ast\Omega^n_X$, as required.
We have to check it's a chain map too. It's enough to check this locally and pretend $X=\Bbb R^N,Y=\Bbb R^M$ with the standard coordinates. Observe that a pure tensor section $1\otimes F^{-1}g$ in $\C_X\otimes_{F^{-1}\C_Y}F^{-1}\C_Y=F^\ast\C_Y$, where $g:Y\to\Bbb R$ is smooth, is identified with $g\circ F$ under $F^\ast\C_Y=\C_X$. Observe further that: $$F\ast(g\,\omega\wedge\omega')=(g\circ F)\,(F^\ast\omega)\wedge(F^\ast\omega')$$Always holds. These are easy checks from the definition, $F^\ast$ is essentially just a precomposition operator. Since, locally, the differential forms have the $g\,dy_\alpha$ as a $\Bbb R$-basis, $\alpha$ a multiindex, to check $d\circ F^\ast=F^\ast\circ d$ it suffices to check it on those basis forms and by the observation and the Leibniz rule and induction on dimension it suffices to check this for the fundamental $0$ and $1$ forms, the smooth functions and the $dy_i$ for $1\le k\le M$.
Let $g$ be a zero form. We need to check $F^\ast(dg)=d(g\circ F)$. Evaluated on any fundamental vector field $\frac{\partial}{\partial x_k}$, the LHS reads: $$\sum_j\frac{\partial F_j}{\partial x_k}F^{-1}(dg(\partial/\partial y_j))=\sum_j\frac{\partial F_j}{\partial x_k}\frac{\partial g}{\partial y_j}\Big|_F=\frac{\partial(g\circ F)}{\partial x_k}$$Which is the right hand side evaluated at $\frac{\partial}{\partial x_k}$.
It now remains to show $d(F^\ast(dy_i))=0$. It is clear $F^\ast(dy_i)=\sum_j\frac{\partial F_i}{\partial x_j}\,dx_j$ as an equality of $1$-forms. The exterior derivative of this evaluated at a fundamental field $(\partial_a,\partial_b)$ equals $\frac{\partial}{\partial x_a}\frac{\partial F_i}{\partial x_b}-\frac{\partial}{\partial x_b}\frac{\partial F_i}{\partial x_a}=0$ by the equality of mixed partials, so we are done.
There is a chain map $F^\ast:\Omega^\bullet_Y\to F_\ast\Omega^\bullet_X$ of $\Bbb R$-sheaves which, in degree zero, looks like precomposition by $F$ as desired. It follows from Iversen's "Scolium" for computing maps on sheaf cohomology that this chain map computes $F^\ast:H^\bullet(Y;\Bbb R)\to H^\bullet(X;\Bbb R)$. We actually only needed $F^\ast$ to preserve the locally constant functions in degree zero. Moreover the map on cohomology just gives something $H^\bullet_{dR}(Y)\to H^\bullet_{dR}(X)$ and it is reasonably easy to see this is functorial in $F$, behaves well under composition. $G_\ast\circ F_\ast=(GF)_\ast$ and $G_\ast(F^\ast)\circ G^\ast=(GF)^\ast:\Omega^\bullet_Z\to G_\ast\Omega^\bullet_Y\to(GF)_\ast\Omega^\bullet_X$ too, for all the various meanings of $(-)^\ast$, because of the chain rule for Jacobians.