In this video, we will prove the following theorem which was stated earlier:
If big F from G to H is a smooth homomorphism of matrix groups and little f denotes the locally-defined map log composed big F composed exp from little g to little h then:
little f is the restriction of a linear map F star from little g to little h to a neighbourhood of 0 in little g.
big F of exp X equals exp of F star X for all X in little g,
F star X bracket Y equals F star X bracket F star Y for all X and Y in little g.
Our first observation is that, for all X in little g, exp t X is a 1-parameter subgroup. Since big F is a smooth homomorphism, and since a 1-parameter subgroup is just a smooth homomorphism from the additive reals, we deduce that big F of exp t X is a 1-parameter subgroup in H. By what we proved about 1-parameter subgroups, big F of exp t X equals exp t Y for some Y in little g.
The figure above shows the groups G and H, the paths exp t X and exp t Y, and (red) neighbourhoods of the identity in each on which the logarithm is well-defined. For small t, exp t X and exp t Y are both close to the identity, so live in the domain of the local logarithm.
We have big F of exp t X equals exp of little f of t X for small t and big F of exp t X equals exp t Y for all t. Therefore, for small t we can take logarithms and deduce that little f of t X equals t Y.
Since little f is a smooth map, we can take the Taylor series little f of t X equals t d at zero of little f applied to X plus terms of higher order in t, where d at zero of little f is the derivative of little f at 0. Because little f of t X equals t Y, we see that d at zero of little f at X equals Y and all higher order terms vanish.
This means that little f of t X equals t Y, equals d at zero of little f applied to t X, equals t times d at zero of little f applied to X for all X and all sufficiently small t. Therefore little f equals d at zero of little f on the domain of the exponential chart. We take F star equals d at zero of little f. This proves the first part of the theorem. Recall that the matrix for the linear map d at zero of little f is the matrix of partial derivatives of components of little f, d at zero of little f equals the matrix whose i,j entry is partial d little f_i by d x_j.
The second part follows from what we have already said: we showed that big F of exp t X equals exp of t Y (for all t), and Y equals d at zero of little f applied to X, which equals F star of X. Setting t=1 we get big F of exp X equals exp of F star of X.
To prove the final part of the theorem, consider the expression exp of t X, times exp of t Y, times exp of minus t X, times exp of minus t Y Use the Baker-Campbell-Hausdorff formula to multiply the first two and last two terms together and we get exp of (t (X plus Y) plus a half t squared X bracket Y, plus dot dot dot Using the Baker-Campbell-Hausdorff formula to multiply these two together, after a little manipulation, we get exp of t squared X bracket Y plus terms of order t cubed
If I apply big F to this whole expression, we get: big F of exp of t squared X bracket Y plus higher order terms, equals exp of t squared F star of X bracket Y plus higher order terms by definition of F star.
Because big F is a homomorphism, big F of (exp t X, times exp t Y, times exp of minus t X, times exp of minus t Y) equals F of exp t X, times F of exp t Y, times F of exp minus t X, times F of exp minus t Y. By definition of F star, this equals exp of t F star X, times exp of t F star Y, times exp of minus t F star X, times exp of minus t F star Y and using the Baker-Campbell-Hausdorff formula in the same way we get exp of t squared F star X bracket F star Y plus higher order terms
If we take t small then we can take logarithms and we get t squared F star X bracket F star Y equals t squared F star of X bracket Y plus terms of order t cubed Differentiating twice and setting t=0 we get F star of X bracket Y equals F star X bracket F star Y as required.