Pullback is a morphism of de rham complexes

Given: A smooth map $F:M\to N$.

De rham cochain complex: Let $M$ be a finite-dimensional Hausdorff second-countable smooth manifold without boundary. Its real de Rham cochain complex is $({\mathrm{\Omega }}^{\bullet }(M),d)$, where ${\mathrm{\Omega }}^k(M)$ is the space of smooth $k$-forms for $0\le k\le \dim M$ and is $0$ otherwise; $d$ has degree $+1$. These are the sections in def-smooth-differential-k-form. The identity $d^{k+1}{d}^k=0$ in thm-the-exterior-derivative-squares-to-zero makes this an instance of def-cochain-complex-in-an-abelian-category. On the empty manifold each section space is the zero vector space. Whenever a product with $[0,1]$ is used, forms mean smooth forms up to the endpoints, locally extendible across them.

The exterior derivative commutes with pullback: For every smooth map $F:M\to N$ and every form $\omega$ on $N$, $d(F^{\ast }\omega )=F^{\ast }(d\omega )\mathrm{.}$

Cochain map: Let $C^{\bullet }$ and $D^{\bullet }$ be cochain complexes. A cochain map $f:C^{\bullet }\to D^{\bullet }$ is a family of morphisms $f^n:C^n\to D^n$ such that $d_D^n\circ f^n=f^{n+1}\circ d_C^n$ for every $n\in \mathbb{Z}$. Thus the upper-index square $\begin{array}{ccc}{C}^n& \stackrel{f^n}{\to }& D^n\\ d_C^n\downarrow & & \downarrow d_D^n\\ C^{n+1}& \stackrel{f^{n+1}}{\to }& D^{n+1}\end{array}$ commutes in each degree.