Lie group exponential map

Stream: Is there code for X?

[Dominic Steinitz]

Does mathlib currently define a Lie group exponential map $\exp : \mathfrak{g} → G$ for general Lie groups or even in special cases?

If it exists, is it defined via flows of left-invariant vector fields?

[Johan Commelin]

I don't think it exists

[Michael Rothgang]

CC @Winston Yin (尹維晨)

[Ben Eltschig]

I don't know if anyone is working on it, but it at least does not exist in mathlib yet - Mathlib.Geometry.Manifold.GroupLieAlgebra, the file that defines the Lie algebra of a Lie group, is not imported by any other files yet.

[Ben Eltschig]

This is a special case of exponential maps on a manifold with an affine connection, right? I'm tempted to say that to avoid API duplication, it would make sense to define exponential maps in this more general setting first - but then again, exponential maps on Lie groups should be a lot easier to define, and if we want the exponential map to actually involve docs#GroupLieAlgebra we need a separate definition / abbrev anyway (or maybe not, since GroupLieAlgebra is itself an abbrev?)

[Matteo Cipollina]

if it can be useful, as a special case we have a concrete implementation for the Lorentz group (matrix Lie groups) in PhysLean, using NormedSpace.exp (the power series definition)

[Dominic Steinitz]

Ben Eltschig said:

This is a special case of exponential maps on a manifold with an affine connection, right? I'm tempted to say that to avoid API duplication, it would make sense to define exponential maps in this more general setting first - but then again, exponential maps on Lie groups should be a lot easier to define, and if we want the exponential map to actually involve docs#GroupLieAlgebra we need a separate definition / abbrev anyway (or maybe not, since GroupLieAlgebra is itself an abbrev?)

Not quite. The idea is you can put a connection on any bundle (a smooth choice of the horizontal subspace) but if you have a principal bundle then you can encode this via a Lie-algebra valued 1-form which is defined using the exponential map. Does that make sense? I think we will need flows to define the exponential map and this may be something else that does not yet exist.

[Winston Yin (尹維晨)]

@Dominic Steinitz , I would recommend first searching the Zulip for mentions of the exponential map, as well as Lie group/algebra. There has been quite a bit of discussion in multiple threads about this. Here's an example thread #Is there code for X? > Lie algebra exponential map? @ 💬 . Wanting to define exponential maps on Lie groups brought me to integral curves and flows on manifolds. There are open PRs which I would like to land: #26394, #26395. Then, you can define exponential maps as global integral curves on the Lie group.

Since manifolds on Mathlib are quite general and could be infinite-dimensional, there's some subtleties surrounding several inequivalent definitions of the tangent space at a point. There's some discussion on Zulip about this point as well, which I recommend reading.

I have now gone in a different direction. I'm now working on the smoothness of flows with respect to the starting position.

[Dominic Steinitz]

@Winston Yin (尹維晨) Thanks very much. I have read some of them. I wasn't aware of the one you reference. I will search more thoroughly.

I wasn't aware of your PRs which I think get us some of the way there (don't we need to know that the flows on left invariant vector fields are complete not just on compact spaces?). Why have they not been merged?

I am not keen to go down this particular rabbit hole just at the moment. I think I can move forward by making the existence of global flows (on left invariant vector fields) a hypothesis on my definitions / theorems and then come back later and prove this existence (this is what seems to have happened with Riemannian metrics unless I missed a previous existence proof). Saying the same thing a different way, I'd like to get the big picture first and then fill in the details. E.g. I'd like to be able to write down the Maurer-Cartin form, the Cartan structure equations, the Bianchi identities - that sort of thing. Then we can start to think of doing general relativity and gauge theory. But maybe this is all too ambitious.