Zulip Chat Archive

Stream: maths

Topic: Issues with manifolds


Yury G. Kudryashov (Sep 26 2021 at 03:08):

I've realized that two things don't fit nicely into the current design of manifold_with_corners. I need neither of them in the nearest future but I think that we should have them in mind (or decide that we're not going to fit them into the definition).

  1. Orbifolds. Probably, they deserve a separate definition but I don't like the idea of duplicating tons of code.
  2. Complex manifolds with corners. E.g., closed triangles on the complex plane. Since complex derivative preserves angles, we either need a model space with all possible angles (and it becomes even more complicated in higher dimension), or do some huge refactor (e.g., drop charted_space and chart_at, use local_equivs with additional properties instead of local_homeomorphs as charts).
    @Sebastien Gouezel @Heather Macbeth @Patrick Massot :up:

Yury G. Kudryashov (Sep 26 2021 at 03:23):

One more question: should we accept {(x, y) | 0 ≤ y ≤ x²} as a manifold with corners? Here the issue is that we don't have unique differentiability at zero.

Patrick Massot (Sep 26 2021 at 03:54):

I don't think the parabola example should be a manifold with corners.

Patrick Massot (Sep 26 2021 at 03:55):

I don't think we should care about complex manifolds with corners unless someone comes up with a really compelling reason. I've never heard of this in the real world.

Patrick Massot (Sep 26 2021 at 03:56):

The orbifold question is trickier. Those definitely exist and indeed redoing everything from scratch would be painful. But I don't think we know enough about formalizing manifolds to think about orbifolds. We first need to actually use manifolds in Lean.

Heather Macbeth (Sep 26 2021 at 04:28):

Orbifolds can at least be charted spaces, so we don't need to start right from the beginning.

Yury G. Kudryashov (Sep 26 2021 at 04:34):

(about complex manifolds with corners: indeed, in all examples I can think of, the boundary is not included)

Yury G. Kudryashov (Sep 26 2021 at 04:35):

I think that it might be easier to modify charted spaces and reuse models with corners.

Yury G. Kudryashov (Sep 26 2021 at 04:35):

Each point knows (a) a finite group acting on H; (b) a local_homeomorph with the quotient by this group.

Yury G. Kudryashov (Sep 26 2021 at 04:36):

Then we should have a typeclass saying "the group is always trivial", and get our old local homeomorphism in this case.

Yury G. Kudryashov (Sep 26 2021 at 04:37):

I guess, it will be hard to do this without breaking some definitional equalities, so probably we'll need more maps and some equality axioms between them.

Patrick Massot (Sep 26 2021 at 04:39):

I think the Cauchy integral formula is much more urgent.

Yury G. Kudryashov (Sep 26 2021 at 04:40):

I understand. I've spent a few days on integrals, and I had to make a small break and think about something else.

Patrick Massot (Sep 26 2021 at 04:41):

Sorry, I didn't want to put pressure on you.

Yury G. Kudryashov (Sep 26 2021 at 04:45):

Actually, I was thinking about extra requirements I need to show that for a smooth map f : M → N from a manifold to a manifold of larger dimension, the complement to the range is dense (needed for the weak Whitney's embedding theorem), then somehow switched to "what other strange things are (not) allowed by our definitions?"

Sebastien Gouezel (Sep 26 2021 at 07:51):

As for orbifolds, my main problem with them is that the tangent bundle does not really exist (as a locally trivial vector bundle in the usual sense), the tangent map is not defined in the usual sense either, and so on. So everything we've constructed in the manifolds library does not even make sense for them. My impression is that the right context to work with orbifolds is rather algebraic varieties, so a completely different setup (and a completely different language).

Kevin Buzzard (Sep 26 2021 at 09:16):

Right -- do people do orbifolds with corners? Should this theory be done via sheaves?

Matthew Ballard (Sep 26 2021 at 13:49):

Kevin Buzzard said:

Right -- do people do orbifolds with corners? Should this theory be done via sheaves?

Pardon’s work would be interesting but very ambitious target

Patrick Massot (Sep 26 2021 at 14:11):

I already tried to sell that project to funding agencies twice...

Adam Topaz (Sep 26 2021 at 18:12):

Another approach to this, which I don't think has ever been formalized, is via something like synthetic differential geometry (e.g. as in http://tildeweb.au.dk/au76680/sdg99.pdf ) I also don't know if anyone has developed a synthetic approach to manifolds with corners, but it can certainly be done.

Matthew Ballard (Oct 05 2021 at 20:31):

Patrick Massot said:

I already tried to sell that project to funding agencies twice...

It is a project that makes a ton of sense but the subject is a bit of a minefield


Last updated: Dec 20 2023 at 11:08 UTC