Zulip Chat Archive

Stream: maths

Topic: Manifold constructors

view this post on Zulip 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 f:MMf : 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 EE, EE' respectively. Since ff is a submersion, I can identify it locally near a point a with a map
f:EEf : E \to E',
for which dfadf|_a, the strict derivative of ff at aa, has range EE'.

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

So the model space for my submanifold will be ker(dfa)\ker(df|_a), in a region of aa. But this will vary from point to point. In finite dimension, these kernels all have dimension k:=dim(M)dim(M)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 Rk\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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Jun 16 2020 at 11:07):

This makes sense. Thanks!

Last updated: May 12 2021 at 07:17 UTC