Topic: Manifold constructors
Heather Macbeth (Jun 16 2020 at 10:47):
TLDR: Does mathlib need a constructor for manifolds which allows the model space to vary?
Suppose I have a submersion 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 , respectively. Since is a submersion, I can identify it locally near a point a with a map
for which , the strict derivative of at , has range .
By Yury's "complemented subspaces" version of the implicit function theorem, there exists a local diffeomorphism (homeomorphism currently, but that will improve)
such that is the projection onto .
So the model space for my submanifold will be , in a region of . But this will vary from point to point. In finite dimension, these kernels all have dimension , and so are isomorphic. This isomorphism allows one to equip the level set with a manifold structure with model space .
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 (Jun 16 2020 at 11:06):
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 (Jun 16 2020 at 11:07):
This makes sense. Thanks!
Last updated: May 12 2021 at 07:17 UTC