Convention for the order on topologies

Stream: Is there code for X?

[Notification Bot]

6 messages were moved here from #Is there code for X? > Characterisation of connectedness using continuous maps by Junyan Xu.

[Junyan Xu]

As a data point, here is an excerpt from Conway's A Course in Functional Analysis, Appendix A.2. He did not introduce the ≤ notation but his use of "larger" of "smaller" is consistent with the subset order. You're welcome to provide your references!
image.png

[Patrick Massot]

Thanks, this excerpt is indeed a very nice argument in favor of mathlib's convention, both through the way he explicitly mentions there are several coexisting convention and the way he very carefully uses the reversed inclusion symbol $\supseteq$

[Junyan Xu]

Thanks for your input, but note that he didn't mention coexisting notations, but only coexisting nomenclature. In mathlib ≥ represents ge which means `greater than or equal to", and I see no difference between "greater" and "larger", so Conway's use of the word "larger" is consistent with the subset order but not the current default, the superset order. I wouldn't exclude the possibility that some authors use ≤ (or another notation of the same directionality) to mean ⊇ in the context of topologies, so you're welcome to provide another data point!

[Patrick Massot]

I'm tired of this discussion and I have actual work to do. I've never seen ≤ used in this context so there is no trouble at all, and our convention simply works better for the way we do topology in mathlib, which is very suitable for formalization and does not exist on paper as far as we know. Maybe we could redefine topological_space X to be a function from X to filter X satisfying the appropriate axiom so that you find the ordering more natural but I don't have time for this. The ordering we use are already fully consistent from filter to uniform spaces through topologies. I really don't see the point of inverting one order relation in the middle of this chain.

[Reid Barton]

From a categorical perspective there's no choice to be made, the forgetful fibration Top -> Set has fibers that are posets, and the least (resp. greatest) elements of these posets are the discrete (resp. indiscrete) topologies.

[Kevin Buzzard]

So mathlib has bought into the categorical perspective, where the existence of arrows X -> Y is another way of saying X <= Y.