Zulip Chat Archive

Stream: maths

Topic: topology


view this post on Zulip Reid Barton (Dec 13 2018 at 22:39):

Hi @Sebastien Gouezel, I was wondering whether you either have proved or were planning to prove Urysohn'slemma or the Tietze extension theorem.
I ask because I have an ugly, but working proof of the former lying around somewhere, and part of a proof of the latter, and it looks like your PR #464 is the main thing I would need to finish it off.

view this post on Zulip Sebastien Gouezel (Dec 14 2018 at 07:13):

No, I have not done it, and I don't plan to do it. You can go ahead if you want!

view this post on Zulip Reid Barton (Oct 07 2019 at 15:03):

So I started trying to write module documentation for topology but (perhaps predictably) I ended up doing another reorganization--hopefully less drastic than the one from March. It is still in progress, but I will be posting a few preliminary PRs.

view this post on Zulip Patrick Massot (Oct 07 2019 at 16:35):

Great!

view this post on Zulip Reid Barton (Oct 07 2019 at 16:46):

Currently, topology.constructions is a big grab-bag which I found difficult to document. For example, it doesn't actually contain any constructions themselves, but rather theorems about them, but sometimes those theorems are somewhere else.
So here's what I'm trying.

  • Move the definitions of product topology, etc. from near the end of topology.order to a new file (working name: topology.basic_constructions) which imports topology.order. Also move the most elementary facts about these constructions there (e.g., projections are continuous).
  • Import topology.basic_constructions in most other modules, in order to move proofs like "if SXS \subset X and TYT \subset Y are compact, then S×TS \times T is compact" to near the definition of compactness.
  • A few basic facts about products and so on (like is_open_prod_iff') use concepts (like is_open_map) which are defined in later files, so those will remain in topology.constructions (which should perhaps be renamed), which will end up a hopefully much smaller grab-bag.

view this post on Zulip Reid Barton (Oct 07 2019 at 16:46):

So far I implemented this for prod and not any of the other constructions, but it appears to be going well.

view this post on Zulip Reid Barton (Oct 07 2019 at 16:47):

@Patrick Massot, you likely tried something like this in the original refactoring; do you see any particular snags?

view this post on Zulip Reid Barton (Oct 07 2019 at 16:59):

I'm really tempted to rename all the space variables to X Y Z W first...

view this post on Zulip Reid Barton (Oct 07 2019 at 17:00):

since it will make this refactoring a lot easier

view this post on Zulip Johan Commelin (Oct 07 2019 at 17:01):

Go for it!

view this post on Zulip Patrick Massot (Oct 07 2019 at 17:25):

Reid, please feel free to reorganize things. I got tired during the previous refactor, and Johannes was pushing towards big files. But the current situation is far from perfect.

view this post on Zulip Johan Commelin (Oct 07 2019 at 18:22):

@Reid Barton One thing I wondered is whether embedding and dense_embedding etc should use old_structure_cmd.

view this post on Zulip Reid Barton (Oct 07 2019 at 18:22):

I also wondered about that

view this post on Zulip Reid Barton (Oct 07 2019 at 18:23):

but I'm trying to leave such changes for separate PRs

view this post on Zulip Johan Commelin (Oct 07 2019 at 18:24):

fair enough

view this post on Zulip Reid Barton (Oct 07 2019 at 18:28):

At the moment I'm just trying to get the right stuff total in each file, then after that each file can be fixed up nicely

view this post on Zulip Patrick Massot (Oct 07 2019 at 20:51):

@Reid Barton while your are refactoring topology, it would be nice to use the new localized notation feature. I think nhds deserves a notation. In the perfectoid project I always use local notation `𝓝` x:70 := nhds x

view this post on Zulip Patrick Massot (Oct 07 2019 at 20:52):

In top of the eye candy, the precedence allows to avoid many parentheses.

view this post on Zulip Reid Barton (Oct 12 2019 at 14:55):

This refactoring is now #1541.

view this post on Zulip Reid Barton (Oct 12 2019 at 15:05):

I ended up doing slightly less reordering of imports than planned, and pretty much every theorem ended up in a logical file, though possibly the ordering of imports is "overfit" to the particular set of theorems we have currently.

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:21):

@Reid Barton did you run sanity_check on all those files?

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:22):

Also, your new README is wonderful, but it should go to https://github.com/leanprover-community/mathlib/tree/master/docs/theories

view this post on Zulip Reid Barton (Oct 12 2019 at 15:22):

It's running currently

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:22):

I think

view this post on Zulip Mario Carneiro (Oct 12 2019 at 15:22):

is sanity_check in travis?

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:23):

Honestly, if such a PR builds and sanity_checks (and makes sense from a general point of view) then I don't see what I should review. Of course the next step is to make sure every file has a toplevel docstring and doc_blame, but that can be done later (super fast merging is crucial to such PRs).

view this post on Zulip Reid Barton (Oct 12 2019 at 15:24):

I'm also going to go through the same process I did for the linear algebra renaming PR to check that I didn't mess up any declarations

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:24):

Oh I see

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:25):

After a couple of uses like this, sharpening your tool, it would be nice to make it available.

view this post on Zulip Patrick Massot (Oct 12 2019 at 15:27):

Reid, could you please label your PR as WIP until your checks are done?

view this post on Zulip Reid Barton (Oct 12 2019 at 15:30):

Good idea, done

view this post on Zulip Reid Barton (Oct 12 2019 at 15:37):

Reid Barton did you run sanity_check on all those files?

sanity_check found a mistake in my #1516, but not this one. I'll fix it in an independent PR.

view this post on Zulip Reid Barton (Oct 12 2019 at 18:34):

(moving back here) I guess we can merge aside from the question about the README.md.
I thought of the file as saying "if you want to find X, look in file Y", rather than trying to list everything that exists in topology, although I guess it also accomplishes that as a side effect.

view this post on Zulip Patrick Massot (Oct 12 2019 at 18:35):

My point is we don't have any other files like that in that place.

view this post on Zulip Reid Barton (Oct 12 2019 at 18:35):

It's true--I think it would be nice if we did; but maybe this PR isn't the place to make that argument?

view this post on Zulip Reid Barton (Oct 12 2019 at 18:36):

What's the alternative? I guess I could append the contents of README.md to the end of docs/theories/topological_spaces.md, under a heading like "File organization"

view this post on Zulip Patrick Massot (Oct 12 2019 at 18:37):

Yes, maybe after renaming it to topology.md

view this post on Zulip Reid Barton (Oct 12 2019 at 18:38):

These docs are just concerned with the contents of the topological_space.lean file.

which no longer exists

view this post on Zulip Reid Barton (Oct 12 2019 at 19:02):

Okay, I've done this (for now, at least)

view this post on Zulip Reid Barton (Oct 12 2019 at 19:02):

oops hang on

view this post on Zulip Reid Barton (Oct 12 2019 at 19:04):

okay, it should be correct now


Last updated: May 10 2021 at 06:13 UTC