Extend manifold smoothness

Stream: mathlib4

[Sébastien Gouëzel]

Currently, in mathlib, we have smooth manifolds, and analytic manifolds, separately. Most of the API is only for smooth manifolds (for instance, we have smooth vector bundles, but no analytic vector bundles).

#19696 (WIP, but builds) merges the two, so that we only have one typeclass ContMDiffManifoldWithCorners I n M, where I is the model with corners, n : WithTop ℕ∞ is the smoothness class (an integer, or ∞, or ω), and M is the space (which already has a charted space structure, so ContMDiffManifoldWithCorners I n M is Prop-valued).

Since it is a big revamp of the manifold library, it's probably the right time to discuss the design decisions and naming. Here are a few questions in this respect.

[Sébastien Gouëzel]

• The name ContMDiffManifoldWithCorners, although coherent with the library, is way too long. I would go for just IsManifold. @Michael Rothgang suggests IsManifoldWithCorners.
• For Lie groups and friends, should we have an arbitrary smoothness index n : WithTop ℕ∞, or should we just go for analytic? All the applications I know are in the analytic framework.
• I've deleted the file AnalyticManifold, as it's superseded by the new construction. Is that ok for everyone?

[Sébastien Gouëzel]

I'd be especially interested in opinions of @Heather Macbeth , @Patrick Massot , @Michael Rothgang , @Floris van Doorn , @Oliver Nash , @Geoffrey Irving , as these changes are quite disruptive. There is no hurry to get this in, but in the long run I think it's a big improvement over the current situation.

[Kim Morrison]

Don't we need the distinction between smooth and analytic Lie groups, just to be able to state that the BCH formula shows they are the same?

[Floris van Doorn]

I like IsManifold as the name. If the docstring states that it can be with corners, that seems good enough to me.
I'll take a look at the other things later.

[Michael Rothgang]

I don't feel strongly over IsManifold or IsManifoldWithCorners: basically, a convention "all manifolds have boundary and/or corners unless mentioned otherwise" is also fine with me, provided the doc-string is clear.

[Michael Rothgang]

This change means topological manifolds are (finally) integrated in this hierarchy as well, right? (I think this is a good change. Long-term, we'll want to have topological manifolds without smooth structures.)

[Sébastien Gouëzel]

Yes, topological manifolds are also part of the new hierarchy, as IsManifold I 0 M. In a sense, they were already there, though, since ChartedSpace H M already contains the information that the change of coordinates are continuous.

[Sébastien Gouëzel]

i.e., IsManifold I 0 M is always true once ChartedSpace H M holds. I should probably register the instance, by the way.

[Oliver Nash]

I'll need a little more time to study this but I'm certainly a fan of IsManifold as the name.

[Kevin Buzzard]

If IsManifoldWithCorners means "I definitely have corners" then that's great, but if it means "I might have corners" then I think IsManifold is a better name for it. There will be plenty of manifolds in parts of the proof of FLT but none will have any corners, so you just say it's a manifold and then you say however you say there are no corners and it's less confusing.

[Sébastien Gouëzel]

It means "I might have corners". It seems there is a consensus on the naming, so I've switched to IsManifold. The PR is still marked as WIP, I'll wait for the end of the discussion before cleaning it up and changing its status.

[Oliver Nash]

On the Lie group point, if we demand analyticity definitionally, it will make it harder to prove certain objects are Lie groups, right? E.g., say I wanted to prove that the holonomy group of a Riemannian manifold was a Lie group?

[Oliver Nash]

I suppose in an ideal world we would have a custom constructor which provided a Lie group which was definitionally analytic but which demanded only C^1 (or whatever weakest condition suffices). Maybe until that constructor exists, we maintain the smoothness class as a parameter?

[Geoffrey Irving]

How does the new type cover analytic manifolds in the infinite dimensional case?

For the finite dimensional case I have a proof of Osgood’s theorem and such in my Mandelbrot repo, so I can recover what I need from IsManifold. I suppose this is the best way if we care only about finite dimensions.

[Geoffrey Irving]

Oh, sorry, I missed the double with-top setup. All good!

[Sébastien Gouëzel]

Here is an update on the PR status: as a result of the above discussion, I've switched to IsManifold and kept the smoothness index in Lie groups and friends. The PR #19696 is now almost ready for review -- I've extracted the bits that could be made independent in #19807, which has been maintainer delegated by @Michael Rothgang (but not yet merged).

Once this is in, #19696 will be painful to review (+1400/-1000, has to be done in one go) but there is mostly no mathematical content, it's just adapting a lot of docstrings (I'm sure I missed some, but I've already fixed a big lot of them) and changing ℕ∞ to WithTop ℕ∞ in many places and fixing the breakage.

[Winston Yin (尹維晨)]

Thank you so much for this significant refactor! I'm very happy to see the generalisation and retirement of the name SmoothManifoldWithCorners. Is ContMDiff going to generalise to WithTop ℕ∞, too?

[Sébastien Gouëzel]

Yes, that's part of the refactor, and done in #19696.

[Michael Rothgang]

Copying what I wrote on github: I can review the rest of #19696/re-review it on (probably) Tuesday or Wednesday.

[Winston Yin (尹維晨)]

Sébastien Gouëzel said:

Yes, that's part of the refactor, and done in #19696.

How did I miss that! Thanks for doing all this.

[Winston Yin (尹維晨)]

I notice that you've registered instances to help typeclass inference for IsManifold I ∞ M → IsManifold I n M where n ≤ ∞ (for which you introduced a new class LEInfty); ω → n where n : WithTop N∞; n → 0 where n : WithTop N∞; and an ad hoc 2 → 1. I believe we need to generalise that last one to n → 1 where [NeZero n] for all differentiable manifolds, because many results (e.g. for the tangent space or integral curves) are stated for (at least) $C^1$ manifolds, but there is currently no easy way for Lean to infer the IsManifold I 1 M instance from an IsManifold I 42 M manifold. Am I missing something?

[Winston Yin (尹維晨)]

I guess we could either state the results generally for [IsManifold I n M] [NeZero n] or for [IsManifold I 1 M] and rely on typeclass inference. The latter seems to be the approach being taken here.

[Winston Yin (尹維晨)]

This would also address Michael's comment in Geometry/Manifold/ContMDiffMFDeriv.lean by doing haveI : NeZero n instead (untested).

[Sébastien Gouëzel]

Unfortunately, an instance like

instance [NeZero n] [IsManifold I n M] : IsManifold I 1 M

can not work: if you're looking for IsManifold I 1 M, there is no way Lean could guess a suitable value of n out of thin air to apply the instance (contrary to fixed values of n like 2 or infinity).

That's the reason why, in the PR, the results about the existence of a topology on the tangent space, and the existence of integral curves, are stated assuming IsManifold I 1 M: because otherwise there would be an n that couldn't be determined from the conclusion of the theorem and that Lean would never be able to guess.

[Winston Yin (尹維晨)]

Thanks for the explanation. I suspected there must've been a catch somewhere!