Some missing, accessible, topology results

Stream: mathlib4

[Josha Dekker]

Hi, in my efforts to track progress on pi-base, I noticed that the following topology results are still open (docstrings refer to theorems in https://topology.pi-base.org) so feel free to pick one and make a PR! I'm a bit too busy at this moment, otherwise I'll probably add them at some distant point in the future.

import Mathlib
open TopologicalSpace

--T000212:
example [TopologicalSpace X] [Countable X] [FirstCountableTopology X]
  : SecondCountableTopology X
 := by exact?

--T000259:
example [TopologicalSpace X] [Countable X]
  : HereditarilyLindelofSpace X
 := by exact?

--T000302:
example [TopologicalSpace X] [Countable X] [CompactSpace X] [R1Space X]
  : PseudoMetrizableSpace X
 := by exact?

--T000345:
example [TopologicalSpace X] [Group X] [TopologicalGroup X]
  : CompletelyRegularSpace X
 := by exact?

[Emilie (Shad Amethyst)]

I can't seem to find those on the pi-base website :/

[Josha Dekker]

Searching on pi-base with numbers seems to be a bit weird sometimes. My go-to strategy is to click any theorem and change the URL for the desired number, e.g.:
T212 : https://topology.pi-base.org/theorems/T000212/
T259 : https://topology.pi-base.org/theorems/T000259/
T302 : https://topology.pi-base.org/theorems/T000302/
T345 : https://topology.pi-base.org/theorems/T000345/

Also, note that the results I just wrote are slightly differently phrased from those in pi-base, as we have some different (naming) conventions, e.g.
CountableSpace -> Countable
FirstCountableSpace -> FirstCountableTopology
Has A Group Topology -> [Group X] and [TopologicalGroup X]

[Josha Dekker]

Also, I needed to tell Lean that we have a [TopologicalSpace X], which pi-base doesn't need to specify of course.

[Johan Commelin]

@Josha Dekker Can you now produce some sort of json dictionary that maps back-and-forth between pi-base results and mathlib results?

[Johan Commelin]

If you can, then we should render that dictionary on the website, if you agree.

[Josha Dekker]

Johan Commelin said:

If you can, then we should render that dictionary on the website, if you agree.

I think that would be very nice, but this is very much WIP still. I need to learn more Lean programming I guess, as I'm currently using Julia for the conversion. I can convert Mathlib properties and theorems to their Lean counterparts and write them to .lean files. I think rendering the dictionary on the website would be very nice, but I'm not familiar with these things, so it'll take quite some time to figure that out.

If someone is more experienced with this and would like access to https://github.com/JADekker/PiBaseTracking to make the necessary modifications or if someone can suggest what exactly I should do, I would be more than happy!

[Josha Dekker]

As this is very much WIP, I haven't written too much documentation either, as things are bound to be changed/optimised at some point!

[Josha Dekker]

I figured I'd post some missing theorems for now, so that people looking for small projects can have some fun with them!

[Josha Dekker]

I could certainly make .md or .json files with lean versions of the definitions and theorems from all the .md files from pi-base, if you like? That would allow us to get a 1-1 correspondence between pi-base pages and lean-version. Let me try that this afternoon!

[Johan Commelin]

It would be interesting to try to prove the theorems that you generate using exact?. If there's a match, that can generate an entry in the db.

[Johan Commelin]

Hopefully this can automate a bunch of the work (-;

[Josha Dekker]

Johan Commelin said:

Hopefully this can automate a bunch of the work (-;

Currently, I automatically get files with all theorems, each of which is checked by exact?, so if the file is error free, we’re done… but checking all theorems separately and automated would certainly be better and allow us to also program exceptions for theorems that can be proven but not by exact? because of some special reason. Let me try to write code in Lean for this, may take a few days though as I’m doing this in my spare time

[Emilie (Shad Amethyst)]

(I'll happily take on T000345 as a break from my Rubin's theorem stuff)

[Emilie (Shad Amethyst)]

Do we not have that uniform spaces are completely regular?

[Emilie (Shad Amethyst)]

I have a working proof that TopologicalGroup G → UniformSpace G, but I guess we're missing one step to get to CompletelyRegularSpace G

[Josha Dekker]

Emilie (Shad Amethyst) said:

Do we not have that uniform spaces are completely regular?

I could only find https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/Separation.html#UniformSpace.to_regularSpace

[Emilie (Shad Amethyst)]

That's unfortunately not proving much new in my case, since we already have an instance for TopologicalGroup G → RegularSpace G

[Anatole Dedecker]

Emilie (Shad Amethyst) said:

I have a working proof that TopologicalGroup G → UniformSpace G, but I guess we're missing one step to get to CompletelyRegularSpace G

We already have TopologicalGroup -> UniformSpace: docs#TopologicalGroup.toUniformSpace

[Josha Dekker]

(deleted)

[Anatole Dedecker]

But indeed I don’t think we have any other instance of docs#CompletelyRegularSpace

[Emilie (Shad Amethyst)]

Looking into this, most (if not all) proofs that a UniformSpace is a CompletelyRegularSpace rely on the pseudometric definition of a uniform space.
We have the first step of the construction of the pseudometric family, docs#UniformSpace.pseudoMetricSpace, but we don't have the next steps, which are to first create for any V ∈ 𝓤 X a uniformity generated by a countable filter, that will be coarser than 𝓤 X, and then show that 𝓤 X = sInf { uniformity generated from V | V ∈ 𝓤 X }.
I can poke at it then and there, but if someone else who actually knows what they're doing wants to do it, then I won't complain :p

[Emilie (Shad Amethyst)]

Alright, I have a working proof of UniformSpace X → CompletelyRegularSpace X

[Emilie (Shad Amethyst)]

Although I am worried that the two are supposed to be equivalent; I'll need to look into the actual books to find a proof for the reverse implication

[Josha Dekker]

Time for a PR!

[Josha Dekker]

Emilie (Shad Amethyst) said:

Although I am worried that the two are supposed to be equivalent; I'll need to look into the actual books to find a proof for the reverse implication

Are they really equivalent?

[Emilie (Shad Amethyst)]

That's what pi-base and wikipedia claim; I can kind of see how they would be, since the condition for a completely regular space gives you a kind of metric, which you can then use to define a filter of entourages

[Josha Dekker]

Yes, indeed, I find the same now that you mention. Weird that we have the two definitions then… perhaps you can try to shiw the equivalence, in which case we might be able to get rid of one of the two definitions? There might be some double work in the API at present if they’re equivalent…

[Emilie (Shad Amethyst)]

CompletelyRegularSpace has substantially fewer lemmas, so the duplication is minimal

[Emilie (Shad Amethyst)]

Problem T345 has progressively gotten more and more difficult :p

[Josha Dekker]

But also more rewarding when resolved, we could get rid of a duplicate definition if it is correct

[Patrick Massot]

Asking whether they are equivalent is meaningless. One of them is a property of a topological structure and the other one is extra data. What is equivalent is having a completely regular topology and the existence of a uniform structure inducing the given topology.

[Josha Dekker]

I see, thank you! I think it would still be nice to have the appropriate reverse implication!

[Junyan Xu]

CompletelyRegularSpace was added relatively recently in #7926, and I too noted that the equivalence with uniformizability is missing. I searched for a proof and first found the original reference by Andre Weil, and then Willard's *General Topology* which contains a proof as Theorem 38.2.
image.png

[Emilie (Shad Amethyst)]

#10678 proves the first half of this equivalence.
Once the other half of the equivalence is proven, we would be able to replace CompletelyRegularSpace X with some UniformizableSpace X class, which says that there exists a UniformSpace.Core X that agrees with the ambient topology, and use the equivalence to either get the existing proposition of CompletelyRegularSpace, or to construct a UniformizableSpace X from that proposition

[Junyan Xu]

I think we can stick with the name CompletelyRegularSpace rather than replacing it with a new name UniformizableSpace. What we should do is to prove CompletelyRegularSpace X ↔ ∃ (u : UniformSpace X), UniformSpace.toTopologicalSpace = t assuming [t : TopologicalSpace X]. And we could provide something like docs#TopologicalSpace.metrizableSpaceMetric.

[Emilie (Shad Amethyst)]

That would work too, yeah :)

[Anatole Dedecker]

I'm a bit late to the discussion, but I would just like to mention this old thread where I also proved the "family of metrics" definition of uniform spaces, and Adam suggested a potential alternative approach. I'll have a look at your PR tomorrow and think about which approach sounds the most efficient.

[Emilie (Shad Amethyst)]

I pretty much did something very similar to yours, with UniformSpace.uniformity_eq_iInf_uniformSpaceOf corresponding to what you had proven back then (although I didn't know about your existing proof, which would have made my day easier)

[Anatole Dedecker]

Yeah sorry, I'm not proud of these never-PR-ed pieces of code...

[Emilie (Shad Amethyst)]

Ah well, technically it was proven decades ago in multiple math papers already. I can definitely have a look at your and see where my proof can be optimized, though

[Junyan Xu]

#10678 proves the first half of this equivalence.

@Aaron Liu's #24096 proves both direction

[Aaron Liu]

Junyan Xu said:

#10678 proves the first half of this equivalence.

Aaron Liu's #24096 proves both direction

Wow I did not see #10678