Why is Lie derivative smooth?

Question

Let $G$ be a linear Lie group, say $\mathrm{SL}(2,\mathbb{R})$. Suppose $X\in\mathfrak{g}$ and $f:G\to\mathbb{R}$ is smooth. The Lie derivative of $f$ with respect to $X$ is the function $\mathcal{L}_X f:G\to\mathbb{R}$ defined as $$\mathcal{L}_X f(y):=\left.\frac{\mathrm{d}}{\mathrm{d}t}\right|_{t=0}f\left(ye^{tX}\right).$$ Why is $\mathcal{L}_X f$ smooth? In his book on $\mathrm{SL}(2,\mathbb{R})$, Lang just says so without any comment (p. 90), but I failed to provide a rigorous justification up to now. A reference is also welcome.

Answer 1

Because the map $$\phi:G\times\Bbb R\to G,~(g,t)\mapsto g\exp(tX)$$ is smooth, as it is obtained from the smooth map $\Bbb R\to G,~t\mapsto \exp(tX)$ and the smooth map $\mu:G\times G\to G,~(g,g')\mapsto gg'$. The Lie derivative of $f$ is the derivative with respect to $t$ of the smooth map $$f\circ\phi:G\times\Bbb R\to\Bbb R,~(g,t)\mapsto f(\phi(g,t))$$ and it is thererfore smooth.

---

To be $100\%$ precise (and pretty pedantic), it is obtained as the composite $$\begin{array}{c} G&\to &T(G\times\Bbb R)&\to& T\Bbb R\simeq \Bbb R\times\Bbb R&\to&\Bbb R\\ g&\mapsto& {\frac{\partial}{\partial t}}\bigg|_{(g,0)}&\mapsto & T_{(g,0)}(f\circ\phi)\bigg({\frac{\partial}{\partial t}}\bigg|_{(g,0)}\bigg)= \underbrace{\lambda}_{=\mathcal L_Xf(g)}\frac{\partial}{\partial t}\bigg|_{f(g)}&\mapsto&\lambda \end{array}$$