topological space ns/locale name

Stream: general

[Yury G. Kudryashov]

I have several loosely related suggestions.

• Rename topological_space locale to topology #18293 or drop it and make nhds/nhds_within a global notation.
• BTW, do we need the uniformity locale?
• Move second_countable_topology etc to the root namespace. These classes have "topology" in their names, so no chances for collisions.
• Move inducing, embedding etc to a NS (either topological_space or topology).
• Possibly, rename the class topological_space to topology.

[Yury G. Kudryashov]

/poll Locale names
Leave as is (topological_space and uniformity)
Rename (topology and uniformity)
Make notations (nhds, nhds_within, uniformity) global

[Yury G. Kudryashov]

/poll NS for first/second countable topology
Leave inside topological_space
Move to the root NS

[Yury G. Kudryashov]

/poll NS for inducing, embedding
Leave in the root NS
Move to the topological_space NS
Move to the topology NS

[Yury G. Kudryashov]

/poll Name for the topological_space typeclass
topological_space
topology

[Patrick Massot]

I don't think we want the neighborhood and uniformity notations to be global. There are single letters notation, this is too tempting to reuse for completely different purposes.

[Patrick Massot]

I already wrote several times that embedding should be in a namespace, this is a very generic word, and same for inducing.

[Yury G. Kudryashov]

Please don't forget to vote.

[Yury G. Kudryashov]

@Sebastien Gouezel and @Floris van Doorn commented on the original PR. Please vote here.

[Patrick Massot]

About the name topological_space, I think he key thing is consistency. If we keep metric_space and measure_space then we should keep topological_space.

[Floris van Doorn]

If we rename the locale topological_space, do we want to also rename the namespace topological_space (even if we don't rename the class)?

[Mario Carneiro]

Can we not be making such foundational name changes at this point in the port?

[Yury G. Kudryashov]

We haven't started porting topological spaces yet.

[Yury G. Kudryashov]

(OK, we have 1 file)

[Mario Carneiro]

perhaps, but by the time this PR makes it through review and is merged we will be halfway into it

[Yury G. Kudryashov]

No, I don't think so. We'll need 1 more PR because of some roadblocks I hit in topology.order anyway.

[Yury G. Kudryashov]

I can make any subset of these changes in <1h, then someone can quickly review them.

[Yury G. Kudryashov]

@Patrick Massot @Floris van Doorn @Riccardo Brasca @Reid Barton I added 1 more answer to the first poll. With this approach, open_locale topology means "I want to use notation about topology, no matter I deal with topological spaces or uniform spaces".

[Yaël Dillies]

Patrick Massot said:

About the name topological_space, I think he key thing is consistency. If we keep metric_space and measure_space then we should keep topological_space.

We have the namespace measure_theory, though. The measure_space namespace is for material that is specifically about measure_space. In contrario, docs#topological_space.opens is not specifically about topological_space.

[Patrick Massot]

That part of the discussion was not the namespace. And I don't see how docs#topological_space.opens isn't about topological_space...

[Yaël Dillies]

There's a difference between material about topological/measurable spaces and material about topological_space/measurable_space. Once you reach topological_space.opens, the fact that we get the topology from topological_space is an implementation detail. In contrast, docs#measurable_space.comap is very measurable_space-specific.

[Yury G. Kudryashov]

We need to break ties in 2 polls.

[Yury G. Kudryashov]

A very loosely related PR: #18312.

[Anatole Dedecker]

I just want to mention that imo the setup we have for metric spaces is nice, where the class is metric_space but all the lemmas are in the metric namespace (and, if there were any notation associated to metric spaces, putting them in locale metric would be fine too)

[Floris van Doorn]

Oh good point, we already have different class names and namespace names for metric_space/metric. I suggest we also do that for topological_space/topology

[Floris van Doorn]

/poll Should we rename the namespace topological_space to topology (keeping the class name as topological_space)?
yes
no

[Floris van Doorn]

For people that prefer topology.first_countable over having first_countable in the root namespace: are there other uses of "first countable" or "second countable" in math?

[Yury G. Kudryashov]

I assumed it would be first_countable_topology in the root NS.

[Yury G. Kudryashov]

Now it is docs#topological_space.first_countable_topology.

[Floris van Doorn]

oh, that's true.

[Floris van Doorn]

I got confused by the last option (which is also fine by me).

[Yury G. Kudryashov]

It turns out that there are 3 notations in the uniformity locale:

• uniformity
• separation_rel
• rel_comp

I'm no longer sure that we need to merge this locale with topology.

[Yury G. Kudryashov]

I suggest that we merge #18293 before it rots, then discuss what to do with the uniformity locale.

[Yury G. Kudryashov]

separation_rel will go away either this week-end (if I find time for this), or soon after porting. It is equal (but not defeq) to inseparable.

[Patrick Massot]

Indeed this is again a historical accident. It was there long before inseparable.