[proofplan] We compare both objects in local frames. A principal connection on $\operatorname{Fr}(E)$ has local connection matrices obtained by pulling back its connection form along a local frame section, and these matrices define a covariant derivative by the formula $df+A f$ on coordinate columns. Conversely, a covariant derivative determines exactly such matrices by differentiating the local frame fields, and the Leibniz rule forces the same gauge transformation law as a principal connection form. Since both constructions are characterized by the same local matrices in every frame, they are inverse to each other. [/proofplan] [step:Pass from a principal connection to local connection matrices] Let $G:=GL(r,\mathbb{R})$, let $\mathfrak{g}:=\mathfrak{gl}(r,\mathbb{R})$, and let $\operatorname{Ad}:G\to GL(\mathfrak{g})$ denote the adjoint representation, so $\operatorname{Ad}_g(X)=gXg^{-1}$ for $g\in G$ and $X\in\mathfrak{g}$. Let $\omega\in \Omega^1(\operatorname{Fr}(E);\mathfrak{g})$ be a principal connection form. Thus $\omega$ reproduces fundamental vertical vector fields and satisfies $R_g^*\omega=\operatorname{Ad}_{g^{-1}}\omega$ for every $g\in G$, where $R_g:\operatorname{Fr}(E)\to\operatorname{Fr}(E)$ is the right action. Let $U\subset M$ be an [open set](/page/Open%20Set) and let $e=(e_1,\dots,e_r)$ be a smooth local frame of $E$ over $U$. Define the associated frame section \begin{align*} \sigma_e:U\to \operatorname{Fr}(E) \end{align*} denote the smooth map whose value at $x\in U$ is the linear isomorphism $\sigma_e(x):\mathbb{R}^r\to E_x$ given by \begin{align*} \sigma_e(x)(a)=\sum_{j=1}^r a_j e_j(x) \end{align*} for $a=(a_1,\dots,a_r)\in\mathbb{R}^r$. Define the local connection matrix of $\omega$ in the frame $e$ by \begin{align*} A_e:=\sigma_e^*\omega\in \Omega^1(U;\mathfrak{g}). \end{align*} If $e'=(e'_1,\dots,e'_r)$ is another local frame over $U$ and $g:U\to G$ is the unique smooth map such that $e'=eg$, meaning \begin{align*} e'_b=\sum_{a=1}^r e_a g_{ab} \end{align*} for $1\leq b\leq r$, then $\sigma_{e'}=\sigma_e g$. The principal equivariance identity for $\omega$ gives the gauge transformation law \begin{align*} A_{e'}=g^{-1}A_e g+g^{-1}dg. \end{align*} Here $dg\in \Omega^1(U;\mathfrak{g})$ is the differential of the smooth map $g:U\to G\subset \mathbb{R}^{r\times r}$. [/step] [step:Use the local matrices to define a covariant derivative] For a section $s\in \Gamma(E)$ and a local frame $e$ over $U$, let \begin{align*} f_e:U&\to \mathbb{R}^r \end{align*} be the unique smooth coordinate column defined by \begin{align*} s(x)=\sum_{a=1}^r (f_e(x))_a e_a(x). \end{align*} Define locally \begin{align*} (\nabla^\omega s)|_U:=e\bigl(df_e+A_e f_e\bigr), \end{align*} where $e:\Omega^1(U;\mathbb{R}^r)\to \Omega^1(U;E)$ denotes the map sending a column of one-forms $\alpha=(\alpha_1,\dots,\alpha_r)$ to $\sum_{a=1}^r \alpha_a\otimes e_a$. We verify that this definition is independent of the local frame. Let $e'=eg$ and write $f_{e'}:U\to\mathbb{R}^r$ for the coordinate column of $s$ in the frame $e'$. Since $s=ef_e=e'f_{e'}=egf_{e'}$, we have $f_e=gf_{e'}$. Using the product rule for the differential of the matrix-vector product, \begin{align*} df_e+A_e f_e=d(gf_{e'})+A_e g f_{e'}. \end{align*} Expanding the differential gives \begin{align*} df_e+A_e f_e=g\,df_{e'}+(dg)f_{e'}+A_e g f_{e'}. \end{align*} The gauge law $A_{e'}=g^{-1}A_e g+g^{-1}dg$ is equivalent to \begin{align*} gA_{e'}=A_e g+dg. \end{align*} Substitution yields \begin{align*} df_e+A_e f_e=g\bigl(df_{e'}+A_{e'}f_{e'}\bigr). \end{align*} Applying the frame $e$ to the left side equals applying the frame $e'=eg$ to the right side, so the local definitions agree on overlaps. Therefore they glue to a global map \begin{align*} \nabla^\omega:\Gamma(E)\to \Omega^1(M;E). \end{align*} [guided] The construction is local because both vector bundle sections and principal connection forms are easiest to compare after choosing a frame. Fix a local frame $e=(e_1,\dots,e_r)$ over $U$. Every section $s\in\Gamma(E)$ has a unique coordinate column \begin{align*} f_e:U&\to \mathbb{R}^r \end{align*} defined by \begin{align*} s(x)=\sum_{a=1}^r (f_e(x))_a e_a(x). \end{align*} The connection form gives a matrix-valued one-form $A_e=\sigma_e^*\omega$ on $U$. The natural candidate for the covariant derivative is therefore \begin{align*} (\nabla^\omega s)|_U:=e\bigl(df_e+A_e f_e\bigr), \end{align*} where a column $\alpha=(\alpha_1,\dots,\alpha_r)$ of one-forms is converted into an $E$-valued one-form by $e(\alpha)=\sum_{a=1}^r \alpha_a\otimes e_a$. The essential point is that this formula must not depend on the chosen frame. Suppose $e'=eg$ for a smooth map $g:U\to GL(r,\mathbb{R})$. If $f_{e'}$ is the coordinate column of $s$ in the frame $e'$, then \begin{align*} ef_e=s=e'f_{e'}=egf_{e'}. \end{align*} Since $e$ is a frame, the coordinate columns satisfy $f_e=gf_{e'}$. Differentiating the matrix-vector product gives \begin{align*} df_e=d(gf_{e'})=g\,df_{e'}+(dg)f_{e'}. \end{align*} Thus \begin{align*} df_e+A_e f_e=g\,df_{e'}+(dg)f_{e'}+A_e g f_{e'}. \end{align*} The local connection matrices of a principal connection satisfy \begin{align*} A_{e'}=g^{-1}A_e g+g^{-1}dg. \end{align*} Multiplying this identity by $g$ on the left gives \begin{align*} gA_{e'}=A_e g+dg. \end{align*} Therefore \begin{align*} df_e+A_e f_e=g\bigl(df_{e'}+A_{e'}f_{e'}\bigr). \end{align*} Applying $e$ to the left column is the same as applying $e'=eg$ to the right column. Hence the expression $e(df_e+A_e f_e)$ is frame-independent and defines a global $E$-valued one-form $\nabla^\omega s$ on $M$. [/guided] The map $\nabla^\omega$ is $\mathbb{R}$-linear because $d$, multiplication by $A_e$, and the frame identification $e$ are $\mathbb{R}$-linear. For $h\in C^\infty(M)$, the coordinate column of $hs$ in the frame $e$ is $hf_e$, so \begin{align*} (\nabla^\omega(hs))|_U=e\bigl(d(hf_e)+A_e(hf_e)\bigr). \end{align*} Using the ordinary product rule, \begin{align*} d(hf_e)+A_e(hf_e)=dh\otimes f_e+h(df_e+A_e f_e). \end{align*} Applying $e$ gives \begin{align*} \nabla^\omega(hs)=dh\otimes s+h\nabla^\omega s. \end{align*} Thus $\nabla^\omega$ is a covariant derivative on $E$. [/step] [step:Extract local connection matrices from a covariant derivative] Conversely, let \begin{align*} \nabla:\Gamma(E)\to \Omega^1(M;E) \end{align*} be a covariant derivative. We first record how $\nabla$ acts on local sections. If $U\subset M$ is open and $\tau\in\Gamma(E|_U)$ is a local section, define $(\nabla_U\tau)_x\in T_x^*M\otimes E_x$ as follows. Choose an open neighbourhood $V\subset U$ of $x$, a smooth function $\rho:M\to\mathbb{R}$ with support contained in $U$ and $\rho=1$ on $V$, and any smooth global section $\widetilde{\tau}\in\Gamma(E)$ whose restriction to $V$ equals $\tau|_V$ after multiplication by $\rho$. Set \begin{align*} (\nabla_U\tau)|_V:=(\nabla\widetilde{\tau})|_V. \end{align*} This definition is independent of the choices: if two global extensions agree on a neighbourhood of $x$, their difference is zero there, hence equals $0\cdot \eta$ locally for a section $\eta$, and the Leibniz rule gives $\nabla(0\cdot\eta)=d0\otimes\eta+0\nabla\eta=0$ on that neighbourhood. Therefore $\nabla_U:\Gamma(E|_U)\to\Omega^1(U;E|_U)$ is well-defined and satisfies the same Leibniz rule on $U$. For a local frame $e=(e_1,\dots,e_r)$ over $U$, define the matrix-valued one-form $A_e\in\Omega^1(U;\mathfrak{gl}(r,\mathbb{R}))$ by the equations \begin{align*} \nabla e_b=\sum_{a=1}^r (A_e)_{ab}\otimes e_a \end{align*} for $1\leq b\leq r$. This uniquely defines the entries $(A_e)_{ab}\in\Omega^1(U)$ because $e_1,\dots,e_r$ form a frame. If $s|_U=\sum_{b=1}^r f_b e_b$ and $f_e:U\to\mathbb{R}^r$ is the coordinate column with entries $f_b$, then $\mathbb{R}$-linearity and the Leibniz rule give \begin{align*} (\nabla s)|_U=\sum_{b=1}^r df_b\otimes e_b+\sum_{b=1}^r f_b\nabla e_b. \end{align*} Using the definition of $A_e$, this becomes \begin{align*} (\nabla s)|_U=e\bigl(df_e+A_e f_e\bigr). \end{align*} Now let $e'=eg$ be another local frame over $U$. Since \begin{align*} e'_b=\sum_{c=1}^r e_c g_{cb}, \end{align*} the Leibniz rule gives \begin{align*} \nabla e'_b=\sum_{c=1}^r dg_{cb}\otimes e_c+\sum_{c=1}^r g_{cb}\nabla e_c. \end{align*} Substituting $\nabla e_c=\sum_{a=1}^r (A_e)_{ac}\otimes e_a$ and collecting coefficients in the frame $e$ gives \begin{align*} \nabla e'_b=\sum_{a=1}^r (dg+A_e g)_{ab}\otimes e_a. \end{align*} Since $e'=eg$, rewriting the same $E$-valued one-form in the frame $e'$ gives \begin{align*} A_{e'}=g^{-1}A_e g+g^{-1}dg. \end{align*} Thus the matrices obtained from $\nabla$ satisfy exactly the principal connection gauge law. [/step] [step:Glue the covariant derivative matrices to a principal connection form] Let $\pi_{\operatorname{Fr}}:\operatorname{Fr}(E)\to M$ denote the bundle projection. For each local frame $e$ over $U$, define a one-form on $\pi_{\operatorname{Fr}}^{-1}(U)\subset\operatorname{Fr}(E)$ as follows. Every frame $u\in\pi_{\operatorname{Fr}}^{-1}(U)$ can be written uniquely as $u=\sigma_e(x)g$ with $x=\pi_{\operatorname{Fr}}(u)$ and $g\in G$. Define \begin{align*} \omega_e:=\operatorname{Ad}_{g^{-1}}\bigl(\pi_{\operatorname{Fr}}^*A_e\bigr)+g^{-1}dg \end{align*} on the local trivialization $U\times G\to \pi_{\operatorname{Fr}}^{-1}(U)$, where $g^{-1}dg$ is the left Maurer-Cartan form on $G$ pulled back along the second projection. We check the overlap compatibility. Let $e'=eg_0$ on $U\cap U'$, and write the same frame $u\in\pi_{\operatorname{Fr}}^{-1}(U\cap U')$ as $u=\sigma_e(x)g=\sigma_{e'}(x)g'$. Since $\sigma_{e'}(x)=\sigma_e(x)g_0(x)$, we have $g=g_0g'$. The transformation law \begin{align*} A_{e'}=g_0^{-1}A_e g_0+g_0^{-1}dg_0 \end{align*} and the product rule for the left Maurer-Cartan form, \begin{align*} (g_0g')^{-1}d(g_0g')=(g')^{-1}g_0^{-1}(dg_0)g'+(g')^{-1}dg', \end{align*} give \begin{align*} \operatorname{Ad}_{(g')^{-1}}A_{e'}+(g')^{-1}dg'=\operatorname{Ad}_{(g_0g')^{-1}}A_e+(g_0g')^{-1}d(g_0g'). \end{align*} Thus the forms $\omega_e$ and $\omega_{e'}$ agree on overlaps. Hence they glue to a global one-form \begin{align*} \omega^\nabla\in\Omega^1(\operatorname{Fr}(E);\mathfrak{g}). \end{align*} By its local expression, $\omega^\nabla$ restricts on each fibre to the left Maurer-Cartan form. Explicitly, for $X\in\mathfrak{g}$ the fundamental vertical vector field $X^\#\in\mathfrak{X}(\operatorname{Fr}(E))$ for the right action is represented at $u=\sigma_e(x)g$ by the curve $t\mapsto u\exp(tX)=\sigma_e(x)g\exp(tX)$. Evaluating the left Maurer-Cartan term on this curve gives \begin{align*} (g\exp(tX))^{-1}\frac{d}{dt}\bigg|_{t=0}g\exp(tX)=X. \end{align*} The base point $x$ is fixed along the curve, so the pulled-back base term $\operatorname{Ad}_{g^{-1}}(\pi_{\operatorname{Fr}}^*A_e)$ vanishes on $X^\#$. Hence $\omega^\nabla(X^\#)=X$. The same local expression gives \begin{align*} R_h^*\omega^\nabla=\operatorname{Ad}_{h^{-1}}\omega^\nabla \end{align*} for every $h\in G$. Therefore $\omega^\nabla$ is a principal connection form on $\operatorname{Fr}(E)$. [/step] [step:Check that the two constructions are inverse] Starting with a principal connection form $\omega$, the construction of $\nabla^\omega$ uses the local matrices $A_e=\sigma_e^*\omega$. Extracting matrices from $\nabla^\omega$ in the same frame gives the same $A_e$, because \begin{align*} \nabla^\omega e_b=e(A_e e_b^{\mathrm{std}}) \end{align*} where $e_b^{\mathrm{std}}\in\mathbb{R}^r$ is the $b$-th standard basis vector. Thus the reconstructed principal connection form has the same local expression as $\omega$ in every local trivialization, and hence equals $\omega$. Conversely, starting with a covariant derivative $\nabla$, the construction of $\omega^\nabla$ uses the local matrices $A_e$ determined by \begin{align*} \nabla e_b=\sum_{a=1}^r (A_e)_{ab}\otimes e_a. \end{align*} The covariant derivative induced back from $\omega^\nabla$ is locally given by \begin{align*} s\mapsto e(df_e+A_e f_e). \end{align*} This is exactly the local formula already obtained from $\nabla$ by the Leibniz rule. Hence the induced covariant derivative equals $\nabla$ on every local frame domain, and therefore globally on $M$. The assignments $\omega\mapsto\nabla^\omega$ and $\nabla\mapsto\omega^\nabla$ are inverse to each other, giving the claimed natural bijection. [/step]