[proofplan]
We prove the two principal-bundle properties of $T=d\theta+\omega\wedge\theta$ directly from the defining properties of the solder form and the connection form. Horizontality follows because the infinitesimal change of $\theta$ in a vertical fundamental direction is exactly cancelled by the term $\omega\wedge\theta$. Equivariance follows by pulling back both terms under the right action and using the standard transformation laws for $\theta$ and $\omega$. Finally, a local frame converts the descended $\mathbb R^n$-valued form into a tangent-valued two-form on $M$, and the pulled-back formula is compared with the local expression for the covariant derivative induced by $\omega$.
[/proofplan]
[step:Record the transformation laws for the solder form and the connection form]
For $g\in GL(n,\mathbb R)$, let $R_g:F(M)\to F(M)$ denote the right action defined by $R_g(u)=u\circ g$ for $u\in F(M)$. Since $\pi\circ R_g=\pi$, for every $u\in F(M)$ and $A\in T_uF(M)$ we have
\begin{align*}
((R_g)^*\theta)_u(A)=\theta_{u\circ g}(dR_g(A))=(u\circ g)^{-1}(d\pi_u(A))=g^{-1}\theta_u(A).
\end{align*}
Thus
\begin{align*}
(R_g)^*\theta=g^{-1}\theta.
\end{align*}
The defining equivariance property of the connection form is
\begin{align*}
(R_g)^*\omega=\operatorname{Ad}(g^{-1})\omega,
\end{align*}
where $\operatorname{Ad}(g^{-1}):\mathfrak{gl}(n,\mathbb R)\to\mathfrak{gl}(n,\mathbb R)$ is the [linear map](/page/Linear%20Map) $A\mapsto g^{-1}Ag$.
[guided]
The first point is to fix the convention for the right action, because it determines whether $g$ or $g^{-1}$ appears. The frame $u$ is an isomorphism $u:\mathbb R^n\to T_xM$, and the right action is
\begin{align*}
R_g(u)=u\circ g.
\end{align*}
The projection $\pi:F(M)\to M$ sends a frame to its base point, so $\pi(R_g(u))=\pi(u)$. Hence $d\pi_{u\circ g}(dR_g(A))=d\pi_u(A)$ for every $A\in T_uF(M)$.
By definition, the solder form is
\begin{align*}
\theta_u(A)=u^{-1}(d\pi_u(A)).
\end{align*}
Therefore
\begin{align*}
((R_g)^*\theta)_u(A)=\theta_{u\circ g}(dR_g(A))=(u\circ g)^{-1}(d\pi_u(A)).
\end{align*}
Since $(u\circ g)^{-1}=g^{-1}\circ u^{-1}$, this becomes
\begin{align*}
((R_g)^*\theta)_u(A)=g^{-1}\theta_u(A).
\end{align*}
So the solder form has equivariance law $(R_g)^*\theta=g^{-1}\theta$.
For the connection form, the principal connection convention gives
\begin{align*}
(R_g)^*\omega=\operatorname{Ad}(g^{-1})\omega,
\end{align*}
where $\operatorname{Ad}(g^{-1})(A)=g^{-1}Ag$ for $A\in\mathfrak{gl}(n,\mathbb R)$. This is the second structural input used below.
[/guided]
[/step]
[step:Show that vertical components cancel in $d\theta+\omega\wedge\theta$]
Let $a\in\mathfrak{gl}(n,\mathbb R)$, and let $a^*:F(M)\to TF(M)$ be the vertical fundamental vector field generated by $a$, defined by
\begin{align*}
a^*(u)=\frac{d}{dt}\Big|_{t=0}u\circ \exp(ta)
\end{align*}
for $u\in F(M)$. Since $\pi(u\circ\exp(ta))=\pi(u)$, we have $\theta(a^*)=0$. Also $\omega(a^*)=a$ by the defining vertical normalization of a connection form.
Let $\mathcal L_{a^*}\theta$ denote the Lie derivative of the $\mathbb R^n$-valued one-form $\theta$ along the vector field $a^*$. The equivariance law $(R_{\exp(ta)})^*\theta=\exp(-ta)\theta$ implies
\begin{align*}
\mathcal L_{a^*}\theta=-a\theta,
\end{align*}
where $a\theta$ denotes pointwise multiplication of the $\mathbb R^n$-valued form $\theta$ by the matrix $a$. Since $\theta(a^*)=0$, Cartan's formula for a one-form, applied componentwise to the $\mathbb R^n$-valued form $\theta$, gives
\begin{align*}
d\theta(a^*,B)=(\mathcal L_{a^*}\theta)(B)=-a\theta(B)
\end{align*}
for every vector field $B$ on $F(M)$. On the other hand,
\begin{align*}
(\omega\wedge\theta)(a^*,B)=\omega(a^*)\theta(B)-\omega(B)\theta(a^*)=a\theta(B).
\end{align*}
Adding the two identities gives
\begin{align*}
T(a^*,B)=d\theta(a^*,B)+(\omega\wedge\theta)(a^*,B)=0.
\end{align*}
By skew-symmetry of the two-form $T$, the same conclusion holds when the vertical vector is in the second argument. Since every vertical tangent vector is of the form $a^*_u$ for a unique $a\in\mathfrak{gl}(n,\mathbb R)$, $T$ is horizontal.
[/step]
[step:Verify the equivariance of the torsion form]
Fix $g\in GL(n,\mathbb R)$. Since exterior differentiation commutes with pullback and $g^{-1}:\mathbb R^n\to\mathbb R^n$ is constant,
\begin{align*}
(R_g)^*d\theta=d((R_g)^*\theta)=d(g^{-1}\theta)=g^{-1}d\theta.
\end{align*}
For $A,B\in T_uF(M)$, using $(R_g)^*\omega=\operatorname{Ad}(g^{-1})\omega$ and $(R_g)^*\theta=g^{-1}\theta$ gives
\begin{align*}
((R_g)^*(\omega\wedge\theta))_u(A,B)=g^{-1}\omega_u(A)\theta_u(B)-g^{-1}\omega_u(B)\theta_u(A).
\end{align*}
Hence
\begin{align*}
(R_g)^*(\omega\wedge\theta)=g^{-1}(\omega\wedge\theta).
\end{align*}
Combining the two transformed terms,
\begin{align*}
(R_g)^*T=(R_g)^*d\theta+(R_g)^*(\omega\wedge\theta)=g^{-1}d\theta+g^{-1}(\omega\wedge\theta)=g^{-1}T.
\end{align*}
[/step]
[step:Descend the horizontal equivariant form to a tangent-valued two-form on $M$]
We construct the descended form directly. In the present convention, define the map $\Phi:F(M)\times_{GL(n,\mathbb R)}\mathbb R^n \to TM$ by $\Phi([u,v])=u(v)$ for $[u,v]\in F(M)\times_{GL(n,\mathbb R)}\mathbb R^n$.
This map is well-defined because
\begin{align*}
\Phi([u\circ g,g^{-1}v])=(u\circ g)(g^{-1}v)=u(v)=\Phi([u,v]).
\end{align*}
It is a vector-bundle isomorphism over $M$.
Since $T$ is horizontal, $T_u(A,B)$ depends only on the projected tangent vectors $d\pi_u(A),d\pi_u(B)\in T_{\pi(u)}M$. Since $T$ satisfies $(R_g)^*T=g^{-1}T$, the associated class $[u,T_u(A,B)]$ is independent of the chosen frame $u$ over the same base point. Let $\Gamma(\Lambda^2T^*M\otimes TM)$ denote the space of smooth sections of the vector bundle $\Lambda^2T^*M\otimes TM\to M$. Therefore $T$ defines a smooth tangent-valued two-form
\begin{align*}
\tau\in\Gamma(\Lambda^2T^*M\otimes TM)
\end{align*}
by the rule
\begin{align*}
\tau_x(\xi,\eta)=u(T_u(A,B)),
\end{align*}
where $u\in F_x(M)$ and $A,B\in T_uF(M)$ satisfy $d\pi_u(A)=\xi$ and $d\pi_u(B)=\eta$.
[guided]
A horizontal equivariant form on a principal bundle is exactly the data needed to make a tensorial form on the base. Here is the construction explicitly.
Let $x\in M$, let $\xi,\eta\in T_xM$, choose a frame $u\in F_x(M)$, and choose tangent vectors $A,B\in T_uF(M)$ such that
\begin{align*}
d\pi_u(A)=\xi,\qquad d\pi_u(B)=\eta.
\end{align*}
Define
\begin{align*}
\tau_x(\xi,\eta)=u(T_u(A,B)).
\end{align*}
We must check that this does not depend on the auxiliary choices.
First, suppose $A$ is replaced by another vector $A'\in T_uF(M)$ with the same projection. Then $A-A'$ is vertical. Since $T$ is horizontal,
\begin{align*}
T_u(A-A',B)=0.
\end{align*}
By bilinearity,
\begin{align*}
T_u(A,B)=T_u(A',B).
\end{align*}
The same argument applies to the second argument. Thus the value depends only on $\xi$ and $\eta$, not on the chosen lifts.
Second, replace the frame $u$ by $u\circ g$ for some $g\in GL(n,\mathbb R)$. Use the lifted vectors $dR_g(A),dR_g(B)$ over $u\circ g$. Equivariance gives
\begin{align*}
T_{u\circ g}(dR_g(A),dR_g(B))=g^{-1}T_u(A,B).
\end{align*}
Applying the new frame $u\circ g$ gives
\begin{align*}
(u\circ g)(T_{u\circ g}(dR_g(A),dR_g(B)))=(u\circ g)(g^{-1}T_u(A,B))=u(T_u(A,B)).
\end{align*}
So the value is independent of the chosen frame. This proves that $T$ descends to a well-defined smooth section
\begin{align*}
\tau\in\Gamma(\Lambda^2T^*M\otimes TM).
\end{align*}
[/guided]
[/step]
[step:Compute the descended form in a local frame]
Let $U\subset M$ be open, and let $s:U\to F(M)$ be a smooth local frame. For $1\le i\le n$, define the smooth vector field $e_i:U\to TM$ by $e_i(x)=s(x)(e_{i,0})$ for $x\in U$, where $(e_{1,0},\dots,e_{n,0})$ is the standard basis of $\mathbb R^n$. Let
\begin{align*}
\vartheta:=s^*\theta\in\Omega^1(U;\mathbb R^n),\qquad \Omega:=s^*\omega\in\Omega^1(U;\mathfrak{gl}(n,\mathbb R)).
\end{align*}
Write $\vartheta_i$ for the component one-forms of $\vartheta$, and write $\Omega_{ij}$ for the matrix entries of $\Omega$, so that
\begin{align*}
X=\sum_{i=1}^n \vartheta_i(X)e_i
\end{align*}
for every $X\in\mathfrak X(U)$, and the induced connection is determined by
\begin{align*}
\nabla_Xe_j=\sum_{i=1}^n \Omega_{ij}(X)e_i.
\end{align*}
Since pullback commutes with exterior differentiation and with the wedge product,
\begin{align*}
s^*T=d\vartheta+\Omega\wedge\vartheta.
\end{align*}
For $X,Y\in\mathfrak X(U)$, its $i$-th component is
\begin{align*}
(s^*T)_i(X,Y)=d\vartheta_i(X,Y)+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)-\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X).
\end{align*}
Using the definition of [exterior derivative](/theorems/1525) on a one-form,
\begin{align*}
d\vartheta_i(X,Y)=X(\vartheta_i(Y))-Y(\vartheta_i(X))-\vartheta_i([X,Y]).
\end{align*}
Therefore
\begin{align*}
(s^*T)_i(X,Y)=X(\vartheta_i(Y))-Y(\vartheta_i(X))-\vartheta_i([X,Y])+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)-\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X).
\end{align*}
On the other hand, expanding $Y=\sum_{j=1}^n\vartheta_j(Y)e_j$ gives
\begin{align*}
\nabla_XY=\sum_{i=1}^n\left(X(\vartheta_i(Y))+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)\right)e_i.
\end{align*}
Similarly,
\begin{align*}
\nabla_YX=\sum_{i=1}^n\left(Y(\vartheta_i(X))+\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X)\right)e_i.
\end{align*}
Subtracting these two expressions and subtracting $[X,Y]=\sum_{i=1}^n\vartheta_i([X,Y])e_i$ yields
\begin{align*}
\nabla_XY-\nabla_YX-[X,Y]=\sum_{i=1}^n(s^*T)_i(X,Y)e_i.
\end{align*}
By the definition of the descended tensor $\tau$, the right-hand side is exactly $\tau(X,Y)$ on $U$. Since $U$ and the local frame $s$ were arbitrary,
\begin{align*}
\tau(X,Y)=\nabla_XY-\nabla_YX-[X,Y]
\end{align*}
for all $X,Y\in\mathfrak X(M)$. This identifies the tensor descended from $T$ with $\operatorname{Tor}_{\nabla}$ and completes the proof.
[guided]
The final task is to compare the principal-bundle formula with the usual torsion tensor in a frame. Let $U\subset M$ be open, and let $s:U\to F(M)$ be a smooth local frame. For $1\le i\le n$, define $e_i:U\to TM$ by $e_i(x)=s(x)(e_{i,0})$, where $(e_{1,0},\dots,e_{n,0})$ is the standard basis of $\mathbb R^n$. The pulled-back solder form $\vartheta:=s^*\theta\in\Omega^1(U;\mathbb R^n)$ records the components of tangent vectors in this frame, so every $X\in\mathfrak X(U)$ has the expansion
\begin{align*}
X=\sum_{i=1}^n \vartheta_i(X)e_i.
\end{align*}
The pulled-back connection form $\Omega:=s^*\omega\in\Omega^1(U;\mathfrak{gl}(n,\mathbb R))$ records the connection coefficients, namely
\begin{align*}
\nabla_Xe_j=\sum_{i=1}^n \Omega_{ij}(X)e_i.
\end{align*}
Pulling back $T=d\theta+\omega\wedge\theta$ by $s$ is legitimate because exterior differentiation and wedge products commute with pullback. Thus
\begin{align*}
s^*T=d\vartheta+\Omega\wedge\vartheta.
\end{align*}
Evaluating the $i$-th component on $X,Y\in\mathfrak X(U)$ gives
\begin{align*}
(s^*T)_i(X,Y)=d\vartheta_i(X,Y)+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)-\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X).
\end{align*}
The exterior derivative of the one-form $\vartheta_i$ is
\begin{align*}
d\vartheta_i(X,Y)=X(\vartheta_i(Y))-Y(\vartheta_i(X))-\vartheta_i([X,Y]).
\end{align*}
Substituting this identity yields
\begin{align*}
(s^*T)_i(X,Y)=X(\vartheta_i(Y))-Y(\vartheta_i(X))-\vartheta_i([X,Y])+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)-\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X).
\end{align*}
Now expand the covariant derivative using the frame. Since $Y=\sum_{j=1}^n\vartheta_j(Y)e_j$, the Leibniz rule for the connection gives
\begin{align*}
\nabla_XY=\sum_{i=1}^n\left(X(\vartheta_i(Y))+\sum_{j=1}^n\Omega_{ij}(X)\vartheta_j(Y)\right)e_i.
\end{align*}
Similarly,
\begin{align*}
\nabla_YX=\sum_{i=1}^n\left(Y(\vartheta_i(X))+\sum_{j=1}^n\Omega_{ij}(Y)\vartheta_j(X)\right)e_i.
\end{align*}
Subtracting these two formulas and then subtracting $[X,Y]=\sum_{i=1}^n\vartheta_i([X,Y])e_i$ gives
\begin{align*}
\nabla_XY-\nabla_YX-[X,Y]=\sum_{i=1}^n(s^*T)_i(X,Y)e_i.
\end{align*}
By construction of the descended tensor, the right-hand side is exactly $\tau(X,Y)$ on $U$. Because the [open set](/page/Open%20Set) $U$ and the local frame $s$ were arbitrary, this identity holds for all vector fields $X,Y\in\mathfrak X(M)$:
\begin{align*}
\tau(X,Y)=\nabla_XY-\nabla_YX-[X,Y].
\end{align*}
Thus the tensor corresponding to the torsion form $T$ is precisely $\operatorname{Tor}_{\nabla}$.
[/guided]
[/step]
