de Rham cohomology of a product with a circle ($H_{\mathrm{dR}}^k(M\times S^1)\cong H_{\mathrm{dR}}^k(M)\oplus H_{\mathrm{dR}}^{k-1}(M)$)

Choose a closed one-form $\nu$ on $S^1$ with integral one and let $p:M\times S^1\to M$ be projection. Every rotation-invariant $k$-form is uniquelyThe exterior derivative acts componentwise. Averaging therefore proves thatis the displayed isomorphism.