Lie algebra exponential map?

Stream: Is there code for X?

[Thomas Murrills]

Do we have the exponential map for a generic Lie algebra anywhere yet? If not, is anyone working on it? If (also) not, I’d like to add it and some basic facts about it! :)

[Kevin Buzzard]

What is the codomain of this map?

[Thomas Murrills]

It ought to be the Lie group which the Lie algebra in question is associated with.

[Thomas Murrills]

(Oh, I suppose I shouldn’t have said “generic Lie algebra”, but instead “generic Lie group”—I was implicitly thinking about a Lie algebra/group pair.)

[Michael Stoll]

There are also Lie algebras over non-topological fields (or even rings).

[Kevin Buzzard]

Thomas Murrills said:

(Oh, I suppose I shouldn’t have said “generic Lie algebra”, but instead “generic Lie group”—I was implicitly thinking about a Lie algebra/group pair.)

Well before we do anything about the exponential map, we need to define Lie groups (not hard), and the Lie algebra associated to a Lie group (an interesting, feasible and in-scope project).

And of course one shouldn't restrict to the reals/complexes ;-) I should imagine (but I didn't think too hard about this) that the whole theory would work over a general complete topological field.

[Thomas Murrills]

Oh, I didn’t realize we didn’t have Lie groups yet! That certainly gives this project a nice starting point. I’ll plan to start in the next day or two—this will be my first contribution of actual mathematical (as opposed to metamathematical) content to mathlib, so I’m really looking forward to it! :D

[Kevin Buzzard]

Yeah that would be a really cool place to start :-)

I have no real idea how hard proving that the circle has a Lie group structure would be; I know the hard work of proving it's a manifold has been done, and the work of proving it's a topological group has also been done, so one could be cautiously optimistic that this would be a nice test case. A perhaps easier case would be the real numbers under addition; this would be an LieAddGroup (see TopologicalGroup and TopologicalAddGroup for how to set this up with the to_additive dance, so that we cover both addition and multiplication).

[Eric Wieser]

https://github.com/leanprover-community/mathlib/pull/15763 may be relevant here

[Kevin Buzzard]

Oh! So we do have docs#LieGroup ? I had never noticed!

[Eric Wieser]

Yes, and we also have docs#instLieGroupRealToNontriviallyNormedFieldDenselyNormedFieldEuclideanSpaceIsROrCFinOfNatNatInstOfNatNatFintypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupNormedAddCommGroupENNRealInstOfNatToNatCastInstCanonicallyOrderedCommSemiringENNRealProof_1Fact_one_le_two_ennrealNormedAddCommGroupNormedSpaceToNormedFieldToNormedSpaceInnerProductSpaceModelWithCornersSelfSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleToGroupCommGroupInstTopologicalSpaceSubtypeToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexInstChartedSpaceEuclideanSpaceRealIsROrCFinOfNatNatInstOfNatNatFintypeToTopologicalSpaceUniformSpaceENNRealInstOfNatToNatCastInstCanonicallyOrderedCommSemiringENNRealProof_1ToUniformSpacePseudoMetricSpaceSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstTopologicalSpaceSubtypeToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex, whatever that is

[Eric Wieser]

Oh, it's the fact that the circle is a lie group!

[Eric Wieser]

Which is obvious from the name

[Kevin Buzzard]

Cool! So in fact the project starts with the fun construction of the Lie algebra of a Lie group (which we don't seem to have).

[Kevin Buzzard]

Eric Wieser said:

Which is obvious from the name

circle.png

[Kevin Buzzard]

We also have docs#TangentSpace so my revised estimate of the first challenge is putting a Lie algebra structure on that.

[Eric Wieser]

It contains circle way more than that!

image.png

[Joachim Breitner]

These circles don’t Lie.

[Ruben Van de Velde]

Joachim Breitner said:

These circles don’t Lie.

No no, the point is that they do!

[Winston Yin (尹維晨)]

Eric Wieser said:

https://github.com/leanprover-community/mathlib/pull/15763 may be relevant here

Thanks for pulling this up again. I’ve been thinking about implementing integral curves on manifolds and proving things about smooth vector fields on Lie groups. @Thomas Murrills happy to work with you on this.

I haven’t touched this in a year or so partly because of the port, the stagnation of PR 15763, the refactor of the manifold/fibre bundle API, and me actually trying to do a PhD in physics. But I’d love to put in some work if there’s interest.

[Winston Yin (尹維晨)]

Just ported mathlib#15763 to mathlib4#8397

[Winston Yin (尹維晨)]

Also ported mathlib#17140 to mathlib4#8483, much improved but still WIP. This is the local existence of integral curves of vector fields on a manifold.

[Thomas Murrills]

That’s wonderful! :D I unexpectedly wasn’t available all last week, but I’m back at my computer once again and hope to start making progress over the next couple days. I’ll reach out again soon when I start! :)

[Winston Yin (尹維晨)]

Things to think about:

• To define exponential maps, we need integral curves on manifolds.
• mathlib4#8483 establishes local existence of integral curves for vector fields using the existence theorem for solutions to ODEs (docs#exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt).
• We still need to translate the uniqueness theorem for solutions to ODEs to manifolds (docs#ODE_solution_unique).
• We need to prove conditions for the global (for all time) existence of solutions (e.g. on compact manifolds, on Lie groups).
• To define the Lie algebra of vector fields, we can make contact between the topological definition of vector fields as sections of the tangent bundle (via docs#TangentSpace and docs#Bundle.TotalSpace.mk'), and the algebraic definition (via docs#Derivation) as derivatives of functions on the manifold. The latter is a Lie algebra (docs#Derivation.instLieAlgebra).
• To define the Lie algebra of smooth left-invariant vector fields of a Lie group, we need some combination of the previous point and docs#LeftInvariantDerivation. The latter is a Lie algebra (docs#LeftInvariantDerivation.instLieAlgebraLeftInvariantDerivationToCommRingToEuclideanDomainToFieldToNormedFieldInstLieRingLeftInvariantDerivation)
• We need that the vector space of smooth left-invariant vector fields of a Lie group is isomorphic to the tangent space at the identity of the Lie group.
• Now we can talk about the exponential map applied to elements of the tangent space at the identity as a way of constructing elements of the Lie group.

A lot of these can be worked on in parallel, and the combined result will probably be very satisfying! As someone in physics, I'm most interested in seeing matrix Lie groups, its Lie bracket coinciding with the matrix commutator, and the exponential map coinciding with matrix exponentiation.

[Kevin Buzzard]

Do you think you could run this via github projects?

[Winston Yin (尹維晨)]

Yes in principle and in spirit, but it'll have to be in the meagre free time outside of my PhD...

[Winston Yin (尹維晨)]

I haven't worked with GitHub projects before. Would be cool to set one up!

[Thomas Murrills]

This looks amazing! :D I'd be happy to help set up the project if time is an issue. I'm out of time for today, but I'm planning on starting Lie algebra-related work tomorrow... :)

[Kevin Buzzard]

@Winston Yin (尹維晨) I once set up a project, stated some goals, forgot all about it and then discovered some time later that a bunch of people had been working on it without my even noticing

[Kevin Buzzard]

People are looking for projects, one big issue I find with PhD students is that they have no idea what is feasible or what kind of a project to work on

[Winston Yin (尹維晨)]

@Kevin Buzzard I'm on the mathlib4 Projects page but do not see a button for creating new projects.

[Winston Yin (尹維晨)]

In hindsight I would've loved to do a maths PhD on formalisation but I'm now years into a physics PhD that I really need to finish.

[Michael Rothgang]

Regarding projects to do: #8397 (which shows that GL(V) is a (possible Banach-) Lie group) could use another pair of eyes for review. I think it's basically ready to go (just a few nits), but there are a few places where I feel there should be a nicer Lean solution... that I don't see yet.

[Kevin Buzzard]

@Winston Yin (尹維晨) with these new projects you create them on your own page and then link to them on mathlib's page I think. I'm still working new projects out.

[Winston Yin (尹維晨)]

Created a project on my own GitHub page but can't seem to link to it from mathlib. I'm guessing I should wait for settings to be tuned on leanprover-community's side.

[Ruben Van de Velde]

I think the @maintainers need to set it up? This seems annoying

[Johan Commelin]

@Winston Yin (尹維晨) How do you want you project to be called?

[Winston Yin (尹維晨)]

Exponential map on Lie groups

[Johan Commelin]

@Winston Yin (尹維晨) Hopefully https://github.com/orgs/leanprover-community/projects/16/views/1 is what you want

[Anne Baanen]

Projects are hidden by default, should I make it public?

[Winston Yin (尹維晨)]

Johan Commelin said:

Winston Yin (尹維晨) Hopefully https://github.com/orgs/leanprover-community/projects/16/views/1 is what you want

404?

[Ruben Van de Velde]

Anne Baanen said:

Projects are hidden by default, should I make it public?

I'm thinking yes

[Floris van Doorn]

I made the project public

[Winston Yin (尹維晨)]

Floris van Doorn said:

I made the project public

Don't mean to be annoying, but I don't seem to have edit access. In any case, I made this public project on my own account, which someone can also copy/link over to mathlib4.

https://github.com/users/winstonyin/projects/1

[Floris van Doorn]

I don't think there is a way to make a project editable for everyone. But I gave you write access to the mathlib version of the project.

[Winston Yin (尹維晨)]

Wrote up major steps towards exponential map on Lie groups in this project! Feel free to adjust / refine.

[Winston Yin (尹維晨)]

Three PRs (#8483, #8624, #8672) along this path ready for review

[Winston Yin (尹維晨)]

Uniqueness of integral curves of vector fields on manifolds just in! (Still WIP but sorry-free) #8886

[Winston Yin (尹維晨)]

Just formalised the uniform-time lemma for the existence of global integral curves on vector fields! (WIP but sorry-free) #9013

This lemma is needed to prove:

• Compactly supported vector fields on manifolds always have global integral curves
• Left-invariant vector fields on Lie groups always have global integral curves (<--- this is on the path towards the exponential map)

[Patrick Massot]

Great!