order on `UpperSet`s

Stream: mathlib4

[Yury G. Kudryashov]

I'm porting order.upper_lower and it seems that we have two different orders on UpperSet: one comes from SetLike (subset order) and one defined in the file (reversed subset).

[Yury G. Kudryashov]

@Yaël Dillies Are there any good reasons to have the reversed order other than Ici becomes a sup_hom?

[Yaël Dillies]

It makes upper_set and lower_set order-isomorphic (under compl), and mostly it follows the filter convention. There's already a thread about this somewhere.

[Yury G. Kudryashov]

How should we avoid the conflict? Introduce a weaker TC for SetLikeNoOrder?

[Yaël Dillies]

I tried removing the order derived from set_like but it didn't turn out great, so probably we just want to get rid of the set_like instance :sad:

[Yury G. Kudryashov]

For now, I'm just overriding some simp priorities. I don't want to change much while porting (done once, don't want to repeat).

[Yury G. Kudryashov]

I think, we should postpone any refactor till after the port.

[Johan Commelin]

I agree that this refactor should wait. But I also think that upper_set and lower_set should be order-anti-isomorphic.

[Yaël Dillies]

Do you want to change the order on filter, then?

[Johan Commelin]

No. I want to change the order on upper_set

[Kevin Buzzard]

Even though the set of closed subsets of a topological space bijects with the set of open subsets, I don't think that's a good reason for arguing that the subset ordering on one of them should be artificially reversed to make the bijection order-preserving, when it's clearly order-reversing

[Kevin Buzzard]

Compl is subset-reversing

[Kevin Buzzard]

Is the problem that we don't have a typeclass for order-reversing maps so we want to shoehorn everything into being order-preserving?

[Reid Barton]

In category theory you can form [C^op, Set] (~ LowerSet) and [C, Set] (~ UpperSet) and of course you could also ^op these if you like.
There is some use to [C, Set]^op (it's the limit-completion of C) but I would say it is still less common than [C, Set].

[Yaël Dillies]

Johan Commelin said:

No. I want to change the order on upper_set

But filters are upper sets.

[Johan Commelin]

Sure, but there is an API boundary in between. Where we decide to think of a "big as a set" filter as a small element.

[Reid Barton]

Specifically, a filter on X is some kind of idealized "part" of X that we identify by keeping track of what sets of X it's contained in. And a bigger part is contained in fewer sets, hence the order is reversed.

[Johan Commelin]

Or, to beat a dead horse: filters are not SetLike for a good reason, but upper sets are SetLike, also for a good reason.

[Reid Barton]

filter X = Pro(set X). Upper sets are one way (& probably the simplest) to represent filter X, but not the only possible way.