A more useful `OrderTopology`

Stream: mathlib4

[Alex Meiburg]

Right now, docs#OrderTopology says that a topology is the least topology with the opens Set.Ioo a b. I would like to propose changing this to say that it is least topology with the closed sets Set.Icc a b. For linear orders, these are equivalent, and as far I can tell this accounts for like >90% of theorems involving OrderTopology.

But for sets that aren't totally ordered, I claim that the latter is much more useful (and holds true on many more objects of interest). For instance, take ℝ × ℝ under the pointwise product order (Prod.instPartialOrder). Now the interval Set.Ioo (ax,ay) (bx,by) is the set ((Set.Icc ax bx) ×' (Set.Icc ay by)) \ {(ax,ay), (bx,by)}; it's a square in the plane, that is closed everywhere except for the bottom-left/top-right corners, where there's a single point missing. This is a relatively awkward set (to me), and isn't closed.

But under this pointwise product ordering, products of closed sets are closed sets, so this works out nicely. The same is true for pi-types (infinitary products). Similar nice things typically work out in many lattices, majorization order, etc. I bumped into this recently when I was looking at operators in a C*-algebra under the spectral order, where again the closed intervals define the topology, but the open intervals are ugly.

[Yury G. Kudryashov]

I've asked a similar question a few times. tl;dr it's hard or impossible to define a typeclass with instances for Prod and pi types that will agree with the (indexed) product topology.

[Yury G. Kudryashov]

What you suggest is Topology.lower X ⊓ Topology.upper X.

[Alex Meiburg]

(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.

[Alex Meiburg]

It's hard or impossible to define a typeclass with instances for Prod and pi types that will agree with the (indexed) product topology

This is very confusing to me. At least for Prod, at least, isn't it true? If α and β are each PartialOrders with the "fixed" (closed set) OrderTopology, then the product topology on α × β is also an OrderTopology?

[Aaron Liu]

Yury G. Kudryashov said:

I've asked a similar question a few times. tl;dr it's hard or impossible to define a typeclass with instances for Prod and pi types that will agree with the (indexed) product topology.

I have an idea I think will work for finite products

[Aaron Liu]

But it's complicated

[Aaron Liu]

Alex Meiburg said:

This is very confusing to me. At least for Prod, at least, isn't it true? If α and β are each PartialOrders with the "fixed" (closed set) OrderTopology, then the product topology on α × β is also an OrderTopology?

Is it the least topology with closed intervals closed? I think not since the antidiagonal in R^2 (probably?) isn't a finite union of intersections of closed boxes

[Anatole Dedecker]

Two things: first, in order to get something useful, you would not asks only for Iccs to be closed, but for Iics and Icis to be closed (otherwise all your closed sets are bounded, which can't be good)

[Anatole Dedecker]

But then, it still doesn't pass to products unless there are top and bottom elements: in $\R^2$, you would still only get set which are bounded in the antidiagonal direction, which does not give you the usual topology

[Anatole Dedecker]

Note that Topology.instIsLowerProd is already false without the OrderBot assumptions for example.

[Alex Meiburg]

Ah, hmm. Right. Okay, clearly there was some mistakes in my thinking :sweat_smile: I guess I want (very informally) a version of OrderClosedTopology that doesn't just say "these (closed intervals) are closed sets", but says something like "the closedness defines the topology". But I don't know what that should actually be

[Alex Meiburg]

(deleted)

[Alex Meiburg]

Nope, still confused.

[Alex Meiburg]

Alright, I guess I see now why it's so tricky. You need to, for instance in R^2, distinguish between { (x,-x) | 0 <= x } as an antidiagonal ray which should be closed; and { (x,-x) | 0 < x } which is an antidiagonal _open_ ray and shouldn't be closed. And you need to distinguish between those using purely order-theoretic properties on R^2 (without referring directly to the order on the individual coordinates).

That is possible in principle, they're not order-theoretically isomorphic. The closed ray S satisfies the predicate, "For all x, if there does not exist a y strictly between x and the upper closure of S, then x is in S". The open ray doesn't. But this puts kind of a lower bound on the complexity of any appropriate predicate

[Anatole Dedecker]

The only thing that may have a chance of working is somehow "doing everything in a suitable completion and then pulling back the topology". I don't recall my precise thoughts about it, but I think I recall that weird things stil happen.

[Aaron Liu]

Anatole Dedecker said:

The only thing that may have a chance of working is somehow "doing everything in a suitable completion and then pulling back the topology". I don't recall my precise thoughts about it, but I think I recall that weird things stil happen.

I don't think we need to complete anything

[Aaron Liu]

Why do you think we need to pass to a completion

[Anatole Dedecker]

Completeness is not really what's needed, I should have said boundedness, because everything works well for products of bounded linear orders (I think?). But then we can't just add bot and top in a stupid way, because in a product order what we really want to add is all the $(\bot, x)$, $(\top, x)$, ...

[Aaron Liu]

That seems a bit contrived

[Aaron Liu]

and there are a lot of "weird" orders too

[Aaron Liu]

What are some conditions we want on order topologies? I think we want it to agree with the usual order topology on linear orders and I think I also want them to be R0-separated (every open set is a union of closed sets)

[Aaron Liu]

For example let's take ℝ × ℝ × Fin 2 with the product order and then quotient by (x, y, 0) ≈ (x, y, 1) whenever x + y ≠ 0 and put the obvious order on this quotient, so we've effectively doubled the antidiagonal. What should the order topology be?

[Alex Meiburg]

I guess I would be content with any definition such the Set.Ici / Set.Iic are closed, agrees with (the current) OrderTopology on linear orders, is closed under products, and uniquely determines the topology.

OrderClosedTopology satisfies the first three but not the fourth. My initial bad definition in terms of generating from Icc satisfies (1) (2) and (4), but not in (3) in the sense that it isn't the correct topology on the product.

[Aaron Liu]

Are we closed under products or closed under finite products

[Aaron Liu]

Closed under products might be tricky

[Alex Meiburg]

Finite products is fine with me! :shrug: I don't know. There has to be something better though.

[Aaron Liu]

There are a lot of things that are "better" but which one do you want

[Alex Meiburg]

Well I don't know! :) Don't you ever look at something and say, "this definitely seems like it could be better, because it's lacking so many properties that I like, but I don't know what the thing that's most better is"?

[Aaron Liu]

Well we can't exactly Classical.choice something better out

[Aaron Liu]

We need to pick one

[Alex Meiburg]

Alright, tell me one that you think is better then?

[Aaron Liu]

I can come up with better things but I need something to start on

[Aaron Liu]

I can Make It Work for R^2 but I want it to work for everything else too which means I need to know what it's supposed to do

[Aaron Liu]

And it's really tricky because there are a lot of really tricky orders

[Aaron Liu]

For example, R^2 with a doubled antidiagonal which I constructed above

[Aaron Liu]

What's the subspace topology on the double antidiagonal?

[Alex Meiburg]

Alright, well I think a good goal would be something that satisfies the four properties I list above. Slightly more explicitly, I want a property P so that:

1) P uniquely determines the topology from a partial ordering.
2) If a type X (equipped with a topology and partial order) has the property P, then all Set.Ici and Set.Iic are closed.
3) On linear orders, P is equivalent to OrderTopology.
4) P is closed under finite products. That is, if X and Y each have property P, then so does Prod X Y. Since we're saying that P uniquely determines the topology, I mean that P determines a topology equal to the standard product topology on X × Y.

Now, I don't see how to construct such a property myself; it sounds like maybe you do. If you still feel like this is too underdetermined, then as stretch goals we could try to have the full HSP trifecta (homomorphisms, subobjects, and products), since we already have products:

5) P is closed under restrictions. So if X has property P, and then I restrict X to a subtype, and get the subtype order and the subspace topology, then the restriction also has property P.
6) P is closed under homomorphisms. So if I map X with a monotone (or should it be strict monotone? or an OrderHom, since we're including partial orders?) and continuous function, then the image with the induced topology and induced order (again, I think there might be a couple different reasonable "induced orders" for partial orders) should also have property P.

[Alex Meiburg]

A particularly nice case is that of lattices of course, so if we focused on just without ever worrying about general partial orders those there might be a lot of degrees of freedom. But my original motivation for this comes from matrices under the Loewner order, which is _not_ a lattice; so if you wanted you could say the property I _really_ want is:

7) This property should correctly determine the topology on Hermitian matrices over ℂ, from the Loewner order. (Where A ≤ B is defined to be that B - A is positive semidefinite.)

[Aaron Liu]

Unfortunately, 1), 3), 5) together derive a contradiction

[Alex Meiburg]

Oh, fantastic! That's exciting! Why? :smiley:

[Alex Meiburg]

Oh, right. Of course.

[Aaron Liu]

There are subspaces of linear orders with the subspace topology which are not any order topology (for example, the sogenfery line)

[Alex Meiburg]

I could just cut out a half-open interval from the reals and get something that's order isomorphic but not connected anymore.

[Alex Meiburg]

Well if you can get (1-4) + (7) that would be pretty great

[Alex Meiburg]

And I guess I would suggest that whatever happens to a doubled-antidiagonal on R^2 in the first definition you come up with must be some kind of natural, then.

[Alex Meiburg]

I have an idea here, it's definitely not fully correct but I think it's in pointing in a workable direction.

[Aaron Liu]

my only intuition on these Hermitian complex matrices comes from quantum mechanics

[Aaron Liu]

I assume the topology is some sort of product topology from copies of ℂ

[Alex Meiburg]

Yeah, they do come from quantum mechanics (largely) - it's exactly your standard topology on matrices, the finite product topology over all the elements. Which is the same topology as you would get induced from any matrix norm, like the Frobenius norm for instance (so that a ball is the L2 norm of the entries).

[Alex Meiburg]

If (7) is unfamiliar, I wouldn't worry about it though

[Violeta Hernández]

I recall not too long ago there was discussion to limit OrderTopology to linear orders, precisely because the concept just doesn't generalize in any nice way to partial orders.

[Aaron Liu]

who knows maybe there is a nice way

[Aaron Liu]

But there are a lot of weird orders so I would want a way that works for them too

[Aaron Liu]

for example I think the line with two origins should be realizable as an order topology

[Aaron Liu]

and the real plane feels like it should be the order topology too

[Aaron Liu]

but then you get these weird cases like the plane with doubled antidiagonal where I'm not sure what the topology should be

[Jireh Loreaux]

Alex Meiburg said:

Yeah, they do come from quantum mechanics (largely) - it's exactly your standard topology on matrices, the finite product topology over all the elements. Which is the same topology as you would get induced from any matrix norm, like the Frobenius norm for instance (so that a ball is the L2 norm of the entries).

I'm very confused Alex. I don't think the Loewner order on matrices induces the product topology in any sort of natural way. In any case, the Loewner order is a very different order from, say, the lexicographical order, but you want them to generate the same topology (i.e., the product topology) on matrices? That seems highly unlikely.

[Jireh Loreaux]

Why don't you just want docs#OrderClosedTopology ?

[Jireh Loreaux]

Note that we have an instance of this for C⋆-algebras: docs#CStarAlgebra.instOrderClosedTopology

[Alex Meiburg]

Yeah, I already have the OrderClosedTopology instance, that's fine. It's just a matter of philosophy I guess, that it does feel like the intervals are reasonable in a way that they should generate the topology.

And no, I wouldn't expect the lexicographical order to generate the product topology, definitely not

[Alex Meiburg]

My intuition I guess is that the closed intervals in the Loewner order are closed, compact sets - so they're homeomorphic to closed balls, so in that sense they should contain enough data to recover the topology in some way.

[Jireh Loreaux]

Alex Meiburg said:

are closed, compact sets - so they're homeomorphic to closed balls

wait, what?

[Jireh Loreaux]

The Cantor set is closed and compact, but it's also nowhere dense, so it doesn't contain any ball.

[Jireh Loreaux]

Likewise, in the Loewner order, your "intervals" are matrices that all have the same imaginary part, so these intervals don't contain a ball either.

[Alex Meiburg]

Jireh Loreaux said:

Alex Meiburg said:

are closed, compact sets - so they're homeomorphic to closed balls

wait, what?

Alright, I said that too loosely, it wasn't mean to be an exact logical implication.
But um, if you pretend that I said "convex, compact sets" then I think it is an actual implication.

[Alex Meiburg]

Jireh Loreaux said:

Likewise, in the Loewner order, your "intervals" are matrices that all have the same imaginary part, so these intervals don't contain a ball either.

I'm only considering hermitian matrices

[Alex Meiburg]

(I'm aware that Mathlib does it for _all_ elements of a CStarAlgebra, not just the self-adjoint ones, but if you look at a standard textbook defn for the Loewner order I've only ever seen it defined for Hermitian matrices!)

[Alex Meiburg]

Mm, maybe the fact that I want is precisely

class MyIccTopology [t : TopologicalSpace x] [Preorder x] : Prop where
  myIccProperty :
    t = TopologicalSpace.generateFrom { s | ∃ a b, s = interior (Set.Icc a b) }

It's "circular" in the sense that it's a self-consistency property for the topology with the intervals, not a formula that spits out a unique topology from the intervals. The interior depends on t itself. But I think this is the property I want

[Alex Meiburg]

At least, it's a very nice property that many types would satisfy. I guess I had to write down exactly what I wanted to get it down on the page

[Jireh Loreaux]

Alex Meiburg said:

But um, if you pretend that I said "convex, compact sets" then I think it is an actual implication.

Still no, a polytope generated by 3 points in ℝ³ does not contain a ball, yet it is compact and convex.

[Alex Meiburg]

Okay, fair enough. :sweat_smile: But again, I didn't actually mean that to be an implication to begin with.
The conclusion I stated is still true!

[Jireh Loreaux]

Alex Meiburg said:

but if you look at a standard textbook defn for the Loewner order I've only ever seen it defined for Hermitian matrices!

Sure, but that's simply inconvenient. For instance, I wrote a paper about numerical ranges a few years ago in which it would have been very nice to consider A ≤ B for nonselfadjoint A and B, but alas, I hadn't adopted this viewpoint yet.

[Alex Meiburg]

Alright, well what's inconvenient or not is contextual I suppose. :)

[Alex Meiburg]

I think the MyIccTopology is a more interesting property when combined with OrderClosedTopology, so that the closed intervals are closed sets, but then you also have that their interiors generate the space. I'm still not sure that it uniquely characterizes the space though

[Aaron Liu]

"interiors of closed intervals are generating"?

[Aaron Liu]

that's satisfied by the indiscrete topology

[Aaron Liu]

the one where the only open sets are empty and univ

[Alex Meiburg]

That doesn't have an OrderClosedTopology though. If I require MyIccTopology and OrderClosedTopology, I get the discrete topology still works (the interior of any set is the set itself), but I _think_ that in R^2 I get just the discrete topology and the standard topology

I have a board filled with many pictures at this point lol

[Alex Meiburg]

(and at least one colleague confidently telling me that "there are people in Europe who do this very much" but can't point to any useful reference..)

[Aaron Liu]

Alex Meiburg said:

I have a board filled with many pictures at this point lol

wow amazing

[Aaron Liu]

Alex Meiburg said:

If I require MyIccTopology and OrderClosedTopology, I get the discrete topology still works (the interior of any set is the set itself)

I don't think complements of singletons are always finite unions of closed intervals

[Aaron Liu]

wait no you want the interior of closed intervals

[Aaron Liu]

oh yeah then discrete topology works

[Alex Meiburg]

Alright, at least for the "nice" cases I care about, the following works:

• The set Set.Ici and Set.Iic are closed
• The interiors of Set.Icc generate the topology
• On any maximal chain S, the induced topology on S is the order topology.
  That defines a consistency condition between the topology and the partial order, and I have proofs (on paper, not checked in Lean :slight_smile: ) that at least for any R^n or for the Loewner order on Hermitian matrices, these uniquely determine the standard topology.

[Aaron Liu]

unfortunately that doesn't give me a lot to work with on antichains

[Jireh Loreaux]

Alex, what I'm still not clear about is exactly what you want to do with this. What common theorems do you want to prove that hold in these cases that would be unified with a type class? Do you have other examples besides products and Hermitian matrices?

I suspect that your third condition above about maximal chains might fail for Hermitian elements in a C*-algebra, although I haven't tried to construct a counterexample.

[Alex Meiburg]

I'm not entirely sure what I would prove from this either, but it still feels like a concept that will be useful. I think any statement of the form "the topology is uniquely determined from this other information" probably becomes useful in lots of places once you have it.

In particular, I'm pretty sure this property is closed under finite (and I suspect even infinite) products.

[Alex Meiburg]

With some more work, I have a tentative proof that three properties above uniquely determine the topology. The interiors of the Set.Icc a b end up being precisely the points p such that: for any maximal chain S, there exist points (c,d) with c < p < d such that the open interval in the chain, (c, d)_S, is a subset of I(a,b). So then the requirement is precisely that these sets generate the topology.

[Aaron Liu]

I think I constructed an order for which there is no topology satisfying the condition

[Alex Meiburg]

Ah, that could be (I proved uniqueness but not existence)

[Aaron Liu]

is that bad?

[Alex Meiburg]

Wait, no, hmmm, because I thought I proved it was that definition I gave.

What's your order?

[Alex Meiburg]

Aaron Liu said:

is that bad?

I don't know.

[Aaron Liu]

Alex Meiburg said:

Wait, no, hmmm, because I thought I proved it was that definition I gave.

What's your order?

(Real) Line with double origin, the doubled origins are incomparable

[Aaron Liu]

I don't think it works

[Alex Meiburg]

Oh, right, the line-with-two-origins topologyfails to be generated by the interiors of the closed intervals. If we treat the two origins as inseparable, then Ici isn't closed.

Okay, what I had proved is that any two topologies must be equal because they both have a basis of those "canonical interiors", which in this case would make those two origins inseparable; but in this case the topology generated by those doesn't make Ici closed.

If we accepted this as our choice of topology anyway, then non-lattices like this can lead to non-T1 spaces, which is sad. Hmmm

[Alex Meiburg]

Or we can say this predicate is our definition, in which case there's no compatible topology on the doubled line;

or we say that the topology's opens are generated by these interiors /and/ the complements of Ici/Iic's, which feels a bit more convoluted

[Alex Meiburg]

I'm gonna try throwing some of these into Aristotle and see if it can check my reasoning :)

[Jireh Loreaux]

I'm still wondering why you want to do this. Which lemmas do you want to generalize to this new class of spaces, presupposing such a class exists?

[Aaron Liu]

Alex Meiburg said:

If we accepted this as our choice of topology anyway, then non-lattices like this can lead to non-T1 spaces, which is sad. Hmmm

What does this mean

[Alex Meiburg]

Jireh Loreaux said:

I'm still wondering why you want to do this. Which lemmas do you want to generalize to this new class of spaces, presupposing such a class exists?

Is this problem not intrinsically interesting to you? "Find a generalization of the order topology on linear orders, such that the product order gives the product topology"?

To me that's an interesting mathematical question, and after doing quite a bit more research online it looks like not one that currently has an answer. There are several other generalizations of the order topology to partial orders that give other nice properties, but not the product property.

[Alex Meiburg]

Maybe this thread belongs more in #math though since I'm really asking what seems to be a not-well-solved math question to begin with. If that helps.

[Aaron Liu]

all my attempts either don't respect (in)distinguishability or don't respect $\mathbb{R}^2$

[Aaron Liu]

it's very tricky

[Jireh Loreaux]

I'm not saying it isn't a reasonable mathematical question, although it's entirely possible that the answer is: "no such generalization exists (satisfying some reasonable set of properties)". So, in order to suspect that there is some generalization, I would want to have either: (a) lots of examples where the partial order gives rise to the topology in some reasonable way, (b) theorems that hold for linear orders that, in certain settings, generalize to other types, and somehow this generalization is uniform.

[Aaron Liu]

Jireh Loreaux said:

(a) lots of examples where the partial order gives rise to the topology in some reasonable way

usually there is some more reasonable way to get the topology which is not from the order

[Jireh Loreaux]

I think this especially because "what is the relationship between partial orders and topology" is a very fundamental question which I'm sure many people have considered, and since poking around online doesn't yield anything, it makes me suspect there is no such nice characterization (besides docs#OrderClosedTopology). Of course, this is only a heuristic, but it's a handy one.

[Aaron Liu]

Jireh Loreaux said:

(b) theorems that hold for linear orders that, in certain settings, generalize to other types

I found one (1) theorem that @Bhavik Mehta helped me prove that was interesting in linear orders but worked for all the other orders too which came out as

import Mathlib

theorem MonotoneOn.closure {X Y : Type*}
    [TopologicalSpace X] [Preorder X] [OrderTopology X]
    [Preorder Y] [TopologicalSpace Y] [ClosedIicTopology Y] [ClosedIciTopology Y]
    {f : X → Y} {s : Set X} (hfc : ContinuousOn f (closure s))
    (hfs : MonotoneOn f s) :
    MonotoneOn f (closure s) := by

[Alex Meiburg]

Jireh Loreaux said:

Of course, this is only a heuristic, but it's a handy one.

That's true! But I guess I'm motivated to think about it. :) Usually when it turns out that I have a 'natural' question whose answer is 'there's no good clean answer', I find several people asking a similar question on math stackexchange or similar being told that. I've been surprised that I can't find anyone asking this.

I tried asking a couple chatbots about this and they gave total nonsense, which also suggests it's just not talked about very much. Also a heuristic, and not a very good one.