Equivalence of Definitions of Principal $G$-bundle

I've finally gotten around to learning about principal $G$-bundles.

In the literature, I've encountered (more than) four different definitions. Since I'm still a beginner, it's unclear to me whether these definitions are equivalent or not. I would appreciate any clarification.

All maps and group actions are assumed continuous.

Definition 1: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:

(1) $G$ acts freely and transitively on fibers.

(2A) $G$ preserves fibers.

Definition 2: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a left action of $G$ on $F$ (note $F$ here) such that:

(1) $G$ acts freely and transitively on $F$.

(2B) There exists a trivializing cover with $G$-valued transition maps.

Definition 3: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:

(1') $G$ acts freely on $P$ and $X = P/G$ and $\pi\colon P \to X$ is $p \mapsto [p]$.

(2C) There exists a trivializing cover that is $G$-equivariant.

Definition 4: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:

(2A) $G$ preserves fibers.

(2C) There exists a trivializing cover that is $G$-equivariant.

Thoughts: It seems to me that Definition 4 is not equivalent to the other three. More than anything else, I am unclear as to why the existence of a trivializing cover that is $G$-equivariant is equivalent (is it?) to the existence of one that has $G$-valued transition functions.

I've also seen a fifth definition which assumes only condition (1).

Thanks in advance.

For the equivalence of these definitions, I would look here: Local triviality of principal bundles.

The existence of a $G$-equivariant cover is equivalent to the existence of $G$-valued transition functions:

Suppose $(U_\alpha,\Phi_\alpha)$, $\Phi_\alpha : P\vert_{U_\alpha} \to U_\alpha\times F$, is a trivializing cover. This defines a collection of maps $\phi_\alpha : P\to F$ by $$ \Phi_\alpha(p) = (\pi(p), \phi_\alpha(p)). $$ For a right principal $G$-bundle, this covering is $G$-equivariant if $\phi_\alpha(pg) = \phi_\alpha(p)g$. Now we have $$ \Phi_\alpha \circ \Phi_\beta^{-1} : U_\alpha \cap U_\beta \times F \to U_\alpha \cap U_\beta \times F $$ is an isomorphism of trivial $G$-bundles and so takes the form $$ (x, f) \mapsto (x, h_{\alpha\beta}(x,f)). $$ If the covering is $G$-equivariant then so is this map, which means that $h_{\alpha\beta}(x,fg) = h_{\alpha\beta}(x,f)g$. Since $G$ is acting freely and transitively, fixing a point of $F$ identities $F$ with $G$ and $h_{\alpha\beta}$ is entirely determined by the function $g_{\alpha\beta}: U_\alpha\cap U_\beta \to G, x \mapsto h_{\alpha\beta}(x,e)$. Thus the transition functions are given by left-multiplication by $g_{\alpha\beta}$. This is what is meant by the transition functions being $G$-valued.

Conversely, if the transition functions are $G$-valued then the trivializations will be $G$-equivariant. This is because $$ P = \sqcup_\alpha U_\alpha \times F/\sim, ~~ (x, f) \sim (x, g_{\alpha\beta}(x)f) \text{ for } x \in U_\alpha\cap U_\beta. $$ The equivariance then comes from the fact that the transition functions are operating by left-multiplication, while the $G$-action is right multiplication.

In fact, these definitions are not equivalent and are not equivalent to the usual notion of a principal $G$-bundle, see e.g. Kobayashi-Nomizu "Foundations of differential geometry", Vol. I, p. 50:

First of all, you have to assume, say, properness of the $G$-action and local compactness of $F$ in all the definitions. Otherwise, the following will be a counter-example to all four: Start with your favorite connected Lie group $G$ of dimension $>0$ (say, $U(1)$) and your favorite topological space $X$ (say, a point). Then $P=G\times X$ is a principal $G$-bundle. Now, consider the same group $G$ but equipped with discrete topology $G^\delta$, but keep the original topology on $P$. Take the obvious action $G^\delta\times P\to P$. This action satisfies (1)---(4) but does not define a $G^\delta$-principal bundle.

This can be (partly) remedied by assuming that $G$ is (2nd countable!) Lie group and $F$ is a manifold. Then (2) and (3) become equivalent to the standard definition.

Here is the situation assuming the extra assumption of properness.

(1) is not equivalent to (2) even if $G$ is a compact metrizable group, see here. Nevertheless, (1) $\iff$ (2) if (in (1)) $G$ is assumed to be a Lie group ($F$ need not be a manifold; this theorem is due to R.Palais).

(2) is equivalent to (3).

(3) is equivalent to (4) provided that in (4) the $G$-action on each fiber is transitive.