Possible future name collision

Stream: mathlib4

[Brendan Seamas Murphy]

The one-point compactification of a space is in Mathlib.Topology.Alexandroff. It would make more sense to me for Mathlib.Topology.Alexandroff to be about Alexandroff spaces, i.e. topological spaces in which arbitrary intersections of open sets are open. Both concepts are named after Pavel Alexandroff. We might want to have code about these at some point, e.g. because of the various stone-ish dualities being formalized right now or if we want to prove something about finite topological spaces (see this book by Peter May on their algebraic topology). Would people be okay with me renaming the "Alexandroff" to "OnePointCompactification"?

[Brendan Seamas Murphy]

(as far as I can tell the only usage of the one point compactification in mathlib is a couple of lemmas in Mathlib.Topology.RatLemmas saying the one point compactification of Q fails to have various countability properties)

[Jireh Loreaux]

I think I'll have use for the one point compactification as it corresponds to the minimal unitization of a C*-algebra. I don't have strong preferences on the name, but OnePointCompactification is pretty long.

[Moritz Doll]

Would namespacing compactifications solve the problem, i.e., Compactification.Alexandroff and Compactification.StoneCech (and probably both files should then also go into Mathlib.Topology.Compactification)

[Johan Commelin]

I've always learned about the thing as "one point compactification". So I would also be quite happy with Compactification.OnePoint.

[Yaël Dillies]

FWIW I was about to call the Alexandrov spaces alexandrov_discrete_space to avoid a conflict with https://en.m.wikipedia.org/wiki/Alexandrov_space. So no filename conflict, but a three way conflict in definition names. And indeed I wanted to introduce them for the sake of Stone duality.

[Reid Barton]

There was a poll before: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238579.20one.20point.20compactification/near/249291726

[Mario Carneiro]

It's fine, we'll just call one alexandroff and the other one alexandrov

[Ruben Van de Velde]

That leaves Алекса́ндров if he has a third thing named after him

[Reid Barton]

Given the number of things named for Alexandroff/v it seems clearly better to name the one-point compactification by what it is. I also I don't think I've ever heard it called the Alexandroff compactification in real life and I wouldn't have understood that phrase if not for these discussions here. In particular I would certainly assume a file in topology with the name Alexandroff is about the Alexandroff topology!

[Patrick Massot]

In France I never heard it called anything else than Alexandroff compactification, but I still agree the descriptive name is better. Of course the docstring needs to include the word Alexandroff.

[Brendan Seamas Murphy]

Okay, I'll move the definition to Topology.Compactifications.OnePoint and pr later

[Yury G. Kudryashov]

@Ruben Van de Velde It's Александров. а́ marks the stressed syllable in Wiki

[Jireh Loreaux]

@Brendan Seamas Murphy sorry, do you mean you'll move it to a file with that name, or you'll move the name of the declaration to that? I don't think the declaration should have the Topology prefix.

[Jireh Loreaux]

Also I think it should be singular, not plural.

[Yury G. Kudryashov]

Note that Alexandroff (X : Type _) : Type _ vs class AlexandroffSpace is not a collision.

[Brendan Seamas Murphy]

Jireh Loreaux said:

Brendan Seamas Murphy sorry, do you mean you'll move it to a file with that name, or you'll move the name of the declaration to that? I don't think the declaration should have the Topology prefix.

I meant I'll move it to a file with that name, and yeah sorry singular is better

[Reid Barton]

Yury G. Kudryashov said:

Note that Alexandroff (X : Type _) : Type _ vs class AlexandroffSpace is not a collision.

There is a construction (https://en.wikipedia.org/wiki/Alexandrov_topology, named for a different Alexandrov!):
Given (X : Type _) [Preorder X], we give X the "Alexandrov topology" by declaring the upwards-closed sets to be open. Of course there are many types with both an order and a topology that is not formed this way, so the topology should go on a type synonym of X.
The obvious name is Alexandrov X...

[Reid Barton]

Sorry, same person as the one-point compactification, but a different person from the one the spaces in differential geometry are named for.

[Johan Commelin]

I could also imagine (on top of a construction) a mixin for this Alexandrov topology. Similar to docs#order_topology

[Brendan Seamas Murphy]

Ready to submit a PR but the CI fails with this
image.png
I'm not sure what the issue is or how to fix it, does anyone have any advice?

[Kevin Buzzard]

If mathlib compiles locally then maybe just restart CI? (you can click somewhere on github to do this)

[Damiano Testa]

Or make sure that the local files that you have are committed?

[Yaël Dillies]

No need to restart CI. Read the error carefully: It's telling you that Mathlib.lean isn't in alphabetical order anymore.

[Brendan Seamas Murphy]

Afaict it doesn't actually say that anywhere, would be nice to have an explicit error message

[Jireh Loreaux]

indeed, but if you read what the "check that all files are imported" task does, you'll see that it just lists the Mathlib source files in alphabetical order and compares it to the existing Mathlib.lean, at which point the existing diff tells you the problem.

[Brendan Seamas Murphy]

Right, I figured that out after Yaël pointed it out. But it would have been nice to just have the error message say what the issue is so I didn't need to ask on zulip

[Jireh Loreaux]

Maybe make a PR to the Github actions file?

[Julian Berman]

I'll also plug pre-commit again which fixes stuff like this automatically (specifically the file-contents-sorter hook).

[Jireh Loreaux]

Julian, can you link to that? I haven't seen those hooks for mathlib.

[Julian Berman]

Yeah sorry, it's not something enabled for mathlib(3 or 4) -- just mentioning it's perhaps worth considering -- it's https://pre-commit.com/index.html and the CI version is https://pre-commit.ci/ -- the hook I mentioned lives in the first repo mentioned here: https://pre-commit.com/hooks.html

[Julian Berman]

Even more specifically, if Mathlib4 committed:

repos:
-   repo: https://github.com/pre-commit/pre-commit-hooks
    rev: v4.4.0
    hooks:
    -   id: file-contents-sorter
        files: "Mathlib.lean"
        args: ["--unique"]

to a file called .pre-commit-config.yaml and enabled pre-commit in CI (or if you run it locally), then if you intentionally move lines around in the Mathlib.lean file you'll see them put back in the right place by pre-commit automatically.

[Johan Commelin]

But I guess Bors doesn't run this, right?

[Julian Berman]

pre-commit.ci has like a bot that will come add commits to the branch which fix things like ^ (or any other hooks mathlib enables -- e.g. removing trailing whitespace or whatever, including if there were some mathlib custom ones we wrote)

So Bors doesn't / wouldn't need to know anything about it, it'd just look like some other normal commit that gets squashed by the time Bors is involved I think.

[Johan Commelin]

@Julian Berman The thing I would (also) like a solution to, is that bors takes N different PRs, and merges them onto a staging branch before running CI again. Merging the N PRs might cause Mathlib.lean to become unsorted... (or a merge conflict might happen, for stupid reasons). If that can be fixed by a little bot, that would be great.

[Julian Berman]

Got it. I'd have to look at how that happens to know (I mean of course that sounds solvable, pre-commit doesn't sound needed per se to just solve that one thing, but yeah, will have a look in a bit).

[Johan Commelin]

Awesome!

[Jannis Limperg]

Maybe this has been discussed before, but arguably the root of the issue is that Mathlib.lean is version-controlled at all. Could lake be instructed to generate it as part of a lake build?

[Johan Commelin]

Isn't it need when you want to do import Mathlib in some project that depends on Mathlib?

[Jannis Limperg]

I don't know how lake handles the building of dependencies. Maybe it would be smart enough to invoke the hypothetical 'generate Mathlib.lean' target also when mathlib is a dependency.

[Christopher Hoskin]

Reid Barton said:

Yury G. Kudryashov said:

Note that Alexandroff (X : Type _) : Type _ vs class AlexandroffSpace is not a collision.

There is a construction (https://en.wikipedia.org/wiki/Alexandrov_topology, named for a different Alexandrov!):
Given (X : Type _) [Preorder X], we give X the "Alexandrov topology" by declaring the upwards-closed sets to be open. Of course there are many types with both an order and a topology that is not formed this way, so the topology should go on a type synonym of X.
The obvious name is Alexandrov X...

This is what I've been calling the UpperSetTopology in https://github.com/leanprover-community/mathlib4/pull/2508

[Christopher Hoskin]

(Now broken out into a separate PR https://github.com/leanprover-community/mathlib4/pull/5672)