chore(topology/order/*): Move

[YaelDillies]

Move files from topology.algebra.order. to topology.order. when they do not contain any algebra. Move the non-algebra bit of topology.algebra.order.basic to topology.order.basic.

---

• depends on: [Merged by Bors] - chore(topology/order/basic): Move #17860

[hrmacbeth]

I fully approve moving topology.algebra.order.* to topology.order.*, but I think it should be done more thoroughly -- I don't think there's a reason to leave anything in the old folder topology.algebra.order.*, everything there is more closely related to the files in the new topology.order.* than the new topology.algebra.*

[eric-wieser]

Can you make sure that this docstring doesn't duplicate topology/order/basic.lean? It looks like right now they're the same as each other.

It looks to me like this docstring is basically all about the non-algebraic file.

[YaelDillies]

I fully approve moving topology.algebra.order.* to topology.order.*, but I think it should be done more thoroughly -- I don't think there's a reason to leave anything in the old folder topology.algebra.order.*, everything there is more closely related to the files in the new topology.order.* than the new topology.algebra.*

In fact I moved all files under topology.algebra.order. that didn't mention algebra to topology.order., but files such as topology.algebra.order.field definitely deserve to stay under topology.algebra..

Note that topology.order. also contains material about categorical logic, where topological spaces and orders interact in ways that are quite different to what you would expect from the reals, say.

[hrmacbeth]

files such as topology.algebra.order.field definitely deserve to stay under topology.algebra..

I disagree somewhat. My criterion would be: if it's about the order topology of a linear_ordered_field, it should live in topology.order.*. If it's about a topological_division_ring, it should live in topology.algebra.*. If it's one of the small number of declarations relating the two concepts, I don't care.

Note that topology.order. also contains material about categorical logic, where topological spaces and orders interact in ways that are quite different to what you would expect from the reals, say.

Do you think it's ambiguous to put this material in the same folder as all the order_topology stuff? If so, we can put them in separate folders, but since the order_topology stuff is much more central in mathlib, maybe it should get the good name topology.order.*? I don't have a strong opinion here.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(topology/order/basic): Move #17860
  By Dependent Issues (🤖). Happy coding!

[urkud]

It's not-too-late but it has lots of merge conflicts. What's your plan: merge master or drop & redo in Mathlib 4?

[eric-wieser]

Removing the not-too-late label; while we may still want this in mathlib4, it doesn't seem likely that mathport will help.

[YaelDillies]

Redone in leanprover-community/mathlib4#11610.