# Proving one version of equivariant formality

Let $G$ be a compact, connected Lie group acting smoothly on a compact, connected and oriented smooth manifold $M$. We denote by $H_G^*(M)$ the corresponding equivariant cohomology.

We have a canonical map, the characteristic map, $$c:H^*(BG)\rightarrow H_G^*(M)$$ that endows $H_G^*(M)$ with the structure of an $H^*(BG)$-module.

There's also a canonical restriction map $$r:H_G^*(M)\rightarrow H^*(M).$$ We say that $M$ is equivariantly formal if $r$ is onto.

Any hints on how to prove the following will be appreciated:

Propositon: If $M$ is equivariantly formal, then $H_G^*(M)\simeq H^*(M)\otimes H^*(BG)$ as $H^*(BG)$-modules.

N.B.: I am aware that there are many different ways to define equivariant formality, but I'd like to use only the given definitions, if possible.

$H_G^{\ast}(M)$ is the ordinary cohomology of a fiber bundle $E$ over $BG$ with fiber $M$. The restriction map $H_G^{\ast}(M)\to H^{\ast}(M)$ is induced by inclusion of $M$ into $E$ as a fiber. Since $H^{m}(BG;\mathbb{Q})$ and $H^n(M;\mathbb{Q})$ are finite dimensional vector spaces over $\mathbb{Q}$ for all $m$ and $n$ and $H_G^{\ast}(M)\to H^{\ast}(M)$ is surjective, all of the conditions of the Leray-Hirsch theorem are satisfied, which gives the desired module isomorphism.