Zulip Chat Archive

Stream: sphere eversion

Topic: Lemma 3.6

Yury G. Kudryashov (Jul 18 2022 at 12:05):

Mathlib branch#YK-sep-L36 has a proof of Lemma 3.6 (assuming is_closed instead of is_compact), both continuous and smooth versions. I've started opening PRs with supporting lemmas, see #15446, #15483, #15484, #15485, #15490 (depends on #15484).

Yury G. Kudryashov (Jul 18 2022 at 12:23):

Now I know how to get my PR merged in 1 day: I just need to prove something in the sphere eversion project using this PR ;)

Yury G. Kudryashov (Jul 18 2022 at 12:24):

@Sebastien Gouezel Thanks a lot for such prompt reviews/merges!

Sebastien Gouezel (Jul 18 2022 at 12:29):

Well, short self-contained PRs are always easy to review. And I have to admit I am not trying to follow the queue any more, since there are too many open PRs there, so a ping on Zulip is always a good idea.

Do you know if there is a way to have a personalized queue, for instance showing all the PRs in the queue whose title contains "proba" or "analysis" or "geometry" or "measure"? I think it would be a dramatic help to me.

Yaël Dillies (Jul 18 2022 at 12:29):

https://github.com/leanprover-community/mathlib/pulls?q=is%3Aopen+label%3Aawaiting-review+sort%3Aupdated-asc+-label%3Ablocked-by-other-PR+-label%3Amerge-conflict+-status%3Afailure+probability+ ?

Yaël Dillies (Jul 18 2022 at 12:30):

Or are you also looking for a OR combinator?

Sebastien Gouezel (Jul 18 2022 at 12:31):

Yes, I am looking for the OR version.

Sebastien Gouezel (Jul 18 2022 at 12:32):

But still your version just showed me three PRs that had gone under my radar!

Yaël Dillies (Jul 18 2022 at 12:32):

Hopefully the information is somewhere on here: https://docs.github.com/en/search-github/searching-on-github/searching-issues-and-pull-requests

Yury G. Kudryashov (Jul 18 2022 at 12:32):

You can have several bookmarks in a drop-down menu in the toolbar (if you're using a bookmark toolbar)

Sebastien Gouezel (Jul 18 2022 at 13:07):

Looks like this is not possible currently to have a global OR search, if I understand https://github.com/orgs/github-community/discussions/4507 correctly (only in label fields is there an OR combinator). If we added tags such as measure_theory, or algebra, or whatever, then this would become possible.

Yaël Dillies (Jul 18 2022 at 13:09):

What about projects? I've been putting all my recent combi work in the Graph Theory & Combinatorics project.

Alex J. Best (Jul 18 2022 at 13:20):

Yeah we could have a bot that tags PRs with the labels picked from the top level directories in the title too so that feat(topology/algebra, measure/basic): some stuff gets the topology and measure labels, this would be very handy I think

Moritz Doll (Jul 18 2022 at 13:25):

I think we should move this discussion to general.

Patrick Massot (Jul 19 2022 at 02:49):

@Yury G. Kudryashov when using partition of unity, feel free to also take stuff from https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/partition.lean and https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/partition2.lean

Patrick Massot (Jul 19 2022 at 02:49):

These files are stuff we should PR to mathlib in any case

Yury G. Kudryashov (Jul 19 2022 at 02:49):

I'm afraid that I duplicated some proofs from these files.

Patrick Massot (Jul 19 2022 at 02:50):

I'm sorry, it's my fault, I should have told you on Friday

Yury G. Kudryashov (Jul 19 2022 at 02:51):

At least, I already have a complete proof.

Patrick Massot (Jul 19 2022 at 02:51):

That's great!

Yury G. Kudryashov (Jul 19 2022 at 03:06):

I'm going to PR the rest in the morning.

Yury G. Kudryashov (Jul 21 2022 at 01:23):

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.

Patrick Massot (Jul 21 2022 at 01:52):

Thanks!

Yury G. Kudryashov (Jul 21 2022 at 02:06):

What's next?

Patrick Massot (Jul 21 2022 at 02:12):

Since @Heather Macbeth already claimed Lemma 3.2 I think Section 3.1.1 is done. I think everything else depends on jet bundles so we'll need an update from @Floris van Doorn to know what are good targets.

Yury G. Kudryashov (Jul 21 2022 at 02:16):

Jets look like something we want to have in mathlib.

Patrick Massot (Jul 21 2022 at 02:17):

Sure, it's in the for_mathlib folder

Patrick Massot (Jul 21 2022 at 02:18):

Although you could argue that mathlib wants higher order jets, but I think we can live the first order jet spaces for a while.

Patrick Massot (Jul 21 2022 at 02:19):

Patrick Massot said:

Sure, it's in the for_mathlib folder

Actually I'm lying, it's not all there.

Floris van Doorn (Jul 21 2022 at 10:13):

I've defined the jet bundle, and shown that j1fj^1f is smooth if ff is. I've been PRing stuff to mathlib in the last few days, but I am now continuing with Definition 3.20 and Lemma 3.21.

Floris van Doorn (Jul 21 2022 at 10:15):

I'm not sure that this development of 1-jet spaces is mathlib-worthy. Some for the definition of pullback/hom of smooth vector bundles I defined. They all use the hacky basic_smooth_vector_bundle_core (which - for the case of pullbacks - is not very pretty)

Floris van Doorn (Jul 21 2022 at 12:02):

Whenever the blueprint says "embedding" (like in Definition 3.20), is it sufficient to do it for open embeddings, or do we also need it for non-open embeddings?

Patrick Massot (Jul 21 2022 at 12:40):

It means open embeddings.

Patrick Massot (Jul 21 2022 at 12:42):

Yury, it would be nice to do Lemma 3.23 but it requires reading a bit more from the blueprint to get the definitions. Also the proof is not in the blueprint but it is meant to be easy.

Yury G. Kudryashov (Jul 22 2022 at 01:03):

Do we have all definitions for L 3.23?

Patrick Massot (Jul 22 2022 at 01:05):

I think so, except for the local definitions of the preceding paragraph.

Patrick Massot (Jul 22 2022 at 01:05):

You should find definitions in global/relation

Last updated: Dec 20 2023 at 11:08 UTC