Ordered uniform spaces?

Stream: maths

[David Loeffler]

The following came up in reviewing #13349.

Any linear order automatically has a topology. Is there some way of naturally "promoting" this topological-space structure to a uniform-space structure in such a way that sets of the form {(a, b) | X < a ∨ b < Y}, for X < Y, are entourages? [Edited to clarify statement]

[David Loeffler]

(If the space has a uniform-group structure that interacts well with the order, then this is true, but it seems strange to require a group structure as a hypothesis when the group operation isn't mentioned in the statement.)

[Anatole Dedecker]

The thing is, taking $\mathbb{R}$ as an example, I don't see how you could refer to all the balls of radius at least $\varepsilon$ without mentioning the length of an interval (or the distance, of course)

[Anatole Dedecker]

Put another way: I don't see how you would imagine a definition of uniform convergence of functions based only on some order structure on the codomain.

[David Loeffler]

OK fair enough, probably asking to actually construct the uniformity from the order would be too much. For the PR review, it would be nice to have some sufficient condition (on a uniformity) for this family of sets to be entourages; but maybe there is no condition nicer than that one itself.

[Anatole Dedecker]

By the way I realize my message my messages sound too much like "I've thought about this there's no hope". I think there's no hope for something like "a purely order-theoretic construction of the uniform structure on $\mathbb{R}$", but there are a bunch of interactions between uniformity/order/groups structure that I don't understand here, even after thinking about them a bit with @Jireh Loreaux, so if anyone has any reference or idea of what could be done (maybe a version of docs#OrderClosedTopology ?) that would be wonderful.

[David Loeffler]

So I played around with this a bit and convinced myself that if we define

class OrderClosedUniformity (α : Type*) [UniformSpace α] [LinearOrder α] where
  mem_uniformity' (a b : α) (_ : a < b) : { p : α × α | a < p.1 ∨ p.2 < b } ∈ 𝓤 α

then we can show that it is satisfied assuming either

    [Group α] [UniformSpace α] [UniformGroup α] [LinearOrder α] [OrderClosedTopology α]
    [MulLeftMono α] [MulRightMono α]

or its add-group analogue. Any thoughts on whether this is a worthwhile addition to mathlib? Opinions on the name, if so?

[Jireh Loreaux]

It would be nice if we had some justification for a class like that beyond: "it seems to do the trick". I'm not complaining about your efforts (indeed, thanks!), I'm just hesitant to add some one-off class.

[Jireh Loreaux]

I'm sorry, I wish I had more time to think about this deeply, but I'm very busy at the moment.

[Chris Birkbeck]

Sorry, I've just caught up with this. I'm happy to add this class if people want it, but I sort of agree with Jireh as to the justification. If this is only to fix the to_additive name issue, then I don't think its worth it.

[Chris Birkbeck]

Also, thanks for the review and opening this thread!

[Jireh Loreaux]

I don't think this has anything to do with to_additive. The naming issue is not a problem.

[David Loeffler]

@Chris Birkbeck just to check, the original lemma from your PR was mostly intended to be applied to $\mathbb{R}$ anyway, wasn't it?

[Chris Birkbeck]

Yes, its only $\mathbb{R}$ that I need it for.

[David Loeffler]

OK, maybe this is a rather silly degree of excess generality then.

[Chris Birkbeck]

We could just do additive groups and leave it there I guess. I was just being greedy and trying to use to_additive to get it in both cases.

[Aaron Liu]

David Loeffler said:

The following came up in reviewing #13349.

Any linear order automatically has a topology. Is there some way of naturally "promoting" this topological-space structure to a uniform-space structure in such a way that sets of the form {(a, b) | X < a ∨ b < Y}, for X < Y, are entourages? [Edited to clarify statement]

Try taking the fine uniformity? It should generate the same topology since linear order topologies are docs#CompletelyRegularSpace. Not sure if this satisfies your condition though.

[Aaron Liu]

The fine uniformity is ⨅ (u : UniformSpace α) (_ : instTopologicalSpace ≤ u.toTopologicalSpace), u

[Aaron Liu]

It's also free in that it's left adjoint to the forgetful functor

[David Loeffler]

@Aaron Liu Thanks for this interesting suggestion, I didn't know about the fine uniformity.

[Antoine Chambert-Loir]

The open interval $\mathopen]0;1\mathclose[$ is not complete for the standard distance, but it has a strictly increasing homeomorphism to $\mathbf R$ which gives him a complete distance. Hence I don't believe there is a reasonable notion.

[Antoine Chambert-Loir]

A similar example exists in Polish spaces: any open subset of a Polish space is Polish, meaning it has a distance which induces the same topology and for which it is complete.