Chapter 3 coordination

Stream: sphere eversion

[Patrick Massot]

We are ready to start working on Chapter 3. This is the chapter where all the manifold theory is concentrated. On paper in the real world this chapter would be three lines long, saying the local proofs obviously globalize (I'm lying a bit because there is also half a page about getting parametricity for free). But mathlib lacks a lot of infrastructure about vector bundles.

[Patrick Massot]

Discussions with Sébastien and Heather gives the following first targets:

• topological vector bundle of continuous linear maps from one topological vector bundle to another.
• pull-back bundles
• induced has_groupoid structure on a topological vector bundle over a base which has_groupoid

[Patrick Massot]

The first two points are not there even for topological vector bundles over topological spaces. Then the third point is needed to get smooth structures everywhere.

[Patrick Massot]

Once these are done, we'll need to upgrade the tangent bundle to a smooth vector bundle, and then define $J^1(M, N)$ for smooth manifolds $M$ and $N$.

[Patrick Massot]

An independent goal is:

• prove existence of nice atlases as discussed in https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Smooth.20extensions

[Patrick Massot]

Anyone who wants to tackle one of those four accessible points is very welcome to say it here.

[Heather Macbeth]

Patrick Massot said:

Discussions with Sébastien and Heather gives the following first targets:

• topological vector bundle of continuous linear maps from one topological vector bundle to another.

I think this one, in particular, should develop quite similarly to the corresponding construction for the direct sum of two vector bundles, which I have nearly finished: branch#vb-direct-sum

[Heather Macbeth]

So that can serve as a model (or I myself can do that, after I finish the direct sum).

[Patrick Massot]

I have another independent target to add:

• Define the homotopy of maps underlying the formal sphere eversion. This is the family $j_t$ of the beginning of the proof of https://leanprover-community.github.io/sphere-eversion/blueprint/chap-global.html#thm:sphere_eversion

[Heather Macbeth]

Patrick Massot said:

• induced has_groupoid structure on a topological vector bundle over a base which has_groupoid

For this one, it's first necessarily to define the correct groupoid. Given a structure groupoid G over a model space H, you want to define the groupoid of local homeomorphisms of F \times H whose sources and targets contain only full fibres of F, and which are linear in each fibre, and which cover G.

[Oliver Nash]

Yesterday I returned to working on Sphere Eversion after a break and I would be grateful for help clarifying:

• Who is working on what
• What has been done so far, in particular I am not clear on the status of each the following:
  • Lemma 3.2
  • Lemma 3.6
  • Lemma 3.10
  • Lemma 3.21
  • Lemma 3.23

I note that:
@Patrick Massot said:

Heather Macbeth already claimed Lemma 3.2

https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Lemma.203.2E6/near/290324201

@Yury G. Kudryashov said:

I'm behind the schedule on Lemma 3.6 (waiting for CI on #15490 to merge it and PR the actual proof)

In the meantime, here is Lemma 3.10: #15580

Do we have all definitions for L 3.23?

https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Lemma.203.2E6/near/290321458
https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Lemma.203.2E6/near/290453258

@Floris van Doorn said:

I am now continuing with Definition 3.20 and Lemma 3.21

https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Lemma.203.2E6/near/290357122

[Oliver Nash]

It seems to me that the Blueprint should be updated since:

• #15580 seems to be a proof of Lemma 3.10
• Earlier this morning I updated the Blueprint with a simpler proof of nice_atlas
• I just pushed https://github.com/leanprover-community/sphere-eversion/commit/730f134f41eff363e0250db7cc1e3895707442b5 to fix a dependency error
• We may have proofs of some of the other lemmas mentioned above

[Oliver Nash]

Finally I would be very grateful if we could permanently fix the issue with the stale dependency graph. I swear the URL has changed more than once. We have both: bad link and good link.

[Oliver Nash]

cc also @Heather Macbeth

[Floris van Doorn]

I restarted to work on Lemma 3.21 again today. It's mostly done, I think.

[Floris van Doorn]

The dependency graph issue is the reason I'm not updating the blueprint myself anymore: my installation generates the dependency graph at the bad link...

[Floris van Doorn]

There is one more thing that needs to be fixed in the dependency graph: I removed the edge from one_jet_extension_prop to holonomic_section, but one_jet_extension_prop needs an edge to some other vertex.

[Patrick Massot]

I agree that clarification is much needed.
Oliver Nash said:

Patrick Massot said:

Heather Macbeth already claimed Lemma 3.2

https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Lemma.203.2E6/near/290324201

I think Heather unclaimed this to work on constructing the family of formal immersions used in the actual sphere eversion case.

[Patrick Massot]

I'm confused about Lemma 3.6. I thought that Yury did it but I'm not 100% sure

[Oliver Nash]

IIUC he had a proof but may not have PR'd it as he waited for some other work to get merged in Mathlib.

[Patrick Massot]

Regarding the blueprint, I know it's currently a mess. In providence I tried to update it but couldn't build on my laptop. I'll try again (but I'm still on my laptop)

[Oliver Nash]

Thanks. If it helps, that revolting commutative diagram is now gone!

[Oliver Nash]

There's no emergency btw and it might not be the best use of your time to do it from your laptop. I just wanted a bit more clarity on where we stand.

[Patrick Massot]

I can explain the dep_graph url issue. The problem is that the blueprint in this project isn't built in CI, it is built locally and pushed to the repository. Hence anyone who has an outdate leanblueprint plugin for plastex will generate the dep graph in the old way. The reason why there is an old way and a new way it that LTE became too big to have a single dep graph and I arranged that each part of a blueprint can have a dep graph.

[Oliver Nash]

Sounds like it's Johan's fault then ;-)

[Johan Commelin]

I'll buy you a beer next time we meet, if that helps...

[Floris van Doorn]

I finished and pushed Lemma 3.21

[Floris van Doorn]

Shall I take a look at Lemma 3.26 next?

[Patrick Massot]

Yes, that would be great.

[Patrick Massot]

Note that the numbering was shifted because I removed an intermediate lemma.

[Patrick Massot]

Patrick Massot said:

I'm confused about Lemma 3.6. I thought that Yury did it but I'm not 100% sure

I managed to find it, Yury indeed did it in #15609.

[Patrick Massot]

Let me try to summarize the current status, knowing that some numbering changed today:

• Properties of updating is currently not claimed by anyone. The definition of smooth open embedding is already there in src/global/smooth_embedding.lean and the required proof is all topology, not differential geometry.
• Existence of a nice atlas is claimed by Oliver and almost done
• The parametricity lemma is available. Yury asked whether definitions are there but I don't think he did anything.
• The localization of a ample relation is ample is claimed by Floris.

[Oliver Nash]

Thanks, this is really helpful!

[Floris van Doorn]

lem:ample_iff_loc turned out to be easy. I'll take a look at the parametricity lemma next.

[Oliver Nash]

I've finished various other non-Sphere-Eversion bits and pieces so while I'm waiting for #15980 to land in Mathlib I'm going to start on lem:updating this morning.

[Oliver Nash]

Today I pushed proofs of lem:nice_atlas and lem:updating (after adding the definition def:update yesterday).

[Oliver Nash]

I also changed the informal statement of lem:updating in the blueprint slightly (the main point being that I dropped the second compact set L from the input since it did nothing).

[Patrick Massot]

Amazing, thank you very much!

[Johan Commelin]

Cool! Looks like you're now rapidly converging!

[Oliver Nash]

I'll start work on lem:localisation_stability later this morning.

[Oliver Nash]

Happily lem:localisation_stability turned out to be trivial: now done!

[Oliver Nash]

I did have to tweak the def:localisation_data and lem:ex_localisation but I think all correct now.

[Johan Commelin]

So what is even left?

[Johan Commelin]

It sounds to me like half of the non-green things at https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph_document.html are actually green already?

[Oliver Nash]

I think that there are five nodes (four lemmas and a definition) which would turn green if we updated the dependency graph now. I believe the following is what remains:

1. lem:param_trick [I think Floris has claimed this]
2. lem:param_for_free
3. lem:ample_parameter
4. lem:improve_htpy_loc
5. lem:open_ample_immersion
6. thm:open_ample
7. thm:sphere_eversion

[Patrick Massot]

A lot of the lemmas that remained were indeed meant to be easy (including lem:localisation_stability), but they still require some work and it's very nice to have them done. And lem:updating still had some content.

[Patrick Massot]

There are also sorries in the project currently, and I don't really know what is their status.

[Oliver Nash]

Yeah I picked off a few easy ones. I'm going to take a day or so to do a little Mathlib work. When I resume on this project, I'll start by surveying the sorrys not captured in the dependency graph.

[Patrick Massot]

I'm very happy this is moving. I still think we can finish before the end of summer.

[Oliver Nash]

We can definitely finish soon. When does the Summer end?

[Patrick Massot]

I'll answer this question when we'll be done

[Oliver Nash]

Patrick Massot said:

There are also sorries in the project currently, and I don't really know what is their status.

I looked over these earlier today. Excluding sorrys in the unused folder we currently have the following sorry counts:

src/to_mathlib/analysis/normed_space/operator_norm.lean:1
src/to_mathlib/geometry/manifold/misc_manifold.lean:1
src/global/relation.lean:8
src/global/one_jet_sec.lean:1
src/global/one_jet_bundle.lean:4
src/global/immersion.lean:5
src/global/gromov.lean:2

Some will definitely not be needed and for others there is some uncertainty about whether they will ultimately be needed. Also at least three are already captured in our dependency graph.

[Oliver Nash]

After this I convinced myself that the best thing I could do would be to start work on the lemma lem:improve_htpy_loc so I have just pushed a commit adding its formal statement.

[Oliver Nash]

I fixed an apparent typo in the Blueprint as part of that commit. The statement of this lemma is quite complicated so hopefully I got it right. I'll start working on the proof later this afternoon so I suppose I'll find out as I work on that over the next day or two.

[Oliver Nash]

I think the easiest remaining node in the dependency graph might be lem:open_ample_immersion if anyone is interested in a target.

[Patrick Massot]

Thank you very much Oliver. I'm sorry I see this so late.

[Patrick Massot]

The story of lem:improve_htpy_loc is that I thought that Chapter 2 was finished but then when I tried to add LaTeX details in Chapter 3 I realized what I wrote in Chapter 2 was not strong enough. So if you aren't too far into that lemma it would probably make more sense to postpone proving it until we make sure we can actually use it in the main theorem.

[Oliver Nash]

OK no problem! I'll pick something else tomorrow morning.

[Patrick Massot]

Picking the main theorem would be nice for instance :wink:

[Oliver Nash]

Indeed! Let's see.

[Oliver Nash]

I started working on lem:open_ample_immersion this morning. I hope to finish later today.

[Oliver Nash]

If anyone is looking for a useful self-contained lemma then I think closing this sorry would make a good target. It is the statement that the immersion relation for smooth maps between manifolds is open.

[Oliver Nash]

(It's just a globalisation of the fact that the set of injective maps is open in the space of linear maps $Hom(E, F)$.)

[Patrick Massot]

Thanks Oliver. Here is a global update:

• Oliver is working on lem:open_ample_immersion
• Floris will soon state a more general version of Gromov theorem than what is currently in the Lean code base. He needs to include the relative version and C⁰-close version
• Floris will work on parametricity for free (this is a set of three nodes in the graph: param_trick, param_for_free and ample_parameter)
• Patrick will sorry the homotopy of formal immersions for sphere eversion, waiting to hear from Heather's rotations and deduce existence of sphere eversion from the statement of Gromov's theorem
• Nobody should work on proving improve_htpy_loc until we made sure it's enough to prove Gromov's theorem
• Gromov's theorem isn't assigned yet, but note that is can be cut in half: use parametricity for free to get rid of parameters and do the actual work.

[Oliver Nash]

I just pushed a proof of lem:open_ample_immersion. In fact, following a suggestion from the blueprint, I really just took the existing proof of lem:open_ample_immersion_loc, split it up a bit and used that. I then also removed lem:open_ample_immersion_loc entirely.

[Patrick Massot]

I just bumped mathlib.

[Oliver Nash]

Today I'm going to work on proving that the (global) immersion relation is open. (We have that it is ample as of yesterday.)

[Patrick Massot]

Very good.

[Patrick Massot]

I'm working in global/immersion.lean right now.

[Johan Commelin]

Is it worth it to regenerate the dependency graph for enthusiastic onlookers like me?

[Oliver Nash]

Sadly it's basically up to date.

[Patrick Massot]

The graph is up to date

[Patrick Massot]

You're confused because Oliver wrote yesterday he proved lem:open_ample_immersion but that was a typo, he proved half of it (the non-trivial half on paper).

[Johan Commelin]

Aha

[Oliver Nash]

That's right. I'm just about to push a commit which will clarify this.

[Patrick Massot]

Actually I can't proceed further until Floris pushes his fix to Gromov's theorem statement.

[Patrick Massot]

So I'll wait for Oliver's push then push my thing in the same file and do something else until Floris pushes

[Oliver Nash]

I should push in about nine minutes. Just waiting on a build after pulling the Mathlib bump.

[Oliver Nash]

OK the build was slow but I have now pushed.

[Patrick Massot]

That was expected, the bump changed files very low in the project hierarchy because the main change was Yury replacing with_top Nat by enat everywhere in calculus.

[Patrick Massot]

I pushed a tiny commit and I'll wait for Floris now.

[Floris van Doorn]

I pushed the fix. Sorry for the delay.

[Patrick Massot]

No problem. I did some admin in the mean time.

[Patrick Massot]

@Floris van Doorn do we agree that you now work on parametricity for free?

[Floris van Doorn]

Yes, I'm working on that and param trick now!

[Patrick Massot]

Great!

[Patrick Massot]

Can I propose that we try to use variable names indicating their type? In places like https://github.com/leanprover-community/sphere-eversion/blob/master/src/global/relation.lean#L150 I find it confusing that we have three manifolds $M$, $P$ and $X$ and lots of ∀ (s : P) (x : M), especially the x : M when the next manifold is called X

[Floris van Doorn]

I understand.
It is a bit tricky to do this consistently, since we sometimes want the codomain manifold to be a topological_space and sometimes to be a metric_space, which means we probably want to use different letters for them.
I have been trying (since yesterday) to use s, t and x for the variable names following the conventions in chapters 1 & 2:

• x is an element in the (domain) space we're considering
• s is a parameter
• t is the variable indicating how far you are along a homotopy

Would you be happy/happier if I replace X by M'' or M₂?

[Patrick Massot]

I never claimed the blueprint was consistent :wink:

[Patrick Massot]

In fact it would be even better to make the union of blueprint and Lean code consistent.

[Patrick Massot]

@Floris van Doorn could you push as soon as you have definitions and statements for the parametricity related stuff? It would allow me to start working on Gromov's theorem.

[Floris van Doorn]

What definitions do you need? $\Psi$ is bundle_snd, the section $\overline F$ is F.uncurry (where F is a family_one_jet_sec) and $\mathcal{R}^P$ is R.relativize IP P

[Floris van Doorn]

Feel free to rename any of these definitions

[Patrick Massot]

I think we have enough definitions indeed. So we need statements.

[Floris van Doorn]

Those are also already there. See blueprint. (ample_parameter in the blueprint is rel_mfld.ample.relativize.)

[Patrick Massot]

I'm sorry, I've doing administration while waiting for answers instead of looking at the project code. I guess I no longer have any excuse to do administration instead of working on the project.

[Floris van Doorn]

I guess I haven't stated param_for_free yet. If you already need that, I can try to prioritize it.

[Patrick Massot]

Oh but the graph isn't updated. Stated stuff should have green outlines.

[Patrick Massot]

Yes, prioritizing stating param_for_free would be great

[Patrick Massot]

I'll try to update the graph in the mean time.

[Floris van Doorn]

You're right, I didn't update the graph yet. I'll prioritize it.

[Patrick Massot]

Compiling the blueprint reveals that param_for_free is stated as rel_mfld.relativize_satisfies_h_principle!

[Patrick Massot]

Actually the graph currently claims that everything is stated! Of course it doesn't mean we won't add 50 lemmas...

[Floris van Doorn]

Yes, I realized that I had already (tried) to state it. I accidentally stated it as an iff though, but I should have stated it as follows. I will push

/-- This might need some additional assumptions or other modifications. -/
lemma rel_mfld.satisfies_h_principle.satisfies_h_principle_with
  (R : rel_mfld I M IX X) (C₁ : set P) (C₂ : set M)
  (ε : M → ℝ) (h : (R.relativize IP P).satisfies_h_principle (C₁ ×ˢ C₂) (λ x, ε x.2)) :
  R.satisfies_h_principle_with IP C₁ C₂ ε :=
sorry

[Patrick Massot]

Working on Gromov's theorem will allow to test all those statements.

[Patrick Massot]

Tell me when you push and I'll recompile the blueprint

[Floris van Doorn]

currently compiling to check if I broke anything...

[Patrick Massot]

Damn, I think I messed up in 04cb6032f9. I asked Yury to prove a lemma from the blueprint and he proved something that looked simpler. It was the middle of my vacations so I didn't check and assumed my version was overcomplicated without a purpose. But now that I reading back the proof of Gromov's theorem I remember why my complicated version was needed.

[Patrick Massot]

The issue is that assumptions in Yury's version are too strong.

[Patrick Massot]

And I was too quickly to happily believe I overcomplicated things.

[Patrick Massot]

This shouldn't be too bad to fix.

[Floris van Doorn]

Oh, that is very unfortunate...

[Floris van Doorn]

I pushed, btw

[Johan Commelin]

Btw, in the current online version of the blueprint, I noticed that https://leanprover-community.github.io/sphere-eversion/blueprint/chap-global.html#def:convenient_indexing is disjoint from the rest of the graph.

[Patrick Massot]

That's very much related to the story I was just telling

[Patrick Massot]

I compiled the blueprint and pushed.

[Oliver Nash]

Did you compile against an unpushed commit? The lean links in the dependency graph reference 4a1d60ccffec5b40c83aadfc5f779fe74147997b which seems to be missing.

[Patrick Massot]

Oh, I see what happened :sad:

[Patrick Massot]

I'll fix it

[Oliver Nash]

Graph is looking good though!

[Patrick Massot]

TODO: find a way to hide the (is_closed_empty : is_closed (∅ : set empty)) I just added to the project.

[Patrick Massot]

@Floris van Doorn do you confirm we don't have:

lemma rel_mfld.is_open_relativize
  {E : Type u_1} {H : Type u_2} {M : Type u_3} {EP : Type u_7}
  {HP : Type u_8} {P : Type u_9} {EX : Type u_10} {HX : Type u_11}
  {X : Type u_12}
  [normed_add_comm_group E]
  [normed_space ℝ E]
  [topological_space H]
  {I : model_with_corners ℝ E H}
  [topological_space M]
  [charted_space H M]
  [smooth_manifold_with_corners I M]
  [normed_add_comm_group EP]
  [normed_space ℝ EP]
  [topological_space HP]
  {IP : model_with_corners ℝ EP HP}
  [topological_space P]
  [charted_space HP P]
  [smooth_manifold_with_corners IP P]
  [normed_add_comm_group EX]
  [normed_space ℝ EX]
  [topological_space HX]
  {IX : model_with_corners ℝ EX HX}
  [topological_space X]
  [charted_space HX X]
  [smooth_manifold_with_corners IX X]
  (R : rel_mfld I M IX X)
  (h2 : is_open R) :
  is_open (rel_mfld.relativize IP P R)

[Patrick Massot]

I pushed anyway, with this statement sorried.

[Floris van Doorn]

That is correct.
It would require continuity of bundle_snd, which shouldn't be too hard (but probably we should prove smoothness first).

[Floris van Doorn]

Feel free to add a bunch of sorry'd lemmas like that, they should be easy to knock down.

[Patrick Massot]

I can confirm that the properties stated for relativize (including the one I just wrote) are enough to deduce the parametric h-principle from the non-parametric one.

[Patrick Massot]

It's becoming harder to avoid confronting the last big proof. Luckily I need to go away for a little while (my family will return from vacations tonight and I need to prepare a bit).

[Patrick Massot]

Patrick Massot said:

TODO: find a way to hide the (is_closed_empty : is_closed (∅ : set empty)) I just added to the project.

This is hilarious. Sometimes Lean goes too far in allowing us to prove things without thinking. Lean was asking me to prove some subset of the parameter space was closed while deducing parametric Gromov from the non-parametric one. So I thought: there is no parameter here so this must be the empty set of the empty type. But actually this was the copy-paste typo that we noticed the other day in the statement but nobody fixed. So that closed set wasn't used at all and Lean would have been happy with any closed set in any topological space! And my vague semi-conscious rationalization wasn't even consistent: I should have written unit instead of empty since the non-parametric situation correspond to a parameter space which is unit, not empty...

[Oliver Nash]

Ha!

[Oliver Nash]

All is well anyway.

[Patrick Massot]

Now I need to find and kill anyone who saw that, in order to protect my academic reputation.

[Oliver Nash]

You just needed an initial object for any old category.

[Oliver Nash]

Your reputation is very safe IMHO.

[Patrick Massot]

My only consolation is that I saw the issue as soon as put begin/end for non-parametric Gromov and looked at the tactic state.

[Patrick Massot]

Speaking of tactic state, I can't wait for the magic tricks Lean 4 will use to turn

E: Type u_1
_inst_1: normed_add_comm_group E
_inst_2: normed_space ℝ E
H: Type u_2
_inst_3: topological_space H
I: model_with_corners ℝ E H
M: Type u_3
_inst_4: topological_space M
_inst_5: charted_space H M
_inst_6: smooth_manifold_with_corners I M

into

M : manifold

[Patrick Massot]

And now Lean seeks revenge and asks me to prove X is non-empty.

[Patrick Massot]

I'm pretty sure the blueprint version of std_localisation_data does not have any non-emptyness assumption, but I guess Lean may be right anyway.

[Oliver Nash]

This could be my fault. I did this for convenience.

[Patrick Massot]

@Oliver Nash could you have a look at global/localization_data.lean and figure out whether those nonempty assumptions are really needed? There are also several linting errors in that file.

[Patrick Massot]

I don't mind proving a preliminary lemma saying the $h$-principle holds for empty manifold (or additing that assumption everywhere if it doesn't, who knows?) but I'd rather avoid it if possible.

[Oliver Nash]

Our comments crossed. I'll take a look. I'm very close to turning an ellipse green though. Would you like me to look now?

[Patrick Massot]

There is no emergency, I can add the assumption to Gromov's theorem for now.

[Oliver Nash]

OK I'll take it up as soon as I've finished my goal. If that means excising it from the statement of Gromov's theorem, then I'll do that too.

[Patrick Massot]

I'm editing Gromov's theorem so please don't touch it yet. If you could simply investigate whether we can remove nonempty from the localisation file it would be great.

[Patrick Massot]

I also noticed that Gromov's theorem misses finite dimensionality assumptions. This didn't occur to me because manifold implies finite dimension in my mind.

[Oliver Nash]

I'm wrestling with some annoying linear algebra and I doubt I'll get to this nonempty M stuff for at least an hour.

[Patrick Massot]

No problem

[Patrick Massot]

I'm adding assumptions to the theorem for now

[Patrick Massot]

There are lots of assumptions to add anyway because all the localization stuff assume finite dimensional manifolds without boundary.

[Patrick Massot]

And this totally makes sense, this is the default meaning of manifold and this should be enough for us.

[Patrick Massot]

And of course the blueprint is totally inconsistent here.

[Oliver Nash]

Patrick Massot said:

You're confused because Oliver wrote yesterday he proved lem:open_ample_immersion but that was a typo, he proved half of it (the non-trivial half on paper).

lem:open_ample_immersion is now genuinely sorry-free.

[Oliver Nash]

I'm being called to dinner now. I'll tidy up the nonempty M issue this evening if I can find some time or else I'll take it up tomorrow morning.

[Patrick Massot]

Great!

[Floris van Doorn]

I just finished the lemma param_trick. By far the hardest part was showing that $\bar F$ is smooth.

[Floris van Doorn]

link: https://leanprover-community.github.io/sphere-eversion/blueprint/chap-global.html#lem:param_trick

[Patrick Massot]

Great!

[Patrick Massot]

It's very sad to read that obvious smoothness proofs are still so hard, but very good to have this lemma!

[Patrick Massot]

I'm currently fighting off-by-one discrepancies when piecing various lemmas together...

[Patrick Massot]

There is no problem at all but it's very time consuming and annoying

[Floris van Doorn]

The main problem was the library building part of it; I had to prove that the derivative (as a continuous linear map) of a smooth map between manifolds is smooth in the point where you take the derivative. And then I had to generalize that to partial derivatives. I think it makes more sense that it is hard if you have to do library building as a part of it.

[Floris van Doorn]

I also finished ample_parameter, so the 4 hour old blueprint is 3 lemmas behind :grinning_face_with_smiling_eyes:

[Patrick Massot]

Wonderful!

[Patrick Massot]

Are those 3 lemmas fully sorry-free or do they still depend on some library building sorries?

[Floris van Doorn]

The 2 lemmas I pushed are fully sorry-free, I checked with #print axioms.

[Patrick Massot]

Do you have a clear view of where the current sorries are used?

[Patrick Massot]

If some are not used then it would be nice to comment them out.

[Floris van Doorn]

I've tried to put a comment near most of my recent sorry's when I think we're likely not using them (and also replacing sorry by admit so we can count by word search). I can go over the sorry's tomorrow to see which ones we are likely not using.
I believe there are not much sorry's in the files I've been recently using.

[Floris van Doorn]

I think htpy_one_jet_sec.unlocalize in global/relation is yours? Will we need that?

[Patrick Massot]

About unlocalize, we should find out pretty soon

[Patrick Massot]

But clearly if it is useful then it will be at the very end.

[Patrick Massot]

What about one_jet_bundle_model_space_chart_at and one_jet_bundle_model_space_homeomorph?

[Patrick Massot]

They are probably stuff I wrote at the very beginning of Chapter 3 and maybe there are n longer relevant

[Patrick Massot]

As unlocalize, they were meant to use allow using Chapter 2 in Chapter 3.

[Floris van Doorn]

Yeah, I haven't touched them, and I don't to what extend we need those to glue chapter 2 to chapter 3.

[Patrick Massot]

Ok, let's wait.

[Patrick Massot]

In the mean time the graph got updated: https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph_document.html

[Patrick Massot]

It's starting to look good. Too bad nice_atlas went in the wrong direction.

[Patrick Massot]

I'm done for today. I just push https://github.com/leanprover-community/sphere-eversion/commit/e7e165e59b366466e620d5ad42c513664adb6712 which features actually starting the main big proof.

[Patrick Massot]

Things are going pretty smoothly so far, but it's always painful to have a local context with more than 60 items.

[Patrick Massot]

(at least there are only 23 numbered instances, which is way less than the maximum reached when deducing the parametric result from the unparametric one).

[Oliver Nash]

Wow, amazing progress! Congratulations @Floris van Doorn

[Oliver Nash]

I’ll fix nice_atlas tomorrow. It’s rather messy because I’ve pushed for the quickest way to cater for the two changes but there are absolutely no mathematical issues so I’m confident I can do it tomorrow.

[Patrick Massot]

I just pushed https://github.com/leanprover-community/sphere-eversion/commit/ba3ab0478213c8d20f3d4829dff54f61ac8217c5 to help handling the very large proof states at the end of the project.

[Johan Commelin]

Nice! Would have been useful in LTE as well :smiley:

[Patrick Massot]

This is a customized version of Ed's interactive_expr file from mathlib. It makes sure goals are printed before the local context so that you don't have to scroll to see the goal. And it adds options for permanent tactic state filtering (hacking the trace option framework as usual)

[Patrick Massot]

All this as been possible in Lean 3 forever, but people were too lazy to dive into this (admittedly rather intimidating) file.

[Patrick Massot]

Let me clarify: the big file I added in that commit is a file taken from mathlib with something like 15 added lines

[Yaël Dillies]

Filtering, as in this?

[Johan Commelin]

Those aren't persistent, for me.

[Patrick Massot]

Yaël, what you show isn't persistent.

[Yaël Dillies]

Ah, so it's being reset when you touch the file?

[Patrick Massot]

It's much worse, it's reset when you move to the next line of your proof.

[Yaël Dillies]

Patrick Massot said:

All this as been possible in Lean 3 forever, but people were too lazy to dive into this (admittedly rather intimidating) file.

Also, #15959 :stuck_out_tongue_closed_eyes:

[Yaël Dillies]

What I really want is being able to inspect error states. This would have been handy countless times.

[Patrick Massot]

Now I need to un-train my brain which is asking my right hand to go to the mouse scroll button every time I finish typing a line.

[Floris van Doorn]

Oh, the new tactic state view looks very useful!

[Floris van Doorn]

FYI: I'm currently reformulating satisfies_h_principle_with, I'm replacing the {C₁ : set P} {C₂ : set M} with a single set {C : set (P × M)}. The previous phrasing was pretty unnatural.

[Patrick Massot]

I guess I'll be able to adapt.

[Floris van Doorn]

I fixed all current proofs, which was trivial.

[Patrick Massot]

Did you push? This will surely create conflicts

[Floris van Doorn]

I just pushed

[Floris van Doorn]

I'm happy to resolve all conflicts if you push a compiling development to a branch (now or later).

[Patrick Massot]

I was talking nonsense, this doesn't affect at all the proof I'm working on since I'm working on the non-parametric case.

[Patrick Massot]

Sorry about the noise.

[Patrick Massot]

Does param_for_free still seem doable?

[Patrick Massot]

For casual observers, let me point out the blueprint proof of that lemma is "This obviously follows from lemma 3.22. "

[Floris van Doorn]

It's doable, but of course, Lemma 3.22 is only part of the work (though hopefully more than half of it).

[Floris van Doorn]

The extra work comes from transforming the homotopy on the product back to a homotopy with parameters.

[Patrick Massot]

Isn't that (un)curryfication?

[Floris van Doorn]

yeah

[Floris van Doorn]

but of course, if you have extra structure, (un)currying might be non-trivial. Lemma 3.22 is uncurrying, and now I have to curry back.

[Floris van Doorn]

@Patrick Massot: shall I change all equalities in rel_mfld.satisfies_h_principle and rel_mfld.satisfies_h_principle_with to equalities of elements in J¹(M, M') (instead of equalities of formal solutions / 1-jet sections)? That might simplify some things.

[Patrick Massot]

Indeed that will probably simplify things a bit.

[Floris van Doorn]

ok, I'll go ahead

[Floris van Doorn]

I pushed. For the non-parametric version only the first Prop-field changed.

[Patrick Massot]

Did you check the immersion file is still ok?

[Patrick Massot]

It seems ok

[Patrick Massot]

I just pushed after reaching what was my goal for this morning.

[Patrick Massot]

I did the last paragraph of the main theorem:

Now that the inductive construction is completed, we apply Lemma 3.9 to make sure our sequence $F_n$ is locally ultimately constant, hence it converges pointwise to a smooth homotopy relative to $A$ and ending at a holonomic section of $\mathcal{R}$.

which is slightly less than 100 lines in Lean.

[Patrick Massot]

But I had to make some change to what I assumed from the inductive construction. One change was clearly correcting a typo but another one has some content, I'll need to think a bit.

[Patrick Massot]

But I only have 12 minutes now so I'll rather remove a tiny sorry I just introduced.

[Patrick Massot]

Ok I proved it and added it to to_mathlib/topology/misc.lean which is now 644 lines long... :innocent:

[Floris van Doorn]

Note: docs#set.bUnion_mono exists.

[Floris van Doorn]

And I'm doing even worse: I have a few tiny topology lemmas currently polluting the relation file :see_no_evil:

[Patrick Massot]

Oh, I'm also polluting.

lemma univ_prod_inter_univ_prod {α β : Type*} {s t : set β} :
  (univ : set α) ×ˢ s ∩ (univ : set α) ×ˢ t = (univ : set α) ×ˢ (s ∩ t) :=
begin
  ext ⟨a, b⟩,
  simp
end

is really properly a part of differential topology.

[Floris van Doorn]

that checks out ^^

[Patrick Massot]

I pushed and I'll move to admin and then go back home. I don't know yet whether I'll have time for the project tonight.

[Oliver Nash]

Patrick Massot said:

Oliver Nash could you have a look at global/localization_data.lean and figure out whether those nonempty assumptions are really needed? There are also several linting errors in that file.

I finally had time to check this. Unfortunately these nonempty instances are necessary because index_type always has at least one element. Thus for example nice_atlas demands that there is at least one embedding of F into M but F always contains 0 and so is non-empty and thus M must be also.

[Oliver Nash]

The way to fix this would be to fix this deficiency in index_type but given that you have already suffered one round of off-by-one-ness pain for indexing, I doubt it's worth it for now.

[Johan Commelin]

How hard would it be to prove the main theorem assuming is_empty M? Can't be that hard, I hope?

[Patrick Massot]

Of course in the worse case scenario we can simply start the proof with a case disjunction according to whether M is empty or not, but it feels a bit silly.

[Patrick Massot]

Oliver Nash said:

The way to fix this would be to fix this deficiency in index_type but given that you have already suffered one round of off-by-one-ness pain for indexing, I doubt it's worth it for now.

Guess what? Today I suffered back and partly reverted yesterday's change of mind.

[Patrick Massot]

Life is so much easier on paper or blackboard.

[Patrick Massot]

Today had a lot more admin and off-by-one suffering than I hoped for, but I'm back to a stable situation (I just pushed). Now I hope the inductive construction is really setup.

[Patrick Massot]

I need to go back home now (and I'm too hungry to Lean anyway), but I'll have at least one more hour tonight.

[Johan Commelin]

It's only 18:20!!

[Patrick Massot]

I have 25 minutes biking and then I need to cook

[Floris van Doorn]

Today was a very long day... But I did finish param_for_free and updated the blueprint.
Now I also need to go home :-)

[Patrick Massot]

Great! Thank you very much for your perseverance!

[Patrick Massot]

Only three dependency graph nodes to go! One is @Heather Macbeth rotation project, one is chapter two coming back for an encore and the last one is Gromov's theorem for open ample relations (aka the whole project, but we are pretty close).

[Patrick Massot]

Nooooo, the definition of updating is also given in the restricted context of smooth_manifold_with_corners 𝓘(𝕜, EX) X

[Patrick Massot]

:cry:

[Patrick Massot]

We really need to put a huge warning in the docstring of docs#model_with_corners_self and the corresponding module docstring.

[Patrick Massot]

Ha Ha! Generalizing in math is so easy!

[Patrick Massot]

It even has some content, the new definition and its companion 40 lines long lemma now work with manifolds with boundaries and corners.

[Floris van Doorn]

I recommend Oliver to do more copy-pasting. Copy-pasting variable lists (or lemma statements) of similar situations is a good way to get the formulation of a particular concept right.
I expected that [smooth_manifold_with_corners 𝓘(𝕜, E)] would not occur in mathlib at all, but actually I am wrong: @Heather Macbeth uses [smooth_manifold_with_corners 𝓘(ℂ, E) M] once in file#geometry/manifold/complex, which likely should also be generalized.

[Oliver Nash]

I agree this is a good tip (which I will follow) and I did formalise the statement of nice_update_of_eq_outside_compact (which was fortunately easy to generalise) but in my defence, I did not formalise the original statement of nice_atlas.

[Oliver Nash]

Super job on param_for_free btw!

[Patrick Massot]

@Floris van Doorn this docstring is outdated, right?

[Oliver Nash]

I'm being told I must help with packing now. See you all in a week!

[Patrick Massot]

Have good vacations!

[Floris van Doorn]

@Oliver Nash That's fair; and if you copied/mimicked these variables from the nice_atlas formulation, then you cannot be faulted for that at all. Good vacations!

[Floris van Doorn]

Patrick Massot said:

Floris van Doorn this docstring is outdated, right?

Yes, that is correct

[Patrick Massot]

I'd like to make clear I wasn't "faulting" anyone :smile:

[Floris van Doorn]

(although mathematically it might still be correct, since 100% of a construction is still a part of a construction :smile: )

[Floris van Doorn]

I think you're missing a negation in your last message?

[Patrick Massot]

And the dependency graph makes it very clear that we were expecting impedance mismatch exactly here. This node has 10 in-going edges!

[Patrick Massot]

I pushed a commit that will create conflict so please pull. I split off parametricity for free from the relation file.

[Patrick Massot]

I reach the first point where I see rel_loc.jet_sec EM EX in the main proof!

[Patrick Massot]

This mean the central object of Chapter 2 is entering the main proof of Chapter 3.

[Patrick Massot]

However it seems that global/relation.lean misses a 1-parameter version of one_jet_sec.localize. I mean it seem we don't have htpy_one_jet_sec.localize (or, more to the point htpy_formal_sol.localize).

[Patrick Massot]

@Floris van Doorn in case you need a new project...

[Patrick Massot]

The funny thing is htpy_one_jet_sec.unlocalize is there.

[Patrick Massot]

I also bumped mathlib. It means we now have access to @Kyle Miller's awesome work on dot notation. This will allow to get rid of a lot of to_one_jet_section etc.

[Patrick Massot]

And I'm done for today.

[Floris van Doorn]

I proved 4 sorry's in localisation, 1 sorry in one-jet_bundle (smoothness of $\Psi$) and 1 in relation (smoothness of transfer $\psi_{g,h}$)

[Patrick Massot]

Great!

[Patrick Massot]

I've been besieged by students all day :sad:

[Patrick Massot]

I wrote some statements but the situation still isn't clarified

[Patrick Massot]

I'll try to work more tonight.

[Patrick Massot]

If you don't know what to do, I think we need tu upgrade transfer to a smooth open embedding.

[Floris van Doorn]

There's still a bunch of sorry's I can attack. I started looking into the computation of $J^1(V,V')$ when $V$ and $V'$ are vector spaces, and I will continue with that tomorrow.

[Floris van Doorn]

But I'll look into that after that, if you are (reasonably) certain that we will use it.

[Patrick Massot]

The story is that on paper I thought it was enough to discuss updating maps from $M$ to $N$ using embeddings $h : X \hookrightarrow M$ and $g : Y \hookrightarrow N$. The reasoning is that a section $F : V \to J^1(V, W)$ is a map from the manifold $V$ to the manifold $J^1(V, W)$ with some extra condition. But now I think this trick isn't usable in a formal context. We need a clean API around modifying sections of jet bundles. The thing is that $h : X \hookrightarrow M$ and $g : Y \hookrightarrow N$ give rise to $\psi : J^1(X, Y) \hookrightarrow J^1(M, N)$ (this is the transfer map) and we can use the updating API with the pair $(h, \psi)$ but this requires an API registering that sections becomes sections and a convenient smoothness condition.

[Patrick Massot]

I've started stating stuff, but many statement miss some side-conditions. At least in global/relation.lean I think all sorries that require additional conditions are clearly marked.