topology

Stream: maths

[Reid Barton]

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.

[Sebastien Gouezel]

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

[Reid Barton]

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.

[Patrick Massot]

Great!

[Reid Barton]

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 $S \subset X$ and $T \subset Y$ are compact, then $S \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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

since it will make this refactoring a lot easier

[Johan Commelin]

Go for it!

[Patrick Massot]

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.

[Johan Commelin]

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

[Reid Barton]

I also wondered about that

[Reid Barton]

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

[Johan Commelin]

fair enough

[Reid Barton]

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

[Patrick Massot]

@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

[Patrick Massot]

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

[Reid Barton]

This refactoring is now #1541.

[Reid Barton]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

It's running currently

[Patrick Massot]

I think

[Mario Carneiro]

is sanity_check in travis?

[Patrick Massot]

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).

[Reid Barton]

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

[Patrick Massot]

Oh I see

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

Good idea, done

[Reid Barton]

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.

[Reid Barton]

(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.

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

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"

[Patrick Massot]

Yes, maybe after renaming it to topology.md

[Reid Barton]

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

which no longer exists

[Reid Barton]

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

[Reid Barton]

oops hang on

[Reid Barton]

okay, it should be correct now