Averaging differential forms over the circle

Let $S^1$ act on $M\times S^1$ by rotation of the second factor. Averaging a differential form over this action is a cochain map. Every rotation is homotopic to the identity through smooth rotations, and integrating Cartan's magic formula along them gives a cochain homotopy between the averaging map and the identity. Consequently every de Rham cohomology class has a rotation-invariant representative, and an invariant exact form has an invariant primitive obtained by averaging any primitive.

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.