[Risolto] Dubbi sulla Derivata di Lie

[giaorl]

L'idea della definizione di derivata di Lie mi è chiara, i testi che ho consultato si sono dilungati abbastanza per dare una definizione intuitiva. Ho però un po' di problemi con il formalismo. Mi occorre richiamare alcuni concetti e alcuni risultati prima di introdurre la definizione interessata. Denoterò con [tex]\chi(M)[/tex] l'insieme dei campi vettoriali differenziabili sulla varietà M, con [tex]\gamma'(t_0)[/tex] il vettore tangente alla curva [tex]\gamma[/tex], con [tex](f_*)_p[/tex] l'applicazione tangente in p di una funzione tra varietà [tex]f[/tex].
Definizione 1: Si dice gruppo locale ad 1 parametro di trasformazioni differenziabili locali di M ogni applicazione differenziabile [tex]\psi:]-\varepsilon, \varepsilon [ \times U \rightarrow M[/tex], con [tex]\varepsilon > 0[/tex] e [tex]U[/tex] aperto di M, tale che:
1) [tex]\forall\ t \in ]-\varepsilon, \varepsilon [:\ \psi_t:= \psi(t,\cdot)[/tex] sia un diffeomorfismo tra [tex]U\ e\ \psi_t(U)[/tex];
2) [tex]\psi_0(U) = U[/tex] e [tex]\psi_0 = id_U[/tex];
3) [tex]\forall\ t,s \in ]-\varepsilon, \varepsilon [\ t.c.\ t+s \in ] -\varepsilon, \varepsilon [\ e\ \psi_s(U) \subset U:\ (\psi_t \circ \psi_s) = \psi_{t+s}[/tex].
Proposizione 2: Sia [tex]X \in \chi(M)[/tex]. Allora [tex]\forall\ p \in M \exist \varepsilon > 0,\ \exist U\ aperto\ di\ M,\ \exist \psi:]-\varepsilon, \varepsilon [ \times U \rightarrow M[/tex] gruppo locale ad 1 parametro di trasformazioni locali di M che generi [tex]X[/tex] in [tex]U[/tex] (cioè [tex]\forall\ p \in U:\ X_p = \psi_p'(0)[/tex]).
Proposizione 3: Sia [tex]f:M \rightarrow M'[/tex] un diffeomorfismo tra varietà. Allora esiste un isomorfismo tra le algebre di Lie [tex]f_*: \chi(M) \rightarrow \chi(M')[/tex]. (Tale isomorfismo opera così: [tex](f_*X)_{f(p)} = (f_*)_p(X_p)[/tex]).

Veniamo al dunque. Siano [tex]X,Y \in \chi(M),\ p \in M,\ \psi:]-\varepsilon,\varepsilon[ \times U \rightarrow M[/tex] gruppo locale ad un parametro che generi X in U, intorno di p.
Definizione: Si dice derivata di Lie di Y lungo X in p: [tex](L_X Y)_p := \lim_{t \to 0} \frac{1}{t}\left( Y_p - ((\psi_t)_* Y)_p \right)[/tex].

Il problema è questo: [tex]\psi_t: U \rightarrow \psi_t(U)[/tex] è un diffeomorfismo locale tra [tex]U[/tex] e [tex]\psi_t(U)[/tex], quindi per la proposizione 3 induce un isomorfismo tra le algebre di Lie [tex]\chi(U), \chi(\psi_t(U))[/tex]. Chi mi assicura che [tex]p \in \psi_t(U)[/tex]? (probabilmente, pensavamo io e un mio compagno di corso, al tendere di t a 0, è per una sorta di continuità e per il punto 2) della definizione 1; ma come si dovrebbe formalizzare una cosa del genere?).
Ho riscontrato lo stessissimo problema sul Warner - "Foundations of Differentiable Manifolds ans Lie Groups" e sul Boothby - "An introduction to Differentiable Manifolds and Riemannian Geometry".

[giaorl]

Probabilmente scrivere su questo forum mi porta consiglio perché finisco spesso col rispondermi da solo!
La risposta è semplice, ed in sostanza è la formalizzazione dell'idea che avevo scritto in precedenza: la curva [tex]\psi_p := \psi(\cdot,p):]-\varepsilon,\varepsilon[ \rightarrow M[/tex] è differenziabile, quindi continua. Inoltre [tex]\psi_p(0) = p \in U[/tex], quindi esiste [tex]\varepsilon' < \varepsilon[/tex] tale che [tex]\psi_p(]-\varepsilon',\varepsilon'[) \subset U[/tex], cioè [tex]\forall t \in ]-\varepsilon',\varepsilon'[:\ \psi_t(p) \in U[/tex]. Fissato [tex]t \in ]-\varepsilon', \varepsilon'[[/tex] si ha che [tex]\psi_{-t}(p) \in U[/tex], quindi, per il punto 3) della definizione 1): [tex]p = \psi_0 (p) = \psi_{t-t}(p) = \psi_t(\psi_{-t}(p)) \in \psi_t(U)[/tex].