Dan Piponi on Nostr: Let me take a first step at explaining my computation, assuming differential geometry ...

Let me take a first step at explaining my computation, assuming differential geometry knowledge.

People working with the exponential map often cheat! Their group may lie in a larger algebra, eg. the n by n matrices, and then you can compute exp via its power series. But that makes no sense here. Our group operation isn't inherited from a containing algebra. This is a good exercise in dealing with exp "intrinsically".

My starting point was the definition of exp(tX) at Wikipedia.

exp: 𝔤→G

with

(d/dt)exp(tX)=exp(tX)⋅X

The LHS and RHS are both tangent vectors at exp(tX).

t→exp(tX) is a path in G so (d/dt)exp(tX) is literally the tangent vector to this path at exp(tX). This vector is the derivation that takes a scalar field f to (d/dt)f(exp(tX)).

X is itself a tangent vector at id. So it is also a derivation, taking f to (d/dt)f(γ(t)) at t = 0, for some curve γ.

exp(tX)⋅X

is the action of the group element exp(tX) on the vector X. By definition, this group action comes from multiplying the path γ(t) by group elements exp(tX). Ie. exp(tX)⋅X is the derivation that takes f to (d/ds)(exp(tX)⋅γ(s)) at s=0.

The original (d/dt)exp(tX)=exp(tX)⋅X becomes the requirement that for any scalar f on the group:

(d/dt)(f(exp(tX)) = (d/ds)f(exp(tX)⋅γ(s))

In particular this is true if we choose f to be coordinates x or y considered as scalar functions on the curve.

Squint and this is similar to the Mathematica code except I (1) swapped t and s (2) took a limit and (3) accidentally wrote the arguments to ⊕ the wrong way round (irrelevant for a commutative group).

What's missing? Explaining my choice of γ, explaining the limit, and a subtlety over whether s is real or complex.

https://en.wikipedia.org/wiki/Exponential_map_(Lie_theory)