Zulip Chat Archive

Stream: maths

Topic: lie groups


view this post on Zulip Johan Commelin (May 04 2020 at 13:29):

  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?

view this post on Zulip Kenny Lau (May 04 2020 at 13:30):

  1. manifolds
  2. implicit function theorem

view this post on Zulip Johan Commelin (May 04 2020 at 13:32):

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

view this post on Zulip Kenny Lau (May 04 2020 at 13:32):

oh I thought Patrick said earlier that manifolds are difficult

view this post on Zulip Johan Commelin (May 04 2020 at 13:32):

He said that 2 years ago

view this post on Zulip Kenny Lau (May 04 2020 at 13:33):

tempus fugit

view this post on Zulip Johan Commelin (May 04 2020 at 13:33):

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

view this post on Zulip Patrick Massot (May 04 2020 at 13:37):

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

view this post on Zulip Patrick Massot (May 04 2020 at 13:37):

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

view this post on Zulip Johan Commelin (May 04 2020 at 13:55):

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

view this post on Zulip Johan Commelin (May 04 2020 at 14:03):

mdifferentiable on gives C^1-functions, right?

view this post on Zulip Johan Commelin (May 04 2020 at 14:04):

Maybe we should wait for the analytic functions PR.

view this post on Zulip Sebastien Gouezel (May 04 2020 at 14:43):

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!

view this post on Zulip Johan Commelin (May 04 2020 at 14:45):

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

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:46):

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

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:47):

(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)

view this post on Zulip Reid Barton (May 04 2020 at 14:51):

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

view this post on Zulip Reid Barton (May 04 2020 at 14:54):

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 _.)

view this post on Zulip Sebastien Gouezel (May 04 2020 at 15:09):

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.

view this post on Zulip Oliver Nash (May 04 2020 at 15:25):

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

view this post on Zulip Michael R Douglas (May 04 2020 at 17:01):

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

view this post on Zulip Nicolò Cavalleri (Jun 13 2020 at 14:06):

@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?

view this post on Zulip Johan Commelin (Jun 13 2020 at 14:07):

@Nicolò Cavalleri See #2962

view this post on Zulip Sebastien Gouezel (Jun 13 2020 at 14:38):

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

view this post on Zulip Nicolò Cavalleri (Jun 13 2020 at 16:09):

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!

view this post on Zulip Patrick Massot (Jun 13 2020 at 16:37):

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).

view this post on Zulip Nicolò Cavalleri (Jun 13 2020 at 16:39):

Ok thanks that's helpful!

view this post on Zulip Patrick Massot (Jun 13 2020 at 16:46):

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

view this post on Zulip Nicolò Cavalleri (Jun 13 2020 at 18:20):

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)!

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:21):

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

view this post on Zulip Johan Commelin (Jun 13 2020 at 18:22):

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

#print notation 

to find out what it is.

view this post on Zulip Johan Commelin (Jun 13 2020 at 18:22):

You'll find that it is has_top.top.

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2020 at 18:22):

In this case, it's with_top ℕ.

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2020 at 18:23):

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

view this post on Zulip Johan Commelin (Jun 13 2020 at 18:23):

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.

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:23):

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

view this post on Zulip Johan Commelin (Jun 13 2020 at 18:24):

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

view this post on Zulip Nicolò Cavalleri (Jun 15 2020 at 10:30):

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)

view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 10:35):

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.


Last updated: May 12 2021 at 08:14 UTC