Let \(\pi:P\rightarrow M\) be a principal \(G\) bundle.
Let \(F\) be a smooth manifold with an action of \(G\) from left (note that action of \(G\) on \(P\) is from right). Given this we want to associate a fiber bundle over \(M\). This action is same thing as giving a smooth map \(G\times F\rightarrow F\).
We look for a fiber bundle with fibre \(G\times F\) and see if we can construct another fibre bundle with fibre \(F\) from the map \(G\times F\rightarrow F\).
Given a principal \(G\) bundle \(P\rightarrow M\), a smooth manifold \(F\) with an action of \(G\), we want to associate a fiber bundle whose fiber is \(F\) and base is \(M\).
Action of \(G\) on \(P, F\) induce action of \(G\) on \(P\times F\) with \((g,(p,f)\mapsto (pf, gf)\).
The map \(P\rightarrow M\) induce map \(P\times F\rightarrow M\) with \((p,f)\mapsto \pi(p)\) for \((p,f)\in P\times F\).
This further induce map \(\pi_F:(P\times F)/G\rightarrow M\) with \(([p,f])\mapsto \pi(p)\).
Is this well defined?
If \((p,f)\sim (q,f')\) then, is \(\pi(p)=\pi(q)\)?
\((p,f)\sim (q,f')\) when there is a \(g\in G\) such that \(q=pg, f'=fg\).
In that case of \(q=pg\), we know that \(\pi(p)=\pi(q)\) (property of principal bundle).
So, the map is well defined.
Now, what is the fiber of an element \(m\in M\) via the map \((P\times F)/G\rightarrow M\)?
An element in fiber is \([(p,f)]\) such that \(\pi(p)=m\).
Fix \(p\in \pi^{-1}(m)\).
Take \(f\in F\) and assign \([(p,f)]\). This gives a map \(\psi:F\rightarrow \pi_F^{-1}(m)\).
let us check one-one nature.
Suppose \(f_1,f_2\in F\) be such that \([(p,f_1)]=[(p,f_2)]\) that means, there exists \(g\in G\) such that \(pg=p\) and \(f_2=f_1g\).
Free action of \(G\) on \(P\) says \(g=1\) which in turn says \(f_2=f_1\).
Let us check onto nature.
Let \([(q,f)]\in \pi_F^{-1}(m)\). We need to find \(f'\in F\) such that, \(\psi(f')=[(q,f)]\); that is, \([(p,f')]=[(q,f)]\).
The condition \(q\in \pi^{-1}(m)\) says that, there exists \(g\in G\) such that, \(p=qg\).
Consider \(f'=gf\).
For this, we have \([(p,f')]=[(q,f)]\), concluding that \(\psi\) is surjective.
Thus, the map \(\psi:F\rightarrow \pi_F^{-1}(m)\) is a bijection.
It is more than a bijection.
More details about this we will see some other time.