There exist neighbourhoods (containing the zero matrix) and (containing the identity matrix) such that and is invertible. We call the inverse .
We have introduced the exponential map, which takes any -by- matrix and returns an invertible -by- matrix. Symbolically, we write: (We could replace with ). Here, denotes the group of invertible -by- matrices with real entries (L stands for "linear", G stands for "general) and denotes the set of all matrices. This notation may look weird now, but as the course goes on we will see that to any group of matrices there is a set of matrices whose exponentials live in and the notation is always to turn the name of the group into lower-case Gothic font (e.g. gives us ).
Can we define an inverse ? It turns out that we can, though we run into some issues: even for numbers we have a problem, namely that , so there are many choices of logarithm. In that situation, we fix this by taking a branch cut from the origin along the negative -axis and only try to define the logarithm for numbers away from the branch cut (when we cross the branch cut we have to change which branch of the logarithm we're using if we want the logarithm to be continuous). We use a similar trick here, in that we only define the logarithm for a subset of matrices, those close to the identity matrix.
This logarithm is infinitely differentiable and even analytic; we'll write down its Taylor series later.
Inverse function theorem
We will prove this theorem by appealing to a result from multivariable calculus called the inverse function theorem. We won't prove the inverse function theorem, but we will explain how to apply it to deduce local invertibility of the exponential map:
Suppose is a continuously differentiable function. Think of as a vector of functions . We define the derivative of at the origin to be the matrix of partial derivatives: If is invertible then there exist neighbourhoods (containing ) and (containing ) such that and is invertible. Moreover, is differentiable with derivative .
The nice thing about calculus is that it replaces nonlinear objects (like ) with much simpler linear approximations (like ), then it proves theorems of the form "assume something about the linearisation, then deduce something local about the nonlinear object". Here we're assuming the linearisation is invertible and we deduce that is locally invertible.
Proof of local invertibility
Let's see how to apply this to the exponential map and deduce the existence of the local logarithm. The exponential map goes from to , and we can think of as the Euclidean space with coordinates given by the matrix entries. Similarly, is contained in (again using matrix entries as local coordinates). So we can think of as a map , which puts us in the setting of the inverse function theorem.
It remains to compute . When we identify with , we're writing each -by- matrix as a vector just by writing the matrix entries in a column instead of a grid. In other words, using matrix entries as coordinates, we need to compute the matrix whose entries are: Here, all partial derivatives are evaluated at . If this big matrix is confusing, think about the -by- matrix you get when .
We know the Taylor series where the dots are higher-order. When we differentiate with respect to , the constant term goes away, and the higher order terms still have factors of in them (for some ) so when we set these go away. All we are left with is the linear term , so . The s are just independent variables, so for example while . Therefore the matrix equals which is the identity matrix.
Another way of thinking about this is that the Taylor expansion of a function is , that is is the first order part of the Taylor expansion of . Therefore and we know the first order part of the Taylor expansion of is , so . So is the identity.
Since the is invertible (it's the identity!), this means that we can apply the inverse function theorem to deduce that admits a local inverse near the identity.
It turns out that the logarithm is analytic, that is its Taylor series converges on some set of matrices. The Taylor series is exactly the same as the Taylor series for the usual logarithm, that is Here, any matrix inside is close to the identity, so can be written as for a small matrix .