Projection formula for sphere bundle integration (source code)

= Projection formula for sphere bundle integration
{title2=$\pi_!(\pi^*b\smile a)=b\smile\pi_!a$}

For the <sphere bundle> of an oriented rank-$r$ real <vector bundle>, the integration map in the <Gysin sequence> lowers degree by $r-1$. Its compatibility with the <cup product> is the displayed projection formula. The construction is the connecting map of the disk/sphere pair followed by the inverse <Thom isomorphism theorem>; the connecting map has its graded module sign, and the degree sign in the conventional fibre-integration map gives the displayed left-module formula.