Quotient.instPreorder

Stream: mathlib4

[David Loeffler]

I just found out about Mathlib.Order.Quotient, which defines an order instance on any quotient type, whenever the parent type is ordered.

Is this really a good idea? I'm concerned that it's too general: one might e.g. want to make a quotient of some standard (ordered) type like ℝ or ℤ and then equip the quotient with a new order structure (different from the one induced by the quotient construction); and if these general order instances are floating around, then the result will be two conflicting order instances on the same type, and hence a world of pain.

(I found out about this because my student @Daniele Bolla has an extended example involving quotient types in his bachelor thesis, which works fine in Mathlib v4.24, but is broken in current Mathlib for this reason).

Can I suggest that the definitions in this file be "hidden" inside a scope (like we already do for the partial order on ℂ, which is only an instance if the namespace ComplexOrder is open)? Or that they be relegated to def's rather than instances?

[David Loeffler]

(Tagging @Violeta Hernández who wrote the quotient order stuff)

[Floris van Doorn]

Given that without any assumptions, this order isn't very well-behaved, I agree that this instance should probably not be global.

As a workaround, if you write def MyQuotient := Quotient ... then this order-instance will invisible on MyQuotient.

[Floris van Doorn]

Note: this was discussed in #29735

[Violeta Hernández]

We had some very long-winded discussion already. The ultimate conclusion was that this was the "categorically correct" ordering and that it should be fine to have. Cases like the reals where you want to put a different order are in practice anyways going to be behind a def.

[Violeta Hernández]

With all that said, I have no problem with just scoping the instance if it's causing problems.