Product order topology on R2 is discrete

Stream: mathlib4

[Pieter Collins]

I managed to prove in Lean+Mathlab that the order topology on ℝ×ℝ is discrete:

import Mathlib.Data.Real.Basic
import Mathlib.Topology.Order.Basic
theorem R2_is_discrete : forall ab : ℝ × ℝ , (Preorder.topology (ℝ×ℝ)).IsOpen (singleton ab) :=
by sorry

This is not what one expects: the order topology on ℝ×ℝ should be the Euclidean topology. I also haven't made any unusual definitions, just used what is already provided in Mathlib. So how could this happen?

Lean/Mathlib automatically produces the partial order (actually, we only need a preorder) ≤ on ℝ. The definition is what one would expect.

Mathlib automatically generates a preorder ≤ on ℝ×ℝ. This is the product order, which is probably the most commonly used option, but other orders are possible (e.g. lexicographic).

Mathlib's Preorder class automatically generates a strict preorder < on ℝ×ℝ by a<b := a≤b∧¬b≤a. This seems fairly standard, but in this case is not topologically reasonable.

Mathlib defines Preorder.topology to be generate by the open sets {x|x<a} and {x|a<x}. This is a standard definition, but there is an approach which only uses ≤ and defines generating closed sets, and yields the Euclidean topology.

While each step may (at first sight) seem reasonable, overall the result is something which is wrong, at least in how a human would interpret the result.

My view is that there are a number of issues here, in decreasing order of severity:

1. Automatically providing a strict preorder < from a reflexive preorder ≤ is the biggest culprit. (I've already raised this; see #mathlib4 > Preorder / PartialOrder synthesised < ). While it might be "standard" in order theory, it doesn't make sense topologically (where < should be open and ≤ closed). Because it's automatically generated, users don't necessarily see it. Because it's a strong property, one can prove many things based on it which might not be true using a more natural < for your applicaton.
2. Automatically generating the product order on the product type. Actually, for this particular application it's not so bad, except that for consistency with the order topology generation, one should have (a,b)≤(c,d) := (a<c∧b<d)∨(a=c∧b-d) so that the automatically generated < on ℝ×ℝ is (a,b)<(c,d) ↔ a<c∧b<d, so the user should choose which ≤ is suitable. More of an issue is if is one wants a different order e.g. lexicographic, graded lexicographic; it seems that Mathlib uses a new type (e.g. Lex (ℝ×ℝ)) because the order is associated with the type.)
3. Generating the order topology from < rather than ≤. Actually I think it is the better choice to define the generating open sets from <, since defining the generating closed sets from ≤ is much more complicated. But it is inconsistent with 1) and 2). I believe that there is a StongLT which gives the right strict order. But this is not automatically generated, and doesn't seem to implement Preorder (so can't be used for the order topology) (maybe I'm missing something from the docs). Advising users to use StrongLT for the product order topology may recover the correct results, but doesn't prevent stating and proving R2_is_discrete.

More generally, I am uncomfortable with all the automatic generation going on. Maybe for arithmetic, there's only one natural +,-,× on a structure. Maybe for discrete mathematics, the automatically generated typeclasses and operations all make sense. But for order relations, there are multiple commonly-used orders on the same set, and having notation '≤' an intrinsic part of any preorder relation looks like it will be restricting and open subtle errors (in how users interpret symbols). (I also see there are ways around this.)

One might argue that the theorem is correct, and the user just has to interpret it's meaning properly. But I think this is a dangerous viewpoint, especially for developers of formal methods tools and libraries. Users can already have high trust that there are no bugs in the kernel and that proved theorems are formally correct. But if the statement doesn't correspond to natural and expected usage, people will believe things that are not true. Also, it shouldn't take an expert to notice such mistakes. Sometimes differences with common mathematical usage will be necessary, such as when combining different theories with different conventions. But it's much better to be explicit about what the usage is, than rely on (locally unstated) assumptions as to what the default usage is. In the example above, there's no mention of ≤ or < in the statement, yet alone of how they are defined, yet mismatches in expectations of the meaning between different Mathlib parts causes a big problem.

[Bhavik Mehta]

Pieter Collins said:

This is not what one expects: the order topology on ℝ×ℝ should be the Euclidean topology.

This is what one expects! The order topology is intended to be meaningful only for linear orders, informally, and in mathlib. Here's a stackexchange post also, explaining why the Euclidean topology on R^n for any n > 1 is never an order topology: https://math.stackexchange.com/a/2836/418148

Pieter Collins said:

having notation '≤' an intrinsic part of any preorder relation looks like it will be restricting

As far as I'm aware, most mathematical literature uses '≤' or a similar symbol to denote a preorder. Do you think we should use a different notation?

Pieter Collins said:

different theories with different conventions

Do you have references for these different conventions? For instance, do you have references which define the concept of a preorder in the way you suggest with weaker assumptions on <? Or references which define the order topology on your concrete example of R^2 using the strict < relation?

[Violeta Hernández]

cf. #mathlib4 > Preorder / PartialOrder synthesised <

[Pieter Collins]

Bhavik Mehta
Thanks! I may be missing some subtleties here.

Bhavik Mehta said:

The order topology is intended to be meaningful only for linear orders, informally, and in mathlib.

Birkhoff in Lattice Theory (p60) defines the order topology for arbitrary lattices. The definition uses closed sets under ≤, not open sets under (strong) <. I'm not sure if the two topologies are always equal (I guess not) though for ℝ×ℝ both definitions of order topology give the same result, the Euclidean topology.
In any case, one can always define an order topology based on any strict order; whether it's (always) useful is another matter.

Here's a stackexchange post also, explaining why the Euclidean topology on R^n for any n > 1 is never an order topology: https://math.stackexchange.com/a/2836/418148

This post shows that the Euclidean topology can't arise as the order topology of a total order; it doesn't say anything about strict partial orders.

As far as I'm aware, most mathematical literature uses '≤' or a similar symbol to denote a preorder. Do you think we should use a different notation?

You say "or a similar symbol". Maybe this is a newbie issue, but it seems Preorder always uses '≤', so what happens when there are different preorders on the same type? Or I could use (Mathlib) IsPreorder, but Preorder does not inherit from this, so presumably theorems which assume Preorder and IsPreorder are not interoperable.

Do you have references for these different conventions?

I meant this more in terms of a general comment.

For instance, do you have references which define the concept of a preorder in the way you suggest with weaker assumptions on <?

I would define preorder by ≤ without < . Or strict-order < without ≤.
Gierz et al "A Compendium of Continuous Lattices" define a "way below" relation '≪' which is a kind of topological-less-than and satisfies a<b≪c<d→a≪b.

Or references which define the order topology on your concrete example of R^2 using the strict < relation?

Well, Mathlib would with the StrongLT < on R^2.
I assumed it was a pretty standard construction. Looking briefly for references only gave the totally-ordered case of the order topology, which I assumed was just for simplicity, but I guess there are subtleties I am not aware of.

[Aaron Liu]

Pieter Collins said:

though for ℝ×ℝ both definitions of order topology give the same result, the Euclidean topology.

which order topology are you saying gives rise to the euclidean topology here?

[Edward van de Meent]

fwiw, it is my understanding that for R2 with the euclidean topology you should be using EuclideanSpace ℝ (Fin 2)

[Edward van de Meent]

note that the norm on ℝ × ℝ is also not the euclidean norm, but instead the maximum of the absolute values of the components.

[Edward van de Meent]

i believe that in general when one wants something euclidean to happen, one should use EuclideanSpace

[Yury G. Kudryashov]

Here is a list of topics where we discussed different ways to define a topology based on the order only. tl;dr Nothing that gives the product/pi topology on products (indexed or not) of linear orders.
Alex Meiburg said:

(Relevant links for others: #mathlib4 > OrderTopology without LinearOrder #mathlib4 > Open Ioi #maths > Multiple topologies? )
I see, okay, it looks like it's a topic that's come up a few times.

[Bhavik Mehta]

Pieter Collins said:

Or I could use (Mathlib) IsPreorder, but Preorder does not inherit from this, so presumably theorems which assume Preorder and IsPreorder are not interoperable.

Note that the lack of inheritance doesn't mean the lack of interoperability: we have docs#instIsPreorderLe which means any theorem about Preorder automatically applies to IsPreorder. There's also docs#partialOrderOfSO which allows any theorem about IsStrictOrder (irreflexive and transitive) to apply to PartialOrder.

Pieter Collins said:

Maybe this is a newbie issue, but it seems Preorder always uses '≤', so what happens when there are different preorders on the same type?

We usually use type synonyms here; this is explained in some of the threads Yury links above, and was mentioned in the previous thread when Lex was discussed. In fact one of my first Lean projects involved an alternative order on finite sets, where in my inexperience I made custom notation for the new order (https://link.springer.com/chapter/10.1007/978-3-031-16681-5_5#Sec10) and showed it forms an docs#IsLinearOrder provided the underlying type formed a docs#LinearOrder. The more modern approach (implemented for this example by Yaël and Violeta) is to use docs#Colex, like docs#Finset.Colex.instLinearOrder.

Pieter Collins said:

This post shows that the Euclidean topology can't arise as the order topology of a total order; it doesn't say anything about strict partial orders.

That's a fair point, it seems to me that the strict partial order on the product is relatively rare to consider!

Indeed Birkhoff's definition of < on partial orders is equivalent to mathlib's, with the comment "This notation and terminology are generally accepted", and on page 61 comments "We also note that it does not work at all to take “open intervals” as a basis of open sets.", with the specific counterexample being the Cartesian plane with the product order (matching mathlib).

Pieter Collins said:

The definition uses closed sets under ≤, not open sets under (strong) <.

This doesn't seem accurate, at least from the edition of Birkhoff that I have. The definition of the order topology on a complete lattice on page 59 uses the supremum and infimum of sets, as a limsup+liminf definition, and then the definition of the order topology on a partial order on page 60 uses the definition on its corresponding Dedekind-Macneille completion. Lemma 1 claims that all the closed intervals are closed sets, but doesn't claim that the closed sets are all generated by closed intervals. In particular, the topology on a partial order whose closed sets are generated by the closed intervals is called the interval topology in Birkhoff, and the remark after Theorem 4 explains that this can be strictly weaker than the order topology, with proof in Example 2.
You also say that the textbook defines the order topology for arbitrary lattices, I presume you intended to mean arbitrary partial orders? Or perhaps I'm unable to find the reference because of edition mismatch.

Pieter Collins said:

Gierz et al "A Compendium of Continuous Lattices" define a "way below" relation '≪' which is a kind of topological-less-than and satisfies a<b≪c<d→a≪b.

Looking at this example, I think it's important to note that this is a different symbol even in that reference, Example 1.3(1) distinguishes ≪ from <. In Example 1.3(2) it's discussed that even in the linear-order setting, the ≪ relation may not agree with the < relation. If your question is about how we could formalise that, this is a great application of either type synonyms, or the IsPartialOrder class. Further, note that this relation isn't in general irreflexive, so it's somewhat different from a < relation in a couple of ways.

[Bhavik Mehta]

Pieter Collins said:

which I assumed was just for simplicity, but I guess there are subtleties I am not aware of.

I think the key thing here is that the definition of order topology by generating open sets with < is poorly behaved outside of Lean for non-linear orders, and you observed that it's also poorly behaved in Lean for non-linear orders. And the definition of order topology given by Birkhoff is somewhat more complex, and in general different from generating closed sets with ≤.

I will add, however, that I can absolutely believe that the documentation in mathlib here is poor, and I'd happily merge a PR which improves it (especially if it adds references!). Perhaps the threads that Yury links suggest we should disallow OrderTopology from working on non-linear orders, or attempt to make it clearer still that it may not work as expected.

[Bhavik Mehta]

Also just to comment that the "said" in Yury's comment is also itself a thread about the same topic, and is a useful read: #mathlib4 > A more useful `OrderTopology`

[Yury G. Kudryashov]

If there is a way to define topology based only on the $\le$ relation that gives the product topology for finite products of linear orders, then I will gladly replace the current definition with the new one (and port the rest of the library). However, all previous threads discussing this issue didn't come up with a definition that "works" for any finite product of linear orders.

[Pieter Collins]

Thanks again for the replies! #mathlib4 > Product order topology on R2 is discrete @ 💬

Note that when I wrote

The definition uses closed sets under ≤, not open sets under (strong) <.

I meant that closed sets are defined only using ≤ (and not strong <), not that the closed intervals are a generating set.

Bhavik Mehta said:

You also say that the textbook defines the order topology for arbitrary lattices, I presume you intended to mean arbitrary partial orders? Or perhaps I'm unable to find the reference because of edition mismatch.

It seems to define an order topology for arbitrary partial orders, but uses the completion to define the convergence relation. Though probably weird things can happen if the order is not complete. One could also define a limit without going to the completion, though I would guess this is different, in general.

[Pieter Collins]

Yury G. Kudryashov said:

If there is a way to define topology based only on the $\le$ relation that gives the product topology for finite products of linear orders, then I will gladly replace the current definition with the new one (and port the rest of the library). However, all previous threads discussing this issue didn't come up with a definition that "works" for any finite product of linear orders.

Did anyone check the definition of Birkhoff? Might this work?

There's a fairly recent paper of Hauser & Kalauch "Order continuity from a topological perspective" (https://link.springer.com/article/10.1007/s11117-021-00834-5) which defines open sets as "net catching":

A subset U ⊆ P is called a net catching set for x ∈ P if for all nets (x̂_α)α∈A and ( x̌_α)α∈A in P with x̂_α ↑ x and x̌_α ↓ x there is α ∈ A such that [x̂_α , x̌_α] ⊆ U .

They then define three kinds of convergence of nets occurring in the literature, and show that each is stronger than topological convergence, and give some other relationships between them. They only mention product topology once in passing.

In any case, I think it's worth formalising some of this and see which approach(es) behave nicely with respect to products. I also think it's worth formalising the topology generated by open intervals (for the strong product strict order).

I could do some work on these things (from a constructive/computable viewpoint, as I'm really interested in how to construct verifiable/falsifiable < / ≤).