Compactly supported de Rham cohomology is contravariant for proper smooth maps

By [F1] and [F3], pullback restricts to a linear cochain map on compactly supported forms. If $\omega$ is closed, then $d(F^{\ast }\omega )=F^{\ast }(d\omega )=0$. If another compactly supported closed representative is $\omega +d\eta$ with $\eta$ compactly supported, [F1] makes $F^{\ast }\eta$ compactly supported and [F3] gives $F^{\ast }(\omega +d\eta )-F^{\ast }\omega =d(F^{\ast }\eta )\mathrm{.}$ Thus the displayed rule is independent of representatives in precisely the quotient [F4], and real linearity follows by applying linear pullback to linear combinations of representatives.

The identity map is proper since its inverse image of a compact set is that set. The composite $G\circ F$ is proper since $(G\circ F{)}^{-1}(K)=F^{-1}(G^{-1}(K))$, and each successive inverse image is compact by the respective hypothesis. Their smoothness and pullback equations follow from [F3]. On a representative class, $(G\circ F{)}_c^{\ast }[\omega ]=[(G\circ F{)}^{\ast }\omega ]=[F^{\ast }{G}^{\ast }\omega ]=F_c^{\ast }{G}_c^{\ast }[\omega ]\mathrm{.}$ The identity equality follows from ${\mathrm{id}}^{\ast }\omega =\omega$. Step 1.1 makes these equalities well defined on every class, proving the claimed contravariant functor.

Inclusion of compactly supported forms into all forms commutes with $d$ and sends every compactly supported primitive to an ordinary primitive. It therefore induces $j_M:H_c^k(M)\to H_{\mathrm{d}\mathrm{R}}^k(M)$, without claiming that $j_M$ is injective. Both $j_M{F}_c^{\ast }[\omega ]$ and $F^{\ast }{j}_N[\omega ]$ are the ordinary class of the same form $F^{\ast }\omega$, with ordinary pullback supplied by [F2] in the boundaryless case and [F3] in the boundary case. Hence $j_M{F}_c^{\ast }=F^{\ast }{j}_N$.

Empty manifolds give zero cohomology. In degree zero no negative-degree primitive exists, and step 1.1 is ordinary composition of closed compactly supported functions. In degree one the changed representative uses a compactly supported function primitive; in top degree it still requires a compactly supported incoming primitive. Negative degrees are zero. Identity maps and constant maps are covered whenever they meet the stated properness hypothesis, and boundaries use [F3]. Only the given representatives and their given compact primitives occur, so there is no choice of a family of representatives or primitives and no AC.