Manifold constructors

Stream: maths

[Heather Macbeth]

TLDR: Does mathlib need a constructor for manifolds which allows the model space to vary?

Suppose I have a submersion $f : M \to M'$ between manifolds, and wanted to put a (sub)manifold structure on one of its level sets.

Let me skip boundary/corners considerations, so my model spaces are normed spaces $E$, $E'$ respectively. Since $f$ is a submersion, I can identify it locally near a point a with a map
$f : E \to E'$,
for which $df|_a$, the strict derivative of $f$ at $a$, has range $E'$.

By Yury's "complemented subspaces" version of the implicit function theorem, there exists a local diffeomorphism (homeomorphism currently, but that will improve)
$\varphi : E' \times \ker(df|_a) \to E$,
such that $f \circ \varphi$ is the projection onto $E'$.

So the model space for my submanifold will be $\ker(df|_a)$, in a region of $a$. But this will vary from point to point. In finite dimension, these kernels all have dimension $k := \dim(M)-\dim(M')$, and so are isomorphic. This isomorphism allows one to equip the level set with a manifold structure with model space $\mathbb{R}^k$.

In infinite dimension, over a connected component of the level set, I believe these kernels will again all be isomorphic, since the differential of a transition function between overlapping charts gives an equivalence of normed spaces. But I don't see how one could prove this directly (without already doing most of the work to show that the connected component is a manifold). Instead, one could have a constructor for smooth manifolds, which has a different model space for each element of the atlas, and has the further conditions that (1) the transition functions are smooth, and (2) the underlying space is connected.

[Sebastien Gouezel]

In some books, manifolds are defined by allowing charts to take values in different vector spaces (i.e., the vector space is allowed to depend on the chart). I considered defining manifolds like this, but it seemed like opening a can of worm (in terms of dependent types and of type classes), so instead I went for a fixed model space.

Having a constructor as you mention is absolutely a good idea, but it has the drawback of requiring the connectedness. My plan was more to concentrate on finite dimension, though, where this issue is not present.

[Heather Macbeth]

This makes sense. Thanks!