Averaging differential forms over the circle (source code)

= 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.