[proofplan]
We prove the correspondence in both directions. Starting from a connection form, its kernel gives the horizontal subspace; the reproduction identity identifies the vertical tangent space with $\mathfrak{g}$, and the equivariance identity transports kernels correctly under the right action. Conversely, a horizontal distribution gives a smooth projection of $TP$ onto $VP$, and each vertical vector is uniquely a fundamental vector; this defines the connection form. Finally, the two constructions are inverse because both recover exactly the same horizontal kernel and the same vertical component.
[/proofplan]
[step:Identify vertical tangent vectors with elements of the Lie algebra]
For each $u \in P$, define the orbit map
\begin{align*}
\theta_u: G \to P,\qquad \theta_u(g) = ug.
\end{align*}
Since $P$ is a principal right $G$-bundle, $\theta_u$ maps $G$ diffeomorphically onto the fibre $\pi^{-1}(\pi(u))$. Therefore
\begin{align*}
d(\theta_u)_e: \mathfrak{g} \to V_uP
\end{align*}
is a linear isomorphism. By definition of the fundamental vector field,
\begin{align*}
d(\theta_u)_e(A) = A_P(u)
\end{align*}
for every $A \in \mathfrak{g}$. Thus the map
\begin{align*}
\iota_u: \mathfrak{g} \to V_uP,\qquad \iota_u(A) = A_P(u)
\end{align*}
is a linear isomorphism for every $u \in P$.
[guided]
Fix $u \in P$. The vertical tangent space $V_uP$ consists of tangent vectors to the fibre through $u$:
\begin{align*}
V_uP = \ker d\pi_u = T_u(\pi^{-1}(\pi(u))).
\end{align*}
The principal bundle action identifies this fibre with the group itself. More precisely, define
\begin{align*}
\theta_u: G \to P,\qquad \theta_u(g) = ug.
\end{align*}
Because the right action is free and transitive on each fibre, $\theta_u$ is a diffeomorphism from $G$ onto $\pi^{-1}(\pi(u))$. Taking the differential at the identity element $e \in G$ gives a linear isomorphism
\begin{align*}
d(\theta_u)_e: T_eG \to T_u(\pi^{-1}(\pi(u))).
\end{align*}
Since $\mathfrak{g} = T_eG$ and $T_u(\pi^{-1}(\pi(u))) = V_uP$, this is a linear isomorphism
\begin{align*}
d(\theta_u)_e: \mathfrak{g} \to V_uP.
\end{align*}
For $A \in \mathfrak{g}$, the curve $t \mapsto u\exp(tA)$ has derivative at $t = 0$ equal to the fundamental vector $A_P(u)$. Hence
\begin{align*}
d(\theta_u)_e(A) = A_P(u).
\end{align*}
Thus every vertical tangent vector at $u$ is represented uniquely as $A_P(u)$ for one element $A \in \mathfrak{g}$. This uniqueness is the mechanism that will let us turn vertical projections into $\mathfrak{g}$-valued $1$-forms.
[/guided]
[/step]
[step:Take the kernel of a connection form to obtain an equivariant horizontal distribution]
Let $\omega \in \Omega^1(P;\mathfrak{g})$ be a connection form. For each $u \in P$, define
\begin{align*}
H^\omega_u = \ker \omega_u \subset T_uP.
\end{align*}
Since $\omega$ is a smooth vector-valued $1$-form, the assignment $u \mapsto H^\omega_u$ is a smooth distribution once its rank is constant.
We prove the direct sum decomposition. Let $X \in H^\omega_u \cap V_uP$. Since $X \in V_uP$, the previous step gives a unique $A \in \mathfrak{g}$ with $X = A_P(u)$. Since $X \in H^\omega_u$ and $\omega$ reproduces fundamental vector fields,
\begin{align*}
0 = \omega_u(X) = \omega_u(A_P(u)) = A.
\end{align*}
Hence $X = 0$, so $H^\omega_u \cap V_uP = \{0\}$.
For an arbitrary $X \in T_uP$, define
\begin{align*}
A = \omega_u(X) \in \mathfrak{g}.
\end{align*}
Then $A_P(u) \in V_uP$, and
\begin{align*}
\omega_u(X - A_P(u)) = \omega_u(X) - \omega_u(A_P(u)) = A - A = 0.
\end{align*}
Thus $X - A_P(u) \in H^\omega_u$, and
\begin{align*}
X = (X - A_P(u)) + A_P(u)
\end{align*}
is a decomposition with horizontal part in $H^\omega_u$ and vertical part in $V_uP$. Therefore
\begin{align*}
T_uP = H^\omega_u \oplus V_uP.
\end{align*}
Since $\dim V_uP = \dim G = \dim \mathfrak{g}$ and $\omega_u$ is surjective by the reproduction identity, $\dim H^\omega_u = \dim P - \dim G = \dim M$, so the rank is constant.
Now let $g \in G$. For $X \in H^\omega_u$, the equivariance of $\omega$ gives
\begin{align*}
\omega_{ug}(d(R_g)_uX) = \operatorname{Ad}_{g^{-1}}(\omega_u(X)) = 0.
\end{align*}
Hence $d(R_g)_u(H^\omega_u) \subset H^\omega_{ug}$. Applying the same argument with $g^{-1}$ gives the reverse inclusion, so
\begin{align*}
d(R_g)_u(H^\omega_u) = H^\omega_{ug}.
\end{align*}
Thus $H^\omega$ is a smooth $G$-equivariant horizontal distribution.
[/step]
[step:Project onto the vertical bundle along a horizontal distribution]
Let $H \subset TP$ be a smooth $G$-equivariant horizontal distribution. For each $u \in P$, the direct sum decomposition
\begin{align*}
T_uP = H_u \oplus V_uP
\end{align*}
defines a linear projection
\begin{align*}
\operatorname{ver}^H_u: T_uP \to V_uP
\end{align*}
by requiring $X - \operatorname{ver}^H_u(X) \in H_u$ for $X \in T_uP$.
Because $H$ and $VP = \ker d\pi$ are smooth subbundles of $TP$ and $TP = H \oplus VP$, the fibrewise projection
\begin{align*}
\operatorname{ver}^H: TP \to VP
\end{align*}
is a smooth vector bundle map. Locally this follows by choosing a smooth frame for $H$ and a smooth frame for $VP$; in the combined frame, $\operatorname{ver}^H$ is represented by the constant block projection onto the vertical coordinates.
[/step]
[step:Define the connection form from the vertical projection]
For $u \in P$ and $X \in T_uP$, define $\omega^H_u(X) \in \mathfrak{g}$ to be the unique element satisfying
\begin{align*}
(\omega^H_u(X))_P(u) = \operatorname{ver}^H_u(X).
\end{align*}
Equivalently,
\begin{align*}
\omega^H_u = \iota_u^{-1} \circ \operatorname{ver}^H_u,
\end{align*}
where $\iota_u: \mathfrak{g} \to V_uP$ is the linear isomorphism $\iota_u(A) = A_P(u)$ from the first step. Define the bundle map
\begin{align*}
\iota: P \times \mathfrak{g} \to VP
\end{align*}
by $\iota(u,A) = A_P(u)$. This map is smooth because it is obtained by differentiating the smooth action map $P \times G \to P$ along the identity direction in $G$. Its fibre map $\iota_u: \mathfrak{g} \to V_uP$ is a linear isomorphism for every $u \in P$, and the inverse bundle map $\iota^{-1}: VP \to P \times \mathfrak{g}$ is smooth because a fibrewise invertible smooth vector bundle map has smooth inverse in local frames. Since $\operatorname{ver}^H$ is smooth, $\omega^H = \operatorname{pr}_{\mathfrak{g}} \circ \iota^{-1} \circ \operatorname{ver}^H$ is a smooth $\mathfrak{g}$-valued $1$-form on $P$, where $\operatorname{pr}_{\mathfrak{g}}: P \times \mathfrak{g} \to \mathfrak{g}$ is the projection.
For $A \in \mathfrak{g}$, the vector $A_P(u)$ is vertical, so
\begin{align*}
\operatorname{ver}^H_u(A_P(u)) = A_P(u).
\end{align*}
Therefore
\begin{align*}
\omega^H_u(A_P(u)) = A.
\end{align*}
Thus $\omega^H$ satisfies the reproduction identity.
[guided]
The definition of $\omega^H$ uses the idea that a connection form should measure the vertical part of a tangent vector. Fix $u \in P$ and $X \in T_uP$. Since $H$ is horizontal, we have a unique decomposition
\begin{align*}
X = X_H + X_V
\end{align*}
with $X_H \in H_u$ and $X_V \in V_uP$. Define
\begin{align*}
\operatorname{ver}^H_u(X) = X_V.
\end{align*}
The first step gives a linear isomorphism
\begin{align*}
\iota_u: \mathfrak{g} \to V_uP,\qquad \iota_u(A) = A_P(u).
\end{align*}
So there is a unique element of the Lie algebra whose fundamental vector at $u$ equals the vertical component of $X$. We define that element to be $\omega^H_u(X)$:
\begin{align*}
\omega^H_u = \iota_u^{-1} \circ \operatorname{ver}^H_u.
\end{align*}
This defines a [linear map](/page/Linear%20Map) $\omega^H_u: T_uP \to \mathfrak{g}$ at every point $u$.
The form is smooth because both ingredients vary smoothly with $u$. The projection $\operatorname{ver}^H: TP \to VP$ is smooth since $H$ and $VP$ are smooth complementary subbundles. Define
\begin{align*}
\iota: P \times \mathfrak{g} \to VP
\end{align*}
by $\iota(u,A) = A_P(u)$. This is a smooth vector bundle map because it is obtained by differentiating the smooth right action of $G$ on $P$ in the identity direction of $G$. Each fibre map $\iota_u: \mathfrak{g} \to V_uP$ is an isomorphism by the first step, so $\iota$ is a smooth vector bundle isomorphism; in local frames its inverse is represented by the inverse of a smooth matrix-valued map with nonzero determinant, hence $\iota^{-1}: VP \to P \times \mathfrak{g}$ is smooth. Therefore $\omega^H = \operatorname{pr}_{\mathfrak{g}} \circ \iota^{-1} \circ \operatorname{ver}^H$ is a smooth section of $T^*P \otimes \mathfrak{g}$, that is, a smooth $\mathfrak{g}$-valued $1$-form, where $\operatorname{pr}_{\mathfrak{g}}: P \times \mathfrak{g} \to \mathfrak{g}$ is the projection.
Now verify the reproduction identity. If $A \in \mathfrak{g}$, then $A_P(u)$ is vertical by construction, because the curve $t \mapsto u\exp(tA)$ stays inside the fibre $\pi^{-1}(\pi(u))$. Hence its vertical projection is itself:
\begin{align*}
\operatorname{ver}^H_u(A_P(u)) = A_P(u).
\end{align*}
Applying $\iota_u^{-1}$ gives
\begin{align*}
\omega^H_u(A_P(u)) = A.
\end{align*}
Thus $\omega^H$ reproduces every fundamental vector field.
[/guided]
[/step]
[step:Use equivariance of the distribution to prove equivariance of the form]
Fix $g \in G$, $u \in P$, and $X \in T_uP$. Define
\begin{align*}
A = \omega^H_u(X) \in \mathfrak{g}.
\end{align*}
Then $\operatorname{ver}^H_u(X) = A_P(u)$.
Since $H$ is $G$-equivariant and $R_g$ maps fibres to fibres, the differential $d(R_g)_u$ carries the horizontal component of $X$ into $H_{ug}$ and the vertical component of $X$ into $V_{ug}P$. Hence
\begin{align*}
\operatorname{ver}^H_{ug}(d(R_g)_uX) = d(R_g)_u(A_P(u)).
\end{align*}
The right action transforms fundamental vector fields by the adjoint action:
\begin{align*}
d(R_g)_u(A_P(u)) = (\operatorname{Ad}_{g^{-1}}A)_P(ug).
\end{align*}
Therefore, by the definition of $\omega^H_{ug}$,
\begin{align*}
\omega^H_{ug}(d(R_g)_uX) = \operatorname{Ad}_{g^{-1}}A = \operatorname{Ad}_{g^{-1}}(\omega^H_u(X)).
\end{align*}
This is exactly
\begin{align*}
(R_g)^*\omega^H = \operatorname{Ad}_{g^{-1}}\omega^H.
\end{align*}
Thus $\omega^H$ is a connection form.
[/step]
[step:Check that the two constructions are inverse]
Start with a connection form $\omega$ and form $H^\omega_u = \ker \omega_u$. Then construct $\omega^{H^\omega}$ from the horizontal distribution $H^\omega$. For $X \in T_uP$, define
\begin{align*}
A = \omega_u(X) \in \mathfrak{g}.
\end{align*}
The decomposition used in the construction of $\omega^{H^\omega}$ is
\begin{align*}
X = (X - A_P(u)) + A_P(u),
\end{align*}
where $X - A_P(u) \in \ker \omega_u$ and $A_P(u) \in V_uP$. Hence the vertical component is $A_P(u)$, and the resulting form satisfies
\begin{align*}
\omega^{H^\omega}_u(X) = A = \omega_u(X).
\end{align*}
Thus $\omega^{H^\omega} = \omega$.
Conversely, start with a horizontal distribution $H$ and construct $\omega^H$. For $X \in T_uP$,
\begin{align*}
\omega^H_u(X) = 0
\end{align*}
if and only if
\begin{align*}
\operatorname{ver}^H_u(X) = 0.
\end{align*}
By definition of the projection along $H_u$, this holds if and only if $X \in H_u$. Therefore
\begin{align*}
\ker \omega^H_u = H_u
\end{align*}
for every $u \in P$, so $H^{\omega^H} = H$.
The assignments $\omega \mapsto H^\omega$ and $H \mapsto \omega^H$ are therefore mutually inverse, giving the claimed natural bijection.
[/step]
