Naturality of the Lie group exponential (source code)

= Naturality of the Lie group exponential
{title2=$F(\exp_Gv)=\exp_H(D_eF\,v)$}

For a <Lie group homomorphism> $F$, the image of the integral curve through the identity of a <left-invariant vector field> is the integral curve of the field induced by its differential. Uniqueness of <integral curves of a vector field> identifies the curves for all times. Evaluating at time one gives the formula. Completeness of invariant fields follows from left translation and repetition of a local integral curve, independently of a matrix-series formula.