## Stream: sphere eversion

### Topic: Smooth extensions

#### Patrick Massot (Feb 19 2022 at 21:53):

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 (Feb 19 2022 at 21:53):

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

#### Patrick Massot (Feb 19 2022 at 21:56):

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 (Feb 19 2022 at 21:57):

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 (Feb 19 2022 at 21:58):

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 (Feb 20 2022 at 21:34):

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 (Feb 20 2022 at 21:38):

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 (Feb 20 2022 at 22:31):

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 (Feb 21 2022 at 12:16):

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 (Feb 21 2022 at 15:01):

@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 (Feb 21 2022 at 15:03):

OK, thanks for the notice.

#### Oliver Nash (Feb 21 2022 at 15:04):

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

#### Floris van Doorn (Feb 21 2022 at 15:17):

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 (Feb 21 2022 at 15:22):

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 (Feb 21 2022 at 15:23):

The reparametrization lemma has U=univ

#### Floris van Doorn (Feb 21 2022 at 15:40):

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

#### Patrick Massot (Feb 21 2022 at 20:06):

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 (Feb 21 2022 at 21:05):

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 (Feb 22 2022 at 10:07):

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

#### Oliver Nash (Feb 22 2022 at 10:30):

Is there a missing file?

#### Oliver Nash (Feb 22 2022 at 10:30):

import notations failing.

Last updated: Dec 20 2023 at 11:08 UTC