Smooth extensions

Stream: sphere eversion

[Patrick Massot]

Recently I've been wondering whether we should try to make everything in Chapter 1 smooth on the whole space to simplify things in Chapter 2. We already know we need things to be defined on a neighborhood of the closure of the open sets we really care about. What I currently think is that we should prove the data in Proposition 1.3 smoothly extend to the whole space. Of course this isn't quite true in this context, $β$ and $g$ could go to infinity near infinity in $U$. But we can pick any closed set $C$ contained in $U$ and find new $g$, $β$ and $Ω$ that are defined everywhere and coincide with the old ones on $C$.

[Patrick Massot]

There is a relevant discussion in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Bump.20functions.

[Patrick Massot]

The idea is to multiply $β$ and $g$ by a function which is one near $C$ and has compact support in $U$, and replace $Ω_x$ by the whole $F$ outside $C$. The new $U$ we actually care about would be the interior of $C$.

[Patrick Massot]

Recall that in real life those $U$ sets come from charts of a manifold and we can definitely assume they are relatively compact in images of larger charts still covering the manifold.

[Patrick Massot]

I'll try to find time this week to make sure this all work on paper and update the blueprint. But anyone should feel free to do it first.

[Patrick Massot]

I thought a bit more about this and actually we won't even have to extend anything if the manifold library is usable enough.

[Patrick Massot]

This will answer a question I've had since the very beginning of manifolds in Lean. What mathlib calls manifolds are manifolds equipped with a preferred atlas. Now we'll learn whether equivalent atlas can indeed be manipulated easily. @Sebastien Gouezel we'll need to tell Lean that every manifold without boundary has an atlas where all charts take value into the whole model vector space and the preimages of the unit ball in the model space cover the manifold. And we'll need Lean to be happy to use only such an atlas instead of whatever came with the original "manifold with a prefered atlas, known as manifold in mathlib". Any advice is welcome.

[Sebastien Gouezel]

You can definitely prove that any manifold is diffeomorphic to a manifold whose atlas satisfies the property you want. But I am not sure it is the way to go: the atlas is only some data useful to get the right notion of smoothness, but it's not something you have to use in your proofs once the notion of smoothness is here. For instance, you could prove that there exists a family of local diffeomorphisms with the properties you mention, with domains covering the manifold, and this should probably be enough for all your proofs without touching the atlas at all.

[Patrick Massot]

If you don't want to use the word "atlas" for a family of local diffeomorphisms whose domains cover the manifold and whose targets are the model space then I'll be happy not to use it (although it will sound a bit silly). The question is whether this family will be easy to use. I guess we'll see when trying.

[Patrick Massot]

@Oliver Nash and @Floris van Doorn I confirm that I'll get rid of U in Chapters 1 and 2, using the existence of nice atlases in Chapter 3. I'm sorry I underestimated how painful it would be to handle U. I thought about how to handle it from a Lean point of view, but it created mathematical complications that I didn't anticipate.

[Oliver Nash]

OK, thanks for the notice.

[Oliver Nash]

I spent all morning reviewing PRs but I'm back working on reparameterisation lemma now.

[Floris van Doorn]

I might be misunderstanding, but we're only changing that the functions are continuous/smooth everywhere instead of just on U, right? That's what we were already doing in the formalization.

[Patrick Massot]

Floris van Doorn said:

I might be misunderstanding, but we're only changing that the functions are continuous/smooth everywhere instead of just on U, right? That's what we were already doing in the formalization.

I mean U=univ in the main proposition of chapter 1. Of course there are still lemmas where open sets appear.

[Patrick Massot]

The reparametrization lemma has U=univ

[Floris van Doorn]

Oh, I see. Yeah, that will probably simplify some things.

[Patrick Massot]

I updated the blueprint. I hope Chapter 1 and 2 are now using the whole E wherever possible. I'll now update Lean code.

[Patrick Massot]

I propagated the change to reparametrization.lean and the files in the local folder. @Floris van Doorn I commented out your WIP version of exists_loop because I wasn't 100% sure how to fix it.

[Floris van Doorn]

Sounds good! I'll take a look at it.

[Oliver Nash]

Is there a missing file?

[Oliver Nash]

import notations failing.