lie groups

Stream: maths

[Johan Commelin]

1. Is there anything blocking the definition of a Lie group?
2. If not, is there anything blocking the definition of examples of Lie groups, such as GL_n and SL_n?

[Kenny Lau]

1. manifolds
2. implicit function theorem

[Johan Commelin]

@Kenny Lau Could you expand? We seem to have both of these.

[Kenny Lau]

oh I thought Patrick said earlier that manifolds are difficult

[Johan Commelin]

He said that 2 years ago

[Kenny Lau]

tempus fugit

[Johan Commelin]

Since then @Sebastien Gouezel appeared. And now manifolds are still difficult. But no longer non-existent.

[Patrick Massot]

We don't quite have implicit function theorem yet. And we certainly don't have the API to use it to build manifolds.

[Patrick Massot]

So I think it should be easy to define Lie groups and prove $GL_n(\mathbb R)$ is a Lie group. But $SL_n(\mathbb R)$ and $O_n(\mathbb R)$ are still out of reach.

[Johan Commelin]

What is the name of the predicate that claims that a function M → M' is "smooth with respect to certain structure groupoids"?

[Johan Commelin]

mdifferentiable on gives C^1-functions, right?

[Johan Commelin]

Maybe we should wait for the analytic functions PR.

[Sebastien Gouezel]

Smooth functions on manifolds have been on my hard drive for a long time, I should PR them. But for now I am refactoring local equivs to use coercions instead of .to_fun and .inv_fun, as this works reasonably well with Lean 3.10. This really improves readability!

[Johan Commelin]

Cool! That's great news. I will park Lie groups for now. But hearing that coercions are returning is really good!

[Kevin Buzzard]

This sounds like a great idea! It's not just readability -- it is somehow expressing "what is actually going on".

[Kevin Buzzard]

(or at least my mental model of what is really going on -- an equiv is a map with some other stuff, but really it's a map)

[Reid Barton]

Are you not running into any issues with inferring arguments of your equivs, then?

[Reid Barton]

I mean for example in your post https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/transitive.20coercions/near/195971827 if you replace my_equiv2 α x with my_equiv2 _ x then Lean can't fill in the _, even though it looks obvious that it should be α. (For instance with .to_fun added it works with or without the _.)

[Sebastien Gouezel]

My equivs are charts on a manifold, and I didn't run into the issue you mention with them. The only issue is that, sometimes, when Lean should coerce a chart to a function, it doesn't want to do it, and I have to provide type annotations.

[Oliver Nash]

I for one would _love_ to have Lie groups as I secretly want to formalise the Yang-Mills equations.

[Michael R Douglas]

You can formalize perturbative quantum Yang-Mills just using the Lie algebra.

[Nicolò Cavalleri]

@Sebastien Gouezel did you by chance have the opportunity to PR smooth functions on manifolds? I had a look at the manifold files and it looks not to be there, but maybe I missed it! In case not, when are you planning to push them?

[Johan Commelin]

@Nicolò Cavalleri See #2962

[Sebastien Gouezel]

Yes, at Johan points out it's PRed in #2962, but I have some clean up to do.

[Nicolò Cavalleri]

Oh ok thanks a lot! Then I will start copying the files and use them locally on my computer and then I will wait for the merge to be approved to import it!

[Patrick Massot]

You don't have to do anything tricky. leanproject get mathlib:times_cont_mdiff will download everything (including compiled oleans) to a mathlib_times_cont_mdiff folder (unless you ask for another folder name).

[Nicolò Cavalleri]

Ok thanks that's helpful!

[Patrick Massot]

That's mostly a convenience for people reviewing pull requests but it can also be useful for impatient people.

[Nicolò Cavalleri]

I am sorry if this is a stupid question, but it is one of the first times I am using lean and I am a bit unfamiliar with it. I see that in times_cont_mdiff C^\infty is expressed as times_cont_mdiff ⊤ times, where ⊤ is not a T but a special character. I cannot find anywhere the definition of ⊤ and I would be really grateful if someone could point out to me some place where I can read how it works (the defining code would be fine)!

[Kevin Buzzard]

It looks like "top" to me, the maximal element of a lattice. What is its type?

[Johan Commelin]

@Nicolò Cavalleri (It's better if new questions start in a new thread.)
You can write

#print notation ⊤

to find out what it is.

[Johan Commelin]

You'll find that it is has_top.top.

[Bryan Gin-ge Chen]

In this case, it's with_top ℕ.

[Bryan Gin-ge Chen]

https://github.com/leanprover-community/mathlib/pull/2962/files#diff-badb0bdbd1d80cdea539f32e49073dfaR51

[Johan Commelin]

If you hover over times_cont_mdiff, you will see that the first parameter is a with_top nat... so that should explain what kind of top this is.

[Kevin Buzzard]

So the lattice is $\mathbb{N}\cup\{\infty\}$ and it's the top element of that.

[Johan Commelin]

In other words, you are looking at $C^\infty$ functions :wink:

[Nicolò Cavalleri]

Ok thanks a lot to everybody. It looks like now the main tools to define Lie groups are there, so I was wondering: is anybody working on a definition that will be PRed on the mathlib? I am writing a temporary definition myself to work to some projects, but depending on when it will be available on mathlib I might spend more or less time proving basic properties. I also saw not a lot has been written about product manifolds (even though the hardest part, the product of models with corners, is there) so I was wondering if anybody is planning to write something more in the near future (just so that I do not spend time writing duplicate code)

[Sebastien Gouezel]

I am not working on this currently. I would like to refactor some things to make the manifold library easier to read and to use, but this is orthogonal to what you want to do, so I'd say go ahead! And don't hesitate to PR to mathlib, or show some code here on Zulip, or even share your thoughts on what you find nice to use / less nice to use: all this would be super-useful.