Issues with manifolds

Stream: maths

[Yury G. Kudryashov]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

I think the Cauchy integral formula is much more urgent.

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

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]

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

[Matthew Ballard]

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]

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

[Adam Topaz]

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]

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