Different definitions of a structure on principal bundles

Let $$P\to B$$ be a principal $$G$$-bundle and $$\psi:H\to G$$ a homomorphism of topological groups. A $$\psi$$-structure for $$P$$ can be defined in two different ways. I am trying to prove their equivalence.

I will give the definitions below. To do so, let us fix models $$EH\to BH$$ and $$EG\to BG$$ for the classifying spaces such that $$B\psi :BH\to BG$$ can be represented by a fibration (where $$B\psi$$ is the classifying map for the balanced product $$EH\times_\psi G$$).

First definition: A $$\psi$$-structure for $$P$$ is an equivalence class of pairs $$(P',\phi')$$ consisting of a principal $$H$$-bundle $$P'\to B$$ together with a $$\psi$$-equivariant bundle map $$\phi':P'\to P$$ where two pairs $$(P',\phi')$$ and $$(P'',\phi'')$$ are equivalent if there exists an isomorphism of principal $$H$$-bundles $$f:P'\to P''$$ such that $$\phi''\circ f=\phi'$$

Second definition: A $$\psi$$-structure for $$P$$ is for a choice of a classifying map for $$P$$, $$g:B\to BG$$, an equivalence class of lifts $$h:B\to BH$$ of $$g$$ in terms of $$B\psi$$, i.e. a map $$h:B\to BH$$ satisfying $$B\psi \circ h=g$$. Two lifts being equivalent if they are homotopic by a homotopy $$H:B\times I \to BH$$ which is a lift of the constant homotopy, i.e. which satisfies $$B\psi \circ H=g\circ proj_1$$.

It is easy to get for a representative $$(P',\phi')$$ a lift as in the second definition and vice versa. Namely, pick a classifying map $$h'$$ for $$P'$$, homotop $$B\psi \circ h'$$ into $$g$$ and lift the homotopy to $$BH$$. For the other direction, we can take the pullback bundles.

I wasn't able to show that this construction gives a well defined 1-1 correspondence between these definitions, i.e. that it respects the equivalence relations. Can anyone help? Is there a literature reference?

• Where do you come across this set up? Never seen this before.. – Praphulla Koushik Jan 7 at 17:54
• For example in the scope of $spin$/$spin^c$-manifolds. $Spin$-structures on manifolds can be definded geometrically by the first definition or topologically by the second. – floating Jan 7 at 19:25
• I would call your first definition topological, the second definition homotopical. – David Roberts Jan 9 at 7:47
• math.stackexchange.com/questions/3070080/… – wonderich Jan 16 at 20:46