Infinite-dimensional manifolds

Stream: maths

[Winston Yin (尹維晨)]

@Michael Rothgang and I are itching to define submanifolds as well as immersions and submersions between manifolds, but we need to make a choice about what to do in the case of infinite-dimensional manifolds, as there are equivalent definitions in finite dimensions that are inequivalent / unnatural in infinite dimensions. We hope a manifold expert here can make a judgment call so we can march ahead.

One generalisation would be Banach manifolds, for which we can follow Lang's Fundamentals of Differential Geometry. Another generalisation is to model manifolds on locally convex spaces, for which we can follow Kriegl and Michor or Schmeding. The latter would be of interest to me for its application in infinite-dimensional Hamiltonian problems in physics. However, this would first require a generalisation of most of mathlib's analysis to locally convex spaces.

In order to start doing something, would it be reasonable for us to assume Banach manifold as the chosen setting for now?

[Yury G. Kudryashov]

Are these definitions incompatible or they agree if the model space is a Banach space?

[Yury G. Kudryashov]

I have neither of these books at home, so can't compare the definitions. Can you post the definitions here?

[Winston Yin (尹維晨)]

Lang:

Let X be a manifold (of class C^p with p ≥ 0). Let Y be a subset of X and assume that for each point y ∈ Y there exists a chart (V, ψ) at y such that ψ gives an isomorphism of V with a product V₁ × V₂ where V₁ is open in some space E₁ and V₂ is open in some space E₂, and such that ψ (Y ∩ V) = V₁ × {a₂} for some point a₂ ∈ V₂ (which we could take to be 0). Then it is clear that Y is locally closed in X. Furthermore, the map ψ induces a bijection ψ₁ : Y ∩ V → V₁. The collection of pairs (Y ∩ V, ψ₁) obtained in the above manner constitutes an atlas for Y, of class C^p.

Let f : Z → X be a morphism, and let z ∈ Z. We shall say that f is an immersion at z if there exists an open neighborhood Z₁ of z in Z such that the restriction of f to Z₁ induces an isomorphism of Z₁ onto a sub- manifold of X. We say that f is an immersion if it is an immersion at every point.

A morphism f: X → Y will be called a submersion at a point x ∈ X if there exists a chart (U, ϕ) at x and a chart (V, ψ) at f(x) such that ϕ gives an isomorphism of U on a products U₁ x U₂ (U₁ and U₂ open in some Banach spaces), and such that the map is a projection. One sees then that the image of a submersion is an open subset (a submersion is in fact an open mapping). We say that f is a submersion if it is a submersion at every point.

[Winston Yin (尹維晨)]

Schmeding: submanifold (1.3.7), immersion/submersion (1.4.1)

Kriegl & Michor: submanifold (27.11)

[Yaël Dillies]

Winston Yin (尹維晨) said:

However, this would first require a generalisation of most of mathlib's analysis to locally convex spaces.

This is something I've been hoping for for several years. So not a malus as far as I am concerned.

[Winston Yin (尹維晨)]

Is somebody working on this generalisation?

[Yury G. Kudryashov]

The first step is to generalize docs#Asymptotics.IsLittleO and docs#HasFDerivAtFilter

[Yury G. Kudryashov]

You can find a recent discussion here

[Yury G. Kudryashov]

tl;dr I have a branch with a definition and theorems saying that it's equivalent to more classical definitions in 2 cases; needs work to make it Mathlib-ready; help is welcome since it's not a high priority project for me

[Winston Yin (尹維晨)]

Schmeding also uses a different approach than Kriegl & Michor. The former uses Bastiani calculus, while the latter uses convenient calculus, which is weaker than Bastiani calculus exactly in that smooth maps don't have to be continuous.

[Yury G. Kudryashov]

I (almost?) never needed calculus outside of the normed (normable) space setting, and I guess many other people here have the same experience. Could you please answer the following questions (applies both to calculus and submanifolds):

1. For each definition you mention, what are the assumptions on the domain and the codomain?
2. How does "a more general version of" graph look like?
3. Are there cases when two definitions apply and give different results?

[Winston Yin (尹維晨)]

I hope these are accurate based on my reading of the references.

Schmeding:

1. Manifolds modelled on locally convex spaces + Hausdorff. Submanifolds are modelled on sequentially closed subspaces. Immersion/submersion requires the model space of the codomain/domain to split in a way compatible with the function.
2. For f : M → N, graph f is a split submanifold of M × N.

Kriegl & Michor:

1. Manifolds modelled on convenient vector spaces (i.e. locally convex, c^∞-complete) + smoothly Hausdorff + domains of charts are c^∞-open. Submanifolds are modelled on closed subspaces. Notions of initial/final mappings between manifolds.
2. No idea

For question 3, I think both are meant to be generalisations of Banach manifolds, so definitions should boil down to some corresponding version in Banach manifolds, but I'm not an expert.

[Winston Yin (尹維晨)]

Since Banach manifolds are more familiar, I'm asking if you think it's reasonable to carry on developing the manifold library in this setting. It's not general enough for certain reasonable applications that I would find interesting, such as Morse theory or diffeomorphism groups, but these distant possibilities should be no reason to block progress today.

[Yury G. Kudryashov]

I'm sorry for misformulating. In (2) I meant, does one of the definition generalize the other? I was talking about the graph with vertices = definitions and directed edge = "definition A is more general than definition B".

[Yury G. Kudryashov]

@Sébastien Gouëzel Do you know anything about submanifolds in settings other than Banach spaces?

[Winston Yin (尹維晨)]

I don't feel confident enough to draw an accurate graph.

[Yury G. Kudryashov]

I think that we should go with normed spaces and HasMFDerivAt etc for now, think about generalizations later.

[Yury G. Kudryashov]

E.g., some day we should figure out how to deal with finitely smooth manifolds.

[Yury G. Kudryashov]

Possibly, we'll have to figure out how to deal with different calculus theories in one code base. But this is not an easy task.

[Sébastien Gouëzel]

No, I don't know anything beyond Banach spaces, and I think we should indeed start with Banach spaces.

[Sébastien Gouëzel]

A comment on submanifolds: it is hard to get this right from a design point of view, and that's why we don't have them already in mathlib. Basic use cases that should absolutely be covered are smooth submanifolds (e.g. the circle in the plane), but also smooth submanifolds with boundary (e.g., the closed disk in the plane) as these are crucial for Stokes formula.

Here is a possible design sketch. Let I be a model with corners (between H and E) and I' another model with corners (between H' and I'). Let J = J (I, I') be some class to be specified, registering an embedding of the model I' in the model I (think a subspace in a space, or a half-space in a whole space). Then consider M which is a smooth manifold with corner with respect to I, and N : Set M which is itself a smooth manifold with corners with respect to I'. Then N is a submanifold for J if it satisfies some properties, also to be specified.

The properties should be strong enough to entail a few basic properties. Like

• M is a submanifold of itself, for some trivial J (basically the identity)
• open sets of M are submanifold, for the same trivial J
• the inclusion of N in M is smooth
• Given another manifold P, a function f : P -> N is smoooth if and only if the composition with the inclusion is smooth as a function from P to M.

And one should have constructors, like: if N is a subset of a manifold M, which is locally given by level lines of a smooth function with onto derivative, then N inherits a charted space structure (with respect to some suitable H'), and a smooth manifold structure, (with respect to some suitable I') and for this smooth structure it is a submanifold (for a suitably defined J).

Finally, the circle and the closed disk should be submanifolds of the plane.

[Winston Yin (尹維晨)]

Thanks for writing this out. I've been experimenting with this over the weekend, and I think we're mostly on the same page so far. I agree with the difficulty of getting the design right. My ongoing approach is to first define immersion/embedding, so that submanifolds of M are defined by an already existing manifold N, not necessarily a subset of M, together with an embedding from N to M. Basically, there won't be a definition of submanifold, just the (injective) image of another manifold via an immersion/embedding. This way we avoid dealing with subsets unnecessarily, and an injective integral curve would automatically be a submanifold. Immersions also induce a charted space / smooth structure on its domain.

On the model side, the class J would be some slice condition, i.e. there exists an injective linear map (with some conditions) from E' to E which embeds range I' into range I. This works for the half-space/quadrant, and the half-line as a slice of the half-space. It doesn't require H' to be a subset of H or E' to be a submodule of E.

This means that a submanifold is really two pieces of data, your J specifying the model embedding and an immersion that is compatible with J.

Your fourth bullet point sounds analogous to what I did in #8397. (And perhaps we should use the number of o's in smoooooooth to refer to the smoothness class for a map :laughing:)

[Igor Khavkine]

Just curious, have you guys considered using Whitney stratifications as a general structure that can implement all sorts of boundaries, corners, conical singularities, etc? They are general enough that they could meet Mathlib needs for many special cases in the future. A quick search doesn't reveal any mention of this in the Zulip archives. This is not directly related to infinite dimensional manifolds. Sorry if I'm bringing this up in the wrong place, or retreading an old topic.

[Winston Yin (尹維晨)]

I'm not familiar with them. Are you proposing that the current ModelWithCorners be generalised somehow?

[Sébastien Gouëzel]

Yes, I've thought abouth them for mathlib when initially defining manifolds, but the design seems really hard to get right with respect to the interaction of subtypes and typeclasses, so I decided to postpone that until much later, when we have a nontrivial differential manifold library with real applications, and a better feeling for what works well and what doesn't work so well in our current framework.

[Antoine Chambert-Loir]

Manifolds with corners pose a difficulty, since the boundary is no more a manifold with corners. (Example: a square in the plane .) There is a theory where the boundary is not a sub-stuff but rather something else which is immersed into the expected boundary. (Example: the disjoint union of the 4 edges of the square.)

[Kevin Buzzard]

Maybe this discussion needs to be moved?

[Igor Khavkine]

I'm no great expert either on Whitney stratifications and especially not on Mathlib internals, but I do know from experience in the differential geometry literature, if you go down the path of defining boundaries, corners, cones, orbifold singularities, etc. by special constructions, you will likely never run out of special cases to cover.

I just think that having such a general structure available is a good target for the future. In particular, if one might want to eventually represent real/complex (semi-)algebraic sets as differential geometric objects (this already covers many examples with boundaries and corners), Whitney startifications are probably the way to go. So it is at least worth keeping them in mind at the level of design discussions.

[Omar Mohsen]

There is a definition used by Melrose school called manifolds with fibered corners which seems to be general enough for the theory of manifolds with corners and their boundaries etc

[David Michael Roberts]

FWIW, the Bastiani calculus is the stronger notion, and extends results on manifolds nontrivially to those modelled on locally convex spaces. In the convenient setting you can have functions that are smooth without even being continuous, IIRC! It essentially redefines the topology to make things "just work", which is fine, but it's very much a different approach.

Convenient calculus and Bastiani calculus agree up to Fréchet spaces, from memory, not just Banach.

[David Michael Roberts]

Note that Wikipedia says of convenient vector spaces:

The corresponding calculus of smooth mappings is called convenient calculus. It is weaker than any other reasonable notion of differentiability, it is easy to apply, but there are smooth mappings which are not continuous. This type of calculus alone is not useful in solving equations.

[Michael Rothgang]

Sébastien Gouëzel said:

A comment on submanifolds: it is hard to get this right from a design point of view, and that's why we don't have them already in mathlib. Basic use cases that should absolutely be covered are smooth submanifolds (e.g. the circle in the plane), but also smooth submanifolds with boundary (e.g., the closed disk in the plane) as these are crucial for Stokes formula.

Here is a possible design sketch. Let I be a model with corners (between H and E) and I' another model with corners (between H' and I'). Let J = J (I, I') be some class to be specified, registering an embedding of the model I' in the model I (think a subspace in a space, or a half-space in a whole space). Then consider M which is a smooth manifold with corner with respect to I, and N : Set M which is itself a smooth manifold with corners with respect to I'. Then N is a submanifold for J if it satisfies some properties, also to be specified.

The properties should be strong enough to entail a few basic properties. Like

• M is a submanifold of itself, for some trivial J (basically the identity)
• open sets of M are submanifold, for the same trivial J
• the inclusion of N in M is smooth
• Given another manifold P, a function f : P -> N is smoooth if and only if the composition with the inclusion is smooth as a function from P to M.

And one should have constructors, like: if N is a subset of a manifold M, which is locally given by level lines of a smooth function with onto derivative, then N inherits a charted space structure (with respect to some suitable H'), and a smooth manifold structure, (with respect to some suitable I') and for this smooth structure it is a submanifold (for a suitably defined J).

Finally, the circle and the closed disk should be submanifolds of the plane.

I have been thinking about submanifolds in the past weeks (on and off, and a bit more in the past days). This post has been helpful, but I am wondering about the details.

• I have a definition of immersions and smooth embeddings (which might need tweaking for manifolds with boundary, but the boundaryless case works well)
• I also have a candidate for the class J=J(I, I') above (let me call it SliceModel), which looks reasonable and satisfies many good properties.

However, I'm not sure if/how that is actually helpful for showing submanifold properties. That will not just depend on a SliceModel instance. At least, the statement "if M is a manifold over I, M' is a manifold over I' and there is a SliceModel I I' instance, then M is a submanifold of M'" is false, for important reasons. If $f: M\to M'$ is a smooth map and a topological embedding, it need not be a smooth embedding --- mere properties of their models with corners don't suffice to construct slice charts, we also need some properties of f.

Here is my standard online reference for a counterexample, if a smooth map which is an embedding, but not a smooth embedding --- and whose image is not an embedded submanifold. More specifically, that answer constructs a smooth map $f:(0,2)\to \mathbb{R}^2$ which is an embedding, but not an immersions. The associated models with corners are slice models, and e.g. $t\mapsto (t,0)$ is a smooth embedding.

[Michael Rothgang]

@Sébastien Gouëzel Do you remember what you meant with your comment? Perhaps this is merely a lost in translation moment.

[Sébastien Gouëzel]

I wrote "Then N is a submanifold for J if it satisfies some properties, also to be specified." Sure, being a submanifold would require additional properties, in addition to being an I'-manifold.

[Michael Rothgang]

(I have an idea for what these properties could be. Hopefully I can write/flesh these out soon.)