Symplectic geometry

Stream: maths

[Paul Lezeau]

Has anyone done stuff on Symplectic geometry? I'd be quite interested in working on proving things in that area, if anyone has already made a start :smile:

[Kevin Buzzard]

In some sense we have little more than the definition of a manifold, when it comes to geometry. My understanding is that we still can't do linear algebra with vector bundles.

[Patrick Massot]

We don't have differential forms yet.

[Heather Macbeth]

Not necessarily worth it, but I think you could prove some symplectic-like results in the two dimensional case even now. Assume you have an oriented 2-manifold equipped with a measure which on each chart is a smooth multiple of Lebesgue, for example. (We don't have oriented manifolds yet but it shouldn't be too hard, define the groupoid of functions whose differentials are pointwise orientation preserving.)

[Heather Macbeth]

For example, maybe it would be accessible to get Moser's theorem on the classification of compact symplectic 2-manifolds.

[Paul Lezeau]

Oh right. I'm also happy to work on manifold theory.

[Paul Lezeau]

Paul Lezeau said:

Oh right. I'm also happy to work on manifold theory.

Would there be any good places to start?

[Heather Macbeth]

I was proposing the Moser project a little while ago actually:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Partition.20of.20unity/near/246103773

[Heather Macbeth]

@Sebastien Gouezel is the person to ask, but in my opinion, a good warmup might be defining the oriented groupoid, we need that anyway!

[Heather Macbeth]

So, the groupoid of things in docs#times_cont_diff_groupoid whose differentials pointwise have positive docs#linear_map.det

[Heather Macbeth]

Now I think about it, Moser's theorem also works in the un-oriented case (as a result about densities rather than area (=symplectic) forms), so that would be an independent direction.

[Paul Lezeau]

Heather Macbeth said:

Sebastien Gouezel is the person to ask, but in my opinion, a good warmup might be defining the oriented groupoid, we need that anyway!

Sounds good, I'll have a go at that!

[Heather Macbeth]

Another nice task would be to extend @Yury G. Kudryashov's recent proof of existence and uniqueness for ODEs to the manifold setting, for example to prove we have existence for all time for flows of a vector field on a compact manifold.

[Heather Macbeth]

And/or to prove the existence of the 1-parameter subgroup associated to a identity tangent vector on a Lie group.

[Heather Macbeth]

docs#exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous ... I think you first need some calculus results about the smoothness of the solution if the data is smooth.